%
%  Test program for cnf.
%

user:file_search_path(common,'../common').
:- load_files(common(cnf)).
:- ensure_loaded(common(io)).
:- ensure_loaded(common(intext)).

test(A) :-
  write_formula(A), nl,
  to_internal(A, AI),
  cnf(AI, A1),
  to_external(A1, A1E),
  write_formula(A1E), nl,
  cnf_to_clausal(A1, A2),
  write_clauses(A2).

t1 :- test(    ~( (p -> q -> r ) -> (p -> q) -> (p -> r) ) ).
t2 :- test( (p -> q) -> (r v p ) -> (r v q) ).
t3 :- test(  ((~p) -> (~q)) -> (p -> q) ).
t4 :- test( ~(p <-> q) ).
t5 :- test(  ( (p -> q -> r ) -> (p -> q) -> (p -> r) ) ).

t6  :- test(all(X, (p(X) -> q(X))) -> (all(X, p(X)) -> all(X, q(X)))).
t7  :- test(ex(X, all(Y, p(X, Y))) -> all(Y, ex(X, p(X, Y)))).
t8  :- test(all(X, p(X)) v all(X, q(X))).
t9  :- test(all(X, all(Y, all(Z, p(X,Y) ^ p(Y,Z) -> p(X,Z))))).
t10 :- test(all(X, all(Y, p(X,Y) -> p(Y,X))) ^
      all(X, all(Y, all(Z, p(X,Y) ^ p(Y,Z) -> p(X,Z)))) ^
      all(X, ex(Y, p(X,Y))) ^
      ~ all(X, p(X,X))).

t11 :- test( (p v all(X,q(X))) ^ (r v ex(Y,s(Y))) ).