1:- module(naot, [prop_to_naot/2, prop_to_naot/3,
    2				subst_aot/4,
    3				eval_ground_aot/2]).    4
    5 :- op(1060, xfy, ~).	% equivalence
    6 :- op(1060, xfy, <->).  % equivalence
    7 :- op(1060, xfy, <=> ). % equivalence
    8 :- op(1040, xfy, \/).	% OR
    9 :- op(1030, xfy, /\).	% AND
   10 :- op(1020, fy, \).	% NOT
   11
   12		/**********************
   13		*     Basic tests.    *
   14		**********************/
   15
   16% ?- prop_to_naot((A; B;C; D;E;F;G;H;I;J;K;L;M;N;O;P;Q;R;S;T;U;V;W;X;Y;Z), RR).
   17%@ RR = d([1, 2, 3, 4, 5, 6, 7, 8|...], [], []).
   18
   19% ?- prop_to_aot((A; B; C), RR).
   20% ?- prop_to_aot((A, B, C), RR).
   21% ?- module(naot).
   22
   23		/*************************
   24		*     Basic operatins    *
   25		*************************/
   26%
   27zip([], [], []).
   28zip([X|Xs], [Y|Ys], [X-Y|Zs]):-zip(Xs, Ys, Zs).
   29
   30% ?- meet([1,2],[3,4]).
   31meet([X|R], S):- (memberchk(X, S)->true
   32				 ; meet(R, S)
   33				 ).
   34%
   35negation(true, false).
   36negation(false, true).
   37%
   38complement_literal(not(I), I).
   39complement_literal(I, not(I)).
   40%
   41no_complement(X):- \+ has_complement(X).
   42%
   43has_complement([X|R]):- complement_literal(X, X0),
   44				   memberchk(X0, R), !.
   45has_complement([_|R]):- has_complement(R).
   46
   47%
   48literal(true).
   49literal(false).
   50literal(not(X)):- must_be(integer, X).
   51literal(X):- integer(X).
   52
   53%
   54sort_aot(c(A1,A2,A3),c(B1,B2,B3)):-
   55	sort(A1,B1),sort(A2,B2),sort(A3,B3).
   56sort_aot(d(A1,A2,A3),d(B1,B2,B3)):-
   57	sort(A1,B1),sort(A2,B2),sort(A3,B3).
   58
   59%
   60make_aot(X, Y):- once(make_aot(X, Y, root)).
   61
   62make_aot(and(X,Y), Z, _):-
   63	once(make_aot(X, X0, and)),
   64	once(make_aot(Y, Y0, and)),
   65	once(make_and_node(X0, Y0, Z)).
   66make_aot(or(X,Y), Z, _):-
   67	once(make_aot(X, X0, or)),
   68	once(make_aot(Y, Y0, or)),
   69	once(make_or_node(X0, Y0, Z)).
   70make_aot(not(X), Y, SW):-
   71	( SW = and -> Y= c([],[X],[])
   72	; SW = or  -> Y= d([],[X],[])
   73	; Y  = not(X)
   74	).
   75make_aot(X, Y, SW):- integer(X), !,
   76	( SW = and -> Y= c([X],[],[])
   77	; SW = or  -> Y= d([X],[],[])
   78	; Y = X
   79	).
   80make_aot(X, X, _).
   81
   82%
   83make_and_node(true, X, X).
   84make_and_node(false, _, false).
   85make_and_node(X, true, X).
   86make_and_node(_, false, false).
   87make_and_node(c(A1,A2,A3), c(B1, B2, B3), c(C1,C2,C3)):-
   88		union(A1,B1,C1),
   89		union(A2,B2,C2),
   90		union(A3,B3,C3).
   91make_and_node(c(A1,A2,A3),  D, c(A1, A2, [D|A3])):-
   92	D=d(_,_,_).
   93make_and_node(D, c(A1,A2,A3),  c(A1, A2, [D|A3])):-
   94	D=d(_,_,_).
   95make_and_node(X, Y, c([], [], [X, Y])):-
   96	X=d(_,_,_), Y=d(_,_,_).
   97
   98%
   99make_or_node(true, _, true).
  100make_or_node(false, X, X).
  101make_or_node(_, true, true).
  102make_or_node(X, false, X).
  103make_or_node(d(A1,A2,A3), d(B1, B2, B3), d(C1,C2,C3)):-
  104		union(A1,B1,C1),
  105		union(A2,B2,C2),
  106		union(A3,B3,C3).
  107make_or_node(d(A1,A2,A3), C, d(A1,A2,[C|A3])):-
  108		C=c(_,_,_).
  109make_or_node(C, d(A1,A2,A3), d(A1,A2,[C|A3])):-
  110		C=c(_,_,_).
  111make_or_node(A, B, d([], [],[A, B])):-
  112		A=c(_,_,_), B=c(_,_,_).
  113
  114
  115
  116% test1
  117% ?- prop_to_naot(true, X).
  118% ?- prop_to_naot(false, X).
  119% ?- prop_to_naot(X, RR).
  120% ?- prop_to_naot(X<->X, RR).
  121% ?- prop_to_naot(\(X<->X), RR).
  122% ?- prop_to_naot(A;B, X).
  123% ?- prop_to_naot(A, X).
  124% ?- prop_to_naot(not(A), X).
  125% ?- prop_to_naot(A;B;C;D,X).
  126% ?- prop_to_naot(\(A;B;C;D), X).
  127% ?- problem(1, P), prop_to_naot(P, X).
  128% ?- problem(2, P), prop_to_naot(P, X).
  129% ?- problem(3, P), prop_to_naot(P, X).
  130% ?- problem(4, P), prop_to_naot(P, X).
  131% ?- problem(5, P), prop_to_naot(P, X).
  132% ?- (time(problem(30, P)), !, time(prop_to_naot(P, X)), !), fail; true.
  133%@ % 14,571 inferences, 0.004 CPU in 0.004 seconds (90% CPU, 4012944 Lips)
  134%@ % 2,028,635 inferences, 3.622 CPU in 3.634 seconds (100% CPU, 560014 Lips)
  135% ?- (time(problem(40, P)), !, time(prop_to_naot(P, X)), !), fail; true.
  136%@ % 33,825 inferences, 0.009 CPU in 0.010 seconds (88% CPU, 3757498 Lips)
  137%@ % 4,717,045 inferences, 20.056 CPU in 20.114 seconds (100% CPU, 235195 Lips)
  138% ?- prop_to_naot((A+B)*(C+D)*(E+F)*(G+H)*(I+J)*(K+L)*(M+N)*
  139% (O+P)*(Q+R)*(S+T)*(U+V)*(W+X)*(Y+Z), RR).
  140% ?- prop_to_naot(\ ((A+B)*(C+D)*(E+F)*(G+H)*(I+J)*(K+L)*(M+N)*
  141% (O+P)*(Q+R)*(S+T)*(U+V)*(W+X)*(Y+Z)), RR, Zip).
  142
  143prop_to_naot(X, Y):- once(prop_to_aot(X, Z, _Zip)),
  144		 once(reduce_aot(Z, Y, a([],[]))).
  145
  146prop_to_naot(X, Y, Zip):- once(prop_to_aot(X, Z, Zip)),
  147		 once(reduce_aot(Z, Y, a([],[]))).
  148
  149%
  150reduce_literal(true, true, _).
  151reduce_literal(false, false, _).
  152reduce_literal(not(X), Y, Anc):- !, Anc=a(P, N),
  153			(	memberchk(X, P)->  Y = false
  154			;   memberchk(X, N)->  Y = true
  155			;	Y = c([],[X],[])
  156			).
  157reduce_literal(X, Y, Anc):- Anc=a(P, N),
  158			(	memberchk(X, P)->  Y = true
  159			;   memberchk(X, N)->  Y = false
  160			;	Y = c([X],[],[])
  161			).
  162
  163%
  164reduce_aot(X, Y, Anc):- literal(X), !,	reduce_literal(X, Y, Anc).
  165reduce_aot(c(A1,A2,_), false, _):- meet(A1, A2), !.
  166reduce_aot(c(A1,A2,_), false, a(P,N)):- (meet(A1, N); meet(A2, P)), !.
  167reduce_aot(d(A1,A2,_), true, _):- meet(A1, A2), !.
  168reduce_aot(d(A1,A2,_), true, a(P,N)):- (meet(A1, P); meet(A2, N)), !.
  169reduce_aot(c(A1,A2,A3), B,  a(P,N)):- subtract(A1, P, B1),
  170					  subtract(A2, N, B2),
  171					  union(B1, P, P0),
  172					  union(B2, N, N0),
  173					  sort(A3, B3),
  174					  reduce_aot_conj(B3, c(B1, B2,[]), B0, a(P0,N0)),
  175					  reduce_singleton(B0, B).
  176
  177reduce_aot(d(A1,A2,A3), B,  a(P,N)):- subtract(A1, N, B1),
  178					  subtract(A2, P, B2),
  179					  sort(A3, B3),
  180					  reduce_aot_disj(B3, d(B1, B2,[]), B0, a(P, N)),
  181					  reduce_singleton(B0, B).
  182%
  183reduce_singleton(d([], [], []), false).
  184reduce_singleton(d([], [], [X]), Y):- reduce_singleton(X, Y).
  185reduce_singleton(c([], [], []), true).
  186reduce_singleton(c([], [], [X]), Y):- reduce_singleton(X, Y).
  187reduce_singleton(d(A1,A2,_), true):-	meet(A1, A2), !.
  188reduce_singleton(d(A1,A2,A3), R):-	select(d(B1,B2,B3), A3, A4), !,
  189	union(A1, B1, C1),
  190	union(A2, B2, C2),
  191	union(B3, A4, A5),
  192	reduce_singleton(d(C1, C2, A5), R).
  193reduce_singleton(c(A1,A2,_), false):-	meet(A1, A2), !.
  194reduce_singleton(c(A1,A2,A3), R):-	select(c(B1,B2,B3), A3, A4), !,
  195	union(A1, B1, C1),
  196	union(A2, B2, C2),
  197	union(B3, A4, A5),
  198	reduce_singleton(c(C1, C2, A5), R).
  199reduce_singleton(c(A1,A2,[d([X],[],[])]),c([X|A1], A2, [])).
  200reduce_singleton(c(A1,A2,[d([],[X],[])]),c(A1, [X|A2], [])).
  201reduce_singleton(c(A1,A2,[d([],[],[X])]),R):- !,
  202	reduce_singleton(c(A1, A2, [X]), R).
  203reduce_singleton(d(A1,A2,[c([X],[],[])]),d([X|A1], A2, [])).
  204reduce_singleton(d(A1,A2,[c([],[X],[])]),d(A1, [X|A2], [])).
  205reduce_singleton(d(A1,A2,[c([],[],[X])]),R):- !,
  206	reduce_singleton(d(A1, A2, [X]), R).
  207reduce_singleton(X, X).
  208
  209%
  210push_aot_disj(d(A1,A2,A3), d(B1,B2,B3), d(C1,C2,C3)):-
  211	union(A1,B1,C1),
  212	union(A2,B2,C2),
  213	union(A3,B3,C3).
  214push_aot_disj(A, d(B1,B2,B3), d(B1,B2,[A|B3])).
  215%
  216reduce_aot_disj([], X, Y, _):-sort_aot(X, Y).
  217reduce_aot_disj([A|As], X, Y, Anc):- reduce_aot(A, A0, Anc),
  218		  ( A0=false -> reduce_aot_disj(As, X, Y, Anc)
  219		  ; A0=true ->  Y=true
  220		  ; push_aot_disj(A0, X, X0),
  221			reduce_aot_disj(As, X0, Y, Anc)
  222		  ).
  223%
  224push_aot_conj(c(A1,A2,A3), c(B1,B2,B3), c(C1,C2,C3)):-
  225	union(A1,B1,C1),
  226	union(A2,B2,C2),
  227	union(A3,B3,C3).
  228push_aot_conj(A, c(B1,B2,B3), c(B1,B2,[A|B3])).
  229
  230%
  231reduce_aot_conj([], X, Y, _):- sort_aot(X, Y).
  232reduce_aot_conj([A|As], X, Y, Anc):- reduce_aot(A, A0, Anc),
  233		  ( A0=true -> reduce_aot_conj(As, X, Y, Anc)
  234		  ; A0=false ->  Y=false
  235		  ; push_aot_conj(A0, X, X0),
  236			reduce_aot_conj(As, X0, Y, Anc)
  237		  ).
  238% ?- module(naot).
  239
  240
  241% ?- trace, prop_to_naot(X->true, R), subst_aot(R, V, 1, true).
  242% ?- trace, prop_to_naot(X=Y, R), subst_aot(R, V, 1, true),
  243%	subst_aot(V, U, 2, true), eval_ground_aot(U, W).
  244
  245% ?- trace, prop_to_naot(X=Y, R), subst_aot(R, V, 1, true),
  246% ?- prop_to_naot(X=Y, R).
  247% ?- prop_to_naot(X=Y, R), subst_aot(R, V, 1, true), subst_aot(V, V0, 2, true).
  248% ?- prop_to_naot(X=Y, R), subst_aot(R, V, 1, true), trace, subst_aot(V, V0, 2, true).
  249% ?- prop_to_naot(X=Y, R), subst_aot(R, V, 1, false), trace, subst_aot(V, V0, 2, false).
  250% ?- prop_to_naot(X=Y, R), subst_aot(R, V, 1, true), trace, subst_aot(V, V0, 2, false).
  251% ?- prop_to_naot(X=Y, R), subst_aot(R, V, 1, false), trace, subst_aot(V, V0, 2, true).
  252
  253subst_aot(true, true, _, _).
  254subst_aot(false, false, _,_).
  255subst_aot(c(X, Y, Z), U, I, V):-
  256	subst_aot_c_p(X, X0,  I, V),
  257	(	X0 = false -> U=false
  258	;	subst_aot_c_n(Y, Y0, I, V),
  259		( Y0 =false -> U=false
  260		; subst_aot_list_c(Z, Z0, I, V),
  261			(	Z0=false -> U = false
  262			;	X0=[], Y0=[], Z0=[] ->  U = true
  263			;	U=c(X0,Y0,Z0)
  264			)
  265		)
  266	).
  267subst_aot(d(X,Y,Z), U, I, V):-
  268	subst_aot_d_p(X, X0, I, V),
  269	(	X0= true -> U=true
  270	;	subst_aot_d_n(Y, Y0, I, V),
  271		( Y0=true -> U=true
  272		; subst_aot_list_d(Z, Z0, I, V),
  273			(	Z0=true -> U = true
  274			;	X0=[], Y0=[], Z0=[] ->  U = false
  275			;	U=d(X0,Y0,Z0)
  276			)
  277		)
  278	).
  279
  280%
  281subst_aot_c_p(Xs, Ys, X, V):- select(X, Xs, Zs), !,
  282	(	V = false -> Ys =false
  283	;	Ys = Zs
  284	).
  285subst_aot_c_p(Xs, Xs, _, _).
  286%
  287subst_aot_c_n(Xs, Ys, X, V):- select(X, Xs, Zs), !,
  288	(	V = true -> Ys =false
  289	;	Ys = Zs
  290	).
  291subst_aot_c_n(Xs, Xs, _, _).
  292%
  293subst_aot_d_p(Xs, Ys, X, V):- select(X, Xs, Zs), !,
  294	(	V = true -> Ys =true
  295	;	Ys = Zs
  296	).
  297subst_aot_d_p(Xs, Xs, _, _).
  298%
  299subst_aot_d_n(Xs, Ys, X, V):- select(X, Xs, Zs), !,
  300	(	V = false -> Ys =true
  301	;	Ys = Zs
  302	).
  303subst_aot_d_n(Xs, Xs, _, _).
  304%
  305subst_aot_list_c(Ms, R, X, V):- subst_aot_list_c(Ms, Ns, Ball, X, V),
  306	( var(Ball)	-> 	R=Ns
  307	; R=Ball
  308	).
  309%
  310subst_aot_list_c([], [], _, _, _).
  311subst_aot_list_c([M|Ms], Ps, Ball, X, V):- subst_aot(M, N, X, V),
  312	(  N = true   -> subst_aot_list_c(Ms, Ps, Ball, X, V)
  313	;  N = false  -> Ball = false
  314	;  Ps=[N|Ns],
  315	   subst_aot_list_c(Ms, Ns, Ball, X, V)
  316	).
  317%
  318subst_aot_list_d(Ms, R, X, V):- subst_aot_list_d(Ms, Ns, Ball, X, V),
  319	( var(Ball)	-> 	R=Ns
  320	; R=Ball
  321	).
  322%
  323subst_aot_list_d([], [], _, _, _).
  324subst_aot_list_d([M|Ms], Ps, Ball, X, V):- subst_aot(M, N, X, V),
  325	(  N = false   -> subst_aot_list_d(Ms, Ps, Ball, X, V)
  326	;  N = true  -> Ball = true
  327	;  Ps = [N|Ns],
  328	   subst_aot_list_d(Ms, Ns, Ball, X, V)
  329	).
  330%
  331prop_to_aot(X,Y):- prop_to_aot(X,Y,_).
  332
  333
  334prop_to_aot(X, Y, Zip):- var_to_int(X, IX, Zip),
  335					once(expand_macro(IX, X0)),
  336					once(demorgan(X0, X1)),
  337					once(make_aot(X1, Y)).
  338
  339%
  340var_to_int(X, Y, Zip):- term_variables(X, Vs),
  341						copy_term((Vs,X), (Us,Y)),
  342						numlist(1, Us),
  343						zip(Us, Vs, Zip).
  344%
  345numlist(_, []).
  346numlist(N, [N|R]):- succ(N, N0), numlist(N0, R).
  347
  348% ?- literal(false).
  349eval_ground_aot(true, true).
  350eval_ground_aot(false, false).
  351eval_ground_aot(c(P,N,L), R):-
  352	( (	memberchk(false, P)
  353	  ;	memberchk(false, N)
  354	  ;	member(M, L),
  355		eval_ground_aot(M, R0),
  356		R0 = false
  357	  ) ->  R = false
  358	; R = true
  359	).
  360eval_ground_aot(d(P,N,L), R):-
  361	( (	memberchk(true, P)
  362	  ;	memberchk(true, N)
  363	  ;	member(M, L),
  364		eval_ground_aot(M, R0),
  365		R0 = true
  366	  ) ->  R = true
  367	; R = false
  368	).
  369
  370% ?- prop_to_aot(X, R).
  371% ?- prop_to_aot((X<->Y)=true, A, Z).
  372% ?- prop_to_aot(true<->true, A, Z).
  373% ?- prop_to_aot(true->true, R).
  374% ?- prop_to_aot(true<->true, R).
  375% ?- prop_to_aot(true<->false, R).
  376
  377macro(\+(X),	not(X)).
  378macro(\(X),		not(X)).
  379macro(X\=Y,		not(X=Y)).
  380macro((X,Y),	and(X,Y)).
  381macro(/\(X, Y), and(X,Y)).
  382macro(X*Y,		and(X,Y)).
  383macro((X;Y),	or(X,Y)).
  384macro(\/(X,Y),	or(X,Y)).
  385macro(X+Y,		or(X,Y)).
  386macro(X->Y,		or(not(X), and(X,Y))).
  387macro(X=Y,		and(X->Y, Y->X)).
  388macro(X<->Y,	X=Y).
  389macro(X<=>Y,	X=Y).
  390macro(X~Y,		X=Y).
  391macro(++(X,Y),	not(X=Y)).
  392macro(exor(X, Y), not(X=Y)).
  393macro(nand(X, Y), not(and(X,Y))).
  394
  395%
  396expand_macro(X, X):- integer(X), !.
  397expand_macro(X, Y):- macro(X, X0), !,
  398	expand_macro(X0, Y).
  399expand_macro(A,  B):- A=..[F|As],
  400	maplist(expand_macro, As, Bs),
  401	B=..[F|Bs].
  402
  403%
  404demorgan(and(X, Y), and(X0, Y0)):- demorgan(X, X0),
  405								   demorgan(Y, Y0).
  406demorgan(or(X, Y), or(X0, Y0)):- demorgan(X, X0),
  407								   demorgan(Y, Y0).
  408
  409demorgan(not(not(X)), Y):- demorgan(X, Y).
  410demorgan(not(and(X, Y)), or(X0, Y0)):- demorgan(not(X), X0),
  411									   demorgan(not(Y), Y0).
  412demorgan(not(or(X,Y)), and(X0, Y0)):- demorgan(not(X), X0),
  413									demorgan(not(Y), Y0).
  414demorgan(not(true), false).
  415demorgan(not(false), true).
  416demorgan(X, X).
  417
  418
  419		/*****************************
  420		*     a la Burse's sample    *
  421		*****************************/
  422% ?-  problem(4, Prop), build_robdd(V0s, Prop, N, Zip), writeln(done).
  423% ?-  problem(5, Prop), build_robdd(V0s, Prop, N, Zip), writeln(done).
  424% ?-  problem(5, Prop), build_robdd(V0s, Prop, N, Zip),
  425
  426matrix(N, M):- length(M, N), maplist(col(N), M).
  427
  428col(N, L):- length(L, N).
  429
  430problem(N, P):- matrix(N, M), constraint(M, P).
  431
  432inner_product([X], [Y], X*Y).
  433inner_product([X|Xs], [Y|Ys], X*Y + Z):- inner_product(Xs, Ys, Z).
  434%
  435
  436constraint([V], E=true):- inner_product(V, V, E).
  437constraint([V|Vs], (E=true)*C*D):- inner_product(V, V, E),
  438	constraint(Vs, D),
  439	inner_constraint_one(V, Vs, C).
  440%
  441inner_constraint_one(V, [U], C=false):- inner_product(V, U, C).
  442inner_constraint_one(V, [U|Us], (C=false)*D):-
  443	inner_product(V, U, C),
  444	inner_constraint_one(V, Us, D)