cnf

t4.pl

:- op(1100,xfy,&).
:-op(600,xfy,=>).
:-op(700,xfy,<=>).
n(-(-A),A1):-!,n(A,A1).
n(-(A&B),R):-!,n(-A,A1),n(-B,B1),d(A1|B1,R).
n(-(A|B),R):-!,n(-A,A1),n(-B,B1),d(A1&B1,R).
n(A&B,R):-!,n(A,A1),n(B,B1),d(A1&B1,R).
n(A|B,R):-!,n(A,A1),n(B,B1),d(A1|B1,R).
n(-true,false).
n(-false,true).
n(A,A).
d(A,R):-d(A,R,_),!.
d(A&B,A1&B1,t):-d(A,A1,_),d(B,B1,_).
d(A|(B&C),R,F):-d((A|B)&(A|C),R,F).
d((A&B)|C,R,F):-d((A|C)&(B|C),R,F).
d(A|B,R,F):-d(A,A1,F1),d(B,B1,F2),((F1=t;F2=t)->d(A1|B1,R,F);R/F=(A1|B1)/f).
d(X,X,f).
c(A,B):- atomic(A),atomic(B),A @=< B.
c(A,-_):- atomic(A).
c(-A,-B):- c(A,B).
c(A,_|_):- atomic(A).
c(-_,_|_).
c(A|B,C|D):-c(A,C);A=C,c(B,D).
c(A&B,C&D):-c(A,C);A=C,c(B,D).

e(A,R):- eand(A,R),!.
eand(A,R):- eand(A,true,R).
eand((A&B)&C)--> eand(A),eand(B),eand(C).
eand(A&B)-->eand(A),eand(B).
eand(A)-->{eor(A,A_)},and(A_).
and(_,false,false):-!.
and(false,_,false):-!.
and(A,true,A):-!.
and(true,A,A):-!.
and(A,B,false):- neg(A,N),ands(N,B).
and(A,B,B):- ands(A,B).
and(A,B&C,A&B&C):- A @=< B,!.
and(A,B&C,B&R):- !,and(A,C,R).
and(A,B,A&B) :- A @=< B,!.
and(A,B,B&A) :- !.
ands(A,A).
ands(A,A&_).
ands(A,_&B):- ands(A,B).
eor(A,R):- eor(A,false,R).
eor((A|B)|C)--> eor(A),eor(B),eor(C).
eor(A|B)--> eor(A),eor(B).
eor(A)-->or(A).
or(_,true,true):-!.
or(true,_,true):-!.
or(A,false,A):-!.
or(false,A,A):-!.
or(A,B,true):- neg(A,N),ors(N,B).
or(A,B,B):- ors(A,B).
or(A,B|C,A|B|C):- A @=< B,!.
or(A,B|C,B|R):- !,or(A,C,R).
or(A,B,A|B) :- A @=< B,!.
or(A,B,B|A) :- !.
ors(A,A).
ors(A,A|_).
ors(A,_|B):- ors(A,B).
neg(-A,A).
neg(A,-A).

dbg(I,A,A):- writeln(I:A).
cnf --> n,e.

:-begin_tests(cnf).
  test(a):- cnf(a&(b|c|(d&e)),R),R=(a&(b|c|d)&(b|c|e)).
  test(a):- cnf(-(-a| -((b|c)|(d&e))),R),R=(a&(b|c|d)&(b|c|e)).
  test(a):- cnf((a&b)|(c&d),R),R=((a|c)&(a|d)&(b|c)&(b|d)).
  test(a):- a @< (a|b).
  test(a):- \+((a|b) @< a).
  test(a):- e(a&b,R),R=(a&b).
  test(a):- e((b|c)&(a|c),R),R=((a|c)&(b|c)).
  test(a):- e((a|d)&(b|d),R),R=((a|d)&(b|d)).
  test(a):- e((b|c)&(a|d),R),R=((a|d)&(b|c)).
  test(a):- e((b|c)&(d|e)&a,R),R=(a&(b|c)&(d|e)).
  test(a):- e(a & true,R),R=a.
  test(a):- e(true&a,R),R=a.
  test(a):- e(true&a&true&true&a,R),R=a.
  test(a):- e(false|a|false|false|a,R),R=a.
  test(a):- e(false|true,R),R=true.
  test(a):- e(true|false,R),R=true.
  test(a):- e(false|true|false,R),R=true.
  test(a):- e(a|true|true,R),R=true.
  test(a):- e(true&a&true&(false|true|false)&a,R),R=a.
  test(a):- e(a&true&a,R),R=a.
  test(a):- e(a&true&true,R),R=a.
:-end_tests(cnf).

t(A,A) :- !.
t(-A,-B):- !,t(A,B).
t(A|B,C|D):-t(A,C)->t(B,D),!;t(A|B,D),!.
t(A,B|C):- t(A,B),!;t(A,C).
t(A&B,C&D):-t(A,C)->t(B,D),!;t(B,C&D),!.
t(A&B,C):-t(A,C),!;t(B,C).
:-begin_tests(sub).
  test(a):- t(int,int).
  test(a):- t(int,int|string).
  test(a):- t(-int,-int).
  test(a):- t(-int,string| -int).
  test(a):- t(int&int,int|int).
  test(a):- t(a|b,a|b|c).
  test(a):- t(a&b,a).
  test(a):- t(a&b,b).
  test(a):- t(a&b,a&b).
  test(a):- t(a&b&c,a&b).
  test(a):- t(a&b&c,b&c).
:-end_tests(sub).
:-run_tests.
:- halt.