% problem-set/circuits/interchange.ver1.clauses
% created : 08/28/86
% revised : 07/11/88 

% description:
%
% Design a circuit with inputs x and y whose outputs are
% y and x, and contains no crossings of wires.

% representation:
%
% We represent the circuit built up so far by
% ckt(Top(x),Middle(y),Bottom(z)), where Top and Bottom are lists
% of outputs, counting outward from the middle.

% split the middle, keeping the middle

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) |  
ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))).

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))).

% split the middle, omitting the middle

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))).

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))).

% join across the middle if it is empty, not keeping the sides

-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | 
ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)).

-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | 
ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)).

% join across the middle, keeping the sides

-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | 
ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))).

-ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | 
ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))).

% join to middle, keeping the sides 

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))).

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))).

% split the wire nearest the middle

% this clause is superseded by the previous four
% -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
% ckt(Top(C(x1,C(x1,x2))),Middle(y),Bot(C(z1,C(z1,z2)))).

% join the two wires nearest the middle

-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | 
ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))).

-ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | 
ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))).

% put inverter on the middle wire

-ckt(Top(x),Middle(y),Bot(z)) | 
ckt(Top(x),Middle(not(y)),Bot(z)).

% put inverter on the adjacent wires

-ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | 
ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))).

-ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) | 
ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))).
   
% cannot construct the answer 

-ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))).

% subsumer to get rid of circuits which are the 
% same on top and bottom

ckt(Top(x),y,Bot(x)).

% input configuration

ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))).

Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))).
Equal(and(0,0),0).
Equal(and(0,1),0).
Equal(and(1,0),0).
Equal(and(1,1),1).
Equal(and(NIL,x),x).
Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))).
Equal(or(0,0),0).
Equal(or(0,1),1).
Equal(or(1,0),1).
Equal(or(1,1),1).
Equal(or(NIL,x),x).
Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))).
Equal(not(0),1).
Equal(not(1),0).
Equal(not(NIL),NIL).
Equal(Tab(0,0,0,0),NIL).
Equal(Tab(1,1,1,1),NIL).
Equal(C(NIL,x),x).
Equal(C(x,C(x,y)),C(x,y)).