1:- module(seq, []).    2
    3:- use_module(library(apply)).    4:- use_module(library(apply_macros)).    5:- use_module(pac(basic)).    6:- use_module(pac(meta)).    7:- use_module(util(misc)).    8:- use_module(zdd('zdd-array')).    9:- use_module(zdd(zdd)).   10:- use_module(pac(op)).   11
   12:-op(1150, fy, seq_zdd).   13
   14:-meta_predicate seq_zdd(:).   15seq_zdd(X):- zdd((set_compare(seq:seq_compare), seq:X)).
   16
   17% ?-  N = 1000,  formula(1, N, _F), conj(1, N, _G), K is N+1,
   18%	time(((seq_zdd set_compare(seq:seq_compare),
   19%	  X << {[_F * _G], [-K]}, resolve(X)))).
   20%@ % 323,410,375 inferences, 23.387 CPU in 25.096 seconds (93% CPU, 13828499 Lips)
   21%@ N = 1000,
   22%@ K = 1001,
   23
   24% ?-  N = 2000,  formula(1, N, _F), conj(1, N, _G), K is N+1,
   25%	time(((seq_zdd set_compare(seq:seq_compare),
   26%	  X << {[_F * _G], [-K]}, resolve(X)))).
   27%@ % 1,290,666,755 inferences, 97.087 CPU in 102.450 seconds (95% CPU, 13293911 Lips)
   28%@ N = 2000,
   29%@ K = 2001,
   30%@ X = 4.
   31
   32% ?- N = 1000,  formula(1, N, _F), conj(1, N, _G), K is N+1,
   33%	time(seq_prove(_F*_G->K)).
   34%@ % 323,406,707 inferences, 23.167 CPU in 23.958 seconds (97% CPU, 13959991 Lips)
   35%@ N = 1000,
   36%@ K = 1001.
   37
   38% ?- N = 2000,  formula(1, N, _F), conj(1, N, _G), K is N+1,
   39%	time(seq_prove(_F*_G->K)).
   40%@ % 1,290,672,325 inferences, 122.266 CPU in 123.987 seconds (99% CPU, 10556291 Lips)
   41%@ N = 2000,
   42%@ K = 2001.
   43
   44seq_prove(X):- fetch_state(S),
   45			   set_compare(seq:seq_compare, S),
   46			   zdd_singleton(-X, X0, S),
   47			   resolve(X0, S).
   48
   49% prepare benchmark
   50formula(I, I, I==J):-!, J is I+1.
   51formula(I, J, I==P):- K is I + 1, formula(K, J, P).
   52
   53% ?- conj(1, 3, P).
   54%@ P = 1*(2*3).
   55conj(I, I, I):-!.
   56conj(I, J, I*P):- I0 is I + 1, conj(I0, J, P).
   57
   58%
   59seq_compare(=, X, X):-!.
   60seq_compare(C, ==(X, Y), ==(U, V)):-!, seq_compare(C, X, Y, U, V).
   61seq_compare(C, ->(X, Y), ->(U, V)):-!, seq_compare(C, X, Y, U, V).
   62seq_compare(C, +(X, Y), +(U, V)):-!, seq_compare(C, X, Y, U, V).
   63seq_compare(C, *(X, Y), *(U, V)):-!, seq_compare(C, X, Y, U, V).
   64seq_compare(C, xor(X, Y), xor(U, V)):-!, seq_compare(C, X, Y, U, V).
   65seq_compare(<, ==(_, _), _):-!.
   66seq_compare(>, _, ==(_, _)):-!.
   67seq_compare(<, ->(_, _), _):-!.
   68seq_compare(>, _, ->(_, _)):-!.
   69seq_compare(<, xor(_, _), _):-!.
   70seq_compare(>, _, xor(_, _)):-!.
   71seq_compare(<, *(_, _), _)	:-!.
   72seq_compare(>, _, *(_, _))	:-!.
   73seq_compare(<, +(_, _), _)	:-!.
   74seq_compare(>, _, +(_, _))	:-!.
   75seq_compare(C, -(X), -(Y))	:-!, seq_compare(C, X, Y).
   76seq_compare(C, X, -(Y))	:-!,
   77	(	X = Y ->  C = (<)
   78	;	seq_compare(C, X, Y)
   79	).
   80seq_compare(C, -(X), Y):-!,
   81	(	X = Y ->  C = (>)
   82	;	seq_compare(C, X, Y)
   83	).
   84seq_compare(C, X, Y):- compare(C, X, Y).
   85
   86%
   87seq_compare(C, X, Y, U, V):-
   88	seq_compare(C0, X, U),
   89	(	C0 = (=) -> seq_compare(C, Y, V)
   90	;	C = C0
   91	).
   92
   93		/****************************
   94		*   a la sequent calculus   *
   95		****************************/
   96
   97resolve(X, S):- zdd_has_1(X, S), !.		% The empty clause found.
   98resolve(X, S):- X > 1,
   99	cofact(X, t(A, L, R), S),
  100	resolve(A, L, R, X0, S),
  101	resolve(X0, S).
  102
  103% compound complementary check is useless because of
  104% prop ordering (see prop_compare/3)
  105% HERE
  106resolve(-(-A), L, R, X0, S):-!, resolve(A, L, R, X0, S).
  107resolve(A, L, R, X0, S):- L>1,
  108		cofact(L, t(B, L0, R0), S),
  109		B = -A,
  110		!,
  111		ltr_merge(R, R0, R1, S),
  112		ltr_join(L0, R1, X0, S).
  113resolve(A0 == A1, L, R, X0, S):-!, resolve((A0->A1)*(A1->A0), L, R, X0, S).
  114% resolve(A0 == A1, L, R, X0, S):-!,
  115% 		 ltr_insert((A0->A1), R, R0, S),
  116%  		 ltr_insert((A1->A0), R, R1, S),
  117% 		 ltr_join_list([L, R0,  R1], X0, S).
  118resolve(A0 -> A1, L, R, X0, S):-!, resolve(-A0+A1, L, R, X0, S).
  119% resolve(A0 -> A1, L, R, X0, S):-!,
  120%  		 zdd_insert_atoms([-A0, A1], R, R0, S),
  121% 		 ltr_join(L, R0, X0, S).
  122
  123resolve(A0 + A1, L, R, X0, S):-!,
  124		 zdd_insert_atoms([A0, A1], R, R0, S),
  125		 ltr_join(L, R0, X0, S).
  126resolve(A0 * A1, L, R, X0, S):-!,
  127		 ltr_insert(A0, R, R0, S),
  128		 ltr_insert(A1, R, R1, S),
  129		 ltr_join_list([R0, R1], L, X0, S).
  130resolve(xor(A0, A1), L, R, X0, S):-!, resolve(-A0*A1 + A0*(-A1), L, R, X0, S).
  131resolve(-(A), L, R, X0, S):- deMorgan(A, M), !,
  132		resolve(M, L, R, X0, S).
  133resolve(-(_), L, _, L, _):-!.		% Negative pure literal rule.
  134resolve(_, 0, _, 0, _):-!.			% Pure literal rule.
  135resolve(A, L, R, X0, S):-			% always L \= 1 here.
  136	     cofact(L, t(B, U, V), S),
  137		 (	B = -(A) ->
  138			ltr_merge(V, R, M, S),  % Resolution + Tautology rule.
  139			ltr_join(U, M, X0, S)	% Updated set of clauses.
  140		 ;	X0 = L					% Posituve pure literal rule.
  141		 ).
  142%
  143deMorgan(A0 == A1, -A0*A1 + A0 * -A1).
  144deMorgan(A0 -> A1, A0 * -A1).
  145deMorgan(A0 + A1, -A0 * -A1).
  146deMorgan(A0 * A1, -A0 + -A1)