%
% Canonicalizing an exclusive-or/and expression with
% lex-dependent demodulation.
%
% This example comes from a verification problem of Smith,
% Kljaich, Wojcik, and Chisholm.
%

op(500, xfy, #).  % exclusive or
op(400, xfy, *).  % and

lex([0, 1, cin, a0, b0, a1, b1, a2, b2, a3, b3, *(_,_), #(_,_)]).

set(demod_inf).
clear(demod_history).
assign(demod_limit, -1).
assign(max_given, 1).
clear(for_sub).
clear(back_sub).

assign(max_mem, 1500).      % 1.5 Megabytes

list(demodulators).

% The following is a set of reductions for Boolean rings.
% Under the following conditions, it produces a canonical form.
%   1. The lex term must be lex([<constants>, *(_,_), #(_,_)]).
%   2. If variables are in the term being rewritten, set(lex_order_vars).

0#x=x.
x#0=x.
x#x=0.
x#x#y=y.
x#y=y#x.
y#x#z=x#y#z.

0*x=0.
x*0=0.
1*x=x.
x*1=x.
x*x=x.
x*x*y=x*y.
x*y=y*x.
y*x*z=x*y*z.

x * (y#z) = (x*y) # (x*z).

end_of_list.

list(sos).

p(
 (a2#b2#1#a2*b2)# (a3#b3)#1# (a0#b0#1#a0*b0)* (1#a0*b0)* (a1#b1#1#a1*b1)* (1#a1*b1)*
 (a2#b2#1#a2*b2)* (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (a1#b1#1#a1*b1)*
 (1#a1*b1)* (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)*
 (1#a2*b2)* (cin#1)# (a0#b0#1#a0*b0)* (1#a0*b0)* (1#a1*b1)* (1#a2*b2)*
 (cin#1)# (a0#b0#1#a0*b0)* (a1#b1#1#a1*b1)* (1#a1*b1)* (1#a2*b2)# (a0#b0#1#a0*b0)*
 (a1#b1#1#a1*b1)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)# (a0#b0#1#a0*b0)* (1#a1*b1)*
 (1#a2*b2)# (a0#b0#1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)# (1#a0*b0)*
 (a1#b1#1#a1*b1)* (1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)* (cin#1)# (1#a0*b0)*
 (a1#b1#1#a1*b1)* (1#a1*b1)* (1#a2*b2)* (cin#1)# (1#a0*b0)* (1#a1*b1)* (a2#b2#1#a2*b2)*
 (1#a2*b2)* (cin#1)# (1#a0*b0)* (1#a1*b1)* (1#a2*b2)* (cin#1)# (a1#b1#1#a1*b1)*
 (1#a2*b2)# (a1#b1#1#a1*b1)* (a2#b2#1#a2*b2)* (1#a2*b2)
).

end_of_list.