% problem-set/circuits/intchg_val.ver1.clauses
% created : 09/02/86 
% revised : 07/11/88

% description:
%
% This run validates one of the circuit designs that will take
% x and y as input and output y and x without crossing any wires.

% representation:
%
% This input file came with no explanation of 
% the representation.
 
lex(And(x,x), Or(x,x) ,i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)).


ckt(Input(i1,i2),Output(a1,a2)).

Equal(a1,And(b1,b3)).
Equal(a2,And(b2,b3)).
Equal(b1,Not(d1)).
Equal(b2,Not(d2)).
Equal(b3,Or(c1,c2)).
Equal(c1,Or(d1,d3)).
Equal(c2,Or(d2,d3)).
Equal(d3,f3).
Equal(d1,Not(e1)).
Equal(d2,Not(e2)).
Equal(e1,Or(f1,f3)).
Equal(e2,Or(f2,f3)).
Equal(f1,Not(i1)).
Equal(f2,Not(i2)).
Equal(f3,And(i1,i2)).

% commutativity and associativity

Equal(And(x,y),And(y,x)).
Equal(Or(x,y),Or(y,x)).
Equal(And(x,And(y,z)),And(And(x,y),z)).
Equal(Or(x,Or(y,z)),Or(Or(x,y),z)).

% sorting

Equal(Or(Or(x,y),z),Or(Or(x,z),y)).
Equal(And(And(x,y),z),And(And(x,z),y)).

% canonicalization to move Not to inside 

Equal(Not(And(x,y)),Or(Not(x),Not(y))).
Equal(Not(Or(x,y)),And(Not(x),Not(y))).

% canonicalization to sum-of-products

Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))).

% simplifiers

Equal(And(x,x),x).
Equal(And(And(x,y),y),And(x,y)).
Equal(And(And(x,y),x),And(x,y)).
Equal(Or(x,x),x).
Equal(Or(Or(x,y),y),Or(x,y)).
Equal(Or(Or(x,y),x),Or(x,y)).
Equal(And(x,Not(x)),0).
Equal(And(And(x,y),Not(y)),0).
Equal(And(And(x,y),Not(x)),0).
Equal(Or(x,Not(x)),1).
Equal(Or(Or(x,y),Not(y)),1).
Equal(Or(Or(x,y),Not(x)),1).
Equal(Not(Not(x)),x).
Equal(Or(And(x,y),And(x,Not(y))),x).
Equal(Or(And(x,y),And(y,Not(x))),y).

% evaluators

Equal(And(x,0),0).
Equal(And(x,1),x).
Equal(Or(x,0),x).
Equal(Or(x,1),1).
Equal(Not(0),1).
Equal(Not(1),0).