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