% This input file can be used to rewrite Boolean expressions into
% canonical if-then-else form. It should rewrite tautologies to 1
% and unsatisfiable expressions to 0. The result is like an OBDD
% (ordered binary decision diagram); it is not very fast, because it
% is done with ordinary rewriting, not with the fast OBDD algorithms
% (structure sharing, caching, etc.).
%
% The propositional "variables" in the expressions to be
% rewritten can be either (Otter) variables, constants, or a
% mixture. If variables are included, the flag lex_order_vars
% must be set
%
% The built-in ordering relation has variables < constants, with
% variables ordered by variable number and constants ordered by
% the C library strcmp() function. The constant ordering can be
% changed with a lex command, e.g., lex([b,c,a]) means that b < c < a,
% variables are still smaller, and other constants are bigger.
%
% There is something tricky going on here, but I think it is
% correct. There are two if-then-else operators: if(x,y,z) is
% the external form, and ite(x,y,z) is the internal form. The
% internal form has the property that it NEVER has propositional
% variables in the second or third argument. This property
% speeds up the rewriting. If the expression to be rewritten
% has if-then-else, if(x,y,z) should be used. These are rewritten
% right away to the ite(x,y,z) form, and the rest of the rewriting is
% done in terms of ite(x,y,z).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Declare Boolean operations as infix or prefix.
% This is for parsing and printing only.
% Note that the defaults for & and | are overridden.
op(400, fx, ~).
op(450, xfy, #). % exclusive or
op(450, xfy, |).
op(460, xfy, &).
op(470, xfx, -->).
op(480, xfx, <-->).
make_evaluable(_>_, $LGT(_,_)).
list(demodulators).
% Define ordinary Boolean operations in terms of if(_,_,_).
if(x,y,z) = ite(x,ite(y,1,0),ite(z,1,0)).
x & y = ite(x,ite(y,1,0),0).
x | y = ite(x,1,ite(y,1,0)).
~x = ite(x,0,1).
x --> y = ~x | y.
x <--> y = (x --> y) & (y --> x).
x # y = ~(x <--> y).
% These can speed things up, because they are applied first.
x <--> x = 1.
x --> x = 1.
x & x = x.
x | x = x.
x # x = 0.
% The rest of the rules rewrite ite-expressions into canonical form.
% basic simplification
ite(x,y,y) = y.
ite(1,x,y) = x.
ite(0,x,y) = y.
% move if-expressions out of conditions
ite(ite(x,y,z),u,v) = ite(x,ite(y,u,v),ite(z,u,v)).
% collapse conditions
ite(x,ite(x,y,z),w) = ite(x,y,w).
ite(x,w,ite(x,y,z)) = ite(x,w,z).
% sort on conditions
(x1 > x2) -> ite(x1,ite(x2,y,z),w) = ite(x2,ite(x1,y,w),ite(x1,z,w)).
(x1 > x2) -> ite(x1,w,ite(x2,y,z)) = ite(x2,ite(x1,w,y),ite(x1,w,z)).
end_of_list.
set(demod_inf). % the "inference rule"
clear(demod_history). % we don't want to see a list of 44775 integers
assign(demod_limit, -1). % no limit
set(sos_queue).
assign(max_given, 4).
set(lex_order_vars).
set(pretty_print).
% Here are the expressions to be rewritten.
list(sos).
P1((A & (B | C)) <--> ((A & B) | (A & C))). % Distributivity (=1)
P2(~(~x | ~y) | ~(~x | y) <--> x). % Huntington identity (=1)
P3(if(D,if(C,if(A,B,I),if(E,F,G)),H)).
P4(
((a2# (b2# (1# (a2&b2))))# ((a3#b3)# (1# (a0# (b0# (1# (a0&b0)))))))
<-->
if(a0,if(a2,if(a3,if(b3,1,0),if(b3,0,1)),if(a3,if(b2,if(b3,1,0),
if(b3,0,1)),if(b2,if(b3,0,1),if(b3,1,0)))),if(a2,if(a3,if(b0,
if(b3,1,0),if(b3,0,1)),if(b0,if(b3,0,1),if(b3,1,0))),if(a3,
if(b0,if(b2,if(b3,1,0),if(b3,0,1)),if(b2,if(b3,0,1),if(b3,1,0))),
if(b0,if(b2,if(b3,0,1),if(b3,1,0)),if(b2,if(b3,1,0),if(b3,0,1))))))
).
end_of_list.