1:- module(zmod,
    2  [		(<<)/2, (<<)/3, fetch_state/1, fetch_state/2
    3	,	card/3
    4	,	ltr_join/4, ltr_join_list/3, ltr_join_list/4
    5  	,	ltr_merge/4, ltr_card/3
    6	,   card_filter_gte/4, card_filter_lte/4, card_filter_between/5
    7	,	max_length/3
    8  	,	sat/1, sat_count/1, sat_count/2
    9	,	set_at/3
   10	,	obj_id/3
   11	,	dnf/3, cnf/3, nnf_dnf/3, nnf_cnf/3
   12	,	all_fun/4, s_map/3, s_map/4
   13	,	all_mono/4, all_epi/4, merge_funs/3
   14	,	bdd_list/3, bdd_list_raise/4, bdd_append/4, bdd_interleave/4
   15	,	opp_compare/3
   16	,	(zdd)/1, zdd0/1, zdd_eval/3, zdd_eval/4, (ltr_zdd)/1
   17	, 	zdd_append/4
   18	, 	zdd_insert/4, zdd_insert/5, zdd_insert_atoms/3, zdd_cons/4
   19	,	l_cons/4
   20	,	zdd_insert_atoms/4
   21	,	zdd_ord_insert/4, zdd_reorder/4
   22	,	zdd_has_1/2
   23  	,	zdd_memberchk/2, zdd_memberchk/3
   24    ,	zdd_family/3
   25    ,	zdd_subfamily/3
   26	,	zdd_join/4, zdd_join_1/3, zdd_join_list/3, zdd_join_list/4
   27  	,	zdd_singleton/3
   28	,	zdd_merge/4
   29	,	zdd_merge_list/4
   30	,	zdd_meet/4
   31	,	zdd_subtr/4, zdd_subtr_1/3, zdd_xor/4
   32  	,	zdd_div/4, zdd_mod/4, zdd_divmod/5, zdd_div_div/5
   33	,	zdd_mod_by_list/4, zdd_div_by_list/4, zdd_divisible_by_list/4
   34	,	zdd_power/3, zdd_ord_power/4
   35	,	zdd_rand_path/2, zdd_rand_path/3, zdd_rand_path/4
   36	,	ltr_meet_filter/4, ltr_join_filter/4
   37	,	get_extra/1, get_extra/2
   38	,	get_key/3, atom_index/2
   39	,	set_key/3, update_key/4, bump_up/3
   40	,   set_pred/2, set_pred/3, set_pred/2, set_pred/3
   41	,	zdd_compare/4
   42	,	zdd_sort/3
   43  	,	open_key/3, close_key/2
   44	,	set_compare/1, set_compare/2, get_compare/2
   45	,	use_zdd/1, use_zdd/2, pred_zdd/2, pred_zdd/3
   46	,	zdd_sort_rev/2, zdd_sort_rev/3
   47	,   map_zdd/4, zdd_find/4
   48    ,	psa/2, psa/0, psa/3, mp/2, mp/3
   49    ,	sets/3, ppoly/2, poly_term/2, poly_term/3
   50    ,	eqns/3
   51	,	zdd_list/3, zdd_lift/3
   52	,	significant_length/3
   53	,	charlist/2, charlist/3, atomlist/2
   54	,	op(900, xfx, <<)
   55	,	op(1150, fy, zdd)
   56	,	op(1150, fy, ltr_zdd)
   57  ]).   58
   59
   60% :- doc_server(7000).
   61% :- use_module(library(pldoc/doc_library)).
   62% :- doc_load_library.
   63% :- doc_browser.
   64
   65:- use_module(library(apply)).   66:- use_module(library(apply_macros)).   67:- use_module(library(clpfd)).   68:- use_module(library(statistics)).   69:- use_module(zdd('zdd-array')).   70:- use_module(util(math)).   71:- use_module(util(meta2)).   72:- use_module(pac(basic)).   73:- use_module(pac(meta)).   74:- use_module(util(misc)).   75:- use_module(pac('expand-pac')). % For the kind block.
   76:- use_module(pac(op)).   77:- use_module(zdd('path-count-by-mate-frontier')).   78
   79:- set_prolog_flag(stack_limit, 10_200_147_483_648).   80
   81attr_unify_hook(V, Y):-
   82	(	get_attr(Y, zdd, A)
   83	->	zdd_unify(V, A)
   84	; 	zdd_unify(V, Y)
   85	).
   86
   87 :- op(800, xfy, &).   88 :- op(820, fy, \).			% NOT
   89 :- op(830, xfy, /\).		% AND
   90 :- op(840, xfy, \/).		% OR
   91 :- op(860, xfy, ~).		% equivalence
   92 :- op(860, xfy, #).		% exor
   93 :- op(860, xfy, <->).		% equivalence
   94 :- op(860, xfy, <=> ).		% equivalence
   95 :- op(870, yfx, <-).   96
   97% for pac query.
   98term_expansion --> pac:expand_pac.
   99
  100% ?- zdd udg_path_count(a, b, [a-b,b-c,a-c], C).
  101% ?- zdd C<< :(!udg_path_count(a, b, [a-b,b-c,a-c])).
  102% ?- udg_path_count(a, b, [a-b,b-c,a-c], C, S).
  103% ?- (zdd true).
  104% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), Z<< (X+Y), U<< card(Z).
  105% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), Z<< :arith(X+Y).
  106% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), { Z is X+Y }.
  107% ?- numlist(1, 16, L), zdd((X<< pow(L), card(X, C))).
  108%@ L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
  109%@ X = 17,
  110%@ C = 65536.
  111% ?- numlist(1, 16, L), zdd((X<< pow(L))).
  112% ?- numlist(1, 10000, L), zdd((X<< pow(L), card(X, C))).
  113% ?- numlist(1, 16, L),
  114% zdd((X<< pow(L), Y<<pow(L), Z << (X+Y),  U<< (X*Y), card(X, C))).
  115% ?- time((numlist(1, 40, L),
  116% zdd((X << pow(L), Y<<pow(L), Z << merge(X, Y), card(Z, C))))).
  117% ?- zdd((set_memo(a-1))).
  118% ?- zdd((set_memo(a-1), set_memo(a-2), memo(a-V))).
  119% ?- zdd set_memo(a-1), set_memo(a-2), memo(a-V).
  120% ?- zdd X<<{[1,1]}, psa(X).
  121% ?- zdd X<< pow(:numlist(0,1)), psa(X).
  122% ?- zdd((X<<pow([1,2,3]), psa(X))).
  123% ?- zdd((X<< *([1,2,3,1]), psa(X))).
  124% ?- zdd((X<< +([1,2,3,1]), psa(X))).
  125% ?- zdd((X<< family([[1],[1,2], [1]]), psa(X))).
  126% ?- zdd((X<< family([[a-b, b-c]]), prz(X))).
  127% ?- zdd  memo(a-1), memo(a-X).
  128
  129% ?- zdd(use_zdd(use_zdd((#memo(a-1), #memo(a-X))))).
  130% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))}, sets(X, Sx))).
  131% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))},
  132%	sets(X, Sx), sets(Y, Sy1))).
  133% ?- zdd((set_key(root, hello), get_key(root, R))).
  134% ?- zdd((all_fun([a],[b], F), psa(F))).
  135% ?- zdd((all_fun([],[b], F), psa(F))).
  136% ?- zdd((all_fun([a],[], F), psa(F))).
  137% ?- zdd((all_fun([a,b],[c,d], F), psa(F), card(F, C))).
  138% ?- N = 20, numlist(1, N, A),  raise_list(A, 2, A2), zdd((all_fun(A2, A, F), card(F, C))).
  139% ?- time((N=100, M=100,  numlist(1, N, Ns), numlist(1, M, Ms),
  140%	zdd((all_fun(Ns, Ms, F), card(F, C))))).
  141
  142% Cardinality # of Y^X = { f | f: X-> Y }.
  143%   ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J).
  144
  145% ?- I=1, J=1, K=1, L=1,
  146%	numlist(1, I, X), numlist(1, K, Y),
  147%	raise_list(X, J, Xj),
  148%	raise_list(Y, L, Yl),
  149%	time( ( call_with_time_limit(200, (
  150%		zdd((all_fun(Xj, Yl, F), card(F, C))))),
  151%		C =:= (K^L)^(I^J),
  152%	    significant_length(C, Keta, 10))).
  153
  154% ?- I=3, J=5, K=3, L=5,
  155%	numlist(1, I, X), numlist(1, K, Y),
  156%	raise_list(X, J, Xj),
  157%	raise_list(Y, L, Yl),
  158%	time( ( call_with_time_limit(200, (
  159%		zdd((all_fun(Xj, Yl, F), card(F, C))))),
  160%		C =:= (K^L)^(I^J),
  161%		significant_length(C, Keta, 10))).
  162
  163significant_length(0, 0, _):-!.
  164significant_length(X, 1, Radix):- X < Radix, !.
  165significant_length(X, L, Radix):- Y is X // Radix,
  166	significant_length(Y, L0, Radix),
  167	L is L0+1.
  168%
  169zdd_atom(X):- shift(zdd_atom(X)).
  170%
  171zdd_atom(X, S):- get_key(is_atom, Pred, S), !,	call(Pred, X).
  172zdd_atom(X, _):- (atomic(X); dvar(X)), !.
 obj_id(?X, ?Y, +S) is det
Bidirectional. Y is the atom of the root X. ?- zdd obj_id([a,b,c], Id), obj_id(Obj, Id).
  177obj_id(X, Id, S):- cofact(Id, t(X, 0, 1), S).
  178%
  179hyphen(X, Y, X-Y).
  180comma(X, Y, (X,Y)).
  181equality(X, Y, (X=Y)).
  182dvar('$VAR'(_)).
  183
  184		/*****************************************
  185		*     all_fun/all_mono/all_epi in ZDD    *
  186		*****************************************/
 all_fun(+D, +R, -F, +S) is det
F is unified with the family of functions from D to R.
  190% ?- zdd all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F).
  191% ?- zdd all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C).
  192% ?- N = 100, numlist(1, N, Ns), (zdd  all_fun(Ns, Ns, F), card(F, C)).
  193% ?-	numlist(1, 5, Ns),  numlist(6, 10, Ms),
  194%		(zdd
  195%			all_fun(Ns, Ns, F),
  196%			all_fun(Ms, Ms, G),
  197%			zdd_merge(F, G, H),
  198%			card(H, C)
  199%		),
  200%		C =:= 5^5 * 5^5.
  201
  202all_fun(D, R, F, S):- zdd_sort(D, D0, S),
  203	zdd_sort(R, R0, S),
  204	length(D0, I),
  205	length(R0, J),
  206	(	I > 0, J = 0  -> F = 0
  207	;	zdd_append(D0, 1, D1, S),
  208		findall_fun(D1, R0, F, S)
  209	).
  210%
  211findall_fun(X, _, X, _):- X < 2, !.
  212findall_fun(X, Rng, Y, S):- memo(findall_fun(X)-Y, S),
  213	(	nonvar(Y) -> true		% , write(.)  % many hits.
  214	;	cofact(X, t(A, L, R), S),
  215		findall_fun(L, Rng, L0, S),
  216		findall_fun(R, Rng, R1, S),
  217		join_for_alt_val(A, Rng, R1, 0, R0, S),
  218		zdd_join(L0, R0, Y, S)
  219	).
  220%
  221join_for_alt_val(_, [], _, V, V, _).
  222join_for_alt_val(A, [B|Bs], F, F0, F1, S):-
  223	zdd_cons(F2, A-B, F, S),
  224	zdd_join(F0, F2, F3, S),
  225	join_for_alt_val(A, Bs, F, F3, F1, S).
 all_mono(+D, +R, -F, +S) is det
F is unified with all injections from D to R.
  230% ?- zdd all_mono([1],[a], Is), psa(Is).
  231% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is).
  232% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is).
  233% ?- zdd all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C).
  234% ?- zdd all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C).
  235% ?- time((numlist(1, 10, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)), factorial(10, C))).
  236% ?- time((numlist(1, 12, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)))).
  237% ?- N =10, numlist(1, N, Ns), time((zdd all_mono(Ns, Ns, F), card(F, C))), factorial(N, C).
  238
  239all_mono(D, R, F, S):-  zdd_sort(D, D0, S),
  240	zdd_sort(R, R0, S),
  241	length(D0, I), length(R0, J),
  242	(	I @=< J ->
  243		zdd_append(D0, 1, D1, S),
  244		findall_mono(D1, R0, F, S)
  245	;	F = 0
  246	).
  247
  248% ?- zdd zdd_append([], 1, X), findall_mono(X, [a], Y).
  249% ?- zdd zdd_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y).
  250% ?- zdd { N=14, numlist(1, N, Ns)}, zdd_append(Ns, 1, X),
  251%   findall_mono(X, Ns, Y), card(Y, C),
  252%	{ factorial(14, D), ( D=:=C -> writeln("OK")) }.
  253
  254findall_mono(X, _, X, _):- X < 2, !.
  255findall_mono(X, Rng, Y, S):- memo(findall_mono(X,Rng)-Y, S),
  256	(	nonvar(Y) -> true		% , write(.)  % many hits.
  257	;	cofact(X, t(A, L, R), S),
  258		findall_mono(L, Rng, L0, S),
  259		findall_mono(A, R, Rng, R0, S),
  260		zdd_join(L0, R0, Y, S)
  261	).
  262%
  263findall_mono(A, R, Rng, R0, S):- findall(B-U, select(B, Rng, U), Cases),
  264	findall_mono(Cases, A, R, 0, R0, S).
  265%
  266findall_mono([], _A, _R, V, V, _).
  267findall_mono([B-Rng|Cases], A, R, U, V, S):-
  268	findall_mono(R, Rng, U0, S),
  269	cofact(U1, t(A-B, 0, U0), S),
  270	zdd_join(U, U1, U2, S),
  271	findall_mono(Cases, A, R, U2, V, S).
 all_epi(+D, +R, -F, +S) is det
F is unified with the family of functions from D to R.
  277% ?- zdd all_epi([],[], F).
  278% ?- zdd all_epi([a],[1], F), psa(F).
  279% ?- zdd all_epi([a,b],[1], F), psa(F).
  280% ?- zdd all_epi([a],[1,2], F), psa(F).
  281% ?- zdd all_epi([a,b,c],[1,2], F), psa(F).
  282% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (zdd all_epi(Ns, Ms, F)).
  283% ?- time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (zdd all_epi(Ns, Ms, F)))).
  284
  285all_epi(D, R, F, S):-
  286	zdd_sort(D, D0, S),
  287	zdd_sort(R, R0, S),
  288	length(D0, I), length(R0, J),
  289	(	I @>= J ->
  290		zdd_append(D0, 1, D1, S),
  291		findall_epi(D1, R0-R0, F, S)
  292	;	F = 0
  293	).
 all_perm(+L, -P, +S) is det
P is unified with the family of permuations of L.
  298% ?- N=2, numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C), psa(X)).
  299% ?- N=3, numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C), psa(X)).
  300% ?- N=10, numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C)).
  301% ?- N=11, numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C)).
  302% ?- N=14, time((numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C)))).
  303% ?- N=15, time((numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C))))X.
  304% ?- N=16, time((numlist(1, N, Ns),  (zdd all_perm(Ns, X), card(X, C)))).
  305%@ % 185,729,299 inferences, 205.838 CPU in 207.237 seconds (99% CPU, 902308 Lips)
  306% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R),
  307%  length(R, L).
  308
  309all_perm(D, P, S):-  zdd_sort(D, D0, S),
  310	findall_perm(D0, P, S).
  311%
  312findall_perm([], 1, _):-!.
  313findall_perm(D, X, S):- memo(perm(D)-X, S),
  314	( nonvar(X) -> true		%	, write(.) % many hits.
  315	;
  316	findall(I-D0, select(I, D, D0), U),
  317	join_perm_for_selection(U, 0, X, S)).
  318%
  319join_perm_for_selection([], X, X, _).
  320join_perm_for_selection([I-D|U], X, Y, S):-
  321	findall_perm(D, X0, S),
  322	zdd_cons(X1, I, X0, S),
  323	zdd_join(X1, X, X2, S),
  324	join_perm_for_selection(U, X2, Y, S).
  325
  326		/*************************************************
  327		*     terms in ZDD based on families of lists    *
  328		*************************************************/
 coalgebra_for_signature(+D, +Sgn, +As, -E, +S) is det
E is unified with the set of all functions from D to the set of signature terms over signature Sgn and with arguments in As. In short, this generates coalgebra for the signature as an operation.
  337% ?- zdd coalgebra_for_signature([x], [f/1], [x], E), psa(E).
  338% ?- zdd coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E).
  339% ?- time((zdd coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2],
  340%	[x,y,z,u,v,0,1], E), card(E, C))).
  341%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips)
  342%@ E = 173825,
  343%@ C = 68641485507.
  344
  345coalgebra_for_signature(D, Sgn, As, E, S):-
  346	signature(Sgn, As, T, S),
  347	signature_map(D, T, E, S).
  348%
  349signature_map([], _, 1, _):-!.
  350signature_map([X|Xs], T, E, S):-
  351	signature_map(Xs, T, E0, S),
  352	extend_signature_map(X, T, E0, E, S).
  353%
  354extend_signature_map(_, 0, _, 0, _):-!.
  355extend_signature_map(_, 1, E, E, _):-!.
  356extend_signature_map(X, T, E, F, S):- cofact(T, t(A, L, _), S),
  357	extend_signature_map(X, L, E, E0, S),
  358	l_cons(X->A, E, E1, S),
  359	zdd_join(E0, E1, F, S).
 term_path(?X, ?Y, +S) is det
bidirectional version of term_to_path/term_to_path.
  364% ?- zdd term_path(a, R), psa(R), term_path(A, R).
  365term_path(X, Y, S):-
  366	(	nonvar(X) -> term_to_path(X, Y, S)
  367	;	path_to_term(Y, X, S)
  368	).
 term_to_path(+X, -Y, S) is det
Y is unified with the family of paths from root term X.
  373% ?- zdd term_to_path(a, R), psa(R).
  374% ?- zdd term_to_path(f(a, b), R), psa(R).
  375% ?- zdd term_to_path(f(g(a, b), h(c, d)), R), psa(R).
  376% ?- zdd term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R).
  377term_to_path(X, Y, S):- functor(X, F, N),
  378	(	N = 0 -> zdd_singleton(X, Y, S)
  379 	;	functor(X, F, N),
  380		arg_path(F/N, 1, X, Y, S)
  381	).
  382%
  383arg_path(_/N, J, _, 0, _):- J>N, !.
  384arg_path(F, I, X, Y, S):- J is I + 1,
  385	arg(I, X, A),
  386	term_to_path(A, U, S),
  387	arg_path(F, J, X, V, S),
  388 	cofact(Y, t(arg(F, I), V, U), S).
 path_to_term(+X, -Y, S) is det
Inverse predicte of term_path/3 Y is unified with term whose family of paths is X.
  394% ?- zdd term_to_path(a, X), path_to_term(X, R).
  395% ?- zdd term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R).
  396% ?- zdd term_to_path(f(1,2), X), path_to_term(X, R).
  397% ?- T=f(h(a), 3, g(b,2), 5),
  398%	(zdd term_to_path(T, X), path_to_term(X, R)),  T = R.
  399
  400path_to_term(X, Y, S):- X>1,  cofact(X, t(A, L, R), S),
  401	(	R = 1 -> Y = A
  402	;	A = arg(F/_, _),
  403		path_to_term(R, R0, S),
  404		path_to_term(L, L0, [], S),
  405		Y =..[F, R0|L0]
  406	).
  407%
  408path_to_term(X, U, U, _):- X<2, !.
  409path_to_term(X, [R0|U], V, S):- cofact(X, t(_, L, R), S),
  410	path_to_term(R, R0, S),
  411	path_to_term(L, U, V, S).
 term_path_compare(-C, +X, +Y, S) is det
X, Y are supposed to be the families of paths of some terms U, V, respectively by term_path/3. Then, C is unified with as if compare(C, U, V) is performed.
  418% ?- X=f(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U),
  419%	term_path_compare(C0, T, U)), compare(C, X, Y).
  420% ?- X=g(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U),
  421%	term_path_compare(C0, T, U)), compare(C, X, Y).
  422% ?- X=g(a,b,c), Y=f(a,b), (zdd term_path(X, T), term_path(Y, U),
  423%	term_path_compare(C0, T, U)), compare(C, X, Y).
  424
  425term_path_compare(=, X, X, _):-!.
  426term_path_compare(<, 0, _, _):-!.
  427term_path_compare(>, _, 0, _):-!.
  428term_path_compare(<, 1, _, _):-!.
  429term_path_compare(>, _, 1, _):-!.
  430term_path_compare(C, X, Y, S):- cofact(X, t(A, L, R), S),
  431	cofact(Y, t(B, L0, R0), S),
  432	arity_compare(C0, A, B),
  433	(	C0 = (=) ->
  434		term_path_compare(C1, R, R0, S),
  435		(	C1 = (=) ->
  436			left_branch_compare(C, L, L0, S)
  437		;	C = C0
  438		)
  439	;	C = C0
  440	).
  441
  442% Left branches are for argument lists of the ame length.
  443left_branch_compare(=, 0, 0, _):-!.
  444left_branch_compare(C, X, Y, S):-
  445    cofact(X, t(_, L, R), S),
  446	cofact(Y, t(_, L0, R0), S),
  447	term_path_compare(C0, R, R0, S),
  448	(	C0 = (=) ->
  449		left_branch_compare(C, L, L0, S)
  450	;	C = C0
  451	).
  452
  453%
  454arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G).
  455arity_compare(C, A, B):-!, compare(C, A, B).
 zdd_lift(+X, -Y, +S) is det
Y is unified with flatted X: if X = {A1, ..., An} then Y = {B1, ..., Bn} where Bi is the singleton of Ai.
  462% ?- zdd zdd_lift(1, X).
  463% ?- zdd X<< pow([1,2]), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D), psa(Y).
  464% ?- N=15, numlist(1, N, Ns),
  465% time((zdd X<< pow(Ns), card(X, C), zdd_lift(X, Y), card(Y, D))).
  466%@ C = D, D = 32768,
  467%@ Y = 131040.
  468
  469zdd_lift(X, X, _):- X<2, !.
  470zdd_lift(X, Y, S):- memo(zdd_lift(X)-Y, S),
  471	(	nonvar(Y) -> true	%, write(.)  % So so hits.
  472	;	cofact(X, t(A, L, R), S),
  473		zdd_lift(L, L0, S),
  474		zdd_lift(R, R0, S),
  475		l_cons(A, R0, R1, S),
  476		zdd_join(L0, R1, Y, S)
  477	).
 zdd_univ(+X, -Y, +S) is det
Y is unified with the family of singletons A where A=..B with B being is a member of the family X.
  483% ?- zdd X<< pow([a,b]), card(X, C), zdd_lift(X, Y), card(Y, D), zdd_univ(Y, Z), psa(Z).
  484
  485zdd_univ(X, X, _):- X<2, !.
  486zdd_univ(X, Y, S):- cofact(X, t(A, L, _), S),
  487	zdd_univ(L, L0, S),
  488	U=..A,
  489	cofact(Y, t(U, L0, 1), S).
  490
  491% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R).
  492zdd_univ(0, _, 0, _):-!.
  493zdd_univ(1, Stack, X, S):-!, reverse(Stack, Stack0),
  494	U =.. Stack0,
  495	zdd_singleton(U, X, S).
  496zdd_univ(X, Stack, Y, S):- cofact(X, t(A, L, R), S),
  497	zdd_univ(L, Stack, L0, S),
  498	zdd_univ(R, [A|Stack], R0, S),
  499	zdd_join(L0, R0, Y, S).
 arity_term(+G, +As, -T, +S) is det
T is unified with the family of terms g(a1, ..., an) where G=g/n and ai in As.
  505% ?- zdd arity_term(f/2, [1, x, y], T), psa(T).
  506arity_term(F/N, As, T, S):- memo((F/N)-T, S),
  507	(	nonvar(T) -> true
  508	;	all_list(N, As, X, S),
  509		l_cons(F, X, T0, S),
  510		zdd_univ(T0, [], T, S)
  511	).
 zdd_functor(+F, +X, -Y, +S) is det
Y is unified with the family of singletons G such that G=..[F|As], where As is the reverse of a list in X. Inefficient space usage. l_cons/distribute_cons should be used for large X instead.
  519% ?- N=10, numlist(1, N, Ns),
  520%	time((zdd X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))).
  521% ?- zdd X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y).
  522% ?- N=100, numlist(1, N, Ns),
  523%	time((zdd X<<pow(Ns), l_cons(f, X, Y), card(Y, C))).
  524% ?- N=100, numlist(1, N, Ns),
  525%	time((zdd X<<pow(Ns), distribute_cons([f, g, h], X, Y), card(Y, C))).
  526
  527zdd_functor(F, X, Y, S):- zdd_functor(F, X, [], Y, S).
  528%
  529zdd_functor(_, 0, _, 0, _):-!.
  530zdd_functor(F, 1, St, Y, S):-!, T =..[F|St],
  531	zdd_singleton(T, Y, S).
  532zdd_functor(F, X, St, Y, S):-cofact(X, t(A, L, R), S),
  533	zdd_functor(F, L, St, Y0, S),
  534	zdd_functor(F, R, [A|St], Y1, S),
  535	zdd_join(Y0, Y1, Y, S).
 signature(+G, +As, -T, +S) is det
T is unified with the set of all terms f(a1, ..., an) with f/n in G and ai in As.
  541% ?- zdd signature([f/1, g/2], [1, x, y], U), psa(U).
  542% ?- time((zdd signature([f/2, g/2, h/3, i/4, k/5],
  543%	[0, 1, 2, x, y, z, u, v, w], U), card(U, C))).
  544
  545signature([], _, 0, _):-!.
  546signature([G|Gs], As, T, S):-
  547	arity_term(G, As, T0, S),
  548	signature(Gs, As, T1, S),
  549	zdd_join(T0, T1, T, S).
 power_list(+N, +As, -P, +S) is det
P is unified with lists L such that length of L is less than N, and all members of L is in As.
  555% ?- spy(power_list).
  556% ?- zdd power_list(0, [a,b], P).
  557% ?- zdd power_list(1, [a,b], P).
  558% ?- N = 100, numlist(1, N, _Ns),
  559%	time(((zdd power_list(N, _Ns, X), card(X, _Count)))),
  560%	_Count > 100^100, writeln(_Count).
  561%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips)
  562%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101
  563%@ N = 100,
  564%@ X = 515002.
  565
  566power_list(N, As, P, S):- obj_id(As, Id, S),
  567	power_list_with_id(N, Id, P, S).
  568%
  569power_list_with_id(0, Id, 1, S):-!, memo(power_list(0, Id)-1, S).
  570power_list_with_id(N, Id, Y, S):-
  571	N0 is N - 1,
  572	power_list_with_id(N0, Id, Y0, S),
  573	all_list_with_id(N, Id, Y1, S),
  574	zdd_join(Y0, Y1, Y, S).
 all_list(+N, +As, -X, +S) is det
X is unified with the family of lists L of length N such that all elements of L are in As.
  580% ?- zdd all_list(0, [a], X), psa(X).
  581% ?- zdd all_list(1, [a], X), psa(X).
  582% ?- N=10, numlist(1, N, Ns), (zdd all_list(4, Ns, X), card(X, C)).
  583% ?- N=100, numlist(1, N, Ns), time(((zdd all_list(100, Ns, X), card(X, C)))).
  584%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips)
  585
  586all_list(N, As, Y, S):- obj_id(As, Id, S),
  587	all_list_with_id(N, Id, Y, S).
  588%
  589all_list_with_id(0, Id, 1, S):-!, memo(all_list(0, Id)-1, S).
  590all_list_with_id(N, Id, Y, S):-  memo(all_list(N, Id)-Y, S),
  591	(	nonvar(Y) -> true
  592	;	N0 is N-1,
  593		all_list_with_id(N0, Id, Y0, S),
  594		obj_id(As, Id, S),
  595		distribute_cons(As, Y0, 0, Y, S)
  596	).
 singleton_family(+L, -F, +S) is det
F is unified with the family of sigletones A for A in L.
  601singleton_family([], 0, _):-!.
  602singleton_family([A|As], X, S):-
  603	singleton_family(As, X0, S),
  604	zdd_singleton(A, U, S),
  605	zdd_join(U, X0, X, S).
 distribute_cons(+F, +X, -Y, +S) is det
Y is unified with the family of lists [A|M] for A in F and M in X.
  610distribute_cons(F, X, Y, S):- distribute_cons(F, X, 0, Y, S).
  611%
  612distribute_cons([], _, Y, Y, _).
  613distribute_cons([A|As], Y, U, V, S):-
  614	l_cons(A, Y, V0, S),
  615	zdd_join(U, V0, U0, S),
  616	distribute_cons(As, Y, U0, V, S).
 l_cons(+A, +X, -Y, +S) is det
Y is unified with the family of lists [A|L] for L in X.
  621% ?- zdd X<<pow([1,2]), l_cons(a, X, Y), psa(Y).
  622l_cons(A, Y, U, S):- cofact(U, t(A, 0, Y), S).
 l_append(+L, +X, -Y, S) is det
Y is unified with the family of lists M such that append(L, U, M) with U in X. ?- zdd X<<pow([1,2]), l_append([a,b], X, Y), psa(Y).
  629l_append([], X, X, _).
  630l_append([A|As], X, Y, S):-
  631	l_append(As, X, X0, S),
  632	l_cons(A, X0, Y, S).
  633
  634% ?- zdd zdd_append([], 1, X), findall_epi(X, [a]-[a], Y).
  635% ?- zdd zdd_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C).
  636% ?- zdd zdd_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C).
  637% ?- zdd zdd_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C).
  638% ?- zdd zdd_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y).
  639% ?- N = 2, (zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)).
  640% ?- N = 3, (zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)).
  641% ?- N = 10,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X),
  642%	{ time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}).
  643% ?- N = 11,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X),
  644%	{ time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}).
  645% ?- N = 12,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X),
  646%	{ time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}).
  647% ?- N = 13,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X),
  648%	{ time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}).
  649
  650select_target(Range, U, B, V):- member(B, Range),
  651	(	select(B, U, V) -> true
  652	;	V = U
  653	).
  654
  655%!
  656findall_epi(0, _, 0, _):-!.
  657findall_epi(1, _-U, X, _):-!,
  658	(	U=[] -> X = 1
  659	;	X = 0
  660	).
  661findall_epi(X, RngU, Y, S):- memo(findall_epi(X, RngU)-Y, S),
  662	(	nonvar(Y) -> true		% , write(.)  % many hits.
  663	;	cofact(X, t(A, L, R), S),
  664		findall_epi(L, RngU, L0, S),
  665		findall_epi(A, R, RngU, R0, S),
  666		zdd_join(L0, R0, Y, S)
  667	).
  668%
  669findall_epi(A, R, Rng-U, R0, S):-
  670	findall(B-(Rng-V), select_target(Rng, U, B, V), Cases),
  671	findall_epi(Cases, A, R, 0, R0, S).
  672%
  673findall_epi([], _, _, V, V, _).
  674findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V, S):-
  675	findall_epi(R, Rng-Rng0, U0, S),
  676	cofact(U1, t(A-B, 0, U0), S),
  677	zdd_join(U, U1, U2, S),
  678	findall_epi(Cases, A, R, U2, V, S).
  679
  680% ?- zdd merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X).
  681merge_funs(Fs, X, S):- fold_merge_funs(Fs, 1, X, S).
  682%
  683fold_merge_funs([], X, X, _).
  684fold_merge_funs([G|Fs], X, Y, S):-
  685	fun_block(G, X0, S),
  686	zdd_merge(X, X0, X1, S),
  687	fold_merge_funs(Fs, X1, Y, S).
  688%
  689fun_block(G, X, S):-
  690	(	G = mono(D-R) -> all_mono(D, R, X, S)
  691	;	G = epi(D-R) -> all_epi(D, R, X, S)
  692	;	G = fun(D-R),
  693		all_fun(D, R, X, S)
  694	).
  695
  696% ?- N=2,  numlist(1, N, Ns),
  697%	(zdd  set_compare(opp_compare),
  698%	X<<pow(Ns), psa(X), set_compare(compare),
  699%	zdd_normalize(X, Y), psa(Y)).
  700
  701zdd_normalize(X, X, _):- X<2, !.
  702zdd_normalize(X, Y, S):- memo(normalize(X)-Y, S),
  703	(	nonvar(Y) -> true	%	, write(.) % Many hits.
  704	;	cofact(X, t(A, L, R), S),
  705		zdd_normalize(L, L0, S),
  706		zdd_normalize(R, R1, S),
  707		zdd_insert(A, R1, R0, S),
  708		zdd_join(L0, R0, Y, S)
  709	).
  710
  711% ?- N = 1000, numlist(1, N, Ns),
  712%	time(zdd((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C)))).
  713
  714% ?- N = 1000, numlist(1, N, Ns),
  715%	time(zdd(( X<<pow(Ns),
  716%			  get_family_of_rank(500, X, Y),
  717%			  card(Y, C)))).
 get_family_of_rank(Order, X, F) is det
Collect sets of a given cardinality.
  722get_family_of_rank(Order, X, F):- shift(get_family_of_rank(Order, X, F)).
  723%
  724get_family_of_rank(Order, X, F, S):- rank_family_by_card(X, _, S),
  725	memo(family_with_card(Order)-F, S).
  726
  727% ?- zdd X<<set([a]), rank_family_by_card(X, P),
  728%	memo(family_with_card(0)-L), sets(L, Sl),
  729%   memo(family_with_card(1)-M), sets(M, Sm).
 rank_family_by_card(X, Y, S) is det
Classifying sets in a family by size.
  734rank_family_by_card(X, Y):- shift(rank_family_by_card(X, Y)).
  735%
  736rank_family_by_card(0, 0, _):-!.
  737rank_family_by_card(1, 0, S):-!, memo(family_with_card(0)-1, S).
  738rank_family_by_card(I, P, S):- memo(rank_family_by_card_done(I)-B, S),
  739	(	nonvar(B) ->  true
  740	; 	cofact(I, t(A, L, R), S),
  741		rank_family_by_card(L, Pl, S),
  742		rank_family_by_card(R, Pr, S),
  743		max(Pl, Pr, P0),
  744		insert_one_to_family(A, P0, New, S),
  745		P is P0 + 1,
  746		memo(family_with_card(P)-New, S),
  747		B = true
  748	).
  749%
  750insert_one_to_family(A, 0, G, S):-!, memo(family_with_card(0)-F, S),
  751	zdd_insert(A, F, G, S).
  752insert_one_to_family(A, P, G, S):- P0 is P-1,
  753	insert_one_to_family(A, P0, G0, S),
  754	memo(family_with_card(P)-Fp, S),
  755	zdd_insert(A, Fp, G, S),
  756	zdd_join(Fp, G0, Gp, S),
  757	set_memo(family_with_card(P)-Gp, S).
  758
  759		/**********************
  760		*     State access    *
  761		**********************/
  762
  763get_extra(Extra):- shift(get_extra(Extra)).
  764get_extra(Extra, S):- arg(2, S, Extra).
  765%
  766set_extra(Extra):- shift(set_extra(Extra)).
  767set_extra(Extra, S):- setarg(2, S, Extra).
  768
  769% ?- zdd bump_up(a, N), bump_up(a, K).
  770bump_up(Key, N, S):- arg(2, S, Extra),
  771	(	select(Key-N0, Extra, Extra0) -> true
  772	;	N0 = 0,
  773		Extra0 = Extra
  774	),
  775	N is N0 + 1,
  776	setarg(2, S,  [Key-N|Extra0]).
  777%
  778:- meta_predicate set_compare(3).  779:- meta_predicate set_compare(3, ?).  780set_compare(Compare):- shift(set_compare(Compare)).
  781set_compare(Compare, S):- setarg(3, S, Compare).
  782
  783% ?- zdd0((zdd_compare(C, a->b, a-b))).
  784% ?- zdd((zdd_compare(C, a, b))).
  785% ?- zdd0((zdd_compare(C, a, b))).
  786
  787get_compare(Compare, S):- arg(3, S, Compare).
  788%
  789%
  790zdd_compare(C, X, Y, S):- arg(3, S, F), call(F, C, X, Y).
  791
  792% ?- zdd((zdd_sort([1->1, 1->2, 1-1, 2-2], X))).
  793%
  794zdd_sort(X, Y, S):- get_compare(Comp, S),
  795					predsort(Comp, X, Y).
  796
  797% ?- zdd get_key(a, V), set_key(a, 1), get_key(a, W). % fail.
  798% ?- zdd set_key(a, 1), get_key(a, W).
  799get_key(K, V, S):- arg(2, S, Assoc), memberchk(K-V, Assoc).
  800%
  801set_key(K, V, S) :- arg(2, S, Assoc),
  802	(	select(K-_, Assoc, Assoc0)
  803	->	setarg(2, S, [K-V|Assoc0])
  804	;	setarg(2, S, [K-V|Assoc])
  805	).
  806
  807:- meta_predicate set_pred(?, :).  808set_pred(K, V):- shift(set_key(K, V)).
  809
  810:- meta_predicate set_pred(?, :, ?).  811set_pred(K, V, S) :- set_key(K, V, S).
  812
  813% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]},
  814%	get_key(a, Z), close_key(a))).
  815% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]},
  816%	get_key(a, Z), close_key(a), get_key(a, U))).	% false
  817
  818update_key(K, New, Old, S):- arg(2, S, Assoc),
  819	(	select(K-Old, Assoc, Assoc0) -> true
  820	;	Assoc0 = Assoc
  821	),
  822	setarg(2, S, [K-New|Assoc0]).
  823%
  824open_key(K, Val, S):- arg(2, S, Assoc),
  825	(	select(K-_, Assoc, Assoc0) 	->	true
  826	;	Assoc0 = Assoc
  827	),
  828	setarg(2, S, [K-Val|Assoc0]).
  829
  830%
  831close_key(K, S):- arg(2, S, Extra),
  832	(	select(K-_, Extra, Extra0) -> setarg(2, S, Extra0)
  833	;	true
  834	).
  835
  836% ?- zdd((varnum(D), varnum(E))).
  837%%	varnum(-D, +S) is det.
  838% update a global variable varnum with D.
  839%
  840varnum(D, S):- get_key(varnum, D, S).
  841
  842% ?- sort([1->1, 1->2, 1-1, 2-2], X).
  843% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X).
  844% ?- zdd(zdd_sort_rev([1,2,3], X)).
  845
  846compare_rev(Comp, C, A, B):- call(Comp, C, B, A).
  847%
  848zdd_sort_rev(X, Y):- shift(zdd_sort_rev(X, Y)).
  849zdd_sort_rev(X, Y, S):- get_compare(Comp, S),
  850	predsort(compare_rev(Comp), X, Y).
  851
  852% ?- pred_zdd(path_count:opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)).
  853:- meta_predicate pred_zdd(3, :).  854pred_zdd(Comp, X):-  open_state(S), pred_zdd(Comp, X, S).
  855%
  856pred_zdd(Comp, X, S):- set_compare(Comp, S), zdd(X, S).
  857
  858% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c], X))).
  859% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([], X))).
  860% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
 zdd_memberchk(L, Z, G) is det
A list L as a set is a member of a family Z of sets.
  865zdd_memberchk(L, Z):- shift(zdd_memberchk(L, Z)).
  866%
  867zdd_memberchk(L, Z, S):- zdd_sort(L, L0, S),
  868	zdd_ord_memberchk(L0, Z, S).
  869%
  870zdd_ord_memberchk(L, Z):- shift(zdd_ord_memberchk(L, Z)).
  871%
  872zdd_ord_memberchk([], Z, S):- !, zdd_has_1(Z, S).
  873zdd_ord_memberchk([A|As], Z, S):- Z>1,
  874	cofact(Z, t(B, L, R), S),
  875	(	A == B
  876	->	zdd_ord_memberchk(As, R, S)
  877	;	A @> B,
  878		zdd_ord_memberchk([A|As], L, S)
  879	).
  880
  881% PASS
  882% ?- zdd X<<pow([a,b]), card(X, C).
  883% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))).
  884% ?- zdd {X=1, Y =2, Z is X + Y}.
  885% ?- zdd X<<set([a]), sets(X, U).
  886% ?- zdd((X<<pow([a,b]), S<<sets(X))).
  887% ?- zdd((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))).
  888% ?- zdd(((X<< *(:append([a,b], [c,d]))), sets(X, Y))).
  889% ?- zdd((X<<(*[a,b]& *[c,d]), S<<sets(X))).
  890% ?- zdd((X<<{[a],[b],[c]}, sets(X,S))).
  891% ?- zdd((X<<{[a],[b, c]}, sets(X,S))).
  892% ?- zdd((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))).
  893% ?- zdd((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))).
  894% ?-  I =1000, J =2000,
  895%	time( (zdd
  896%	 {	numlist(1, I, L),
  897%		numlist(1, J, M)},
  898%		X << pow(L),
  899%		Y << pow(M),
  900%		Z << (Y - X),
  901%		card(Z, C),
  902%		{C =:= 2^J-2^I}  )).
  903
  904
  905% PASS
  906% ?- zdd((X<<cnf(0), Y<<sets(X))).
  907% ?- zdd((X<<cnf(1), Y<<sets(X))).
  908% ?- zdd((X<<cnf(2), Y<<sets(X))).
  909% ?- zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))).
  910% ?- ltr_zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))).
  911% ?- zdd((X<<cnf(a), Y<<sets(X))).
  912% ?- zdd((X<<cnf(-a), Y<<sets(X))).
  913% ?- zdd((X<<cnf(a+b), Y<<sets(X))).
  914% ?- zdd((X<<cnf(-(a+b)), Y<<sets(X))).
  915% ?- zdd((X<<cnf(-(a+b+b+a)), Y<<sets(X))).
  916% ?- zdd((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))).
  917% ?- zdd((X<<cnf(-(-a + -b)), Y<<sets(X))).
  918% ?- zdd((X<<dnf(a), Y<<sets(X), extern(Y, Y0))).
  919% ?- zdd((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))).
  920% ?- zdd((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))).
  921% ?- zdd((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))).
  922% ?- zdd((X<<dnf(a+b), Y<<sets(X))).
  923% ?- zdd((X<<dnf(-(a+b)), Y<<sets(X))).
  924% ?- zdd((X<<dnf(-(a+b+b+a)), Y<<sets(X))).
  925% ?- zdd((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))).
  926% ?- zdd((X<<dnf(-(-a + -b)), Y<<sets(X))).
  927% ?- zdd((X<<dnf((-a + a)), Y<<sets(X))).
  928% ?- zdd((X<<dnf(-(-a + a)), Y<<sets(X))).
  929% ?- zdd(X << *(:append([a,b], [c,d]))).
  930% ?- zdd((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))).
  931% ?- zdd((X << *[a,b], sets(X, S))).
  932% ?- zdd((X << +[a,b], sets(X, S))).
  933% ?- zdd((X << dnf(a*b+c*d+c*d*d), sets(X, S))).
  934% ?- zdd((zdd_list_to_singletons([], X), prz(X))).
  935% ?- zdd((zdd_list_to_singletons([a], X), prz(X))).
  936% ?- zdd((zdd_list_to_singletons([a,b], X), prz(X))).
  937% ?- zdd((zdd_list_to_singletons([c, a, b], X), prz(X))).
  938
  939
  940% ERROR (intentional)
  941% ?- I =1000, J is I + 1, numlist(1, I, L),
  942%	prepare_ltr_list(L, L0),
  943%	time(zdd(( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
 zdd_list_to_singletons(+As, -X, +S) is det
X is unified with a ZDD which is the family of singletons of an element of X. Example. If X=[a,b,c] then X is [[a], [b], [c]] as a family of sets in ZDD.
  951zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)).
  952%
  953zdd_list_to_singletons([], 1, _).
  954zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S),
  955		zdd_singleton(A, Y0, S),
  956		zdd_join(Y0, Y, X, S).
  957
  958% PASS.
  959% ?- zdd((zdd_partial_choices([], X), prz(X))).
  960% ?- zdd((zdd_partial_choices([[a], [b]], X), prz(X))).
  961% ?- zdd((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))).
  962% ?- zdd((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))).
  963% ?- zdd((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))).
  964% ?- zdd((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))).
  965% ?- zdd((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))).
  966% ?- zdd((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))).
  967% ?- zdd((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))).
  968% ?- findall([I], between(1, 10000, I),  Ls),
  969%	zdd((zdd_partial_choices(Ls, X),
  970%	card(X, C))), !, C =:= 2^10000.
 zdd_partial_choices(+X, -Y, +S) is det
Y is the ZDD of all possible partial choices from a list X of lists.
  975zdd_partial_choices(X, Y):- shift(zdd_partial_choices(X, Y)).
  976%
  977zdd_partial_choices([], 1, _):-!.
  978zdd_partial_choices([L|Ls], X, S):- zdd_partial_choices(Ls, X0, S),
  979	sw_fold_insert(zdd, L, X0, 0, X1, S),
  980	zdd_join(X0, X1, X, S).
 s_map(+F:pred/3, ?Xs, ?Ys, +S) is det
Almost equal to maplist(F(S), Xs, Ys).
  985:- meta_predicate s_map(:, ?, ?, ?).  986%
  987s_map(_, [], [], _):-!.
  988s_map(F, [X|Xs], [Y|Ys], S):- call(F, X, Y, S), !, s_map(F, Xs, Ys, S).
 s_map(+F:pred/2, ?Xs, ?Ys, +S) is det
Almost equal to maplist(F(S), Xs).
  993:- meta_predicate s_map(:, ?, ?).  994%
  995s_map(_, [], _):-!.
  996s_map(F, [X|Xs], S):- call(F, X, S), !, s_map(F, Xs, S).
  997
  998
  999:- meta_predicate zdd_find(:, ?, ?, ?).
 zdd_find(+F, +X, -Y, +S) is nondet
Unify Y with an atom in X which satisfies F(X).
 1004% ?- zdd X<< pow([a,b,c]), zdd_find(=(c), X, Y).
 1005% ?- zdd X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y).
 1006% ?- zdd X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y).
 1007
 1008zdd_find(F, X, Y, S):- X>1,
 1009	cofact(X, t(A, L, R), S),
 1010	(	call(F, A),	Y = A
 1011	;	zdd_find(F, L, Y, S)
 1012	;	zdd_find(F, R, Y, S)
 1013	).
 1014
 1015% PASS.
 1016%
 1017% ?- zdd((P<<pow([1,2,3]), {X=1;X=2}, card(P,C))).
 1018
 1019% ?- zdd((P<<pow([1,2,3]), card(P,C))).
 1020% ?- zdd P<<pow([1,2,3]), card(P,C).
 1021% ?- zdd((P << (set([1,2,3,2,3])+set([4, 2,4])), psa(P))).
 1022% ?- zdd({append([a,b], [c,d], X)}).
 1023% ?- zdd(X << :append([a,b], [c,d])).
 1024% ?- zdd(zdd(X << :append([a,b], [c,d]))).
 1025% ?- zdd(zdd(zdd((X << :append([a,b], [c,d]))))).
 1026% ?- zdd(zdd(zdd(((X<<pow([1,2]), true, true))))).
 1027% ?- zdd(zdd(zdd((X<<pow([1,2]), true, true, card(X, C))))).
 1028% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), card(X, C)).
 1029
 1030
 1031fetch_state(S):- setup_state_for_query(S, '$zdd').  % for short.
 1032%
 1033fetch_state(S, G):- setup_state_for_query(S, G).  % for short.
S: state, Gv: gloval variable name for state. state S is created when S is unbound, and Gv is set to S by b_setval/2. Otherwise Gv is set to S.
 1040setup_state_for_query(S, Gv):-
 1041	(	var(S) ->
 1042		(	nb_current(Gv, S), S\==[] -> true
 1043		;	open_state(S),
 1044			b_setval(Gv, S)
 1045		)
 1046	;	b_setval(Gv, S)
 1047	).
 ltr_zdd(+E) is det
Solve E as command on families of clauses.
 1052:-meta_predicate ltr_zdd(:). 1053ltr_zdd(M:G):- ltr_open_state(S),
 1054			   fetch_state(S),
 1055			   zdd_solve(G, S, M).
 zdd(+E, +S) is det
Solve E as commands on ZDD with compare/3 for ordering atoms.
 1059:- meta_predicate zdd(:).   % zdd(0) does not work.
 1060zdd(M:G):- 	fetch_state(S),
 1061			set_key(atom_index, 0, S),
 1062			set_compare(compare, S),
 1063			zdd_solve(G, S, M).
 1064
 1065%
 1066:- meta_predicate zdd(:, ?). 1067zdd(M:A, S):- zdd_solve(A, S, M).
 zdd0(+E, +S) is det
Solve E as commands on ZDD with opp_compare/3 for ordering atoms, which is the reverse ordering of the standard compare predicate.
 1073:- meta_predicate zdd0(:). 1074zdd0(X):- zdd((set_compare(opp_compare), X)).
 opp_compare(-C, +X, +Y) is det
Equivalent to opp_compare(C, Y, X).
 1079% PASS.
 1080% ?- zdd((zdd_sort([a-b,a->b, b-c, b->c], X))).
 1081% ?- zdd0((zdd_sort([a-b,a->b, b-c, b->c], X))).
 1082% ?- opp_compare(C, 1, 2).
 1083% ?- opp_compare(C, a->b, b).
 1084% ?- opp_compare(C, p(0,0), p(1,0)).
 1085% ?- opp_compare(C, p(1,0)-p(0,0), p(1,0)-p(1,0)).
 1086
 1087opp_compare(<, -(_,_), ->(_,_)):-!.
 1088opp_compare(>, ->(_,_), -(_,_)):-!.
 1089opp_compare(C, X, Y):- compare(C, Y, X). % reverse order
 1090
 1091% PASS.
 1092% ?- zdd((set_key(a, 1), get_key(a, X))).
 1093:- meta_predicate  use_zdd(:). 1094use_zdd(X):- use_zdd(X, [hash_size(128)]).
 1095
 1096:- meta_predicate  use_zdd(:, ?). 1097use_zdd(X, Options):-
 1098	setup_call_cleanup(
 1099		open_state(S, Options),
 1100		zdd(X, S),
 1101		close_state(S)).
 1102
 1103% ?- zdd X<< @(abc), psa(X).
 1104% ?- zdd X<<pow([1,2]), memo(a-X), card(X, C).
 zdd_solve(+G, +S, +M) is det
G: Goal expression, S: a state, M: a module name. G is interpreted as a command on S in module M. (A, B) (A, B). sequentiual (AND) (A ; B) (A; B) (OR) (A -> B) A->B (COND) X<<E unify X with the value of an expression E. #(G) call(G, S) (Deprecated) M:G Solve G in module M true true {G} call(G) with G as a plain prolog goal. A call(M:A, S). Call an atomic goal A with S in M.
 1121% ?- zdd X<< +[ *[a,b], *[c, d]], psa(X).
 1122% ?- zdd X<< +[ *[a,b], *[c, d]], #(psa(X)).
 1123% ?- zdd <<(X, +[*[a,b], *[c,d]]), psa(X).
 1124
 1125% ?- zdd X<<1, Y<<2.
 1126% ?- zdd X<< card(pow([1,2])+pow([a,b])).
 1127
 1128:- meta_predicate <<(?, :). 1129<<(X, E) :- setup_state_for_query(S), zdd_eval(E, X, S).
 <<(-X, +E, +S) is det
Evaluate expression E in state S then unify obtained value with X.
 1134:- meta_predicate <<(?, :, ?). 1135<<(X, E, S) :- setup_state_for_query(S), zdd_eval(E, X, S).
 zdd_solve(+G, +S, +M) is det
Solve goal G with state S and module M.
 1140% ?- zdd X<< *[0, 1, 2, 3], psa(X).
 1141% ?- zdd X<< *[*[]], psa(X).
 1142% ?- zdd X<< *[[]], psa(X).
 1143% ?- zdd X<< *[+[]], psa(X).
 1144% ?- zdd X<< +[ *[1,2], *[3,4]], psa(X).
 1145% ?- zdd X<<pow(:numlist(1, 100)), card(X, C).
 1146% ?- zdd X<< :numlist(1, 100).
 1147%@ X = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].
 1148
 1149%
 1150zdd_solve(true, _, _)	:-!.
 1151zdd_solve(M:G, S, _)	:-!, zdd_solve(G, S, M).
 1152zdd_solve({G}, _, M)	:-!, call(M:G).
 1153% zdd_solve(#(G), S, M)	:-!, zdd_solve(G, S, M). % Dropped.
 1154zdd_solve(X<<E, S, M)	:-!, zdd_numbervars(E, S), zdd_eval(E, X, S, M).
 1155zdd_solve((A,B), S, M)	:-!, zdd_solve(A, S, M), zdd_solve(B, S, M).
 1156zdd_solve((A;B), S, M)	:-!, (zdd_solve(A, S, M); zdd_solvde(B, S, M)).
 1157zdd_solve((A->B), S, M)	:-!, (zdd_solve(A, S, M) -> zdd_solve(B, S, M)).
 1158zdd_solve(G, S, M):- call(M:G, S).
 zdd_eval(+E, -V, +S) is det
Evaluate E recursively and unify the obtained value with V in state S.

--- only basic expressions follow ---

x		x		if x is nummber, string, or list.
$E		E	(quote).
@(a)	{{a}} as  a singleton family of a.

:E eval E as prolog term with last argument as output. #E eval E as zdd term using state. !E apply E without evaluating args.

--- zdd expression ---

X + Y join (union) of X and Y X - Y subtract Y from X X \ Y subtract Y from X X & Y intersection of X and Y merge(X, Y) merge/multiply X and Y X * Y merge/multiply X and Y X // Y quotient X by Y. X / Y remainder of X by Y. prod(X, YO) product of X and Y X ** Y product of X and Y pow(X) powerset of X power(X) powerset of X set(L) read L a singleton family {L}. sets(X, S) convet X in S to list of lists *E merge all elements of a list E. +E join all elements of a list E. {A,B,..} family of sets [A, B, ...]

--- Boolean terms ---

cnf(F, X)	X is CNF of F.
dnf(F, X)	X is DNF of F,
 1197% Pass.
 1198% ?- zdd((X<<dnf(a*b), psa(X))).
 1199% ?- zdd((X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C))).
 1200% ?- zdd((X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))).
 1201% ?- zdd((X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C))).
 1202
 1203% Pass.
 1204% ?- zdd X<< @a.
 1205% ?- zdd X<< a, psa(X).
 1206% ?- zdd X<<pow([a,b]), card(X, C).
 1207% ?- zdd X<<pow([a,b])-pow([a]), card(X, C).
 1208% ?- zdd X<< set(:(append([1,2],[3,4]))), psa(X).
 1209% ?- zdd((X<< +(:append([1,2],[3,4])), psa(X))).
 1210% ?- zdd((X<< (@a + @b), psa(X))).
 1211% ?- zdd((X<< ((@a + @b)* @c), psa(X))).
 1212% ?- zdd((X<< [a,b])).
 1213% ?- zdd((X<< set(:(append([a,b],[c,d]))), psa(X))).
 1214% ?- zdd((X<< set(!append([a,b],[c,d])), psa(X))). % error
 1215% ?- zdd(X<< card(pow([a,b]))).
 1216% ?- zdd(X<< card(pow(:numlist(1, 100)))).
 1217% ?- zdd((X<< set([1]), Y<< (X+X), psa(X))).
 1218% ?- zdd((X<< set([1]), psa(X))).
 1219% ?- zdd((X<< set([]))).
 1220% ?- zdd((X << {[a], [b], [c]}, psa(X))).
 1221% ?- zdd((X << {[a], [b], [c]}, card(X, C))).
 1222
 1223% PASS.
 1224% ?- zdd((X << card(pow(:append(numlist(1,3), numlist(4,5)))))).
 1225% ?- zdd((X << set(:append(numlist(1,2), numlist(4,5))))).
 1226% ?- zdd((X << set(:append(numlist(1,10), numlist(11,20))))).
 1227% ?- zdd { numlist(1,10,A), numlist(11,20, B)}, X<< pow( :append(A, B)),
 1228%	card(X, C).
 1229% ?- zdd((X << pow(:(numlist(1,2))), card(X, C))).
 1230% ?- zdd((X << pow(:(! charlist(a,z))), card(X, C))).
 1231% ?- zdd((X << pow(:(! charlist(a-z))), card(X, C))).
 1232% ?- zdd((X << pow([a,b]))).
 1233% ?- zdd((X << *[a, b, c])).
 1234% ?- zdd((X << (*[a, b, c] + *[a,b,c]), psa(X))).
 1235% ?- zdd((X << (*[a, b, c] + *[2, 3]), psa(X))).
 1236% ?- zdd((C << card(pow([a,b,c,1,2,3])))).
 1237% ?- zdd((C << card(pow(:append([a,b,c], [1,2,3]))))).
 1238% ?- zdd((C << pow(:numlist(1, 3)))).
 1239% ?- zdd((C << @(a), psa(C))).
 1240
 1241% Pass.
 1242% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))).
 1243% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))).
 1244% ?- zdd((U << +(:(append([a,b,c], [d,e,f]))), psa(U))).
 1245% ?- zdd((U << *(:(append([a,b,c], [d,e,f]))), psa(U))).
 1246% ?- zdd((U << +(:(append(:append([a,b,c], [x,y,z]), [1, 2]))), psa(U))).
 1247% ?- zdd((U << +[ *[a,b], *[c,d]],  psa(U))).
 1248% ?- zdd((U << *[ +[a,b], +[c,d]],  psa(U))).
 1249% ?- zdd((U << *[ *[a,b], *[c,d]],  psa(U))).
 1250% ?- zdd((U << *[ *[a,b], +[c,d]],  psa(U))).
 1251% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))).
 1252% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))).
 1253% ?- zdd((U << #(card(pow([a]))))).
 1254% ?- zdd((U << :succ(#(card(pow([a])))))).
 1255% ?- zdd((U << card(pow([a])))).
 1256
 1257% Pass.
 1258% ?- zdd((U << :(=(3)))).
 1259% ?- zdd((U << *([1,2,3]), psa(U))).
 1260% ?- zdd((U << :plus(#(card(pow([a,b]))), #(card(pow([1,2])))))).
 1261% ?- zdd((U << @a)).  % singleton.
 1262% ?- zdd((U << @2)).
 1263% ?- zdd((U << [a,b])).
 1264% ?- zdd((U << *[a,b], psa(U))).
 1265% ?- zdd((U << +[a,b], psa(U))).
 1266% ?- zdd((U << +[*[a,b], *[c,d]], psa(U))).
 1267% ?- zdd((U << +[+[a,b], +[c,d]], psa(U))).
 1268% ?- zdd((U << *[+[a,b], +[c,d]], psa(U))).
 1269% ?- zdd((U << *[*[a,b], *[c,d]], psa(U))).
 1270% ?- zdd((U << :(!call(=, hello)))).
 1271% ?- zdd((U << :(call($(=), :append([a,b],[c,d]))))).
 1272% ?- zdd X<< *[a,b], Y<< *[c,d], Z<<  zdd_join(X, Y), psa(Z).
 1273% ?- zdd X<< *[a,b], Y<< *[c,d], Z<<  (X+Y), psa(Z).
 1274%
 1275basic_type(X):-	number(X);
 1276	string(X);
 1277	is_list(X);
 1278	var(X).
 zdd_eval(+X, -Y, +S) is det
Evaluate X and unify the value with Y in state S.
 1283zdd_eval(X, Y, S):- context_module(M),
 1284					zdd_numbervars(X, S),
 1285					zdd_eval(X, Y, S, M).
 1286
 1287% illegal use of pragma.
 1288% ?- zdd((U << @(=(3)))).					% Error
 1289% ?- zdd((U << #append([a], [b]))).			% Error
 1290% ?- zdd((U << +(!append([a], [b])))), psa(U).	% Error
 1291% ?- zdd((U << #(get_compare), psa(U))).		% Error
 1292% ?- zdd( #(get_compare, X)).					% Error
 1293
 1294% Normal use of pragmas, though meaningless.
 1295% ?- zdd((U << (@a+ @b+ @c), psa(U))).
 1296% ?- zdd((U << :append([a], [b]))).
 1297% ?- zdd((U << get_compare)).
 1298% ?- zdd((U << +(:append([[a]], [[b]])), psa(U))).
 1299% ?- zdd(U << get_compare).
 1300% ?- zdd( get_compare(X)).
 1301% ?- zdd( U << :arith(1+2)).
 1302% ?- zdd( U << :plus(arith(1+2), arith(3+4))).
 1303% ?- zdd((U << (@A+ @B+ @C), psa(U))).
 1304% ?- zdd((U << (@A), psa(U))).
 zdd_eval(+E, -V, +S, +M) is det
Evaluate E in state S in context module M, and unify the value with V.
 1309%	Note that intgeger is used as a unique name of a ZDD.
 1310%	use indicator `@` as `@(3)` for 3 as an atom.
 1311
 1312zdd_eval(X, X, _, _)	:- basic_type(X), !.
 1313zdd_eval(@(X), Y, S, _)	:-!, zdd_singleton(X, Y, S).
 1314zdd_eval({}, 0, _, _)	:-!. % The empty family of sets.
 1315zdd_eval({X}, Y, S, _)	:-!, associative_comma(X, U, []), zdd_family(U, Y, S).
 1316zdd_eval($(X), X, _, _)	:-!.
 1317zdd_eval(!(X), Y, S, M)	:-!, call(M:X, Y, S).
 1318zdd_eval(:(X), Y, S, M)	:-!, prolog_eval(X, Y, S, M).
 1319zdd_eval(#(X), Y, S, M) :-!, zdd_eval(X, Y, S, M).
 1320zdd_eval(M:X, Y, S, _)	:-!, zdd_eval(X, Y, S, M).
 1321zdd_eval(X, Y, S, M)	:-
 1322	(	zdd_apply(X, Y, S, M) -> true
 1323	;	zdd_atom(X, S) -> zdd_singleton(X, Y, S)
 1324	;	zdd_eval_args(X, X0, S, M),
 1325		zdd_apply0(X0, Y, S, M)
 1326	).
 1327%
 1328zdd_eval_args(A, A, _, _):- atomic(A), !.
 1329zdd_eval_args(A, B, S, M):-
 1330	functor(A, Fa, Na),
 1331	functor(B, Fa, Na),
 1332	zdd_eval_args(1, A, B, S, M).
 1333%
 1334zdd_eval_args(I, A, B, S, M):- arg(I, A, U), !,
 1335	zdd_eval(U, V, S, M),
 1336	arg(I, B, V),
 1337	J is I+1,
 1338	zdd_eval_args(J, A, B, S, M).
 1339zdd_eval_args(_, _, _, _, _).
 prolog_eval(E, V, S, M) is det
With context module M, evaluate E without referring to state S as default, and unify the value with V.
 1345prolog_eval(X, X, _, _)		:- basic_type(X), !.
 1346prolog_eval($(X), X, _, _)	:-!.
 1347prolog_eval(!(X), Y, _, M)	:-!, call(M:X, Y).
 1348prolog_eval(:(X), Y, S, M)	:-!, prolog_eval(X, Y, S, M).
 1349prolog_eval(#(X), Y, S, M)	:-!, zdd_eval(X, Y, S, M).
 1350prolog_eval(M:X, Y, S, _)	:-!, prolog_eval(X, Y, S, M).
 1351prolog_eval(arith(X), Y, _, _)	:-!, Y is X.
 1352prolog_eval(X, Y,  S, M)	:- prolog_eval_args(X, X0, S, M),
 1353		call(M:X0, Y).
 1354%
 1355prolog_eval_args(A, A, _, _):- atomic(A), !.
 1356prolog_eval_args(A, B, S, M):-
 1357	functor(A, Fa, Na),
 1358	functor(B, Fa, Na),
 1359	prolog_eval_args(1, A, B, S, M).
 1360%
 1361prolog_eval_args(I, A, B, S, M):- arg(I, A, U),!,
 1362	prolog_eval(U, V, S, M),
 1363	arg(I, B, V),
 1364	J is I+1,
 1365	prolog_eval_args(J, A, B, S, M).
 1366prolog_eval_args(_, _, _, _, _).
 1367
 1368		/*********************************
 1369		*     zdd vecrtor expressions    *
 1370		*********************************/
 zdd_vector_exp(+E, -V, +S) is det
Evaluate vector notation for ZDD, and unify the value with S.
 1375% ?- zdd((X<< *(: (=([[a,b],[c,d]]))), psa(X))).
 1376% ?- zdd((X<< +(: (=([[a,b],[c,d]]))), psa(X))).
 1377% ?- zdd((X<< +(: (=([*[a,b], *[c,d]]))), psa(X))).
 1378% ?- zdd((X<< +[[1,2],[a,b]], psa(X), card(X, C))).
 1379% ?- zdd((X<< *[[1,2],[a,b]], psa(X), card(X, C))).
 1380% ?- zdd((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))).
 1381% ?- zdd((X<< +[*[1,2],*[a,b]], psa(X), card(X, C))).
 1382% ?- zdd((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))).
 1383% ?- zdd((X<< *[1,2], psa(X), card(X, C))).
 1384% ?- zdd((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))).
 1385% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X).
 1386% ?- zdd zdd_vector_exp(+[[a],*[b,c]], X), psa(X).
 1387% ?- zdd zdd_vector_exp(+[a,b,c], X), psa(X).
 1388% ?- zdd zdd_vector_exp(*[a,b,c], X), psa(X).
 1389% ?- zdd zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X).
 1390% ?- zdd zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X).
 1391% ?- zdd zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X).
 1392% ?- zdd X<< *[a, b], psa(X).
 1393% ?- zdd X<< +[a, b], psa(X).
 1394% ?- zdd X<< *[A, B], psa(X).
 1395% ?- zdd X<< *[*[0, 1], *[2,3]], psa(X).
 1396% ?- zdd X<< *[*[], *[2,3]], psa(X).
 1397% ?- zdd X<< *[0, 1, *[2,3]], psa(X).
 1398
 1399zdd_vector_exp(*(X), Y, S):-!, zdd_vector_exp(*, X, Y, S).
 1400zdd_vector_exp(+(X), Y, S):-!, zdd_vector_exp(+, X, Y, S).
 1401% zdd_vector_exp(X, X, _):- (X = 0; X=1),!.
 1402zdd_vector_exp(X, Y, S):- zdd_singleton(X, Y, S).
 1403
 1404%
 1405zdd_vector_exp(*, [], 1, _):-!.
 1406zdd_vector_exp(+, [], 0, _):-!.
 1407zdd_vector_exp(F, [A|As], R, S):-!, % F in [*,+].
 1408	zdd_vector_exp(A, U, S),
 1409	zdd_vector_exp(F, As, V, S),
 1410	apply_binary_basic(F, U, V, R, S).
 1411
 1412%
 1413apply_binary_basic(*, X, Y, Z, S):-!, zdd_merge(X, Y, Z, S).
 1414apply_binary_basic(+, X, Y, Z, S):- zdd_join(X, Y, Z, S).
 1415
 1416%
 1417zdd_fold_join([], Z, Z, _).
 1418zdd_fold_join([X|Xs], Z, Z0, S):-
 1419	zdd_join(X, Z, Z1, S),
 1420	zdd_fold_join(Xs, Z1, Z0, S).
 1421%
 1422zdd_fold_merge([], Z, Z, _).
 1423zdd_fold_merge([X|Xs], Z, Z0, S):-
 1424	zdd_merge(X, Z, Z1, S),
 1425	zdd_fold_merge(Xs, Z1, Z0, S).
 1426%
 1427fold_singleton_join([], X, X, _).
 1428fold_singleton_join([A|As], X, Y, S):-
 1429	zdd_singleton(A, U, S),
 1430	zdd_join(U, X, X0, S),
 1431	fold_singleton_join(As, X0, Y, S).
 1432
 1433		/***********************************************
 1434		*    Currently reserved names of operations.   *
 1435		***********************************************/
 zdd_apply(+E, -V, +S) is det
With state S, apply E (without evaluate arguments) and unify the value with V.
 1440zdd_apply(@(A), Y, S, _)	:-!, zdd_singleton(A, Y, S).
 1441zdd_apply(X, Y, S, _)		:- dvar(X), !, zdd_singleton(X, Y, S).
 1442zdd_apply(ltr_set(L), Y, S, _)	:-!, ltr_append(L, 1, Y, S).
 1443zdd_apply(dnf(A), X, S, _)	:-!, dnf(A, X, S).
 1444zdd_apply(cnf(A), X, S, _)	:-!, cnf(A, X, S).
 1445zdd_apply(gf2(A), X, S, _)	:-!, gf2(A, X, S).
 1446zdd_apply(qp(A), X, S, _)	:-!, mqp(A, X, S).
 1447zdd_apply(cofact(A, L, R), X, S, _)	:-!, cofact(X, t(A, L, R), S).
 1448zdd_apply(cofact(X), Y, S, _)	:-!, integer(X), X>1, cofact(X, Y, S).
 1449zdd_apply(fact(X), Y, S, _)	:- integer(X), X>1, cofact(X, Y, S).
 1450zdd_apply(+(X), Y, S, _)	:-!, zdd_vector_exp(+(X), Y, S).
 1451zdd_apply(*(X), Y, S, _)	:-!, zdd_vector_exp(*(X), Y, S).
 1452
 1453
 1454%
 1455zdd_apply0(X + Y, Z, S, _)	:-!, zdd_join(X, Y, Z, S).
 1456zdd_apply0(X * Y, Z, S, _)	:-!, zdd_merge(X, Y, Z, S).
 1457zdd_apply0(merge(X, Y), Z, S, _)	:-!, zdd_merge(X, Y, Z, S).
 1458zdd_apply0(X - Y, Z, S, _)	:-!, zdd_subtr(X, Y, Z, S).
 1459zdd_apply0(\(X,Y), Z, S, _)	:-!, zdd_subtr(X, Y, Z, S).
 1460zdd_apply0((X // Y), Z, S, _):-!, zdd_div(X, Y, Z, S).
 1461zdd_apply0((X / Y), Z, S, _)	:-!, zdd_mod(X, Y, Z, S).
 1462zdd_apply0((X mod Y), Z, S, _)	:-!, zdd_mod(X, Y, Z, S).
 1463zdd_apply0(&(X, Y), Z, S, _)	:-!, zdd_meet(X, Y, Z, S).
 1464zdd_apply0(prod(X, Y), Z, S, _)	:-!, zdd_product(X, Y, Z, S).
 1465zdd_apply0(**(X, Y), Z, S, _):-!, zdd_product(X, Y, Z, S).
 1466zdd_apply0(pow(X), Z, S, _)	:-!, zdd_sort(X, Y, S),	zdd_power(Y, Z, S).
 1467zdd_apply0(power(X), Z, S, _):-!, zdd_sort(X, Y, S), zdd_power(Y, Z, S).
 1468zdd_apply0(sets(X), Z, S, _)	:-!, sets(X, Z, S).
 1469zdd_apply0(X, Y, S, M)		:- call(M:X, Y, S).
 1470
 1471% ?- zdd X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X).
 1472% ?- zdd X<< +[*[a,b]] + +[*[c,d]], psa(X).
 1473% ?- zdd((X<<pow([1,2,3,4]), Y<<pow([1,2,3]),
 1474%	card(X, C), card(Y, D), Z<<(X-Y), card(Z, E))).
 1475zdd_super_power([], P, P, _).
 1476zdd_super_power([A|As], P, Q, S):-
 1477	zdd_super_power(As, P, Q0, S),
 1478	zdd_insert(A, Q0, Q, S).
 1479
 1480%
 1481set(L, Y, S)	:-!, zdd_append(L, 1, Y, S).
 1482
 1483% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))).
 1484family(X, Y, S):- zdd_numbervars(X, S),
 1485				  zdd_family(X, Y, S).
 zdd_family(+L, -X, +S) is det
For a list L of lists of atoms, build a zdd in S whose index is unified with X.
 1491zdd_family(X, Y, S):- zdd_numbervars(X, S),
 1492					  zdd_family(X, 0, Y, S).
 1493
 1494% ?- zdd zdd_family([[a],[a,b]], X), card(X, C), psa(X).
 1495% ?- zdd zdd_family([[], [a,a],[a,b]], X), psa(X).
 1496zdd_family([], U, U, _).
 1497zdd_family([X|Xs], U, V, S):-
 1498	zdd_insert_atoms(X, 1, X1, S),
 1499	zdd_join(X1, U, U0, S),
 1500	zdd_family(Xs, U0, V, S).
 1501
 1502% ?- zdd((ltr_family([[a, b], [c, d]], X), sets(X,S))).
 1503% ?- zdd((ltr_family([[a, b], [c, -c]], X), sets(X,S))).
 1504% ?- zdd((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))).
 1505% ?- zdd((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))).
 1506% ?- zdd((X << dnf((a+(-b)+a)), psa(X))).
 1507% ?- zdd((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))).
 1508% ?- zdd((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))).
 1509% ?- ltr_zdd ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X).
 1510% ?- ltr_zdd ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X).
 1511% ?- ltr_zdd ltr_family([[a],[-b, -a,-c]], X), psa(X).
 1512%
 1513%
 1514ltr_family(X, Y, S):- ltr_family(X, 0, Y, S).
 1515
 1516%
 1517ltr_family([], U, U, _).
 1518ltr_family([X|Xs], U, V, S):-
 1519	ltr_append(X, 1, X0, S),
 1520	ltr_join(X0, U, U0, S),
 1521	ltr_family(Xs, U0, V, S).
 1522
 1523		/************************
 1524		*		choices		    *
 1525		************************/
 1526
 1527% ?- zdd  X<< pow([a,b]), card(X, C).
 1528%!	zdd_choices(+X, -Y, +S) is det.
 1529%   Y = { W | U in W iff all A in U some V in X such that A in X }.
 1530
 1531% ?- zdd X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y).
 1532% ?- N=10, numlist(1, N, Ns), (zdd X<< pow(Ns), zdd_subtr(X, 1, Y),
 1533%	zdd_choices(X, Y), card(Y, C)).
 1534% ?- N=1000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y),
 1535%	zdd_choices(X, Y), card(Y, C))).
 1536
 1537zdd_choices(0, 1, _):-!.
 1538zdd_choices(1, 0, _):-!.
 1539zdd_choices(X, Y, S):- memo(choices(X)-Y, S),
 1540	(	nonvar(Y)->true %, write(+) % many hits when X has the empty set.
 1541	;	cofact(X, t(A, L, R), S),
 1542		zdd_choices(L, L0, S),
 1543		zdd_choices(R, R0, S),
 1544		cofact(R1, t(A, R0, 1), S),
 1545		zdd_merge(L0, R1, Y, S)
 1546	).
 1547
 1548
 1549		/*************************************************
 1550		*   Operation on zdd join/merge/meet/subtr/cons  *
 1551		*************************************************/
 zdd_join(+X, +Y, -Z, +S) is det
Z is the union of X and Y.
 1556%
 1557zdd_join(0, X, X, _):-!.
 1558zdd_join(X, 0, X, _):-!.
 1559zdd_join(X, X, X, _):-!.
 1560zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S).
 1561zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S).
 1562zdd_join(X, Y, Z, S):-
 1563	(	X@<Y -> memo(zdd_join(X,Y)-Z, S)
 1564	;	memo(zdd_join(Y, X)-Z, S)
 1565	),
 1566	(	nonvar(Z) -> true  %, write(.)
 1567	;	cofact(X, t(A, L, R), S),
 1568		cofact(Y, t(A0, L0, R0), S),
 1569		zdd_compare(C, A, A0, S),
 1570		(	C = (<)	->
 1571 			zdd_join(L, Y, U, S),
 1572			cofact(Z, t(A, U, R), S)
 1573		;	C = (=)	->
 1574			zdd_join(L, L0, U, S),
 1575			zdd_join(R, R0, V, S),
 1576			cofact(Z, t(A, U, V), S)
 1577		;	zdd_join(L0, X, U, S),
 1578			cofact(Z, t(A0, U, R0), S)
 1579		)
 1580	).
 zdd_cons(+X, +Y, -Z, +S) is det
Short hand for cofact(Z, t(X, 0, Y), S). Having analogy Z = [X|Y] in mind.
 1586% ?- zdd zdd_cons(X, a, 1), zdd_cons(X, A, B).
 1587% ?- zdd zdd_cons(X, a, 0), zdd_cons(X, A, B). % false
 1588
 1589zdd_cons(X, Y, Z, S):- ( var(X);  X>1 ), !, cofact(X, t(Y, 0, Z), S).
 1590
 1591% ?- zdd((X<<(*[a]+ *[b]+ []), psa(X))).  % false for [].
 1592% ?- zdd((X<<(*[a]+ *[b]+ 1), psa(X))).
 1593% ?- zdd((X<<(*[a]+ *[b]+ 0), psa(X))).
 1594% ?- zdd((X<<(*[a]+ *[b]), psa(X))).
 1595% ?- zdd((A<<{[a]},  psa(A), zdd_join_1(A, X), psa(X))).
 1596
 1597%	zdd_join_1(+X, -Y, +G) is det.
 1598%	Y is the union of X and 1 (the singleton {{}}).
 1599
 1600% ?- numlist(1,100, Ns), (zdd X<<pow(Ns), {fetch_state(S), time(repeat(100, zdd_join_1(X,_,S)))}).
 1601zdd_join_1(X, X, S):- zdd_has_1(X, S), !.
 1602zdd_join_1(X, Y, S):- zdd_add_1(X, Y, S).
 1603%
 1604zdd_add_1(0, 1, _):-!.
 1605zdd_add_1(X, Y, S):- cofact(X, t(A, L, R), S),
 1606	zdd_add_1(L, L0, S),
 1607	cofact(Y, t(A, L0, R), S).
 1608
 1609% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))).
 1610% ?- zdd((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))).
 1611% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))).
 1612% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))).
 1613% ?- trace, zdd(X=[b, a]).
 1614% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))).
 1615% ?- zdd((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
 zdd_meet(+X, +Y, -Z, +G) is det
Z is the intersection of X and Y.
 1620zdd_meet(0, _, 0, _):-!.
 1621zdd_meet(_, 0, 0, _):-!.
 1622zdd_meet(1, X, Y, S):-!, zdd_meet_1(X, Y, S).
 1623zdd_meet(X, 1, Y, S):-!, zdd_meet_1(X, Y, S).
 1624zdd_meet(X, X, X, _):-!.
 1625zdd_meet(X, Y, Z, S):-
 1626	(	X @< Y -> memo(zdd_meet(X,Y)-Z, S)
 1627	;	memo(zdd_meet(Y,X)-Z, S)
 1628	),
 1629	(	nonvar(Z) -> true
 1630	;	cofact(X, t(A, L, R), S),
 1631		cofact(Y, t(A0, L0, R0), S),
 1632		zdd_compare(C, A, A0, S),
 1633		(	C = (<) -> zdd_meet(L, Y, Z, S)
 1634		;	C = (=) ->
 1635			zdd_meet(L, L0, U, S),
 1636			zdd_meet(R, R0, V, S),
 1637			cofact(Z, t(A, U, V), S)
 1638		;	zdd_meet(L0, X, Z, S)
 1639		)
 1640	).
 zdd_meet_1(+X, -Y, +G) is semidet
Y is the intersection of X and 1 {the singleton of the emptyset {{}}}.
 1645zdd_meet_1(X, 1, S):- zdd_has_1(X, S), !.
 1646zdd_meet_1(_, 0, _).
 zdd_subtr(+X, +Y, -Z, +G) is det
Z is the subtraction of Y from X: Z = Y \ Z.
 1651% ?- zdd((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))).
 1652% ?- zdd0((X<<pow([a,b,c]), Y<<pow([a,b]), zdd_subtr(X, Y, Z), card(Z, C))).
 1653%
 1654zdd_subtr(X, X, 0, _):-!.
 1655zdd_subtr(0, _, 0, _):-!.
 1656zdd_subtr(X, 0, X, _):-!.
 1657zdd_subtr(X, 1, Y, S):-!, zdd_subtr_1(X, Y, S).
 1658zdd_subtr(1, X, Y, S):-!,
 1659	(	zdd_has_1(X, S) ->	Y = 0
 1660	;	Y = 1
 1661	).
 1662zdd_subtr(X, Y, Z, S):- memo(zdd_subtr(X,Y)-Z, S),
 1663	(	nonvar(Z) -> true
 1664	; 	cofact(X, t(A, L, R), S),
 1665		cofact(Y, t(A0, L0, R0), S),
 1666		zdd_compare(C, A, A0, S),
 1667		(	C = (<)	->
 1668			zdd_subtr(L, Y, U, S),
 1669			cofact(Z, t(A, U, R), S)
 1670		;	C = (=) ->
 1671			zdd_subtr(L, L0, U, S),
 1672			zdd_subtr(R, R0, V, S),
 1673			cofact(Z, t(A, U, V), S)
 1674		;	zdd_subtr(X, L0, Z, S)
 1675		)
 1676	).
 zdd_subtr_1(+X, -Y, +G) is det
Y is the subtraction of 1 (the set {{}}) from X: Y = X \ {{}}.
 1681% ?- zdd((X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y))).
 1682% ?- zdd((X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y))).
 1683% ?- zdd((X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y))).
 1684%
 1685zdd_subtr_1(X, 0, _):- X < 2, !. % empty family or singleton of the empty.
 1686zdd_subtr_1(X, Y, S):- cofact(X, t(A, L, R), S),
 1687	zdd_subtr_1(L, L0, S),
 1688	cofact(Y, t(A, L0, R), S).
 zdd_xor(+X, +Y, -Z, +G) is det
Z is the exclusive-or of family X and Y.
 1693% ?- zdd X<<{[a]}, Z << zdd_xor(X, X).
 1694% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z).
 1695% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms),
 1696%	time((zdd X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))).
 1697% ?- time((zdd Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))).
 1698zdd_xor(X, Y, Z, S):-zdd_subtr(X, Y, A, S),
 1699	zdd_subtr(Y, X, B, S),
 1700	zdd_join(A, B, Z, S).
 1701
 1702
 1703% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S),
 1704% 	zdd_meet(X, Y, B, S),
 1705% 	zdd_subtr(A, B, Z, S).
 zdd_merge(X, Y, Z, G) is det
Z is the merge of X and Y, that is, Z = { U | U is the union of A in X and B in Y}.
Remark. The merge is associative and commutative, but not idempotent.
 1714% ?- zdd(( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))).
 1715% ?- time(zdd(( X<<pow(!charlist(a-z)), Y<<pow(:numlist(1, 26))))).
 1716% ?- time(zdd(( X<<pow(:charlist($(a-z))), Y<<pow(:numlist(1, 26)),
 1717%	 zdd_merge(X, Y, Z),  U << zdd_meet(X, Z), card(X, C)))), C is 2^26.
 1718%
 1719zdd_merge(0, _, 0, _):-!.
 1720zdd_merge(_, 0, 0, _):-!.
 1721zdd_merge(1, X, X, _):-!.
 1722zdd_merge(X, 1, X, _):-!.
 1723zdd_merge(X, Y, Z, S):-
 1724	(	X > Y -> memo(zdd_merge(Y, X)-Z, S)
 1725	;	memo(zdd_merge(X, Y)-Z, S)
 1726	),
 1727	(	nonvar(Z) -> true
 1728	;	cofact(X, t(A, L, R), S),
 1729		zdd_merge(L, Y, L0, S),
 1730		zdd_merge(R, Y, R0, S),
 1731		zdd_insert(A, R0, R1, S),
 1732		zdd_join(L0, R1, Z, S)
 1733	).
 1734%
 1735
 1736zdd_merge_list([], X, X, _).
 1737zdd_merge_list([A|As], X, Y, S):-
 1738	(	integer(A) -> zdd_merge(A, X, X0, S)
 1739	;	zdd_insert(A, X, X0, S)					% atom case
 1740	),
 1741	zdd_merge_list(As, X0, Y, S).
 1742
 1743% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))).
 1744%@ X = 7,
 1745%@ Y = 3.
 1746% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false
 1747%@ false.
 1748% ?- zdd((X<< {[a,b], [a,c], [a]},  Y<<{[a,b], [a]}, zdd_subfamily(Y, X))).
 1749% ?- zdd((X<< {[a,b],  [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false
 1750% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))).
 1751% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
 zdd_subfamily(+X, +Y, +S) is det
True if a ZDD X is a subfamily of a ZDD Y.
 1756zdd_subfamily(X, X, _):-!.
 1757zdd_subfamily(0, _, _):-!.
 1758zdd_subfamily(_, 0, _):-!, fail.
 1759zdd_subfamily(1, X, S):-!, zdd_has_1(X, S).
 1760zdd_subfamily(X, X0, S):-
 1761		cofact(X, t(A, L, R), S),
 1762		cofact(X0, t(A0, L0, R0), S),
 1763		zdd_compare(C, A, A0, S),
 1764		(	C = (=) ->
 1765			zdd_subfamily(L, L0, S),
 1766			zdd_subfamily(R, R0, S)
 1767		;	C = (>),
 1768			zdd_subfamily(X, L0, S)
 1769		).
 1770
 1771		/*********************************
 1772		*     division/residue  in ZDD   *
 1773		*********************************/
 zdd_divmod(X, Y, D, M, S) is det
D = { A-B | A in X, B is Y, B is a subset of A }. M = { A in X | forall B in Y B is not a subset of A }. ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod(X, Y, D, M, S), psa(X, S), psa(D, S), psa(M, S).
 1781zdd_divmod(X, Y, D, M, S):-
 1782	zdd_div_div(X, Y, D1, D, S),
 1783	zdd_subtr(X, D1, M, S).
 zdd_divmod0(X, Y, D, D0, S) is det
D = { A in X | A is a subset of B for some B in Y}, D0 = { A-B | A in X, B in Y, B is a subset of A}.
 1789% ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S),
 1790%  psa(X, S), psa(D, S), psa(M, S).
 1791zdd_divmod0(X, Y, D, M, S):-
 1792	zdd_divisible(X, Y, D, S),
 1793	zdd_subtr(X, D, M, S).
 zdd_div_div(X, Y, D, D0, S) is det
D is the set of elements in X divisible by an element of Y, D0 is the set A-B (= A//B) s.t. A in X, B in Y and B is subset of A.
 1799% ?- zdd X<< +[b], zdd_div_div(X, 1, D, M, S),
 1800%  psa(X, S), psa(D, S), psa(M, S).
 1801% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M, S),
 1802%  psa(X, S), psa(Y, S), psa(D, S), psa(M, S).
 1803% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M, S),
 1804%  psa(X, S), psa(Y, S), psa(D, S), psa(M, S).
 1805% ?- zdd X<< +[*[a,b]], Y<< +[*[b]], psa(X, S), psa(Y, S), zdd_div_div(X, Y, D, M, S), psa(D, S), psa(M, S).
 1806% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]],
 1807%	zdd_div_div(X, Y, D, D1, S),
 1808%	psa(D, S), psa(D1, S).
 1809
 1810zdd_div_div(0, _, 0, 0, _):-!.
 1811zdd_div_div(1, X, Y, Y, S):-!,
 1812	(	zdd_has_1(X, S) ->	Y = 1
 1813	;	Y = 0
 1814	).
 1815zdd_div_div(_, 0, 0, 0, _):-!.
 1816zdd_div_div(X, 1, X, X, _):-!.
 1817zdd_div_div(X, Y, Z, U, S):- memo(div_div(X, Y)- P, S),
 1818	(	nonvar(P) -> P = (Z, U)
 1819	;	cofact(X, t(A, L, R), S),
 1820		zdd_div_div(L, Y, L0, U0, S),
 1821		zdd_div_div(A, R, Y, R0, V0, S),
 1822		zdd_join(L0, R0, Z, S),
 1823		zdd_join(U0, V0, U, S),
 1824		P = (Z, U)
 1825	).
 1826%
 1827zdd_div_div(_, 0, _, 0, 0, _):-!.
 1828zdd_div_div(_, 1, 0, 0, 0, _):-!.  % ???
 1829zdd_div_div(A, 1, 1, Z, Z, S):-!, zdd_singleton(A, Z, S).
 1830zdd_div_div(_, _, 0, 0, 0, _):-!.
 1831zdd_div_div(A, X, 1, Z, Z, S):-!, cofact(Z, t(A, 0, X), S).
 1832zdd_div_div(A, X, Y, Z, U, S):- cofact(Y, t(B, L, R), S),
 1833		zdd_compare(C, A, B, S),
 1834		(	C = (<) ->
 1835			zdd_div_div(X, Y, Z0, U0, S),
 1836			zdd_insert(A, Z0, Z, S),
 1837			zdd_insert(A, U0, U, S)
 1838		;	C = (=)	->
 1839			zdd_div_div(X, L, Z0, U0, S),
 1840			zdd_insert(A, Z0, Z1, S),
 1841			zdd_insert(A, U0, U1, S),
 1842			zdd_div_div(X, R, Z2, U2, S),
 1843			zdd_insert(A, Z2, Z3, S),       % A is absorbed due to hit (A=B).
 1844			zdd_join(Z1, Z3, Z, S),
 1845			zdd_join(U1, U2, U, S)
 1846		; 	zdd_div_div(A, X, L, Z, U, S)
 1847		).
 zdd_div(+X, +Y, -Z, +S) is det
Z is the quotient of X divided by Y; Z = { A - B | A in X, B in Y, B is a subset of A }
 1853% ?- zdd(( X<< {[a]}, zdd_div(X, X, Z), psa(Z))).
 1854% ?- zdd(( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1855% ?- zdd(( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))).
 1856% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1857% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1858% ?- zdd(( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1859% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))).
 1860% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1861% ?- zdd(( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))).
 1862% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1863% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))).
 1864% ?- zdd(( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))).
 1865% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))).
 1866% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))).
 1867% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))).
 1868% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))).
 1869% ?- zdd(( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))).
 1870% ?- zdd(( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))).
 1871% ?- zdd(( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))).
 1872% ?- zdd(( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))).
 1873% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))).
 1874% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))).
 1875% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))).
 1876
 1877%
 1878zdd_div(0, _, 0, _):-!.
 1879zdd_div(1, X, Y, S):-!,
 1880	(	zdd_has_1(X, S) ->	Y = 1
 1881	;	Y = 0
 1882	).
 1883zdd_div(X, Y, Z, S):- memo(zdd_div(X, Y)- Z, S),
 1884	(	nonvar(Z) -> true
 1885	;	cofact(X, t(A, L, R), S),
 1886		zdd_div(L, Y, L0, S),
 1887		zdd_div(A, R, Y, R0, S),
 1888		zdd_join(L0, R0, Z, S)
 1889	).
 1890%
 1891zdd_div(_, _, 0, 0, _):-!.
 1892zdd_div(A, X, 1, Z, S):-!, cofact(Z, t(A, 0, X), S).
 1893zdd_div(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
 1894		zdd_compare(C, A, B, S),
 1895		(	C = (<) ->
 1896			zdd_div(X, Y, Z0, S),
 1897			cofact(Z, t(A, 0, Z0), S)
 1898		;	C = (=)	->
 1899			zdd_div(X, L, L0, S),
 1900			zdd_div(X, R, R0, S),
 1901			cofact(Z, t(A, R0, L0), S)
 1902		;	zdd_div(A, X, L, Z, S)
 1903		).
 zdd_divisible(+X, +Y, -Z, +S) is det
Y = { A in X | for some B in Y, B is a subset of A }.
 1909% ?- zdd {N=10, numlist(1, N, Ns), numlist(1, 10, Js)}, X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z).
 1910% ?- zdd  X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z).
 1911% ?- zdd X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z).
 1912% ?- zdd X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z).
 1913% ?- zdd X<<pow([a, b,  c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z).
 1914
 1915zdd_divisible(0, _, 0, _):-!.
 1916zdd_divisible(1, X, Y, S):-!,
 1917	(	zdd_has_1(X, S) ->	Y = 1
 1918	;	Y = 0
 1919	).
 1920zdd_divisible(X, Y, Z, S):- memo(zdd_divisible(X, Y)- Z, S),
 1921	(	nonvar(Z) -> true
 1922	;	cofact(X, t(A, L, R), S),
 1923		zdd_divisible(L, Y, L0, S),
 1924		zdd_divisible(A, R, Y, R0, S),
 1925		zdd_join(L0, R0, Z, S)
 1926	).
 1927%
 1928zdd_divisible(_, _, 0, 0, _):-!.
 1929zdd_divisible(A, X, 1, Z, S):-!, cofact(Z, t(A, 0, X), S).
 1930zdd_divisible(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
 1931		zdd_compare(C, A, B, S),
 1932		(	C = (<) ->
 1933			zdd_divisible(X, Y, Z0, S),
 1934			cofact(Z, t(A, 0, Z0), S)
 1935		;	C = (=)	->
 1936			zdd_divisible(X, L, L0, S),
 1937			zdd_divisible(X, R, R0, S),
 1938			zdd_join(L0, R0, Z0, S),
 1939			cofact(Z, t(A, 0, Z0), S)
 1940		;	zdd_divisible(A, X, L, Z, S)
 1941		).
 zdd_divisible_by_all(+X, +Y, -Z, +S) is det
Z = { A in X | forall B in Y B is a subset of A }.
 1946% ?- zdd X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S).
 1947% ?- zdd X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S).
 1948% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S).
 1949% ?- zdd X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S).
 1950% ?- N = 300, zdd numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns],
 1951%	time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S).
 1952
 1953% ?- zdd X<< +[*[a,b], *[c,d], *[a, d]],  Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z).
 1954
 1955zdd_divisible_by_all(X, Y, X, _):-Y<2, !.    % It was hard to find this.
 1956zdd_divisible_by_all(X, _, 0, _):-X<2, !.    % It was a little bit hard to find this.
 1957zdd_divisible_by_all(X, Y, Z, S):- memo(div_by_all(X, Y)-Z, S),
 1958	(	nonvar(Z) -> true
 1959	; 	cofact(X, t(A, L, R), S),
 1960		zdd_divisible_by_all(L, Y, L0, S),
 1961		zdd_divisible_by_all(A, R, Y, R0, S),
 1962		zdd_join(L0, R0, Z, S)
 1963	).
 1964%
 1965zdd_divisible_by_all(A, X, Y, Z, S):- Y<2, !,
 1966	cofact(Z, t(A, 0, X), S).
 1967zdd_divisible_by_all(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
 1968	zdd_compare(C, A, B, S),
 1969	(	C = (<) ->
 1970		zdd_divisible_by_all(X, Y, Z0, S),
 1971		zdd_insert(A, Z0, Z, S)
 1972	;	C = (=) ->
 1973		zdd_divisible_by_all(X, R, R1, S),
 1974		zdd_insert(A, R1, R0, S),
 1975		zdd_divisible_by_all(R0, L, Z, S)
 1976	;	Z = 0				% It was hard to find this.
 1977	).
 zdd_mod(+X, +Y, -Z, +S) is det
Z = { A in X | forall B in Y B is not a subset of A }.
 1981zdd_mod(X, Y, Z, S)	:- zdd_divisible(Y, X, X0, S),
 1982	zdd_subtr(X, X0, Z, S).
 zdd_multiple(+X, +Y, -Z, +S) is det
Z = { B in Y | exists A in X A is a subset of B}.
 1987% ?- zdd zdd_list(X, [[a]], S), zdd_list(Y, [[a,c],[a,d]], S),
 1988% zdd_multiple(X, Y, Z, S), psa(Z, S).
 1989% ?- zdd zdd_list(X, [[a,b]], S), zdd_list(Y, [[a,c],[a,d]], S),
 1990% zdd_multiple(X, Y, Z, S), psa(Z, S).
 1991% ?- zdd zdd_list(X, [[a,b]], S), Y<<pow([a,b,c]),
 1992% zdd_multiple(X, Y, Z, S), psa(Z, S).
 1993% ?- zdd Y<<pow([a,b,c]), zdd_multiple(0, Y, Z, S), psa(Z, S).
 1994% ?- zdd Y<<pow([a,b]), zdd_multiple(1, Y, Z, S), psa(Z, S).
 1995
 1996zdd_multiple(0, _, 0, _):-!.
 1997zdd_multiple(1, Y, Y, _):-!.
 1998zdd_multiple(_, Y, 0, _):-Y<2, !.
 1999zdd_multiple(X, Y, Z, S):-memo(multiple(X, Y)-Z, S),
 2000	(	nonvar(Z) -> true
 2001	;	cofact(X, t(A, L, R), S),
 2002		zdd_multiple(L, Y, L0, S),
 2003		zdd_multiple(A, R, Y, R0, S),
 2004		zdd_join(L0, R0, Z, S)
 2005	).
 2006%
 2007zdd_multiple(_, _, Y, 0, _):- Y<2, !.
 2008zdd_multiple(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S),
 2009	zdd_multiple(A, X, L, L0, S),
 2010	zdd_compare(C, A, B, S),
 2011	(	C = (<) -> R0 = 0
 2012	;	C = (=) ->
 2013		zdd_multiple(X, R, R1, S),
 2014		zdd_insert(A, R1, R0, S)
 2015	;	zdd_multiple(A, X, R, R1, S),
 2016		zdd_insert(B, R1, R0, S)
 2017	),
 2018	zdd_join(L0, R0, Z, S).
 2019
 2020		/*********************************
 2021		*     division/resudue in List   *
 2022		*********************************/
 zdd_mod_by_list(+X, +Y, -Z, +S) is det
Equivalent to zdd_list(Y, U, Z), zdd_mod_by_list(X, U, Z, S).
 2028% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a], Y), psa(Y))).
 2029% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [], Y), psa(Y))).
 2030% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a, b], Y), psa(Y))).
 2031% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [b,c], Y), psa(Y))).
 2032% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [a,c], Y), psa(Y))).
 2033% ?- zdd((X<<pow([a]), zdd_mod_by_list(X, [c], Y), psa(Y))).
 2034% ?- N=100, numlist(1, N, Ns), numlist(1, N, Js), zdd((X<<pow(Ns), zdd_mod_by_list(X, Js, Z), card(Z, C))).
 2035
 2036zdd_mod_by_list(X, Y, Z, S):- zdd_divisible_by_list(X, Y, Z0, S),
 2037	zdd_subtr(X, Z0, Z, S).
 zdd_div_by_list(+X, +Y, -Z, +S) is det
Eqivalent to zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).
 2043% ?- zdd((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))).
 2044% ?- zdd((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))).
 2045
 2046zdd_div_by_list(X, [], X, _):-!.
 2047zdd_div_by_list(X, F, Y, S):- F=[A|As],
 2048 	(	X<2 -> Y = 0
 2049	;	cofact(X, t(B, L, R), S),
 2050		zdd_div_by_list(L, F, L0, S),
 2051		zdd_compare(C, B, A, S),
 2052		(	C = (>) -> R0 = 0
 2053		;	C = (=) ->
 2054			zdd_div_by_list(R, As, R0, S)
 2055		;	zdd_div_by_list(R, F, R1, S),
 2056			zdd_insert(B, R1, R0, S)
 2057		),
 2058		zdd_join(L0, R0, Y, S)
 2059	).
 zdd_divisible_by_list(X, Y, Z, S) is det
Equivalent to zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).
 2065% ?- zdd((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))).
 2066% ?- zdd((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))).
 2067
 2068zdd_divisible_by_list(X, [], X, _):-!.
 2069zdd_divisible_by_list(X, F, Y, S):- F=[A|As],
 2070 	(	X<2 -> Y = 0
 2071	;	cofact(X, t(B, L, R), S),
 2072		zdd_divisible_by_list(L, F, L0, S),
 2073		zdd_compare(C, B, A, S),
 2074		(	C = (>) ->	R0 = 0
 2075		;	C = (=) -> 	zdd_divisible_by_list(R, As, R0, S)
 2076		;	zdd_divisible_by_list(R, F, R0, S)
 2077		),
 2078		cofact(Y, t(B, L0, R0), S)
 2079
 2080	).
 2081
 2082
 2083
 2084		/*********************
 2085		*     meta on ZDD    *
 2086		*********************/
 2087
 2088% ?- zdd((X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))).
 2089% ?- zdd((X<<pow([1,2,4,5,6]), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))).
 2090% ?- N=2, numlist(1, N, L), zdd((X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))).
 2091% ?- N=10, numlist(1, N, L), zdd((X<<pow(L),
 2092%	map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))).
 2093% ?- N=10, numlist(1, N, L), zdd((X<<pow(L),
 2094%	map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N.
 2095% ?- N=1000, numlist(1, N, L), zdd((X<<pow(L),
 2096%	map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N.
 map_zdd(+F, +X, -Y, +G) is det
Y is the set of all F_S with S running in X, where f_S = { F(a) | a in S}.

map_zdd(F, X, Y) works roughly like maplist(maplist(F), X, Y)) with a list X of lists.

 2105:- meta_predicate map_zdd(2,?,?,?). 2106
 2107map_zdd(_, X, X, _):- X<2, !.
 2108map_zdd(F, X, Y, S):- memo(map(X,F)-Y, S),
 2109	(	nonvar(Y)-> true
 2110	;	cofact(X, t(A, L, R), S),
 2111		map_zdd(F, L, L0, S),
 2112		map_zdd(F, R, R0, S),
 2113		call(F, A, B),
 2114		zdd_insert(B, R0, R1, S),
 2115		zdd_join(L0, R1, Y, S)
 2116	).
 2117
 2118% ?- zdd((memo(a-1), set_memo(a-2), memo(a-V))).
 2119% ?- zdd((X<<pow([a,b,c,d]), prz(X))).
 2120% ?- zdd((X<<pow([a,b,c]), psa(X))).
 2121% ?- zdd((prz(1))).
 2122% ?- zdd((prz(0))).
 2123% ?- zdd((mp(hello, 1))).
 2124% ?- zdd((mp(hello, 0))).
 prz(Z, S) is det
Print all sets of Z.
 2128prz(X, S):- print_set_at(X, S).
 psa(+X, +S) is det
print all sets of X ?- zdd X<<pow([a]), psa(X). ?- zdd X<<{[a]}, psa(X).
 2135psa(M, X, S):- writeln(M),
 2136	print_set_at(X, S),
 2137	writeln('-------------------').
 2138
 2139psa(X, S):- print_set_at(X, S),
 2140	writeln('-------------------').
 2141%
 2142psa :- sat_fetch(S), get_key(root, R, S),
 2143	  psa(R, S).
 2144%
 2145mp(M, X) :- shift(mp(M, X)).
 mp(+M, +X, +S) is det
print all sets of X with message M.
 2149mp(M, X, S) :- format("~w\n", [M]), print_set_at(X, S).
 print_set_at(+X, _S) is det
Pprint all sets in X.
 2153print_set_at(0, _):-!, format("\szid = 0\n\t0\n").
 2154print_set_at(1, _):-!, format("\szid = 1\n\t[]\n").
 2155print_set_at(X, S):- format("\szid = ~w\n", [X]),
 2156	forall(set_at(P, X, S), format("\t~w\n", [P])).
 2157
 2158% ?- zdd((X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X))).
 2159% ?- zdd((X<<pow([1,2]), set_at(U, X))).
 2160% ?- zdd((X<<pow([1,2]), mp(powerset, X))).
 2161
 2162set_at([], 1, _):-!.
 2163set_at(P, X, S):- X>1,
 2164	cofact(X, t(A, L, R), S),
 2165	(	set_at(P, L, S)
 2166	;	set_at(As, R, S),
 2167		P=[A|As]
 2168	).
 2169
 2170% set_at(P, X, S):- X>1,
 2171% 	cofact(X, t(A, L, R), S),
 2172% 	(	set_at(P, L, S)
 2173% 	;	set_at(As, R, S),
 2174% 		P=[A|As]
 2175% 	).
 2176
 2177% ?- zdd zdd_singleton(a, X), show_fos(X).
 2178% ?- zdd X<< {[a,b], [b,c]}, show_fos(X).
 2179% ?- zdd X<< pow([a,b]), show_fos(X).
 show_fos(+X, +S) is det
Show a family of set-likes objs in ZDD.
 2183show_fos(X, S):- X > 1,
 2184	accessible_nodes(X, Ns, S),
 2185	forall(	member(M, Ns),
 2186			( cofact(M, T, S),
 2187%			  cofact_intern(T, T0),
 2188			  writeln(M->T))).
 2189%
 2190accessible_nodes(X, Ns, S):-
 2191	accessible_nodes(X, Ns0, [], S),
 2192	sort(Ns0, Ns1),
 2193	reverse(Ns1, Ns).
 2194%
 2195accessible_nodes(X, A, A, _):- X<2, !.
 2196accessible_nodes(X, [X|A], B, S):-
 2197	cofact(X, t(_, L, R), S),
 2198	accessible_nodes(L, A, A0, S),
 2199	accessible_nodes(R, A0, B, S).
 zdd_list(?X, ?Y, +S) is det
Two way converter between zdd and list. Y is the list of zdd X.
 2205% ?- zdd((X<<pow([a,b,c]), zdd_list(X, Y),  zdd_list(X0, Y))).
 2206% ?- powerset([a,b,c], Y), zdd((zdd_list(X, Y),  zdd_list(X, Y0), zdd_list(X0, Y0))),
 2207%  maplist(sort, Y, Y1),  sort(Y1, Y2).
 2208%
 2209zdd_list(X, Y, S):- nonvar(X), !, zdd_sets(X, Y, S).
 2210zdd_list(X, Y, S):- zdd_family(Y, X, S).
 2211
 2212% ?- zdd((X<<pow([a,b,c]), sets(X, P))).
 2213% ?- zdd((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))).
 2214% ?- zdd((X<<pow([]), sets(X, P))).
 2215% ?- zdd((X<<pow([a]), sets(X, P))).
 2216% ?- zdd((X<<pow(:numlist(1,3)), sets(X, Y))).
 2217% ?- zdd((X<<pow([a,b,c]), sets(X, Y))).
 2218% ?- zdd((X<<pow(:charlist($a, $c)), sets(X, Y))).
 2219% ?- zdd((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))),  sets(X, Y))).
 sets(+X, -Y, +S)
Y is the list in X.
 2224sets(X, Y, S):- zdd_sets(X, Y0, S), zdd_sort(Y0, Y, S).
 2225%
 2226zdd_sets(1, [[]], _):-!.
 2227zdd_sets(0, [], _):-!.
 2228zdd_sets(X, P, S):-
 2229	cofact(X, t(A,L,R), S),
 2230	zdd_sets(L, Y, S),
 2231	zdd_sets(R, Z, S),
 2232	maplist(cons(A), Z, AZ),
 2233	append(AZ, Y, P).
 2234
 2235% ?- open_state(S), zdd_eval(pow([a, b, c, d, e, f]), I, S), eqns(I, X, S),
 2236%	maplist(writeln, X).
 2237%
 2238eqns(X, Y, S):- zdd_eqns(X, Y, S).
 2239
 2240basic_zdd(0).
 2241basic_zdd(1).
 2242
 2243% ?- zdd X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es).
 2244% ?- zdd X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es).
 2245
 2246zdd_eqns(I, Es, S):- nonvar(I), var(Es), !,
 2247	zdd_to_eqns(I, Es, [], S).
 2248zdd_eqns(I, Es, S):- var(I), nonvar(Es), !,
 2249	(	check_eqns_for_zdd(Es, S)
 2250	->	Es =  [X=_|_],
 2251		eqns_to_zdd(Es, X, I, S)
 2252	;	throw('Violating-underlying-ordering-on-atoms.'(Es))
 2253	).
 2254%
 2255zdd_to_eqns(I, X, S):- zdd_to_eqns(I, X, [], S),
 2256	zdd_sort(X, X1, S),
 2257	reverse(X1, X).
 2258%
 2259zdd_to_eqns(I, X, X, _):- I<2, !.
 2260zdd_to_eqns(I, X, Y, S):- memo(visited(I)-F, S),
 2261	(	nonvar(F) 	->	Y = X
 2262	;	F = true,
 2263		cofact(I, t(A, L, R), S),
 2264		X = [I=t(A, L, R)|X0],
 2265		zdd_to_eqns(L, X0, X1, S),
 2266		zdd_to_eqns(R, X1, Y, S)
 2267	).
 2268%
 2269check_eqns_for_zdd(Es, S):- are_eqns_closed(Es, Es, S),
 2270	sort(Es, Fs),
 2271	has_unique_left(Fs),
 2272	sort(2, @=<, Es, Gs),
 2273	has_unique_right(Gs).
 2274%
 2275are_eqns_closed([], _, _).
 2276are_eqns_closed([_ = t(A, L, R)|Rest], Es, S):-
 2277	(	basic_zdd(L) -> true
 2278	; 	memberchk(L = t(B, _, _), Es),
 2279		zdd_compare(<, A, B, S)
 2280	),
 2281	(	basic_zdd(R) -> true
 2282	; 	memberchk(L = t(C, _, _), Es),
 2283		zdd_compare(<, A, C, S)
 2284	),
 2285	are_eqns_closed(Rest, Es, S).
 2286%
 2287eqns_to_zdd(_, 0, 0, _):-!.
 2288eqns_to_zdd(_, 1, 1, _):-!.
 2289eqns_to_zdd(Es, X, I, S):- memo(solve(X)-I, S),
 2290	(	nonvar(I) -> true
 2291	;	memberchk(X = t(A, L, R), Es),
 2292		eqns_to_zdd(Es, L, L0, S),
 2293		eqns_to_zdd(Es, R, R0, S),
 2294		cofact(I, t(A, L0, R0), S)
 2295	).
 is_function(+X) is det
True if X is a function. ?- is_function([a-1,b-2,c-3]). ?- is_function([a-1,b-2,a-3]).
 2301is_function(X):- sort(X, Y), has_unique_left(Y).
 2302%
 2303has_unique_left([X,Y|Z]):-!,
 2304	(	arg(1, X, A), arg(1, Y, A) -> false
 2305	; 	has_unique_left([Y|Z])
 2306	).
 2307has_unique_left(_).
 check_one_to_one(X) is det
True if X is one-to-one mapping.
 2312% ?- check_one_to_one([a-1,b-2,c-3]).
 2313% ?- check_one_to_one([a-1,b-2,c-1]). % false
 2314
 2315check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y).
 2316%
 2317has_unique_right([X,Y|Z]):-!,
 2318	(	arg(2, X, A), arg(2, Y, A)  -> false
 2319	; 	has_unique_right([Y|Z])
 2320	).
 2321has_unique_right(_).
 ppoly(+X) is det
Print X in polynomical form.
 2325ppoly(X, S):- poly_term(X, Poly, S),
 2326	writeln(Poly).
 2327
 2328% ?- zdd((X<<pow([a,b]), poly_term(X, P))).
 2329% ?- zdd((X<<pow([a,b,c]), poly_term(X, P))).
 2330% ?- zdd((X<<(@a + @b), psa(X))).
 2331%
 2332poly_term(X, Poly):- shift(poly_term(X, Poly)).
 2333%
 2334poly_term(X, Poly, S):- zdd_sets(X, Sets, S),
 2335	get_compare(Pred, S),
 2336	maplist(predsort(Pred), Sets, Sets0),
 2337	predsort(Pred, Sets0, Sets1),
 2338	poly_term0(Sets1, Poly).
 2339
 2340% ?- poly_term0([], Y).
 2341% ?- poly_term0([[]], Y).
 2342% ?- poly_term0([[a], [b]], Y).
 2343% ?- poly_term0([[a*b], [c]], Y).
 2344
 2345poly_term0(X, Y):- 	maplist(mul_term, X, X0),
 2346	sum_term(X0, Y).
 2347%
 2348mul_term([], 1):-!.
 2349mul_term([X], X):-!.
 2350mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z).
 2351%
 2352sum_term([], 0):-!.
 2353sum_term([X], X):-!.
 2354sum_term([X, Y|Xs], Z):-sum_term([X+Y|Xs], Z).
 zdd_rand_path(+I, +S) is det
Print a set at random in In.

?- zdd((X << pow([a, b, c]), zdd_rand_path(X))). ?- zdd((X << {[a], [b], [c]}, zdd_rand_path(X))). ?- zdd((X << pow([a, b, c, d, e, f, g]), zdd_rand_path(X))). @ [a,c,e,f] @ X = 8.

 2366zdd_rand_path(I, S):- zdd_rand_path(I, P, [], S), writeln(P).
 2367%
 2368zdd_rand_path(I, P, S):- zdd_rand_path(I, P, [], S).
 2369%
 2370zdd_rand_path(1, X, X, _):-!.
 2371zdd_rand_path(I, X, Y, S):- I>1,
 2372	cofact(I, t(A, L, R), S),
 2373	(	L == 0 ->
 2374		X = [A|X0],
 2375		zdd_rand_path(R, X0, Y, S)
 2376	;	random(2) =:= 0 ->
 2377	 	X = [A|X0],
 2378		zdd_rand_path(R, X0, Y, S)
 2379	; 	zdd_rand_path(L, X, Y, S)
 2380	).
 zdd_atoms(+X, -Y, +S) is det
Y is the set of atoms appearing on ZDD X. ?- zdd((zdd_atoms(1, S))). ?- zdd((family([[a,b],[b,c]], X), zdd_atoms(X, S))). ?- N = 10000, time(zdd(({numlist(1, N, L)}, X<<pow(L), zdd_atoms(X, S)))). ?- zdd X<<pow([a,b,c,d]), zdd_atoms(X, U).
 2389zdd_atoms(X, [], _):- X<2, !.
 2390zdd_atoms(X, P, S):- memo(atoms(X)-P, S),
 2391	(	nonvar(P) -> true
 2392	; 	cofact(X, t(A, L, R), S),
 2393		zdd_atoms(L, Al, S),
 2394		zdd_atoms(R, Ar, S),
 2395		ord_union(Al, Ar, P0),
 2396		P=[A|P0]
 2397	).
 2398
 2399% ?- delete(pred([a-_]), [a-b, c-d, a-e], L).
 2400:- meta_predicate delete(1, ?, ?). 2401delete(X, Y, Z):- delete(X, Y, Z, []).
 2402
 2403:- meta_predicate delete(1, ?, ?, ?). 2404delete(_, [], L, L).
 2405delete(Pred, [X|Xs], L, L0):-
 2406	(	call(Pred, X)
 2407	->	delete(Pred, Xs, L, L0)
 2408	;	L = [X|L1],
 2409		delete(Pred, Xs, L1, L0)
 2410	).
 2411
 2412% ?- zdd((zdd_power([a,b], R), sets(R, U))).
 2413% ?- zdd((X<< zdd_power(:charlist($(a-c))), sets(X, U))).
 2414% ?- zdd((R<< pow(: !charlist(a-d)), card(R, C))).
 2415%%
 2416zdd_power(X, Y, S):- zdd_sort(X, X0, S),
 2417	zdd_ord_power(X0, 1, Y, S).
 zdd_ord_power(+L, +X, -Y, +S) is det
Y is the merge of powerset of L and X. ?- zdd zdd_ord_power([a,b], 1, X), psa(X).
 2422zdd_ord_power([], P, P, _).
 2423zdd_ord_power([X|Xs], P, Q, S):- zdd_ord_power(Xs, P, R, S),
 2424	cofact(Q, t(X, R,  R), S).
 atomlist(+T, -A) is det
T is a term of the form a(e0,e1), where a is an atom, e0 and e1 are integer expressions. A is the list of atoms ai with suffix i (j=<i=<k), where j and k is the value of e0 and e1.
 2432% ?- atomlist(ax(1+1, 3+1), As).
 2433% ?- atomlist(ax(1, 3), As).
 2434atomlist(X, As):- X=..[A, I, J],
 2435	I0 is I,
 2436	J0 is J,
 2437	findall(Y, (	between(I0, J0, K),
 2438					atom_concat(A, K, Y)
 2439			   ),
 2440			As).
 charlist(+U, -I) is det
U = A-B. I is unified with the list of characters X such that A @=< X @=< B.
 2446% ?- charlist(a-c, X).
 2447charlist(A-B, I):-
 2448	findall(X, (	char_type(X, alnum),
 2449				    X @>= A,
 2450					X @=< B
 2451			   ),
 2452			I).
 charlist(+A, +B, X) is det
Equivalent to charlist(A-B, X). ?- charlist(a, c, X). @ X = [a, b, c].
 2458charlist(A, B, I):- charlist(A-B, I).
 2459
 2460% ?- term_atoms(a+b=c, L).
 2461% ?- term_atoms(a+b, L).
 2462% ?- term_atoms(f(a+a), L).
 term_atoms(+X, -L, +S) is det
Unify L with a sorted list of atomic boolean subterms of X.
 2468term_atoms(X, L):- term_atoms(X, L0, []),
 2469	sort(L0, L).
 2470
 2471%
 2472term_atoms(X, L, L):- var(X), !.
 2473term_atoms(X, [X|L], L):- atom(X), !.
 2474term_atoms([X|Y], L, L0):-!,
 2475	term_atoms(X, L, L1),
 2476	term_atoms(Y, L1, L0).
 2477term_atoms(X, L, L0):- compound(X), !,
 2478	X =..[_|As],
 2479	term_atoms(As, L, L0).
 2480term_atoms(_, L, L).
 2481
 2482% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]).
 2483% ?- subst_opp(a, X, [b-a]).
 2484% ?- subst_opp([a], X, [b-a]).
 2485
 2486subst_opp(X, Y, L):-  memberchk(Y-X, L).
 2487subst_opp([X|Y], [X0|Y0], L):-!,
 2488	subst_opp(X, X0, L),
 2489	subst_opp(Y, Y0, L).
 2490subst_opp(X, Y, L):- compound(X), !,
 2491	X =..[F|As],
 2492	subst_opp(As, Bs, L),
 2493	Y =..[F|Bs].
 2494subst_opp(X, X, _).
 2495
 2496% ?- subst_term(f(a), R, [a-b]).
 2497% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]).
 2498% ?- subst_term(f(a), R, [a-X]).
 2499% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]).
 2500% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]).
 2501% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
 subst_term(+X, -Y, +S) is det
Apply an assoc list X as substitution S to X to unify Y with the result.
 2507subst_term(X, Y, S):-  member(X0-Y, S), X0==X, !.
 2508subst_term(A, B, S):-  compound(A), !,
 2509	(	A = [X|Y]	->
 2510		B = [X0|Y0],
 2511		subst_term(X, X0, S),
 2512		subst_term(Y, Y0, S)
 2513	; 	functor(A, F, N),
 2514		functor(B, F, N),
 2515		subst_term(N, A, B, S)
 2516	).
 2517subst_term(X, X, _).
 2518%
 2519subst_term(0, _, _, _):-!.
 2520subst_term(I, X, Y, S):-
 2521	arg(I, X, A),
 2522	arg(I, Y, B),
 2523	subst_term(A, B, S),
 2524	J is I - 1,
 2525	subst_term(J, X, Y, S).
 2526
 2527% ?- all_instances([a,b], [0,1], a+b=b, R).
 2528% ?- all_instances([x,y], [0,1], x+y=x, R).
 2529%!	all_instances(+As, +Vs, +X, -Y) is det.
 2530%	Unify Y with the list of possible variations P of X,
 2531%	where P is a variation of X if for each A in As with some
 2532%	V in Vs which depends on A,  P is obtained from X by replacing
 2533%	all occurrences of A appearing in X with V for A in As.
 2534
 2535all_instances(Ks, Ts, X, Y):- 	all_maps(Ks, Ts, Fs),
 2536	apply_maps(Fs, X, Y, []).
 2537%
 2538apply_maps([], _, Y, Y).
 2539apply_maps([F|Fs], X, [X0|Y], Z):-
 2540	subst_term(X, X0, F),
 2541	apply_maps(Fs, X, Y, Z).
 2542
 2543% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table).
 2544% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table).
 2545% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table).
 2546% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table).
 2547%!	mod_table(+M, +X, +E, -T) is det.
 2548%	Unify T with a set of form E' = V where
 2549%	E' is a possible ground instance  of an integer expression E
 2550%	and V is the value of E' with modulo M, where X is a set of
 2551%	parameters appearing in E.
 2552
 2553mod_table(M, Xs, Exp, Table):-	M0 is M-1,
 2554	numlist(0, M0, V),
 2555	all_instances(Xs, V, Exp, Exps),
 2556	!,
 2557	maplist(mod_arith(M), Exps, Table).
 2558%
 2559mod_arith(M, Exp, Exp=V):- V is Exp mod M.
 2560
 2561%
 2562unify_all([]).
 2563unify_all([_]).
 2564unify_all([X,Y|Z]):- zdd:(X=Y), unify_all([Y|Z]).
 2565
 2566% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))).
 2567% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false
 2568% ?- zdd((X<< {[a,b], [a,c], [a]},  Y<<{[a,b], [a]}, zdd_subfamily(Y, X))).
 2569% ?- zdd((X<< {[a,b],  [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false
 2570% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))).
 2571% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
 zdd_appear(+A, +X, +S) is det
True if A is a member of a member of X. ?- zdd((X <<{[a,b], [a,c]}, zdd_appear(e, X))). % false ?- zdd((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X))). % false ?- zdd((X <<(*[a,b]+ *[a,c]), psa(X), zdd_appear(c, X))). ?- numlist(1, 10000, Ns), zdd((X<<pow(Ns), zdd_appear(10000, X))). ?- zdd X<<pow(:numlist(1, 10000)), zdd_appear(10000, X).
 2581zdd_appear(A, X, S):- open_memo(S),
 2582					  get_child(S, M),
 2583					  zdd_appear(A, X, S, M),
 2584					  close_memo(S).
 2585%
 2586zdd_appear(A, X, S, M):- X > 1,
 2587	memo(visited(X)-B, M),
 2588	var(B),
 2589	cofact(X, t(U,L,R), S),
 2590	zdd_compare(C, A, U, S),
 2591	(	C = (=)
 2592	->  true
 2593	;	C = (>),
 2594	 	(	zdd_appear(A, L, S, M) -> true
 2595		;	L < 2
 2596		->  zdd_appear(A, R, S, M)
 2597		; 	memo(visited(L)-true, M),  %  for earlier fail.
 2598			zdd_appear(A, R, S, M)
 2599		)
 2600	).
 zdd_singleton(+X, -P, +G) is det
Unify P with a sigleton ZDD for X.
 2605zdd_singleton(X, P, S):- cofact(P, t(X, 0, 1), S).
 zdd_has_1(+X, +G) is det
true if X has 1 (the empty set). ?- zdd0((X<<pow([a,b,c]), zdd_subtr(1, X, Y), card(Y, C))).
 2611zdd_has_1(1, _):-!.
 2612zdd_has_1(X, S):- X>1,
 2613   cofact(X, t(_, L, _), S),
 2614   zdd_has_1(L, S).
 zdd_subst(+X, +U, +P, -Q, +S) is det
X : an atom. U, P: zdd. Unify Q with a substitute of P replacing all occurrences of atom X with U. The replacing operation is the merge of U and the child zdd of X. This is analogy of the familiar substitution operation on factored expressions. ex. (a+b)/x : u*x*(y+z) --> a*u*y + a*u*z + b*u*y + b*u*z . ?- zdd((U<<{[a]}, P<<pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q))).
 2625zdd_subst(_, _, X, X, _):- X<2, !.
 2626zdd_subst(X, U, P, Q, S):- memo(zdd_subst(X, U, P)-Q, S),
 2627	(	nonvar(Q) -> true
 2628	;	cofact(P, t(Y, L, R), S),
 2629		zdd_subst(X, U, L, L0, S),
 2630		zdd_compare(C, X, Y, S),
 2631		(	C = (=) 	->	zdd_merge(U, R, R0, S)
 2632		;	C = (<)		->  zdd_cons(R0, Y, R, S)
 2633		;	zdd_subst(X, U, R, R1, S),
 2634			zdd_insert(Y, R1, R0, S)
 2635		),
 2636		zdd_join(L0, R0, Q, S)
 2637	).
 2638
 2639		/***********************
 2640		*    product on zdd    *
 2641		***********************/
 2642
 2643% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))).
 2644% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y))).
 2645% ?- zdd((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))).
 2646% ?- zdd((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))).
 2647% ?- time(zdd((X<<pow(@numlist(1,16)), Z<<(X**X), card(Z, C)))).
 2648% ?- call_with_time_limit(120, (numlist(1, 16, R),
 2649%	time(zdd((X<<pow(R), Z<<(X**X), card(Z, C)))))).
 2650
 2651zdd_product(X, Y, Z):- shift(zdd_product(X, Y, Z)).
 2652%
 2653zdd_product(X, Y, 0, _):- (X<2; Y<2), !.
 2654zdd_product(X, Y, Z, S):- memo(prod(X, Y)-Z, S),
 2655	(	nonvar(Z) -> true	 % , write(.)	% hits found.
 2656	;	zdd_product(X, Y, [], Bs, 0, Z0, S),
 2657		append_pairs_list(X, Bs, Z1, S),
 2658		zdd_join(Z0, Z1, Z, S)
 2659	).
 2660%
 2661zdd_product(_, X, Bs, Bs, Z, Z, _):- X<2, !.
 2662zdd_product(X, Y, Bs, Q, U, V, S):- cofact(Y, t(B, L, R), S),
 2663	zdd_product(X, L, L0, S),
 2664	zdd_join(L0, U, U0, S),
 2665	zdd_product(X, R, [B|Bs], Q, U0, V, S).
 2666%
 2667append_pairs_list(X, _, X, _):- X<2, !.
 2668append_pairs_list(X, Bs, U, S):- cofact(X, t(A, L, R), S),
 2669	append_pairs_list(R, Bs, R0, S),
 2670	append_pairs_list(L, Bs, L0, S),
 2671	insert_pairs(A, Bs, R0, R1, S),
 2672	zdd_join(L0, R1, U, S).
 2673
 2674%
 2675insert_pairs(_, [], U, U, _):-!.
 2676insert_pairs(A, [B|Bs], U, V, S):-
 2677	zdd_insert((A-B), U, U0, S),
 2678	insert_pairs(A, Bs, U0, V, S).
 2679
 2680		/*************************
 2681		*     Quotient on ZDD    *
 2682		*************************/
 zdd_insert(+A, +Y, -Z, +S) is det
Insert A to each set in a ZDD Y, and unify Z. Z = { union of U and {A} | U in Y }.

?- zdd((zdd_insert(a, 1, X), zdd_insert(b, X, X1), prz(X1))). ?- zdd((X<<pow([a,b,c]), zdd_insert(x, X, X1), psa(X1))).

 2691zdd_insert(_, 0, 0, _):-!.
 2692zdd_insert(A, 1, J, S):-!, zdd_singleton(A, J, S).
 2693zdd_insert(A, I, J, S):- memo(insert(A, I)-J, S),
 2694		(	nonvar(J) -> true
 2695		;	cofact(I, t(X, L, R), S),
 2696			zdd_compare(C, A, X, S),
 2697			(	C = (=)	->
 2698				zdd_join(L, R, K, S),
 2699				cofact(J, t(X, 0, K), S)
 2700			;	C = (<)	->
 2701				cofact(J, t(A, 0, I), S)
 2702			;  	zdd_insert(A, L, L0, S),
 2703				zdd_insert(A, R, R0, S),
 2704				cofact(J, t(X, L0, R0), S)
 2705			)
 2706		).
 2707
 2708% ?- zdd X<<pow([a,b]), Y<<pow([c,d]),
 2709% psa(X, S), psa(Y, S),
 2710% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S).
 2711
 2712% ?- zdd X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S),
 2713%	psa(Y, S).
 2714% ?- listing(zdd_insert).
 2715
 2716:- meta_predicate zdd_insert(3, ?, ?, ?, ?). 2717zdd_insert(_, _, 0, 0, _):-!.
 2718zdd_insert(_, A, 1, Y, S):-!, zdd_singleton(A, Y, S).
 2719zdd_insert(F, A, X, Y, S):- memo(zdd_insert(X, A, F)-Y, S),
 2720	(	nonvar(Y) -> true  %	, write(.) % many hits
 2721	;	cofact(X, t(B, L, R), S),
 2722		zdd_insert(F, A, L, L0, S),
 2723		call(F, C, A, B),
 2724		(	C = (=) -> zdd_cons(R0, A, R, S)
 2725		;	C = (<) -> bdd_append([A, B], R, R0, S)
 2726		;	zdd_insert(F, A, R, R1, S),
 2727			zdd_cons(R0, B, R1, S)
 2728		),
 2729		zdd_join(L0, R0, Y, S)
 2730	).
 2731
 2732% ?- zdd((family([[a, b],[b]], X), sets(X, Sx),
 2733%	zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
 zdd_insert_atoms(+As, +X, -Y) is det
Insert all atoms in As to X to get the result Y.
 2738% ?- numlist(1, 10000, Ns), zdd((zdd_insert_atoms(Ns, 1, X), psa(X))).
 2739zdd_insert_atoms(As, X, Y):- shift(zdd_insert_atoms(As, X, Y)).
 2740
 2741% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))).
 2742% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))).
 2743zdd_insert_atoms(X, Y, Z, S):- zdd_sort(X, X0, S),
 2744	zdd_ord_insert(X0, Y, Z, S).
 2745%
 2746zdd_ord_insert(_, 0, 0, _):-!.
 2747zdd_ord_insert([], X, X, _):-!.
 2748zdd_ord_insert(As, 1, Y, S):-!, zdd_ord_append(As, 1, Y, S).
 2749zdd_ord_insert(As, X, Y, S):- memo(ord_insert(X, As)-Y, S),
 2750	(	nonvar(Y) -> true % , write(.)   % many hits.
 2751	;	As = [A|U],
 2752		cofact(X, t(B, L, R), S),
 2753		zdd_compare(C, A, B, S),
 2754		(	C = (<) ->
 2755			zdd_ord_insert(U, X, Y0, S),
 2756			cofact(Y, t(A, 0, Y0), S)
 2757		;	C = (=) ->
 2758			zdd_ord_insert(U, L, L1, S),
 2759			zdd_ord_insert(U, R, R1, S),
 2760			zdd_join(R1, L1, Y0, S),
 2761			cofact(Y, t(A, 0, Y0), S)
 2762		;	zdd_ord_insert(As, L, L1, S),
 2763			zdd_ord_insert(As, R, R1, S),
 2764			cofact(Y, t(B, L1, R1), S)
 2765		)
 2766	).
 zdd_append(+X, +Y, -Z, +G) is det
Z is result of inserting all elements of X into Y. Y is assumed to have no atom in X.
 2772% ?- numlist(1, 100, Ns), zdd((X<<pow(Ns), card(X, C))).
 2773% ?- numlist(1, 100, Ns), zdd((X<<pow(Ns))).
 2774
 2775% ?- zdd((zdd_append([c, a, b,c], 1, Z), psa(Z))).
 2776zdd_append(X, Y, Z, S):- zdd_sort(X, X0, S),
 2777	zdd_ord_append(X0, Y, Z, S).
 2778%
 2779zdd_ord_append([], X, X, _).
 2780zdd_ord_append([A|As], X, Y, S):-
 2781	zdd_ord_append(As, X, Y0, S),
 2782	cofact(Y, t(A, 0, Y0), S).
 2783
 2784% ?- zdd X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y, S), psa(Y, S).
 2785:- meta_predicate zdd_reorder(3, ?, ?, ?). 2786zdd_reorder(_, X, X, _):- X<2, !.
 2787zdd_reorder(F, X, Y, S):- cofact(X, t(A, L, R), S),
 2788	zdd_reorder(F, L, L0, S),
 2789	zdd_reorder(F, R, R1, S),
 2790	zdd_insert(F, A, R1, R0, S),
 2791	zdd_join(L0, R0, Y, S).
 2792
 2793
 2794		/*****************
 2795		*     filters    *
 2796		*****************/
 2797
 2798% ?- zdd X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y, S), psa(Y, S).
 2799% ?- zdd X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y, S), psa(Y, S).
 2800% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y, S), psa(Y, S).
 2801% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, 3], X, Y, S), psa(Y, S).
 2802% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y, S), psa(Y, S).
 2803% ?- zdd numlist(1, 1000, Ns), X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y, S), card(Y, C, S),
 2804%	card(X, D, S), compare(E, C, D), U is D-C.
 2805%
 2806ltr_meet_filter([], X, X, _):-!.
 2807ltr_meet_filter([A|F], X, Y, S):-
 2808	ltr_filter(A, X, X0, S),
 2809	ltr_meet_filter(F, X0, Y, S).
 2810
 2811% ?- zdd X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y, S), psa(Y, S).
 2812% ?- zdd X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y, S), psa(Y, S).
 2813ltr_join_filter(F, X, Y, S):-
 2814	ltr_join_filter(F, X, 0, Y, S).
 2815%
 2816ltr_join_filter([], _, Y, Y, _):-!.
 2817ltr_join_filter([P|F], X, Y, Y0, S):-!,
 2818	ltr_filter(P, X, Y1, S),
 2819	zdd_join(Y, Y1, Y2, S),
 2820	ltr_join_filter(F, X, Y2, Y0, S).
 2821
 2822%
 2823ltr_filter(-A, X, Y, S):-!, ltr_filter_negative(A, X, Y, S).
 2824ltr_filter(A, X, Y, S):- ltr_filter_positive(A, X, Y, S).
 2825
 2826%
 2827ltr_filter_negative(_, X, X, _):- X<2, !.
 2828ltr_filter_negative(A, X, Y, S):- memo(letral_neg(X, A)-Y, S),
 2829	(	nonvar(Y) -> true
 2830	;	cofact(X, t(B, L, R), S),
 2831		ltr_filter_negative(A, L, L0, S),
 2832		zdd_compare(C, A, B, S),
 2833		(	C = (=) -> R0 = 0
 2834		;	C = (<) ->  R0 = R
 2835		;	ltr_filter_negative(A, R, R0, S)
 2836		),
 2837		cofact(Y, t(B, L0, R0), S)
 2838	).
 2839%
 2840ltr_filter_positive(_, X, 0, _):- X<2, !.
 2841ltr_filter_positive(A, X, Y, S):- memo(ltr_pos(X, A)-Y, S),
 2842	(	nonvar(Y) -> true
 2843	;	cofact(X, t(B, L, R), S),
 2844		ltr_filter_positive(A, L, L0, S),
 2845		zdd_compare(C, A, B, S),
 2846		(	C = (=) -> R0 = R
 2847		;	C = (<) ->  R0 = 0
 2848		;	ltr_filter_positive(A, R, R0, S)
 2849		),
 2850		cofact(Y, t(B, L0, R0), S)
 2851	).
 2852
 2853% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[-b,-c]], X, Y)), psa(Y))).
 2854% ?- zdd((X<<pow([a,b]), shift(dnf_filter([[b]], X, Y)), psa(Y))).
 2855% ?- zdd((X<<pow([a,b]), shift(dnf_filter([[a,b]], X, Y)), psa(Y))).
 2856% ?- zdd((X<<pow([a,b]), shift(dnf_filter([], X, Y)), psa(Y))).
 2857% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[c]], X, Y)), psa(Y))).
 2858% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([], X, Y)), psa(Y))).
 2859% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[a],[-c]], X, Y)), psa(Y))).
 2860dnf_filter(DNF, X, Y, S):- dnf_filter(DNF, X, 0, Y, S).
 2861%
 2862dnf_filter([], _, Y, Y, _).
 2863dnf_filter([F|Fs], X, Y, Z, S):-
 2864	ltr_meet_filter(F, X, X0, S),
 2865	zdd_join(X0, Y, Y0, S),
 2866	dnf_filter(Fs, X, Y0, Z, S).
 2867
 2868% ?- zdd((X<<pow([a,b,c]), shift(cnf_filter([[-b,-c]], X, Y)), psa(Y))).
 2869% ?- zdd((X<<pow([a,b,c]), shift(cnf_filter([[-a, -b, -c]], X, Y)), psa(Y))).
 2870cnf_filter([], X, X, _).
 2871cnf_filter([F|Fs], X, Y, S):-
 2872	ltr_join_filter(F, X, X0, S),
 2873	cnf_filter(Fs, X0, Y, S).
 2874
 2875%
 2876zdd_meet_list([A], A, _):-!.
 2877zdd_meet_list([A|As], B, S):- zdd_meet_list(As, A, B, S).
 2878%
 2879zdd_meet_list([], X, X, _).
 2880zdd_meet_list([A|As], X, Y, S):- zdd_meet(A, X, X0, S),
 2881	zdd_meet_list(As, X0, Y, S).
 2882%
 2883zdd_join_list([], 0, _):-!.
 2884zdd_join_list([X|Xs], Y, S):- zdd_join_list(Xs, X, Y, S).
 2885%
 2886zdd_join_list([], X, X, _):-!.
 2887zdd_join_list([A|As], X, Y, S):- zdd_join(A, X, X0, S),
 2888	zdd_join_list(As, X0, Y, S).
 2889
 2890%
 2891ltr_join_list([], 0, _):-!.
 2892ltr_join_list([X|Xs], Y, S):-ltr_join_list(Xs, X, Y, S).
 2893%
 2894ltr_join_list([], X, X, _):-!.
 2895ltr_join_list([A|As], X, Y, S):- zdd_join(A, X, X0, S),
 2896	ltr_join_list(As, X0, Y, S).
 2897
 2898		/*********************
 2899		*     remove atom    *
 2900		*********************/
 zdd_remove(+A, +X, -Y, +S) is det
Remove an atom A from each set in a ZDD X. Y = { U\{A} | U in X }
 2906% ?- zdd((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y),
 2907%	sets(Y, Sy))).
 2908zdd_remove(X, Y, Z, S):- setup_call_cleanup(
 2909							 open_state(M, [hash_size(256)]),
 2910							 zdd_remove(X, Y, Z, S, M),
 2911							 close_state(M)).
 2912%
 2913zdd_remove(_, X, X,  _, _):- X<2, !.
 2914zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S),
 2915	(	nonvar(J)	->  true
 2916	; 	cofact(I, t(Ai, Li, Ri), S),
 2917		zdd_compare(C, A, Ai, S),
 2918		(	C = (<)  -> J = I
 2919		;   C = (>)  -> zdd_remove(A, Li, Lia, S, M),
 2920						zdd_remove(A, Ri, Ria, S, M),
 2921						cofact(J, t(Ai, Lia, Ria), S)
 2922		; 	zdd_join(Li, Ri, J, S)
 2923		)
 2924	).
 2925
 2926
 2927		/*********************
 2928		*     Cardinality    *
 2929		*********************/
 card(+I, -C, +S) is det
unify C with the cardinality of a family I of sets.
 2934% ?-N = 10000,  numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:= 2^N.
 2935%@ % 1,298,553 inferences, 0.105 CPU in 0.114 seconds (92% CPU, 12364110 Lips)
 2936%@ N = 10000,
 2937%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
 2938%@ X = 10001.
 2939
 2940%
 2941card(X, Y, S):- setup_call_cleanup(
 2942	open_state(M),
 2943	card_with_memo(X, Y, S, M),
 2944	close_state(M)).
 2945
 2946%
 2947card_with_memo(I, I, _, _):- I < 2, !.
 2948card_with_memo(I, C, S, M):- memo(I-C, M),
 2949	(	nonvar(C) -> true
 2950	;	cofact(I, t(_, L, R), S),
 2951		card_with_memo(R, Cr, S, M),
 2952		card_with_memo(L, Cl, S, M),
 2953		C is Cl + Cr
 2954	).
 max_length(+X, -Max, +S) is det
Unify Max with max of size of members of X.
 2959max_length(X, Max, S):-
 2960	setup_call_cleanup(
 2961		open_memo(S),
 2962		max_length_with_memo(X, Max, S),
 2963		close_memo(S)).
 2964%
 2965max_length_with_memo(X, 0, _):- X<2, !.
 2966max_length_with_memo(X, Max, S):-
 2967	memo(max(X)-Max, S),
 2968	cofact(X, t(_, L, R), S),
 2969	(	nonvar(Max) -> true
 2970	;	max_length_with_memo(L, ML, S),
 2971		max_length_with_memo(R, MR, S),	Max is max(1 + MR, ML)
 2972	).
 2973
 2974		/***********************
 2975		*     Handy helpers    *
 2976		***********************/
 2977
 2978%
 2979unify_zip([]).
 2980unify_zip([X-X|R]):- unify_zip(R).
 2981
 2982
 2983		/******************************************
 2984		*     Oprations on clauses of literals    *
 2985		******************************************/
 2986
 2987% ?- ltr_compare(C, a, -a).
 2988% ?- ltr_compare(C, -(a), a).
 2989% ?- ltr_compare(C, -(b), a).
 2990% ?- ltr_compare(C, -(a), b).
 2991% ?- ltr_compare(C, -(a), -(b)).
 2992% ?- ltr_compare(C, -(a), -(a)).
 ltr_compare(-C, +X, +Y) is det
Compare literals X and Y, and C is unified with <, =, > as the standard compare/3. ex. a<b, a < -a, -a < b, -a < -b.
 2999ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y).
 3000ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y),
 3001		(	C0 == (=) ->  C =(<)
 3002		;	C0 = C
 3003		).
 3004ltr_compare(C, -(X), Y):-!, compare(C0, X, Y),
 3005		(	C0 == (=) -> C = (>)
 3006		;	C0 = C
 3007		).
 3008ltr_compare(C, X, Y):- compare(C, X, Y).
 3009
 3010% ?- zdd {ltr_compare(C, a, b)}.
 3011% ?- zdd {ltr_compare(C, -a, a)}.
 3012% ?- zdd {ltr_compare(C, a, -a)}.
 3013% ?- zdd {ltr_compare(C, -a, b)}.
 3014ltr_compare(C, X, Y, S):- get_compare(F, S),
 3015	call(F, C, X, Y).
 ltr_sort(+X, -Y) is det
Y is unified with sorted X by ltr_compare.
 3020% ?- ltr_sort([b, b, a], X).
 3021% ?- ltr_sort([-b, b,-b, -a], X).
 3022
 3023% ?- zdd(shift(ltr_sort([-c, a, -b, -a, b, c], X))).
 3024ltr_sort(X, Y):- predsort(ltr_compare, X, Y).
 ltr_sort(+X, -Y, +S) is det
Y is the sorted as literals based on the order set in S.
 3028ltr_sort(X, Y, S):- get_compare(F, S),
 3029	predsort(F, X, Y).
 3030
 3031
 3032% ?- zdd((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false
 3033% ?- zdd((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))).
 3034%
 3035ltr_memberchk(L, Z, S):- ltr_sort(L, L0, S),
 3036	ltr_ord_memberchk(L0, Z, S).
 3037%
 3038ltr_ord_memberchk([], Z, S):- !,  zdd_has_1(Z, S).
 3039ltr_ord_memberchk([A|As], Z, S):- Z > 1,
 3040	cofact(Z, t(B, L, R), S),
 3041	ltr_compare(C, A, B),
 3042	(	C = (=) -> ltr_ord_memberchk(As, R, S)
 3043	;	ltr_ord_memberchk([A|As], L, S)
 3044	).
 3045
 3046% ?- call_with_time_limit(100, time(zdd((big_normal_form(30, X), resolve(X))))).
 3047% ?- zdd((big_normal_form(1, X), ltr_card(X, C))).
 3048% ?- zdd((big_normal_form(2, X), ltr_card(X, C))).
 3049% ?- zdd((big_normal_form(3, X), ltr_card(X, C))).
 3050% ?- zdd((big_normal_form(10, X), ltr_card(X, C))).
 3051% ?- zdd((big_normal_form(20, X), ltr_card(X, C))).
 3052% ?- time(zdd((big_normal_form(100, X), ltr_card(X, C)))).
 3053% ?- N=10, time(zdd((big_normal_form(N, X), ltr_card(X, C)))), C=:=2^N.
 3054% ?- N=300, time(zdd((big_normal_form(N, X), ltr_card(X, C, N)))), C=:=2^N.
 3055
 3056big_normal_form(X, Y):- shift(big_normal_form(X, Y)).
 3057%
 3058big_normal_form(0, 1, _).
 3059big_normal_form(N, X, S):- N>0,
 3060	N0 is N-1,
 3061	big_normal_form(N0, X0, S),
 3062	ltr_insert(N, X0, R, S),
 3063	ltr_insert(-N, X0, L, S),
 3064	zdd_join(L, R, X, S).
 3065
 3066% ?- numlist(1, 3, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), psa(X), psa(Y), card(Y, C))).
 3067% ?- time((numlist(1, 20, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), card(Y, C))))).
 3068% ?- zdd((X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y))).
 3069% ?- zdd((X<<{[a,b],[c,d]},  ltr_choices(X, Y), ltr_choices(Y, Z),
 3070%	ltr_choices(Z, U), psa(X),  psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V))).
 3071% ?- zdd(( (X<< {[a,b]}), ltr_choices(X, Y), psa(X), {nl}, psa(Y))).
 3072% ?- zdd(( (X<< {[a,b,c]}), ltr_choices(X, Y),	psa(X), {nl}, psa(Y))).
 3073% ?- zdd(( (X<< {[a, b], [c, d]}), ltr_choices(X, Y), psa(Y))).
 3074% ?- zdd(( (X<< {[], [a, b], [c, d]}), ltr_choices(X, Y), psa(Y))).
 3075% ?- zdd(( (X<< {[a], [c, d]}), ltr_choices(X, Y), psa(Y))).
 3076% ?- zdd(( X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y))).
 3077% ?- zdd(( X<< {[a,b]}, ltr_choices(X, Y), psa(Y))).
 3078% ?- zdd(( X<< {[]}, ltr_choices(X, Y), psa(Y))).
 3079% ?- zdd(( cnf(a, X), ltr_choices(X, Y), psa(Y))).
 3080% ?- zdd(( cnf(a*b, X), ltr_choices(X, Y), psa(Y))).
 3081% ?- zdd(( cnf(a* (-a), X), ltr_choices(X, Y), psa(Y))).
 3082
 3083% ?- N=10, numlist(2, 10, Ns), zdd((sample_cnf(Ns, X), card(X, C))).
 3084% ?- N=100, numlist(2, N, Ns), time(zdd((sample_cnf(Ns, X), card(X, C), resolve(X)))).
 3085%@
 3086
 3087sample_cnf([], 1, _).
 3088sample_cnf([J|Js], X, S):- sample_cnf(Js, Y, S),
 3089	ltr_insert(J, Y, Z, S),
 3090	ltr_insert(-J, Y, U, S),
 3091	ltr_join(Z, U, X, S).
 3092
 3093%  test sat. PASSED. [2023/11/09]
 3094% ?- sat(-true).  % false
 3095% ?- sat(a+b), sat_count(C).
 3096% ?- sat(a), sat(b).
 3097% ?- sat(-(a + -a)). % false
 3098% ?- sat(a), sat(b), sat_count(C).
 3099% ?- sat(or(a, b)), sat_count(C).
 3100% ?- sat(b), sat_count(C).
 3101% ?- sat(xor(a, b)), sat_count(C).
 3102% ?- sat(exor(a, b)), sat_count(C).
 3103% ?- sat(e_x_o_r(a, b)), sat_count(C).
 3104% ?- sat(a), sat(-a).	% false.
 3105% ?- sat(a), sat(a+b), sat_count(C).
 3106% ?- sat(a(1)+a(2)), sat_count(C).
 3107% ?- sat(A+a(2)), sat_count(C).
 3108% ?- sat(A + B), sat_count(C).
 3109% ?- sat(a+b+c+d), sat_count(C).
 3110% ?- sat(a+b), sat(c+d),  sat_count(C).
 3111% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C).
 3112% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C).
 3113% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false.
 3114% ?- sat(*[p(1),p(2)]), sat_count(C).
 3115% ?- sat(+[p(1),p(2)]), sat_count(C).
 3116% ?- N=10, findall(p(I, J),
 3117%	(between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C).
 3118% ?- N=10, findall(p(I, J),
 3119%	(between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C).
 3120% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false
 3121% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C).
 3122% ?- sat(A + B), sat_count(C).
 3123% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C).
 3124% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C).
 3125% ?- sat(a=<(b=<a)), sat_count(Count).
 3126% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C).
 3127% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K).
 3128% ?- Prop =
 3129%	( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)),
 3130%	sat(Prop), sat_count(C).
 3131% ?- sat(a+b), sat(b+c), b_getval(sat_state, S),
 3132%	get_key(root, R, S), ltr_card(R, C, S).
 3133% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false
 3134% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false
 3135
 3136% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa.
 3137% ?- sat(A=:=B), psa, sat(B=:=C), psa.
 3138sat(X):-
 3139	sat_fetch(S),
 3140	get_key(root, Root, S),
 3141	dnf(X, Y, S),
 3142	ltr_merge(Y, Root, Root0, S),
 3143	set_key(root, Root0, S),
 3144	!,
 3145	Root0 \== 0.
 3146%
 3147sat_fetch(S):-
 3148	(	nb_current(sat_state, S),  S \== [] -> true
 3149	; 	open_state(S, [extra([root-1, varnum-0, atom_index-0])]),
 3150		set_compare(ltr_compare, S),
 3151		b_setval(sat_state, S)
 3152	).
 3153
 3154sat_close:- sat_fetch(S),
 3155	close_state(S),
 3156	b_setval(sat_state, S).  % nb_setval ?
 3157
 3158% ?- Prop =
 3159%	( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)),
 3160%	sat(Prop),
 3161%	sat_count(Count).
 3162
 3163% ?- Prop =
 3164%	( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)),
 3165%	sat(-Prop),
 3166%	sat_count(Count).
 3167
 3168zdd_numbervars(X, S):-	get_key(varnum, N, S),
 3169	numbervars(X, N, N0),
 3170	set_key(varnum, N0, S).
 3171
 3172% ?- sat(a).
 3173% ?- sat(a->(b->a)), sat(a->(b->a)),  sat_count(C).
 3174% ?- sat(A->(B->A)), sat(A->(B->A)),  sat_count(C).
 3175% ?- sat(a), sat(b), sat_count(C).
 3176% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C).
 3177% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K).
 3178% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C).
 3179% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C).
 3180% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C).
 3181% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C).
 3182
 3183sat_count(C):- sat_fetch(S),
 3184	get_key(root, X, S),
 3185	ltr_card(X, C, S).
 3186
 3187% ?- sat(a), b_getval(sat_state, S), write(S),
 3188% get_key(root, R, S),
 3189% psa(R, S), get_key(atom_index, A, S), ltr_card(R, C, S).
 3190sat_count(F, C):-sat(F), sat_count(C).
 3191
 3192%
 3193print_root :- sat_fetch(S),
 3194	 get_key(root, R, S),
 3195	 psa(R, S).
 3196%
 3197sat_clear:- sat_fetch(S),
 3198			close_state(S),
 3199			b_setval(sat_state, []).
 3200
 3201% ?- time(forall(valid_formula(A), prove(A))).
 3202% ?- time(forall(invalid_formula(A), prove(A))).
 3203
 3204% ?- heavy_valid_formula(H), prove(H). % Take time. Should be wrapped
 3205%	with call_with_time_limit/1.
 3206
 3207heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10)
 3208<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3)
 3209<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10)
 3210<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3)
 3211<=> p2) <=> p1) <=> p0)).
 3212
 3213% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y).
 3214% ?- mk_left_assoc_term(=, 1, X), prove(X).
 3215
 3216% ?- ltr_zdd X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z).
 3217% ?- run(1, 100).
 3218% ?- run(2, 100).
 3219% ?- run(5, 100).
 3220% ?- run(1-9, 100).
 3221% ?- run(11, 100).
 3222%@
 3223%@ Propositions: p(0) ... p(11).
 3224%@ % 447,630,303 inferences, 47.959 CPU in 49.907 seconds (96% CPU, 9333572 Lips)
 3225%@ true.
 3226% ?- run(12, 360).
 3227%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips)
 3228% imac
 3229% on M1 mbp pro 32 GB, timeout.
 3230
 3231% ?- mk_left_assoc_term(==, 1, F), prove(F).
 3232
 3233
 3234run(N0-N, T_limit) :-!,  forall( between(N0, N, K),
 3235		( mk_left_assoc_term(==, K, F),
 3236		format("~nPropositions: p(0) ... p(~w).~n", [K]),
 3237		call_with_time_limit(T_limit, time(prove(F))))).
 3238% run(N0-N, T_limit) :-!,  forall( between(N0, N, K),
 3239% 		( mk_left_assoc_term(==, K, F),
 3240% 		format("~nPropositions: p(0) ... p(~w).~n", [K]),
 3241% 		call_with_time_limit(T_limit, time(seq:seq_prove(F))))).
 3242
 3243%
 3244run(N, T) :- run(N-N, T).
 3245
 3246% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X).
 3247% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X).
 3248
 3249mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L),
 3250			  append(L, L, L2),
 3251			  reverse(L2, R),
 3252			  apply_left_assoc(Bop, R, Ex).
 3253%
 3254apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex).
 3255%
 3256apply_left_assoc(_, X, [], X):-!.
 3257apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X],
 3258	apply_left_assoc(Bop, V, Y, W).
 3259
 3260demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law
 3261
 3262demorgan1( ((a * b) -> -((-a + -b)))).
 3263demorgan2(-((-a + -b)) -> (a * b)).
 3264
 3265% ?- forall(valid_formula(A), prove(A)).
 3266% Valid formulae.
 3267valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)).
 3268valid_formula((-(-a) -> a) * (a -> -(-a))).		% Double Negation
 3269valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law
 3270valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b).
 3271valid_formula(a + -a).
 3272valid_formula(((a -> b) -> a) -> a).  % Peirce’s Law
 3273valid_formula(-(-a)->a).
 3274valid_formula(a -> a).
 3275valid_formula(a -> (b -> a)).
 3276valid_formula((a->b)->((b->c)->(a->c))).
 3277valid_formula(a->((a->b)->b)).
 3278valid_formula((a*(a->b))->b).
 3279valid_formula((a->b)->(-b -> -a)).
 3280valid_formula((a->b)->((b->c)->(a->c))).
 3281valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)).
 3282
 3283% ?- forall(invalid_formula(A), prove(A)).
 3284invalid_formula(a).
 3285invalid_formula((a->b)->a).
 3286invalid_formula((a->b)->(b->a)).
 3287invalid_formula(a -> (b -> c)).
 3288invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)).
 3289invalid_formula( -((-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f))).
 prove(X) is det
True if negation of X is refutable
 3294% ?- prove(a).
 3295% ?- prove(a*b->a).
 3296% ?- prove(a*a->a).
 3297% ?- prove((-a) + a).
 3298% ?- prove((-A) + A).
 3299% ?- prove(A -> (p(B)->A)).
 3300% ?- prove(-(a->a)).
 3301% ?- prove(a->a).
 3302% ?- prove((a->b)->(b->a)).
 3303% ?- prove((a->b)->(a->b)).
 3304% ?- prove((a->b)->(a)).
 3305% ?- prove(a->(b->a)).
 3306% ?- prove((-(a) * a)).
 3307% ?- prove(-(-(a) * a)).
 3308% ?- prove(a+ (-a)).
 3309% ?- prove((-true)*true).
 3310% ?- prove(true*true).
 3311% ?- prove(true*false).
 3312% ?- prove(false*true).
 3313% ?- prove(false*false).
 3314% ?- prove(true+true).
 3315% ?- prove(true+false).
 3316% ?- prove(false+true).
 3317% ?- prove(false+false).
 3318% ?- prove((a->b)*(b->c) -> (a->c)).
 3319% ?- prove((a->b) -> ((b->c) -> (a->c))).
 3320
 3321prove(X):-
 3322	ltr_open_state(S),
 3323	(	prove(X, S)
 3324	->	writeln('VALID')
 3325	;	writeln('INVALID')
 3326	),
 3327	close_state(S).
 3328%
 3329prove(X, S):- cnf(-X, CNF, S),
 3330	get_key(atom_index, N, S),
 3331	(	CNF = 0 ->  N = 0
 3332	;	CNF = 1 ->  N > 0
 3333	;  	resolve(CNF, S)
 3334	).
 resolve(+P, +S) is det
P is a set of ground complementary-free clauses. True if refutation by resolution prinficple for P is successful.
 3340% ?- ltr_open_state(S), ltr_pow([a,b,c], P, S), resolve(P, S), psa(P, S).
 3341% ?- open_state(S), numlist(1, 10, L), ltr_pow(L, P, S), card(P, C, S).
 3342% ?- open_state(S), numlist(1, 100, L), ltr_pow(L, P, S), card(P, C, S).
 3343% ?- N = 100000, time((ltr_open_state(S), numlist(1, N, L), ltr_pow(L, P, S),
 3344%	resolve(P, S))).
 3345
 3346resolve(X, S):- zdd_has_1(X, S), !.		% The empty clause found.
 3347resolve(X, S):- X > 1,
 3348	cofact(X, t(A, L, R), S),
 3349	(	L = 0	-> fail					% Pure literal rule.
 3350	; 	A = -(_) -> resolve(L, S)		% Negative pure literal rule.
 3351	;	(	cofact(L, t(B, U, V), S),	% Pure literal rule.
 3352			(	B = -(A)
 3353			->  ltr_merge(V, R, M, S),  % Resolution + Tautology rule.
 3354				ltr_join(U, M, W, S),
 3355				resolve(W, S)			% Updated set of clauses.
 3356			;	resolve(L, S)			% Posituve pure literal rule.
 3357			)
 3358		)
 3359	).
 3360
 3361% ?- N=100,  numlist(0, N, Ns), sat(*Ns),  sat_count(C).
 3362% ?- N = 100, (zdd {numlist(1, N, L)}, ltr_pow(L, P),
 3363%	A << set(L), zdd_subtr(P, A, Q), card(Q, C),
 3364%	{writeln(C)}, resolve(Q)).   % false
 3365
 3366% ?- N = 40, time((open_state(S), numlist(1, N, L), ltr_pow(L, P, S),
 3367%	zdd_eval(set(L), A, S), zdd_subtr(P, A, Q, S), card(Q, C, S),
 3368%	writeln(C), resolve(Q, S))).  % false
 3369% ?- N = 100000, time((ltr_open_state(S), numlist(1, N, _L), ltr_pow(_L, P, S),
 3370%	card(P, _C, S))), _C=:= 2^N.
 3371
 3372atom_index(X, S):- memo(atom_index(X)-Y, S),
 3373	(	nonvar(Y) -> true
 3374	;	get_key(atom_index, Y, S),
 3375		memo(index_atom(Y)-X, S),
 3376		Y0 is Y + 1,
 3377		set_key(atom_index, Y0, S)
 3378	).
 3379
 3380
 3381% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_zdd nnf_cnf(Y, Z), psa(Z)).
 3382
 3383boole_nnf(X, Y):- % numbervars_index(X, S),
 3384	basic_boole(X, Z),
 3385	once(neg_normal(Z, Y)).
 3386
 3387% ?- basic_boole(a, A).
 3388% ?- basic_boole(@(a), A).
 3389% ?- basic_boole(0, A).
 3390% ?- basic_boole(1, A).
 3391% ?- basic_boole(true, A).
 3392% ?- basic_boole(a+b, A).
 3393% ?- basic_boole(a+b+c, A).
 3394% ?- basic_boole(-a + b + c, A).
 3395% ?- basic_boole(a -> b -> c, A).
 3396% ?- basic_boole((a -> b) -> c, A).
 3397% ?- basic_boole(*[(a -> b), c], A).
 3398% ?- basic_boole(*[(0 -> 1)->2], A).
 3399
 3400basic_boole(A, BoolConst):-atomic(A),
 3401	boole_op(0, [], Fs, BoolConst),
 3402	memberchk(A, Fs),
 3403	!.
 3404basic_boole(I, @(I)):- integer(I), !.
 3405basic_boole(@(I), @(I)):-!.
 3406basic_boole(*(L), F):-!, basic_boole_vector(L, *, F).
 3407basic_boole(+(L), F):-!, basic_boole_vector(L, +, F).
 3408basic_boole(X, Y):- X=..[F|Xs],
 3409	length(Xs, N),
 3410	boole_op(N, As, Fs, Y),
 3411	memberchk(F, Fs),
 3412	!,
 3413	basic_boole_list(Xs, As).
 3414basic_boole(X, @(X)).
 3415
 3416%
 3417basic_boole_list([], []).
 3418basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y),
 3419	basic_boole_list(Xs, Ys).
 3420%
 3421basic_boole_vector([], +, false):-!.
 3422basic_boole_vector([], *, true):-!.
 3423basic_boole_vector([X|Xs], F, Y):-
 3424	basic_boole(X, X0),
 3425	Y=..[F, X0, Z],
 3426	basic_boole_vector(Xs, F, Z).
 3427
 3428% Remark [2023/11/13]:
 3429%	Use of 0/1 as Boolean constants has been dropped.
 3430%	Any integer is now usable for a boolean variable, which
 3431%	may be useful or (nested) vectors of integers *[...],  +[...].
 3432%	0/1 as boolean is error prone because ZDD must use 0/1 internally
 3433%	as basic constant similar, but not exactly the same,
 3434%	to true/flase. They are different.
 3435%	This decision was hard because 0/1 is traditionally useful
 3436%	as  boolean constrants, but clear separation and simplicity
 3437%	were preferred.
 3438
 3439boole_op(0, [], [false, ff], false).	% 0 for false dropped.
 3440boole_op(0, [], [true, tt], true).		% 1 for true  dropped.
 3441boole_op(1, [X], [-, ~, \+, not], -(X)).
 3442boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y).
 3443boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y).
 3444boole_op(2, [X, Y], [->, imply], -X + Y).
 3445boole_op(2, [X, Y], [<-], Y->X).
 3446boole_op(2, [X, Y], [iff, ==, =,  =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y).
 3447boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)).  % -(X==Y) = xor(X, Y)
 3448boole_op(2, [X, Y], [nand], -(X) + (-Y)).
 3449
 3450
 3451% ?- neg_normal(-(true + b), X).
 3452% ?- neg_normal(-(a), X).
 3453% ?- neg_normal(-(a), X).
 3454% ?- neg_normal(-(a), X).
 3455neg_normal(true, true).
 3456neg_normal(false, false).
 3457neg_normal(-(false), true).
 3458neg_normal(-(true), false).
 3459neg_normal(-(-X), Z)	:- neg_normal(X, Z).
 3460neg_normal(-(X+Y), Z)	:- neg_normal(-X* -Y, Z).
 3461neg_normal(-(X*Y), Z)	:- neg_normal(-X+ -Y, Z).
 3462neg_normal(-(X), -(Y))	:- neg_normal(X, Y).
 3463neg_normal(X+Y, X0+Y0)	:- neg_normal(X, X0),
 3464						   neg_normal(Y, Y0).
 3465neg_normal(X*Y, X0*Y0)	:- neg_normal(X, X0),
 3466						   neg_normal(Y, Y0).
 3467neg_normal(@(X), @(X)):-!.
 3468neg_normal(X, @(X)):-!.
 3469
 3470% ?- zdd((intern(-(a;b;c), X), boole_to_dnf(X, Z),  sets(Z, U), extern(U, Y))).
 3471%%	extern(+X, -Y) is det.
 3472% Convert an internal form X into an external one
 3473% in order to unify Y with the result.
 3474
 3475extern(X, Y):-shift(extern(X, Y)).
 3476%
 3477extern(X, Y, S):-integer(X), !,
 3478	(	X < 2  -> Y = X
 3479	;	memo(index_atom(X)-Y, S)
 3480	).
 3481extern(X, X, _):- atomic(X), !.
 3482extern(X, Y, S):- X =.. [F|Xs],
 3483	extern_list(Xs, Ys, S),
 3484	Y =..[F|Ys].
 3485%
 3486extern_list([], [], _).
 3487extern_list([X|Xs], [Y|Ys], S):- extern(X, Y, S),
 3488	extern_list(Xs, Ys, S).
 3489
 3490		/*********************************************
 3491		*    Cofact/insert/join/merge on literals    *
 3492		*********************************************/
 ltr_cofact(?X, ?Y:t(A,L,R), +S) is det
Bidirectional. If X is given then Y is a triple t(A, L, R) such that A is the minimum literal in X w.r.t. specified literal compare predicate, L = { U in X | not ( A in U ) }, R = { V \ {A} | V in X, A in V }. If Y is given then X = union of L and A*R = { unionf of U and {A} | U in R }. Due to ltr_cofact/3 and itr_insert/4, it is guaranteed that every clause is complentary-free ( no complementary pair ).
 3507ltr_cofact(Z, Y, S):- nonvar(Z), !, cofact(Z, Y, S).
 3508ltr_cofact(Z, t(A, V, U), S):- U > 1, !,
 3509	cofact(U, t(B, L, _), S),
 3510	(	ltr_invert(A, B)
 3511	->  ltr_cofact(Z, t(A, V, L), S)
 3512	;	cofact(Z, t(A, V, U), S)
 3513	).
 3514ltr_cofact(Z, T, S):- cofact(Z, T, S).
 ltr_insert(+X, +Y, -Z, +S) is det
Insert a literal X into each set of literals in Y, and the result is unified with Z. Z = { union of U and {X} | U in Y, and the complement of X is not in U }.
 3523% PASS.
 3524% ?- ltr_zdd cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S).
 3525% ?- ltr_zdd dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S).
 3526% ?- ltr_zdd ltr_insert(a, 1, X), sets(X, S).
 3527% ?- ltr_zdd ltr_insert(a, 1, X),	ltr_insert(b, X, Y), sets(Y, S).
 3528% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y),
 3529%	ltr_insert(-b, Y, Z), sets(Z, S).
 3530% ?- ltr_zdd X<<set([a]), ltr_insert(b, X, Y), psa(Y).
 3531% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y).
 3532% ?- ltr_zdd X<<set([b]), ltr_insert(a, X, Y), psa(Y).
 3533% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y).
 3534% ?- ltr_zdd X<<set([-a]), ltr_insert(a, X, Y), psa(Y))).
 3535% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y).
 3536% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y).
 3537% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y).
 3538% ?- ltr_zdd X<<{[a]}, ltr_insert(a, X, Y), psa(Y).
 3539% ?- ltr_zdd X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y).
 3540% ?- ltr_zdd X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y).
 3541% ?- ltr_zdd X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y).
 3542% ?- ltr_zdd X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y).
 3543% ?- ltr_zdd X<< dnf(a), ltr_insert(b, X, Y), psa(Y).
 3544% ?- ltr_zdd X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y).
 3545% ?- ltr_zdd X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y).
 3546% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X).
 3547% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X).
 3548% ?- sat((x=\=y)*x*y).  % false
 3549% ?- sat((a * -a)).		% false
 3550% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y).
 3551
 3552% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y).
 3553% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y).
 3554% ?- ltr_zdd dnf((-a)*b, X), psa(X).
 3555% ?- ltr_zdd cnf((-a)*b, X).
 3556% ?- ltr_zdd cnf((a), X).
 3557% ?- spy(cnf).
 3558% ?- spy(atom_index).
 3559%
 3560ltr_insert(_, 0, 0, _):-!.
 3561ltr_insert(A, 1, J, S):-!, zdd_singleton(A, J, S).
 3562ltr_insert(A, I, J, S):- memo(ltr_insert(A,I)-J, S),
 3563	(	nonvar(J)	-> true
 3564	;	cofact(I, t(B, L, R), S),
 3565		zdd_compare(C, A, B, S),
 3566		(	C = (<) ->
 3567			(	complementary(A, B) ->
 3568				cofact(J, t(A, 0, L), S)
 3569			;	cofact(J, t(A, 0, I), S)
 3570			)
 3571		; 	C = (=) ->
 3572			(	negative(A) ->
 3573				ltr_join(L, R, K, S),
 3574				cofact(J, t(A, 0, K), S)
 3575			;	ltr_insert_aux(J, A, L, R, S)
 3576			)
 3577		;	(	complementary(A, B) -> ltr_insert(A, L, J, S)
 3578			;	ltr_insert(A, L, L0, S),
 3579				ltr_insert(A, R, R0, S),
 3580				cofact(J, t(B, L0, R0), S)
 3581			)
 3582		)
 3583	).
 3584
 3585% for suppressing use of cofact/3 and ltr_insert/4
 3586ltr_insert_aux(J, A, L, R, S):-  % A is positive. R has no -A.
 3587	(	L < 2 -> cofact(J, t(A, L, R), S)
 3588	;	cofact(L, t(B, L0, _), S),
 3589		(	complementary(A, B)->
 3590			ltr_join(L0, R, K, S),
 3591			cofact(J, t(A, 0, K), S)
 3592		;	ltr_join(L, R, K, S),
 3593			cofact(J, t(A, 0, K), S)
 3594		)
 3595	).
 ltr_join(+X, +Y, -Z, +S) is det
Unify Z with a ZDD that represents the union of the ZDD X and Y as a family of sets (ltr_invert_free clauses) of literals.
 3601%
 3602ltr_join(X, X, X, _):-!.	% idemopotent law of logical disjunction (OR)
 3603ltr_join(0, X, X, _):-!.
 3604ltr_join(X, 0, X, _):-!.
 3605ltr_join(1, _, 1, _):-!.
 3606ltr_join(_, 1, 1, _):-!.
 3607ltr_join(X, Y, Z, S):-
 3608	(	X=<Y -> memo(ltr_join(X,Y)-Z, S)
 3609	;	memo(ltr_join(Y,X)-Z, S)
 3610	),
 3611	(	nonvar(Z) -> true %, write(.)
 3612	; 	cofact(X, t(A, L, R), S),
 3613		cofact(Y, t(A0, L0, R0), S),
 3614		zdd_compare(C, A, A0, S),
 3615		(	C = (=)	->
 3616			ltr_join(R, R0, U, S),
 3617			ltr_join(L, L0, V, S),
 3618			cofact(Z, t(A, V, U), S)
 3619		;	C = (<) ->
 3620			ltr_join(L, Y, U, S),
 3621			cofact(Z, t(A, U, R), S)
 3622		; 	ltr_join(L0, X, U, S),
 3623			cofact(Z, t(A0, U, R0), S)
 3624		)
 3625	).
 ltr_merge(+X, +Y, -Z, +S) is det
Z = { U | A in X, B in Y, U is the union of A and B, U is ltr_invert-free }.
 3633ltr_merge(X, X, X, _):-!.   % idempotent law of logical conjunction (AND).
 3634ltr_merge(0, _, 0, _):-!.
 3635ltr_merge(_, 0, 0, _):-!.
 3636ltr_merge(1, X, X, _):-!.
 3637ltr_merge(X, 1, X, _):-!.
 3638ltr_merge(X, Y, Z, S):-
 3639	(	X =< Y -> memo(ltr_merge(X,Y)-Z, S)
 3640	;	memo(ltr_merge(Y,X)-Z, S)
 3641	),
 3642 	(	nonvar(Z) -> true
 3643	;	cofact(Y, t(A, L, R), S),
 3644		ltr_merge(X, R, U, S),
 3645		ltr_merge(X, L, V, S),
 3646		ltr_insert(A, U, U0, S),
 3647		ltr_join(V, U0, Z, S)
 3648	).
 3649
 3650		/******************************************
 3651		*     Auxiliary operations on literals    *
 3652		******************************************/
 complementay(+A, -B) is det
B is unfied with the complement of B.
 3656complementary(-(A), A):-!.
 3657complementary(A, -(A)).
 3658%
 3659negative(-(_)).
 ltr_pow(+As, -P, +S) is det
As is a list of atoms. P is unified with the set of all complementary-free clauses C such that every B in C is complementary with some A in As, and for all A in As A is complementary with some B in C.
 3668% ?- ltr_zdd ltr_pow([a], X), card(X, C), psa(X).
 3669% ?- ltr_zdd ltr_pow([a, b], X), card(X, C), psa(X).
 3670% ?- ltr_zdd {numlist(1, 100, L)}, ltr_pow(L, X), card(X, C).
 3671ltr_pow([], 1, _).
 3672ltr_pow([A|As], P, S):- ltr_pow(As, Q, S),
 3673	ltr_insert(A, Q, R, S),
 3674	ltr_insert(-A, Q, L, S),
 3675	ltr_join(L, R, P, S).
 ltr_append(+X, +Y, -Z, +S) is det
X is a list of atoms and zdd Y is a family of cluases. Z is unified with zdd { U | U is union of X and V in Y such that U is complementary-free }.
 3683% ?- ltr_zdd ltr_append([-b, a, -d, c], 1, X), psa(X).
 3684% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X).
 3685% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X).
 3686% ?- ltr_zdd X<<dnf(a->a), ltr_card(X, C),  psa(X).
 3687ltr_append(X, Y, Z):- shift(ltr_append(X, Y, Z)).
 3688%
 3689ltr_append([], X, X, _).
 3690ltr_append([A|As], X, Y, S):- ltr_append(As, X, X0, S),
 3691	 	ltr_insert(A, X0, Y, S).
 ltr_set(+X, -Y, S) is det
Euivalent to ltr_append(X, 1, Y, S). ?- ltr_zdd X<<(ltr_set([a])+ltr_set([b])), psa(X))). ?- ltr_zdd X<<(ltr_set([-a])+ltr_set([b])), psa(X))). ?- ltr_zdd X<<(ltr_set([-a])+ltr_set([a])), psa(X))).
 3699ltr_set(X, Y):- shift(ltr_set(X, Y)).
 3700%
 3701ltr_set(X, Y, S):- ltr_append(X, 1, Y, S).
 ltr_negate(+X, -Y, +S) is det
X is a zdd of a family of clauses. Y is unified with the zdd which is the choice of the complement of X.
 3708% ?- zdd((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))).
 3709% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))).
 3710% ?- zdd((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))).
 3711% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))).
 3712% ?- zdd((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))).
 3713
 3714% ?- ltr_zdd X<<dnf(a), ltr_negate(X, Y), psa(Y).
 3715% ?- ltr_zdd ltr_negate(0, Y), psa(Y).
 3716% ?- ltr_zdd ltr_negate(1, Y), psa(Y).
 3717
 3718ltr_negate(X, Y):- shift(ltr_negate(X, Y)).
 3719%
 3720ltr_negate(X, Y, S):- ltr_complement(X, X0, S),
 3721		ltr_choices(X0, Y, S).
 ltr_complement(+X, -Y, +S) is det
X is a zdd for a family of clauses. Y is unified with a zdd of clauses C such that for some D in X, if literal A in C then the complement of A is in D, and if literal A in D then the complement of A is in C.
 3730% ?- zdd  X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y).
 3731% ?- zdd  X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y).
 3732%
 3733ltr_complement(X, X, _):- X<2, !.
 3734ltr_complement(I, Y, S):- memo(ltr_complement(I)-Y, S),
 3735	(	nonvar(Y) -> true
 3736	; 	cofact(I, t(A, L, R), S),
 3737		ltr_complement(L, L0, S),
 3738		ltr_complement(R, R0, S),
 3739		complementary(A, NA),
 3740		ltr_insert(NA, R0, R1, S),
 3741		ltr_join(L0, R1, Y, S)
 3742	).
 3743
 3744		/************************************
 3745		*  Convert Boolean Form to DNF/CNF  *
 3746		************************************/
 dnf(+X, -Y, +S) is det
Y is a disjuntive normal form of a boolean formula X.
 3751% ?- boole_nnf(-(a+b), X).
 3752% ?- zdd dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V).
 3753% ?- zdd((dnf(-(a=:=b), X), psa(X))).
 3754% ?- zdd((dnf((a=\=b), X), psa(X))).
 3755% ?- zdd((dnf((0), X), psa(X))).
 3756% ?- zdd((dnf(*[1,3,2,3], X), psa(X))).
 3757% ?- zdd dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I).
 3758% ?- zdd((dnf(*[@(1),3,2,3], X), psa(X))).
 3759
 3760dnf(X, Y, S):- zdd_numbervars(X, S),
 3761	boole_nnf(X, Z),
 3762	nnf_dnf(Z, Y, S).
 dnf_cnf(?DNF, ?CNF, +S) is det
 cnf_dnf(?DNF, ?CNF, +S) is det
Bidirectional. DNF is converted to an equivalent CNF, and vice versa. REMARK: DNF 0 means false. DNF 1 means true CNF 0 means true. CNF 1 means false
 3771% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y).
 3772% ?- ltr_zdd X<<dnf(a+b),  dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U).
 3773% ?- ltr_zdd big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D).
 3774
 3775dnf_cnf(X, Y, S):- nonvar(X), !, ltr_choices(X, Y, S).
 3776dnf_cnf(X, Y, S):- ltr_choices(Y, X, S).
 3777%
 3778cnf_dnf(X, Y, S):- dnf_cnf(X, Y, S).
 3779
 3780% ?- ltr_zdd X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y).
 3781%@  * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug
 3782% ?- ltr_zdd X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y).
 3783% ?- ltr_zdd X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y).
 3784% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y).
 3785% ?- ltr_zdd X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y).
 3786% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y).
 3787% ?- ltr_zdd X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y).
 3788% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y),
 3789%	dnf_cnf(Z, Y), psa(X), psa(Y).
 3790
 3791% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y),
 3792%	dnf_cnf(Z, Y), psa(X), psa(Y).
 3793
 3794% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y),
 3795%	dnf_cnf(Z, Y).
 3796
 3797% ?- ltr_zdd X<<dnf(a+b),  dnf_cnf(X, Y), dnf_cnf(Z, Y),
 3798%	dnf_cnf(Z, U).
 3799
 3800% ?- N=100,  time((ltr_zdd big_normal_form(N, X),
 3801%	dnf_cnf(Y, X),  card(X, C), card(Y, D))).
 3802%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips)
 3803%@ N = 100,
 3804%@ X = 39901,
 3805%@ Y = D, D = 0,   %  <==  CORRECT.
 3806%@ C = 1267650600228229401496703205376 .
 3807
 3808% ?- N=1000,  time((ltr_zdd big_normal_form(N, X),
 3809%	dnf_cnf(Y, X),  card(X, C), card(Y, D))).
 3810%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips)
 3811%@ N = 1000,
 3812%@ X = 3999001,
 3813%@ Y = D, D = 0,  % <== CORRECT.
 3814%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
 ltr_choices(+InNF, -OutNF, +S) is det
OutNF is unified with a set of clauses which is logically equivlalent to OutNF. If InNF is read as DNF, then OutNF must be read as CNF, an if InNF is read as CNF, then OutNF must be read as DNF.
REMARK: DNF 0 means false. DNF 1 means true CNF 0 means true. CNF 1 means false which is logically sound reading. REMARK: ltr_choices reflects a well-known duality law % on disjunction and conjunction.
 3828ltr_choices(0, 1, _):-!.
 3829ltr_choices(1, 0, _):-!.
 3830ltr_choices(X, Y, S):- memo(ltr_choices(X)-Y, S),
 3831	(	nonvar(Y)->true	%, write(.)  % many hits.
 3832	;	cofact(X, t(A, L, R), S),
 3833		ltr_choices(L, L0, S),
 3834		ltr_choices(R, R0, S),
 3835		cofact(R1, t(A, R0, 1), S),
 3836		ltr_merge(L0, R1, Y, S)
 3837	).
 nnf_dnf(+E, -Z, +S) is det
Z is unified with a dnf for nnf (Negation Normal Form) E.
 3842nnf_dnf(false * _, 0, _):-!.
 3843nnf_dnf(_ * false, 0, _):-!.
 3844nnf_dnf(true * X, Y, S):-!, nnf_dnf(X, Y, S).
 3845nnf_dnf(X * true, Y, S):-!, nnf_dnf(X, Y, S).
 3846nnf_dnf(X * Y, Z, S):-!, memo(dnf(X*Y)-Z, S),
 3847	(	nonvar(Z) -> true
 3848	;	nnf_dnf(X, U, S),
 3849		nnf_dnf(Y, V, S),
 3850		ltr_merge(U, V, Z, S)
 3851	).
 3852nnf_dnf(false + X, Y, S):-!, nnf_dnf(X, Y, S).
 3853nnf_dnf(X + false, Y, S):-!, nnf_dnf(X, Y, S).
 3854nnf_dnf(true + X, Y, S):-!, nnf_dnf(X, Z, S),
 3855	ltr_join(1, Z, Y, S).
 3856nnf_dnf(X + true, Y, S):-!, nnf_dnf(X, Z, S),
 3857	ltr_join(1, Z, Y, S).
 3858nnf_dnf(X + Y, Z, S):-!, memo(dnf(X+Y)-Z, S),
 3859	(	nonvar(Z) -> true
 3860	; 	nnf_dnf(X, U, S),
 3861		nnf_dnf(Y, V, S),
 3862		ltr_join(U, V, Z, S)
 3863	).
 3864nnf_dnf(@(X), I, S):-!, atom_index(X, S),
 3865	zdd_singleton(X, I, S).
 3866nnf_dnf(-(@(X)), I, S):- atom_index(X, S),
 3867	zdd_singleton(-(X), I, S).
 cnf(+X, -Y, +S) is det
Y is unified with a conjuntive normal form of a boolean nnf X.
 3873% ?- zdd((cnf(a, X), S<<sets(X))).
 3874% ?- ltr_zdd((cnf(a*b, X), S<<sets(X))).
 3875% ?- zdd((X<<cnf(-a), Y<<sets(X))).
 3876% ?- zdd((X<<cnf(a+b), Y<<sets(X))).
 3877% ?- zdd((X<<cnf(+([a,b,c])), Y<<sets(X))).
 3878% ?- zdd((X<<cnf(*([a,b,c])), Y<<sets(X))).
 3879% ?- zdd((X<<dnf(+([a,b,c])), Y<<sets(X))).
 3880% ?- zdd((X<<dnf(*([a,b,c])), Y<<sets(X))).
 3881% ?- zdd((cnf(a, X), psa(X))).
 3882% ?- zdd((cnf(-a, X), psa(X))).
 3883% ?- zdd((cnf(a+b, X), psa(X))).
 3884% ?- zdd((cnf(a+b+(-c), X), psa(X))).
 3885% ?- zdd((cnf(-a * a,  X), psa(X))).
 3886% ?- zdd((cnf(a->a,  X), psa(X))).
 3887% ?- zdd((cnf(-a * a,  X), psa(X))).
 3888% ?- zdd((cnf( a + a,  X), psa(X))).
 3889% ?- zdd((cnf( A + A,  X), psa(X))).
 3890% ?- zdd((cnf(-(a*b), X), psa(X))).
 3891% ?- zdd((cnf(*([a,b,c]), X), psa(X))).
 3892% ?- zdd {N = 10, numlist(2, N, Ns)}, cnf(*(Ns), X), ltr_card(X, C, K).
 3893% ?- ltr_zdd((dnf(a, X), psa(X))).
 3894% ?- ltr_zdd((cnf(-(a->b), X), psa(X))).
 3895% ?- ltr_zdd((cnf(a, X), psa(X))).
 3896% ?- boole_nnf(-(*[0,1,2]), X).
 3897% ?- ltr_zdd {mk_left_assoc_term(==, 1, F)}, cnf(F, X), psa(X).
 3898cnf(X, Y, S):- zdd_numbervars(X, S),
 3899	 boole_nnf(X, Z),
 3900	 nnf_cnf(Z, Y, S).
 3901%
 3902nnf_cnf(true, 1, _):-!.
 3903nnf_cnf(false, 0, _):-!.
 3904nnf_cnf(false * _, 0, _):-!.
 3905nnf_cnf(_ * false, 0, _):-!.
 3906nnf_cnf(true * X, Y, S):-!, nnf_cnf(X, Y, S).
 3907nnf_cnf(X * true, Y, S):-!, nnf_cnf(X, Y, S).
 3908nnf_cnf(X * X, Y, S):-!, nnf_cnf(X, Y, S).
 3909nnf_cnf(X * Y, Z, S):-!, memo(cnf(X*Y)-Z, S),
 3910	(	nonvar(Z)->true	%, write(.)   % many hits.
 3911	;	nnf_cnf(X, U, S),
 3912		nnf_cnf(Y, V, S),
 3913		ltr_join(U, V, Z, S)
 3914	).
 3915nnf_cnf(false + X, Y, S):-!, nnf_cnf(X, Y, S).
 3916nnf_cnf(X + false, Y, S):-!, nnf_cnf(X, Y, S).
 3917nnf_cnf(true + _, 1, _):-!.
 3918nnf_cnf(_ + true, 1, _):-!.
 3919nnf_cnf(X + X, Y, S):-!, nnf_cnf(X, Y, S).
 3920nnf_cnf(X + Y, Z, S):-!, memo(cnf(X+Y)-Z, S),
 3921	(	nonvar(Z)->true	%, write(+)  % many hits.
 3922	;	nnf_cnf(X, U, S),
 3923		nnf_cnf(Y, V, S),
 3924		ltr_merge(U, V, Z, S)
 3925	).
 3926nnf_cnf(@(X), I, S):-!, atom_index(X, S),
 3927	zdd_singleton(X, I, S).
 3928nnf_cnf(-(@(X)), I, S):- atom_index(X, S),
 3929	zdd_singleton(-(X), I, S).
 3930
 3931
 3932		/*****************************************************
 3933		*     ltr_card/[3,4] Counting solutions of a DNF.    *
 3934		*****************************************************/
 3935
 3936
 3937% ?- sat_count_by_collect_atoms(a, C).
 3938% ?- sat_count_by_collect_atoms(a+b, C).
 3939% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C).
 3940% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C).
 3941sat_count_by_collect_atoms(X, C):- sat_fetch(S),
 3942	dnf(X, Y, S),
 3943	sat_count_by_collect_atoms(Y, C, S),
 3944	sat_close.
 3945%
 3946sat_count_by_collect_atoms(X, C, S):-
 3947	zdd_boole_atoms(Us, S),
 3948	zdd_sort(Us, Vs, S),
 3949	expand_dnf(Vs, X, Y, S),
 3950	card(Y, C, S).
 3951
 3952% ?- ltr_zdd X<<dnf(b+a), zdd_boole_atoms(Us).
 3953zdd_boole_atoms(Us, S):-
 3954	(	get_key(atom_index, N, S) ->
 3955		collect_boole_atoms(0, N, Us, S)
 3956	;	Us = []
 3957	).
 3958
 3959%
 3960collect_boole_atoms(I, N, [], _):- I>=N, !.
 3961collect_boole_atoms(I, N, [A|U], S):- memo(index_atom(I)-A, S),
 3962	J is I+1,
 3963	collect_boole_atoms(J, N, U, S).
 3964
 3965		/******************************
 3966		*     find_counter_example    *
 3967		******************************/
 findall_counter_examples(+In, -Out, +S) is det
(Experimental.)
 3971% ?- findall_counter_examples(a, X, S), psa(X, S).
 3972% ?- findall_counter_examples((a->b)->a, X, S), psa(X, S).
 3973% ?- findall_counter_examples((a->b)->(b->a), X, S), psa(X, S).
 3974% ?- findall_counter_examples(a->b, X, S), psa(X, S).
 3975% ?- findall_counter_examples((a->b)->(b->a), X, S), psa(X, S).
 3976% ?- findall_counter_examples(a->b, Out, S), psa(Out,S).
 3977findall_counter_examples(In, Out, S):-
 3978	ltr_open_state(S),
 3979	dnf(In, InZ, S),
 3980	zdd_boole_atoms(Us, S),
 3981	zdd_sort(Us, Vs, S),
 3982	expand_prefix_dnf(Vs, 1, All, S),
 3983	expand_dnf(Vs, InZ, Y, S),
 3984	zdd_subtr(All, Y, Out, S).
 ltr_open_state(-S) is det
open_state(S) and set ltr_compare/3 in S as the compare predicate.
 3989ltr_open_state(S):- open_state(S),
 3990					set_compare(ltr_compare, S),
 3991					set_key(varnum, 0, S),
 3992					set_key(atom_index,0, S).
 ltr_card(+X, -C, -N, S) is det
C is the number of solutions of boolean formula X. N is the number of boolean variable appearing in X.
 3998% ?- ltr_zdd X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C).
 3999% ?- ltr_zdd X<< dnf(a), psa(X), ltr_card(X, C).
 4000% ?- ltr_zdd X<< dnf(a->a), ltr_card(X, C).
 4001% ?- ltr_zdd X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C).
 4002% ?- ltr_zdd X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C).
 4003% ?- findall(p(J), between(1, 100, J), Ps),
 4004%	time(ltr_zdd((X<< dnf(+Ps), ltr_card(X, C)))).
 4005% ?- N = 1000, findall(p(J), between(1, N, J), Ps),
 4006%	time((ltr_zdd X<< dnf(+Ps),ltr_card(X, C))),
 4007%	C =:= 2^1000 - 1.
 4008
 4009ltr_card(In, Out, S):-
 4010	zdd_boole_atoms(Us, S),
 4011	zdd_sort(Us, Vs, S),
 4012	expand_dnf(Vs, In, Y, S),
 4013	card(Y, Out, S).
 4014
 4015% ?- ltr_var(-(5), X).
 4016ltr_var(-(V), V):-!.
 4017ltr_var(V, V).
 expand_dnf(+Vs, +X, -Y, +S) is det
With U the set of all atoms appearing in X, Y is the all maximal complemental-free clauses C over the union of Vs and U such that C is an extension of some clause in X.
 4024% ?- ltr_zdd((X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y))).
 4025% ?- ltr_zdd((X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), card(Y, C))).
 4026% ?- ltr_zdd((X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C))).
 4027% ?- ltr_zdd((X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y))).
 4028% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))).
 4029% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))).
 4030% ?- ltr_zdd((X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))).
 4031
 4032expand_dnf([], X, X, _):-!.
 4033expand_dnf(_, 0, 0, _):-!.
 4034expand_dnf(Vs, 1, Y, S):-!, expand_prefix_dnf(Vs, 1, Y, S).
 4035expand_dnf(Vs, X, Y, S):- memo(expand_dnf(X,Vs)-Y, S),
 4036	(	nonvar(Y) -> true	%, write(.) %  Many hits.
 4037	;	cofact(X, t(A, L, R), S),
 4038		ltr_var(A, K),
 4039		divide_ord_list(Vs, K, [], Us, Ws),
 4040		expand_dnf(Us, R, R0, S),
 4041		ltr_insert(A, R0, R1, S),
 4042		expand_left_dnf(K, Us, L, L0, S),
 4043		ltr_join(L0, R1, X0, S),
 4044		expand_prefix_dnf(Ws, X0, Y, S)
 4045	).
 divide_ord_list(+L, +A, +U, -T, -W) is det
Divide list L at A into two parts head H and tail T so that reverse of H = diffrence list W-U. ?- divide_ord_list([a,b,c,d,e], c, [u], T, W). ?- divide_ord_list([a,b,c, d], e, [], X, Y). % false
 4053divide_ord_list([V|Vs], V, Us, Vs, Us):-!.
 4054divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U),
 4055	divide_ord_list(Vs, U, [V|Us], Ws, Ps).
 expand_prefix_dnf(+Vs, +X, -Y, +S) is det
With U the set of all atoms appearing in X, Y is the all maximal complemental-free clauses C over the union of Vs and U such that C is consistent with all clauses in X.
 4062% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))).
 4063expand_prefix_dnf(Vs, X, Y, S):- zdd_sort(Vs, OrdVs, S),
 4064	expand_ord_prefix_dnf(OrdVs, X, Y, S).
 4065
 4066%
 4067expand_ord_prefix_dnf([], X, X, _):-!.
 4068expand_ord_prefix_dnf([V|Vs], X, Y, S):-
 4069	expand_ord_prefix_dnf(Vs, X, X0, S),
 4070	ltr_insert(V, X0, X1, S),
 4071	ltr_insert(-V, X0, X2, S),
 4072	ltr_join(X1, X2, Y, S).
 expand_left_dnf(+K, +Vs, +X, -Y, +S) is det
X is assumed to have no occurrence of positive literal K (negative on may appear). With U the set of all atoms appearing in X, Y is the all maximal complemental-free clauses C over the union of Vs and U such that C is an extension of some clause in X and has not the postive literal K.
 4082expand_left_dnf(_, _, 0, 0, _):-!.
 4083expand_left_dnf(K, Us, 1, Y, S):-!, expand_prefix_dnf([K|Us], 1, Y, S).
 4084expand_left_dnf(K, Us, X, Y, S):- cofact(X, t(A, L, R), S),
 4085	ltr_var(A, J),
 4086	(	K = J ->
 4087		expand_dnf(Us, R, R0, S),
 4088		ltr_insert(A, R0, R1, S)
 4089	;	divide_ord_list([K|Us], J, [], Vs, Ws),
 4090		expand_dnf(Vs, R, R0, S),
 4091		ltr_insert(A, R0, Q, S),
 4092		expand_prefix_dnf(Ws, Q, R1, S)
 4093	),
 4094	expand_dnf([K|Us], L, L0, S),
 4095	ltr_join(L0, R1, Y, S).
 4096
 4097		/*******************************
 4098		*     Filter on cardinality    *
 4099		*******************************/
 card_filter_gte(+N, +X, -Y, +S) is det
Y = { A in X | #A >= N }, where #A is the number of elements of A.
 4105% ?- zdd((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))).
 4106card_filter_gte(0, X, X, _):- !.	% gte: greater than or equal
 4107card_filter_gte(1, X, Y, S):- !, zdd_subtr(X, 1, Y, S).
 4108card_filter_gte(_, X, 0, _):- X<2, !.
 4109card_filter_gte(N, X, Y, S):- memo(filter_gte(N,X)-Y, S),
 4110	(	nonvar(Y) -> true		% many hits.
 4111	;   cofact(X, t(A, L, R), S),
 4112		N0 is N - 1,
 4113		card_filter_gte(N, L, L0, S),
 4114		card_filter_gte(N0, R, R0, S),
 4115		cofact(Y, t(A, L0, R0), S)
 4116	).
 card_filter_lte(+N, +X, -Y, +S) is det
Y = { A in X | #A =< N }, where #A is the cardinality of A.
 4122% ?- zdd((X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y))).
 4123card_filter_lte(0, X, Y, S):-    % lte: less than or equal
 4124	(	zdd_has_1(X, S) -> Y = 1
 4125	;	Y = 0
 4126	).
 4127card_filter_lte(_, X, X, _):- X<2, !.
 4128card_filter_lte(N, X, Y, S):- memo(filter_lte(N,X)-Y, S),
 4129	(	nonvar(Y) -> true		% many hits.
 4130	;    cofact(X, t(A, L, R), S),
 4131		N0 is N - 1,
 4132		card_filter_lte(N, L, L0, S),
 4133		card_filter_lte(N0, R, R0, S),
 4134		cofact(Y, t(A, L0, R0), S)
 4135	).
 card_filter_between(+I, +J, +X, -Y, +S) is det
Y = { A in X | I =< #A =< J }.
 4140% ?- time(( N = 100, numlist(1, N, Ns), zdd((X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))))).
 4141card_filter_between(I, J, X, Y, S):-
 4142	card_filter_gte(I, X, Z, S),
 4143	card_filter_lte(J, Z, Y, S).
 4144
 4145% ?- time(( N = 100, numlist(1, N, Ns), zdd((X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))))).
 4146card_filter_between_by_meet(I, J, X, Y, S):-
 4147	card_filter_gte(I, X, Z, S),
 4148	card_filter_lte(J, X, U, S),
 4149	zdd_meet(Z, U, Y, S).
 4150
 4151
 4152		/*********************************************************
 4153		*     Solve boolean equations and verify the solution    *
 4154		*********************************************************/
 4155% Recovered [2023/11/14]
 4156%!	dnf_subst(+V, +T, +X, -Y, +S) is det.
 4157%	Y is the ZDD obtained by substituting each
 4158%	occurrence of atom V in X with T.
 4159
 4160% ?-ltr_zdd X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y).
 4161% ?-ltr_zdd X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y).
 4162% ?-ltr_zdd X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y).
 4163
 4164dnf_subst(_, _, X, X, _):- X < 2, !.
 4165dnf_subst(V, D, X, Y, S):-
 4166	cofact(X, t(A, L, R), S),
 4167	dnf_subst(V, D, L, L0, S),
 4168	once( A = -(U); U = A ),
 4169	ltr_compare(C, V, U),
 4170	(	C = (<) -> Y = X
 4171	;	(	C = (=) ->
 4172			(	A = (-V) ->
 4173				ltr_negate(D, D0, S),
 4174				ltr_merge(D0, R, R0, S)
 4175			;	A = V ->
 4176				ltr_merge(D, R, R0, S)
 4177			)
 4178		;	dnf_subst(V, D, R, R1, S),
 4179			ltr_insert(A, R1, R0, S)
 4180		),
 4181		ltr_join(L0, R0, Y, S)
 4182	).
 solve_boole_with_check(+Exp, +Vs, +Ps, +S) is det
Solve bolean equation equation expressed as Exp with unknown variables Vs and free parameters Ps. Check that the result is really solutions. Ref. Hosoi.
 4190%  exists x  s.t. C0*(L,-x) + C1*x = 1
 4191% 	if and only if
 4192%  C0 + C1 = 1  satisfiable
 4193%  x = a*C1 + (-C0).
 4194
 4195% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S).
 4196% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S).
 4197% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S).
 4198
 4199solve_boole_with_check(Exp, Xs, Ps, S):- ltr_open_state(S),
 4200	dnf(Exp, E, S),
 4201	solve_boolean_equations(E, Xs, Ps, Sols, S),
 4202	eliminate_variables(E, Sols, Cond, S),
 4203	!,
 4204	dnf_valid_check(Cond, S).
 4205
 4206% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols),
 4207%	solutions_to_sets(Sols, Sols0).
 4208% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0).
 4209
 4210solve_boolean_equations(_, [], _, [], _):-!.
 4211solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols], S):-
 4212	solve_boolean_equations_basic(E, X, A, Sol0, E0, S),
 4213	solve_boolean_equations(E0, Xs, As, Sols, S),
 4214	dnf_subst_list(Sols, Sol0, Sol, S).
 4215
 4216% ?- ltr_zdd E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond).
 4217solve_boolean_equations_basic(E, X, A, Sol, Cond, S):-
 4218	dnf_subst(X, 1,  E, C1, S),
 4219	dnf_subst(X, 0,  E, C0, S),
 4220	ltr_join(C0, C0, Cond, S),
 4221	ltr_negate(C0, NC0, S),
 4222	ltr_insert(A, C1, AC1, S),
 4223	ltr_join(NC0, AC1, Sol, S).
 4224%
 4225dnf_subst_list([], E, E, _).
 4226dnf_subst_list([X=A|Eqs], E, F, S):-
 4227	dnf_subst(X, A, E, E0, S),
 4228	dnf_subst_list(Eqs, E0, F, S).
 4229%
 4230solutions_to_sets([], [], _).
 4231solutions_to_sets([X = E|Sols], [X = E0|Sols0], S):-
 4232	sets(E, E0, S),
 4233	solutions_to_sets(Sols, Sols0, S).
 4234
 4235% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check).
 4236
 4237% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check), psa(Cond), dnf_valid_check(Cond).
 4238
 4239% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check), psa(Cond).
 4240
 4241eliminate_variables(Exp, Eqns, Cond, S):-
 4242	apply_subst_list(Eqns, Exp, Cond, S).
 4243%
 4244apply_subst_list([], E, E, _).
 4245apply_subst_list([X=U|Eqns], E, E0, S):-
 4246	dnf_subst(X, U, E, E1, S),
 4247	dnf_subst_list(Eqns, E1, E0, S).
 4248%
 4249dnf_valid_check(X, S):-
 4250	ltr_atoms_by_scan(X, As, S),
 4251	ltr_sort(As, Bs),
 4252	expand_dnf(Bs, X, Y, S),
 4253	card(Y, C, S),
 4254	length(Bs, N),
 4255	(	C =:= (1<< N) -> writeln('Solved and Verified.')
 4256	;	writeln('Solved but NOT verified.')
 4257	).
 4258
 4259% ?- ltr_zdd X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), {sort(As, Bs)}.
 4260ltr_atoms_by_scan(X, [], _):- X<2, !.
 4261ltr_atoms_by_scan(X, P, S):- memo(ltr_atoms(X)-P, S),
 4262	(	nonvar(P) -> true
 4263	; 	cofact(X, t(A, L, R), S),
 4264		ltr_atoms_by_scan(L, Al, S),
 4265		ltr_atoms_by_scan(R, Ar, S),
 4266		ltr_var(A, A0),
 4267		union([A0|Al], Ar, P)
 4268	).
 4269
 4270		/*********************************
 4271		*  operations on reducible zdd   *
 4272		*********************************/
 4273
 4274% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y).
 4275% ?- zdd bdd_append([x, a, y, b], 0, Y), psa(Y).
 4276% ?- zdd bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z).
 4277
 4278bdd_append([], Z, Z, _).
 4279bdd_append([X|Y], Z, U, S):-
 4280	bdd_append(Y, Z, Z0, S),
 4281	cofact(U, t(X, 0, Z0), S).
 4282
 4283% ?- zdd bdd_list([b, b], Y), zdd_append([b,b], Y, Z), psa(Z).
 4284% ?- zdd bdd_list([b, b], Y), bdd_list(X,  Y).
 4285bdd_list(List, X, S):- var(X), !, bdd_append(List, 1, X, S).
 4286bdd_list(List, X, S):- get_bdd_list(X, List, S).
 4287
 4288% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L).
 4289% ?- zdd bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L).
 4290get_bdd_list(1, [], _):-!.
 4291get_bdd_list(X, [A|As], S):- X>1, zdd_cons(X, A, X0, S),
 4292	get_bdd_list(X0, As, S).
 4293
 4294% ?- zdd bdd_append([a,a,b,b], 1, X),
 4295%	bdd_append([1,1,2,2], 1, Y),
 4296%	bdd_zip(X, Y, Z), psa(Z).
 4297bdd_zip(0, _, 0, _):-!.
 4298bdd_zip(_, 0, 0, _):-!.
 4299bdd_zip(1, _, 1, _):-!.
 4300bdd_zip(_, 1, 1, _):-!.
 4301bdd_zip(X, Y, Z, S):- zdd_cons(X, A, X0, S),
 4302	zdd_cons(Y, B, Y0, S),
 4303	bdd_zip(X0, Y0, Z0, S),
 4304	zdd_cons(Z, A-B, Z0, S).
 4305
 4306% ?- zdd bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y).
 4307bdd_normal(X, X, _):- X<2, !.
 4308bdd_normal(X, Y, S):- cofact(X, t(A, L, R), S),
 4309	bdd_normal(L, L0, S),
 4310	bdd_normal(R, R1, S),
 4311	zdd_insert(A, R1, R0, S),
 4312	zdd_join(L0, R0, Y, S).
 4313
 4314% ?- zdd bdd_append([a,b,a,b], 1, X),
 4315%	bdd_append([a,b, c, a,b, c], 1, Y),
 4316%	bdd_append([b, a, b, a, a,b ], 1, Z),
 4317%	bdd_list_normal([X, Y, Z], R), psa(R).
 4318
 4319bdd_list_normal([], 0, _).
 4320bdd_list_normal([A|As], R, S):- bdd_list_normal(As, R0, S),
 4321	bdd_normal(A, A0, S),
 4322	zdd_join(A0, R0, R, S).
 4323
 4324%
 4325bdd_insert(_, 0, 0, _):-!.
 4326bdd_insert(A, 1, X, S):-!, zdd_singleton(A, X, S).
 4327bdd_insert(A, X, Y, S):- cofact(X, t(B, L, R), S),
 4328	bdd_insert(A, L, L0, S),
 4329	bdd_append([A,B], R, R0, S),
 4330	zdd_join(L0, R0, Y, S).
 bdd_list_raise(+L, +N, -X, +S) is det
L: list of atoms. N: integer exponent. X is unified with a BDD L^N=LL...L (N times), i.e., the set of lists of lenghth N which consists of elements of L.
 4339% ?- zdd bdd_list_raise([], 0, X).
 4340% ?- zdd bdd_list_raise([a], 0, X).
 4341% ?- zdd bdd_list_raise([a], 1, X), psa(X).
 4342% ?- zdd bdd_list_raise([a,b], 1, X), psa(X).
 4343% ?- zdd {N = 1, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X), card(X, C).
 4344% ?- zdd {N = 15, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X),card(X, C).
 4345
 4346bdd_list_raise(_, 0, 1, _):-!.
 4347bdd_list_raise(L, N, X, S):- N0 is N-1,
 4348	bdd_list_raise(L, N0, X0, S),
 4349	bdd_map_insert(L, X0, X, S).
 4350%
 4351bdd_map_insert([], _, 0, _).
 4352bdd_map_insert([A|As], X, Y, S):-
 4353	bdd_insert(A, X, X0, S),
 4354	bdd_map_insert(As, X, Y0, S),
 4355	zdd_join(X0, Y0, Y, S).
 4356
 4357% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert,
 4358% also work for bddered zdd.
 4359
 4360% ?- zdd X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U),
 4361%  psa(X), psa(Y), psa(Z), psa(U).
 4362% ?- zdd X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z),
 4363%	psa(Z, S), card(Z, C).
 4364% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z),
 4365%	card(Z, C).
 4366% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z),
 4367%	card(Z, C), card(X, D).
 4368
 4369bdd_merge(0, _, 0, _):-!.
 4370bdd_merge(_, 0, 0, _):-!.
 4371bdd_merge(1, X, X, _):-!.
 4372bdd_merge(X, 1, X, _):-!.
 4373bdd_merge(X, Y, Z, S):- memo(bdd_merge(X, Y)-Z, S),
 4374	(	nonvar(Z) -> true		% , write(.)	% So so frequently hits.
 4375	;	cofact(X, t(A, L, R), S),
 4376		bdd_merge(L, Y, L0, S),
 4377		bdd_merge(R, Y, R1, S),
 4378		zdd_cons(R0, A, R1, S),
 4379		zdd_join(L0, R0, Z, S)
 4380	).
 4381
 4382		/**************n***************************
 4383		*    Interleave bddered atoms in BDD    *
 4384		******************************************/
 bdd_interleave(+X, +Y, -Z, +S) is det
Z = { an interleave of A and B | A in X, B in Y }, where a list M is an interleave of a list A and and a list B if length(M) = length(A)+length(B), and both A and B are sublists of M. A list U is a sublist of a list V if U is a subsequence of V, provided that a list is viewed as a sequence.
 4393% ?- zdd X<< +[*[a,b], *[x,y]],  Y<< +[*[1]],
 4394%	bdd_interleave(X, Y, Z), psa(Z).
 4395% ?- zdd X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z).
 4396% ?- zdd X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z).
 4397
 4398bdd_interleave(0, _, 0, _):-!.
 4399bdd_interleave(_, 0, 0, _):-!.
 4400bdd_interleave(1, X, X, _):-!.
 4401bdd_interleave(X, 1, X, _):-!.
 4402bdd_interleave(X, Y, Z, S):-	 % memo is useless here.
 4403	cofact(Y, t(B, L, R), S),
 4404	(	L < 2  ->  L0 = 0
 4405	;	bdd_interleave(X, L, L0, S)
 4406	),
 4407	bdd_interleave(X, B, R, R0, S),
 4408	zdd_join(L0, R0, Z, S).
 4409%
 4410bdd_interleave(0, _, _, 0, _):-!.
 4411bdd_interleave(1, B, Y, Z, S):-!, cofact(Z, t(B, 0, Y), S).
 4412bdd_interleave(X, B, Y, Z, S):- memo(merge(X, Y, B)-Z, S),
 4413	(	nonvar(Z) -> true			% , write(+)			% many hits.
 4414	;	cofact(X, t(A, L, R), S),
 4415		(	L < 2 -> L0 = 0
 4416		;	bdd_interleave(L, B, Y, L0, S)
 4417		),
 4418		bdd_interleave(A, R, B, Y, R0, S),
 4419		zdd_join(L0, R0, Z, S)
 4420	).
 4421%
 4422bdd_interleave(A, X, B, Y, Z, S):-  % memo is useless here.
 4423	bdd_interleave(X, B, Y, U, S),
 4424	cofact(Z0, t(A, 0, U), S),
 4425	bdd_interleave(Y, A, X, V, S),
 4426	cofact(Z1, t(B, 0, V), S),
 4427	zdd_join(Z0, Z1, Z, S).
 bdd_funs(+PartExp, -F, +S) is det
PartExp is an expressions built from mono(A-B), epi(A-B), fun(A-B), and operator * (merge), & (interleave). F is the function space in ZDD built from these parts. mono(A-B) means function restricted to A is one-to-one mappings to B. epi(A-B) one-to-onto, and fun(A-B) mapping.
 4436% ?- zdd bdd_funs(mono([1,2]-[a,b])*mono([3,4]-[c,d]), X), psa(X).
 4437% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), psa(X).
 4438% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X),
 4439%	zdd_normalize(X, Y), psa(Y).
 4440
 4441bdd_funs(A*B, F, S):-!, bdd_funs(A, A0, S),
 4442	bdd_funs(B, B0, S),
 4443	bdd_merge(A0, B0, F, S).
 4444bdd_funs(A&B, F, S):-!, bdd_funs(A, A0, S),
 4445	bdd_funs(B, B0, S),
 4446	bdd_interleave(A0, B0, F, S).
 4447bdd_funs(A, F, S):- fun_block(A, F, S).
 4448
 4449		/**************
 4450		*     misc    *
 4451		**************/
 zdd_flatten(+X, -Y, +S) is det
Y = { {A} | A in U, U in X }.
 4456% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), zdd_flatten(X, Y), psa(Y)).
 4457zdd_flatten(X, 0, _):- X<2, !.
 4458zdd_flatten(X, Y, S):- memo(flatten(X)-Y, S),
 4459	(	nonvar(Y) -> true	% Many hits.
 4460	;	cofact(X, t(A, L, R), S),
 4461		zdd_flatten(L, L0, S),
 4462		zdd_flatten(R, R0, S),
 4463		zdd_join(L0, R0, Y0, S),
 4464   		cofact(Y, t(A, Y0, 1), S)
 4465	)