1%
2% Canonicalizing an exclusive-or/and expression with
3% lex-dependent demodulation.
4%
5% This example comes from a verification problem of Smith,
6% Kljaich, Wojcik, and Chisholm.
7%
8
9op(500, xfy, #).  % exclusive or
10op(400, xfy, *).  % and
11
12lex([0, 1, cin, a0, b0, a1, b1, a2, b2, a3, b3, *(_,_), #(_,_)]).
13
14set(demod_inf).
15clear(demod_history).
16assign(demod_limit, -1).
17assign(max_given, 1).
18clear(for_sub).
19clear(back_sub).
20
21
22list(demodulators).
23
24% The following is a set of reductions for Boolean rings.
25% Under the following conditions, it produces a canonical form.
26%   1. The lex term must be lex([<constants>, *(_,_), #(_,_)]).
27%   2. If variables are in the term being rewritten, set(lex_order_vars).
28
290#x=x.
30x#0=x.
31x#x=0.
32x#x#y=y.
33x#y=y#x.
34y#x#z=x#y#z.
35
360*x=0.
37x*0=0.
381*x=x.
39x*1=x.
40x*x=x.
41x*x*y=x*y.
42x*y=y*x.
43y*x*z=x*y*z.
44
45x * (y#z) = (x*y) # (x*z).
46
47end_of_list.
48
49list(sos).
50
51p(
52 (a2#b2#1#a2*b2)# (a3#b3)#1# (a0#b0#1#a0*b0)* (1#a0*b0)* (a1#b1#1#a1*b1)* (1#a1*b1)*
53 (a2#b2#1#a2*b2)* (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (a1#b1#1#a1*b1)*
54 (1#a1*b1)* (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)*
55 (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (1#a1*b1)* (1#a2*b2)*
56 (cin#1)# (a0#b0#1#a0*b0)* (a1#b1#1#a1*b1)* (1#a1*b1)* (1#a2*b2)# (a0#b0#1#a0*b0)*
57 (a1#b1#1#a1*b1)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)# (a0#b0#1#a0*b0)* (1#a1*b1)*
58 (1#a2*b2)# (a0#b0#1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)# (1#a0*b0)*
59 (a1#b1#1#a1*b1)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)* (cin#1)# (1#a0*b0)*
60 (a1#b1#1#a1*b1)* (1#a1*b1)* (1#a2*b2)* (cin#1)# (1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)*
61 (1#a2*b2)* (cin#1)# (1#a0*b0)* (1#a1*b1)* (1#a2*b2)* (cin#1)# (a1#b1#1#a1*b1)*
62 (1#a2*b2)# (a1#b1#1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)
63).
64
65end_of_list.
66