2:- module(zdd, 3 [ card/2, card/3 4 , ltr_cofact/2, ltr_cofact/3 5 , ltr_join/3, ltr_join/4 6 , ltr_merge/3, ltr_merge/4, ltr_card/3, ltr_card/4 7 , sat/1, sat_count/1, sat_count/2 8 , sat0/1, sat_count0/1, sat_count0/2 9 , fos/1, fos_count/0, fos_count/1, fos_count/2 10 , make_boole_canonical/2, simple_boole/2 11 , boole_to_dnf/2, ltr_card/3 12 , dnf/2, dnf/3, dnf0/2, dnf0/3 13 , cnf/2, cnf/3, cnf0/2, cnf0/3 14 , zdd_funs/3, zdd_funs/4 15 , cofact0/3, cofact0/4 16 , zdd/1 17 , zdd_append/3, zdd_append/4, zdd_insert/4 18 , zdd_insert_atoms/3, zdd_insert_atoms/4 19 , zdd_has_1/2 20 , zdd_join/3, zdd_join/4 21 , zdd_singleton/2, zdd_singleton/3 22 , zdd_merge/3, zdd_merge/4 23 , zdd_meet/3, zdd_meet/4 24 , zdd_subtr/3, zdd_subtr/4 25 , zdd_divide/3, zdd_divide/4, zdd_residue/3, zdd_residue/4 26 , zdd_div_by_list/3, zdd_div_by_list/4 27 , zdd_res_by_list/3, zdd_res_by_list/4 28 , zdd_power/2, zdd_power/3 29 , get_extra/1, get_extra/2 30 , get_key/2, get_key/3, set_key/2, set_key/3 31 , delete_key/1, delete_key/2 32 , intern/3 33 , make_boole_canonical/2 34 , use_zdd/1, use_zdd/2 35 , zdd_shift/1 36 , psa/1, psa/2, sets/2, sets/3, ppoly/1, ppoly/2, poly_term/2, poly_term/3 37 , @/1, significant_length/3 38 , charlist/2, charlist/3, atomlist/2 39 ]). 40 41% ?- fos(pow(1..3)//(1+2)), fos_count. 42% ?- fos(pow(1..3)//(1*2)), fos_count. 43 44:- use_module(library(apply)). 45:- use_module(library(apply_macros)). 46:- use_module(library(clpfd)). 47:- use_module(library(statistics)). 48:- use_module(zdd('zdd-array')). 49:- use_module(util(math)). 50:- use_module(util(meta2)). 51:- use_module(pac(basic)). 52:- use_module(pac(meta)). 53:- use_module(util(misc)). 54:- use_module(pac('expand-pac')). % For the kind block. 55:- use_module(zdd('zdd-misc')). 56:- use_module(zdd('zdd-plain')). 57:- use_module(pac(op)). 58 59:- set_prolog_flag(stack_limit, 10_200_147_483_648). 60% :- use_module(zdd('zdd-misc')). 61% :- use_module(zdd('zdd-graphviz')). 62% :- use_module(zdd('zdd-euler')). 63% :- use_module(zdd('zdd-reset-shift')). 64attr_unify_hook(V, Y):- 65 ( get_attr(Y, zdd, A) 66 -> zdd_unify(V, A) 67 ; zdd_unify(V, Y) 68 ). 69 70 :- op(1060, xfy, ~). % equivalence 71 :- op(1060, xfy, #). % exor 72 :- op(1060, xfy, <->). % equivalence 73 :- op(1050, yfx, <-). 74 :- op(1060, xfy, <=> ). % equivalence 75 :- op(1040, xfy, \/). % OR 76 :- op(1030, xfy, /\). % AND 77 :- op(1020, fy, \). % NOT 78 :- op(700, xfx, :=). % Assignment 79 :- op(1000, xfy, &). 80 81% for pac query. 82 :- pac:op(1000, xfy, &). 83 :- pac:op(700, xfx, :=). 84 85 86% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))). 87 88term_expansion --> pac:expand_pac. 89 90:- meta_predicate @(). 91@(X):- shift(X). 92 93% ?- zdd({X=1}). 94% ?- zdd(X=1). 95% ?- zdd((append([], [], X))). 96% ?- zdd((true, true)). 97% ?- zdd((Y<<cnf((a+b)*(-(a)+c)), ltr_remove(-(a), Y, U), sets(U, S))). 98% ?- numlist(1, 16, L), zdd((X<< pow(L), card(X, C))). 99% ?- numlist(1, 16, L), zdd((X<< pow(L))). 100% ?- numlist(1, 10000, L), zdd((X<< pow(L), card(X, C))). 101% ?- numlist(1, 16, L), 102% zdd((X<< pow(L), Y<<pow(L), Z << (X+Y), U<< (X*Y), card(X, C))). 103% ?- time((numlist(1, 40, L), 104% zdd((X << pow(L), Y<<pow(L), Z << merge(X, Y), card(Z, C))))). 105% ?- zdd((setmemo(a-1), setmemo(a-2), memo(a-V))). 106% ?- zdd(X<<{[1,1]}). 107% ?- zdd((X<<pow([1,2,3]), prz(X))). 108% ?- zdd((X<< [1,2,3,1], prz(X))). 109% ?- zdd((X<< [[1],[1]], prz(X))). 110% ?- zdd((X<< [[a-b, b-c]], prz(X))). 111% ?- zdd( use_zdd((memo(a-1), memo(a-X)))). 112% ?- zdd(use_zdd(zdd(use_zdd((memo(a-1), memo(a-X)))))). 113% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))}, sets(X, Sx))). 114% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))}, 115% sets(X, Sx), sets(Y, Sy1))). 116% ?- zdd((set_key(root, hello), get_key(root, R))). 117% ?- zdd((intern(a, X), show_state)). 118% ?- zdd((intern(a, X), intern(b, Y))). 119% ?- zdd((intern(A, X), intern(B, Y))). 120% ?- zdd((zdd_funs([a],[b], F), psa(F))). 121% ?- zdd((zdd_funs([],[b], F), psa(F))). 122% ?- zdd((zdd_funs([a],[], F), psa(F))). 123% ?- zdd((zdd_funs([a,b],[c,d], F), psa(F), card(F, C))). 124% ?- N=3, numlist(1, N, Ns), zdd((zdd_funs(Ns, Ns, F), psa(F), card(F, C))). 125% ?- N=3, M=5, numlist(1, N, Ns), numlist(1, M, Ms), 126% zdd((zdd_funs(Ns, Ms, F), card(F, C))). 127% ?- time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 128% zdd((zdd_funs(Ns, Ms, F), card(F, C))))). 129 130% Cardinality # of Y^X = { f | f: X-> Y }. 131% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 132 133% ?- I=1, J=1, K=1, L=1, 134% numlist(1, I, X), numlist(1, K, Y), 135% raise_list(X, J, Xj), 136% raise_list(Y, L, Yl), 137% time( ( call_with_time_limit(200, ( 138% zdd((zdd_funs(Xj, Yl, F, default_pair), card(F, C))))), 139% C =:= (K^L)^(I^J), 140% significant_length(C, Keta, 10))). 141 142% ?- I=3, J=5, K=3, L=5, 143% numlist(1, I, X), numlist(1, K, Y), 144% raise_list(X, J, Xj), 145% raise_list(Y, L, Yl), 146% time( ( call_with_time_limit(200, ( 147% zdd((zdd_funs(Xj, Yl, F), card(F, C))))), 148% C =:= (K^L)^(I^J), 149% significant_length(C, Keta, 10))). 150 151significant_length(0, 0, _):-!. 152significant_length(X, 1, Radix):- X < Radix, !. 153significant_length(X, L, Radix):- Y is X // Radix, 154 significant_length(Y, L0, Radix), 155 L is L0+1. 156% 157 158default_pair(X, Y, X-Y). 159 160equational_mapsto([A,B], C, A+B = C). 161 162:- meta_predicate zdd_funs(,,,). 163zdd_funs(D, R, F):- zdd_funs(D, R, F, default_pair). 164 165:- meta_predicate zdd_funs(,,,). 166zdd_funs(D, R, F, Pred):- shift(zdd_funs(D, R, F, Pred)). 167% 168zdd_funs([], _, 1, _, _). 169zdd_funs([A|As], Bs, F, Pred, S):- 170 zdd_funs(As, Bs, F0, Pred, S), 171 extend_funs_by_one(A, Bs, F0, 0, F, Pred, S). 172% 173extend_funs_by_one(_, [], _, F, F, _, _):-!. 174extend_funs_by_one(A, [B|Bs], H, F0, F, Pred, S):- call(Pred, A, B, Pair), !, 175 zdd_insert(Pair, H, H0, S), 176 zdd_join(H0, F0, F1, S), 177 extend_funs_by_one(A, Bs, H, F1, F, Pred, S). 178extend_funs_by_one(A, [_|Bs], H, F0, F, Pred, S):- 179 extend_funs_by_one(A, Bs, H, F0, F, Pred, S). 180 181% ?- N = 1000, numlist(1, N, Ns), 182% time(zdd((X<<pow(Ns), rank_family_by_card(X, P), 183% memo(family_with_card(500)-L), card(L, C)))). 184%@ % 90,174,772 inferences, 10.355 CPU in 10.540 seconds (98% CPU, 8708585 Lips) 185 186% ?- N = 1000, numlist(1, N, Ns), 187% time(zdd(( X<<pow(Ns), 188% get_family_of_rank(500, X, Y), 189% card(Y, C)))).
194get_family_of_rank(Order, X, F):- shift(get_family_of_rank(Order, X, F)). 195% 196get_family_of_rank(Order, X, F, S):- rank_family_by_card(X, _, S), 197 memo(family_with_card(Order)-F, S). 198 199 200% ?- zdd((X<<set([a]), rank_family_by_card(X, P), 201% memo(family_with_card(0)-L), sets(L, Sl), 202% memo(family_with_card(1)-M), sets(M, Sm))).
207rank_family_by_card(X, Y):- shift(rank_family_by_card(X, Y)). 208% 209rank_family_by_card(0, 0, _):-!. 210rank_family_by_card(1, 0, S):-!, memo(family_with_card(0)-1, S). 211rank_family_by_card(I, P, S):- memo(rank_family_by_card_done(I)-B, S), 212 ( nonvar(B) -> true 213 ; cofact(I, t(A, L, R), S), 214 rank_family_by_card(L, Pl, S), 215 rank_family_by_card(R, Pr, S), 216 max(Pl, Pr, P0), 217 insert_one_to_family(A, P0, New, S), 218 P is P0 + 1, 219 memo(family_with_card(P)-New, S), 220 B = true 221 ). 222% 223insert_one_to_family(A, 0, G, S):-!, memo(family_with_card(0)-F, S), 224 zdd_insert(A, F, G, S). 225insert_one_to_family(A, P, G, S):- P0 is P-1, 226 insert_one_to_family(A, P0, G0, S), 227 memo(family_with_card(P)-Fp, S), 228 zdd_insert(A, Fp, G, S), 229 zdd_join(Fp, G0, Gp, S), 230 setmemo(family_with_card(P)-Gp, S). 231 232% 233max(A, B, A):- A@>B, !. 234max(_, B, B). 235 236 237 /********************** 238 * State access * 239 **********************/ 240 241get_extra(Extra):- shift(get_extra(Extra)). 242get_extra(Extra, s(_, Extra)). 243 244% 245set_extra(Extra):- shift(set_extra(Extra)). 246set_extra(Extra, S):- setarg(2, S, Extra). 247% 248get_key(K, V):- shift(get_key(K, V)). 249get_key(K, V, s(_, Assoc)):- memberchk(K-V, Assoc). 250 251set_key(K, V):- shift(set_key(K, V)). 252set_key(K, V, S) :- S = s(_, Assoc), 253 ( select(K-_, Assoc, Assoc0) 254 -> setarg(2, S, [K-V|Assoc0]) 255 ; setarg(2, S, [K-V|Assoc]) 256 ). 257 258delete_key(K):- shift(delete_key(K)). 259% 260delete_key(K, S):- S = s(_, Extra), 261 ( select(K-_, Extra, Extra0) -> setarg(2, S, Extra0) 262 ; true 263 ). 264 265% 266get_state(X):- shift(=(X)). 267 268% 269set_state(X):- shift(set_state(X)). 270set_state(X, Y):- arg(1, X, A), 271 setarg(1, Y, A), 272 arg(2, X, B), 273 setarg(2, Y, B). 274% 275show_state :- get_state(s(#(N, #(K,_),_), Extra)), 276 format("array max = ~w~n", [N]), 277 format("hash keys count = ~w~n", [K]), 278 format("extra = ~w~n", [Extra]). 279% 280get_vector(X):- shift(get_vector(X)). 281get_vector(Vec, s(#(_,_,Vec),_)). 282% 283vector(X):- get_vector(X). 284 285% ?- zdd((X<<pow([a,b,c,d]), zdd_dump, card(X, C))). 286zdd_dump:- get_state(s(#(N, _, Vec), _)), 287 forall( between(2, N, I), 288 ( arg(I, Vec, X), 289 format("~w = ~w\n", [I, X]) 290 )). 291 292% ?- time((numlist(1, 10000, Ns), zdd((X<<pow(Ns), 293% zdd_export(X, Y, S), card(X, Mx), card(Y, My, S))))), 294% Mx = My. 295% ?- zdd((zdd((X<<pow([a,b]), zdd_export(X, Y, S), card(X, Sx))), card(Y, Sy, S))). 296% ?- zdd((zdd((X<<pow([a,b]), zdd_export(X, Y, S))), card(X, Sx), card(Y, Sy, S))). % false 297 298zdd_export(I, I0, S0):- shift(zdd_export(I, I0, S0)). 299% 300zdd_export(I, I0, S0, S):- open_state(S0), 301 zdd_shift(zdd_export(I, S, I0, S0)). 302% 303zdd_export(I, _, I, _, _):- I<2, !. 304zdd_export(I, S, I0, S0, M):- memo(I-I0, M), 305 ( nonvar(I0) -> true 306 ; cofact(I, t(A, L, R), S), 307 zdd_export(L, S, L0, S0, M), 308 zdd_export(R, S, R0, S0, M), 309 cofact(I0, t(A, L0, R0), S0) 310 ). 311 312% ?- zdd((varnum(D), varnum(E))).
317varnum(D):- shift(get_key(varnum, D)). 318 319% ?- zdd((cofact0(X, a, 1), psa(X), cofact0(X, A, B))). 320% ?- zdd((cofact0(X, 1, a), psa(X), cofact0(X, A, B))). 321% ?- zdd((cofact0(X, 1, 0), psa(X), cofact0(X, A, B))).
326cofact0(X, A, Y):- shift(cofact0(X, A, Y)). 327% 328cofact0(X, A, Y, S):- var(X), !, cofact(X, t(A, 0, Y), S). 329cofact0(X, A, Y, S):- X > 1, cofact(X, t(A, 0, Y), S). 330 331% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c], X))). 332% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false 333% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([b,c], X))). 334% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([], X))).
338zdd_memberchk(L, Z):- shift(zdd_memberchk(L, Z)). 339% 340zdd_memberchk(L, Z, S):- sort(L, L0), 341 zdd_ord_memberchk(L0, Z, S). 342% 343zdd_ord_memberchk(L, Z):- shift(zdd_ord_memberchk(L, Z)). 344% 345zdd_ord_memberchk([], Z, S):- !, zdd_has_1(Z, S). 346zdd_ord_memberchk([A|As], Z, S):- Z>1, 347 cofact(Z, t(B, L, R), S), 348 ( A == B 349 -> zdd_ord_memberchk(As, R, S) 350 ; A @> B, 351 zdd_ord_memberchk([A|As], L, S) 352 ). 353 354% ?- zdd((X=1, Y =2, Z is X + Y)). 355% ?- zdd((X<<[a], sets(X, S))). 356% ?- zdd((X<<[a], S<<sets(X))). 357% ?- zdd((X<<pow([a,b]), S<<sets(X))). 358% ?- zdd((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 359% ?- zdd((X<< ([a,b]+[c,d]), S<<sets(X))). 360% ?- zdd((X<<([a,b]&[c,d]), S<<sets(X))). 361% ?- zdd((X<<{[a],[b],[c]}, sets(X,S))). 362% ?- zdd((X<<{[a],[b, c]}, sets(X,S))). 363% ?- zdd((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 364% ?- zdd((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 365% ?- I =1000, J =2000, 366% time(zdd(( numlist(1, I, L), numlist(1, J, M), X << pow(L), Y << pow(M), 367% Z << (Y - X), card(Z, C), C =:= 2^J-2^I))). 368% ?- I =1000, J is I + 1, numlist(1, I, L), prepare_ltr_list(L, L0), 369% time(zdd(( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I],X)))). 370 371% ?- zdd((X<<cnf(a), Y<<sets(X))). 372% ?- zdd((X<<cnf(-a), Y<<sets(X))). 373% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 374% ?- zdd((X<<cnf(-(a+b)), Y<<sets(X))). 375% ?- zdd((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 376% ?- zdd((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 377% ?- zdd((X<<cnf(-(-a + -b)), Y<<sets(X))). 378% ?- zdd((X<<dnf(a), Y<<sets(X))). 379% ?- zdd((X<<dnf(-(-a)), Y<<sets(X))). 380% ?- zdd((X<<dnf(a+b), Y<<sets(X))). 381% ?- zdd((X<<dnf(-(a+b)), Y<<sets(X))). 382% ?- zdd((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 383% ?- zdd((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 384% ?- zdd((X<<dnf(-(-a + -b)), Y<<sets(X))). 385% ?- zdd((X<<dnf((-a + a)), Y<<sets(X))). 386% ?- zdd((X<<dnf(-(-a + a)), Y<<sets(X))). 387% ?- zdd(X << append([a,b], [c,d])). 388% ?- zdd((X << (([a,b]+[c,d])*[c,d]), sets(X, S))). 389% ?- zdd((X << (([a,b]+[c,d])*[c, d, d]), sets(X, S))). 390% ?- zdd((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 391% ?- zdd((X << dnf(a*b+c*d+c*d*d))). 392% ?- zdd((zdd_list_to_singletons([], X), prz(X))). 393% ?- zdd((zdd_list_to_singletons([a], X), prz(X))). 394% ?- zdd((zdd_list_to_singletons([a,b], X), prz(X))). 395% ?- zdd((zdd_list_to_singletons([c, a, b], X), prz(X))).
401% For example, if X=[a,b,c] then ZDD I is [[a], [b], [c]] 402% as a family of sets in ZDD. 403 404zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 405% 406zdd_list_to_singletons([], 1, _). 407zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 408 zdd_singleton(A, Y0, S), 409 zdd_join(Y0, Y, X, S). 410 411% ?- zdd((zdd_partial_choices([], X), prz(X))). 412% ?- zdd((zdd_partial_choices([[a], [b]], X), prz(X))). 413% ?- zdd((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 414% ?- zdd((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 415% ?- zdd((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 416% ?- zdd((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 417% ?- zdd((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X)).) 418% ?- zdd((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 419% ?- zdd((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 420 421% ?- findall([I], between(1, 10000, I), Ls), 422% zdd((zdd_partial_choices(Ls, X), 423% card(X, C))), !, C =:= 2^10000.
431zdd_partial_choices(X, Y):- shift(zdd_partial_choices(X, Y)). 432% 433zdd_partial_choices([], 1, _):-!. 434zdd_partial_choices([L|Ls], X, S):- zdd_partial_choices(Ls, X0, S), 435 zdd_fold_insert(L, X0, 0, X1, S), 436 zdd_join(X0, X1, X, S). 437 438% ?- zdd((dnf((A+B)*(C+D)*(E+F), F), sets(F, G))), maplist(writeln, G). 439 440% ?- zdd((dnf((A+B)*(C+D)*(E+F), F1), sets(F1, G))), maplist(writeln, G). 441% ?- zdd((dnf((A+B)*(C+D)*(E+F), G), zdd_dump)). 442% ?- zdd:zdd((P<<pow([1,2,3]), use_zdd((X=1;X=2)), card(P,C))). 443% ?- zdd((P << (set([1,2,3,2,3])+set([4, 2,4])), prz(P))). 444% ?- zdd({append([a,b], [c,d], X)}). 445% ?- zdd(X << append([a,b], [c,d])). 446% ?- zdd(zdd(X << append([a,b], [c,d]))). 447% ?- zdd(zdd(zdd((X << append([a,b], [c,d]), psa(X))))). 448% ?- zdd(zdd(zdd((X<<pow([1,2]), true, true)))). 449% ?- zdd(zdd(zdd((X<<pow([1,2]), true, true, card(X, C))))).
454:- meta_predicate zdd(). 455zdd(Exp):- use_zdd(Exp). 456 457% ?- listing(zdd). 458 459:- meta_predicate zdd(, ). 460zdd(M:A, S):- zdd(A, S, M).
zdd(E), without closing the state.464:- meta_predicate zdd0(). 465zdd0(Exp):- open_state(S), zdd(Exp, S). 466 467% ?- open_state(M), zdd_reset_continue((memo(a-1), memo(a-R)), M), close_state(M). 468% ?- open_state(M), zdd_reset_continue(( zdd((X<<pow([1,2]), 469% memo(a-X), card(X, C)))), M).
474:- meta_predicate zdd_reset_continue(, ). 475zdd_reset_continue(Goal, S):- reset(Goal, Ball, Rest), 476 ( var(Ball) -> true 477 ; call(Ball, S) 478 ), 479 zdd(Rest, S).
484:- meta_predicate use_zdd(). 485use_zdd(X):- use_zdd(X, [hash_size(128)]). 486 487:- meta_predicate use_zdd(, ). 488use_zdd(X, Options):- 489 setup_call_cleanup( 490 open_state(S, Options), 491 zdd(X, S), 492 close_state(S)).
used_zdd(shift(G))
for convenience.497:- meta_predicate zdd_shift(). 498zdd_shift(G):- use_zdd(shift(G)). 499 500 501% ?- zdd((X<<pow([1,2]), memo(a-X), card(X, C))).
516zdd((A,B), S, M):-!, zdd(A, S, M), zdd(B, S, M). 517zdd(X<<E, S, _):-!, zdd_eval(E, X, S). 518zdd(M:G, S, _):-!, zdd(G, S, M). 519zdd(0, _, _):-!. 520zdd(true, _, _):-!. 521zdd({G}, _, _):-!, call(G). 522zdd((A;B), S, M):-!, (zdd(A, S, M); zdd(B, S, M)). 523zdd((A->B), S, M):-!, (zdd(A, S, M)->zdd(B, S, M)). 524zdd(Cont, S, M):- zdd_reset_continue(M:Cont, S). 525 526% ?- zdd((X<<cofact(a, 1, 1), psa(X), Y<<cofact(X), card(X, C))).
531% x x (integer) 532% x x (list) 533% set a singleton family. 534% {a,b,..} a family of sets. 535% + join 536% - subtract 537% \ subtract 538% * intersection 539% merge merge 540% & merge 541% prod product 542% ** product 543% pow powerset 544% power powerset 545% sets convert to a usual list of lists 546% cnf CNF 547% dnf DNF 548% exp(E) user-defined expression 549% cofact/3 cofact (for tutorial purpose, to be dropped) 550% cofact/1 cofact (for tutorial purpose), to be dropped) 551% prolog call with last argument as output 552% E evaluate E recursively. 553 554% ?- zdd((X << card(pow([a,b])))). 555% ?- zdd((X << pow([a,b]))). 556% ?- zdd((X << [a, b, c])). 557% ?- zdd((X << set([a, b, c]))). 558% ?- zdd((X << (set([a, b, c]) + set([1,2,3])), psa(X))). 559% ?- zdd((C << card(pow([a,b,c,1,2,3])))). 560% ?- zdd((C << card(pow(prolog(append([a,b,c], [1,2,3])))))). 561 562% 563zdd_eval(X, X, _) :- integer(X), !. % for any x >= 0. 564zdd_eval(L, Y, _) :- is_list(L), !, sort(L, Y). 565zdd_eval(set(L), Y, S) :- zdd_eval(L, L0, S), 566 zdd_append(L0, 1, Y, S). 567zdd_eval(ltr_set(L), Y, S) :- zdd_eval(L, L0, S), 568 ltr_append(L0, 1, Y, S). 569zdd_eval({X}, Y, S) :-!, associative_comma(X, U, []), zdd_family(U, Y, S). 570zdd_eval(dnf(A), X, S):-!, dnf(A, X, S). 571zdd_eval(cnf(A), X, S):-!, cnf(A, X, S). 572zdd_eval(gf2(A), X, S):-!, gf2(A, X, S). 573zdd_eval(fos(A), X, S):-!, fos(A, X, S). 574zdd_eval(X + Y, A1, S):-!, zdd_eval(X, A2, S), 575 zdd_eval(Y, A3, S), 576 zdd_join(A2, A3, A1, S). 577zdd_eval(X * Y, A1, S):-!, zdd_eval(X, A2, S), 578 zdd_eval(Y, A3, S), 579 zdd_meet(A2, A3, A1, S). 580zdd_eval(X - Y, A1, S):-!, zdd_eval(X, A2, S), 581 zdd_eval(Y, A3, S), 582 zdd_subtr(A2, A3, A1, S). 583zdd_eval(\(X,Y), A, S):-!, zdd_eval(X-Y, A, S). 584zdd_eval(merge(X, Y), A1, S):-!, zdd_eval(X, A2, S), 585 zdd_eval(Y, A3, S), 586 zdd_merge(A2, A3, A1, S). 587zdd_eval(&(X, Y), A, S):-!, zdd_eval(merge(X, Y), A, S). 588zdd_eval(prod(X, Y), A1, S):-!, zdd_eval(X, A2, S), 589 zdd_eval(Y, A3, S), 590 zdd_product(A2, A3, A1, S). 591zdd_eval(**(X, Y), A, S):-!, zdd_eval(prod(X, Y), A, S). 592zdd_eval(pow(X), A, S) :-!, zdd_eval(X, X0, S), 593 sort(X0, X1), 594 zdd_power(X1, A, S). 595zdd_eval(power(X), A, S):-!, zdd_eval(pow(X), A, S). 596zdd_eval(sets(X), A, S) :-!, zdd_eval(X, Y, S), 597 sets(Y, A, S). 598zdd_eval(cofact(A, L, R), X, S):-!, cofact(X, t(A, L, R), S). 599zdd_eval(cofact(X), Y, S):-!, cofact(X, Y, S). 600zdd_eval(prolog(E), Y, _):-!, call(E, Y). 601zdd_eval(E, A, S) :- E =.. [F|As], 602 maplist(zdd_eval_flip(S), As, Bs), 603 E0 =.. [F|Bs], 604 zdd(call(E0, A), S). 605 606% 607zdd_eval_flip(S, A, B):- zdd_eval(A, B, S). 608 609% ?- zdd(C<<card(pow([a,b]))). 610% ?- zdd((X<<pow([a, b, c]), zdd_super_power([a, b], X, Y), psa(Y))). 611 612% ?- N = 2, numlist(1, N, Ns), cartesian(Ns, Ns, P), 613% zip(Ns, Ns, Z), maplist(pred([A-B, (A, B)]), Z, Z0), 614% zdd((X<<pow(P), 615% zdd_super_power(Z0, X, Q), 616% card(Q, C))), C=:= 2^(N^2-N). 617 618% ?- N = 100, numlist(1, N, Ns), cartesian(Ns, Ns, P), 619% zip(Ns, Ns, Z), maplist(pred([A-B, (A, B)]), Z, Z0), 620% time(zdd((X<<pow(P), zdd_super_power(Z0, X, Q), 621% card(Q, C)))), C=:= 2^(N^2-N). 622 623 624zdd_super_power(X, Y, Z):- shift(zdd_super_power(X, Y, Z)). 625 626zdd_super_power([], P, P, _). 627zdd_super_power([A|As], P, Q, S):- 628 zdd_super_power(As, P, Q0, S), 629 zdd_insert(A, Q0, Q, S). 630 631% 632family(X, Y):- shift(family(X, Y)). 633 634family(X, Y, S):- zdd_family(X, Y, S). 635% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 636 637 638zdd_family(X, Y):- shift(zdd_family(X, Y)). 639% 640zdd_family(X, Y, S):- zdd_family(X, 0, Y, S). 641 642% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 643% ?- zdd((zdd_family([[], [a],[a,b]], X), psa(X))). 644% 645zdd_family([], U, U, _). 646zdd_family([X|Xs], U, V, S):- 647 zdd_append(X, 1, X0, S), 648 zdd_join(X0, U, U0, S), 649 zdd_family(Xs, U0, V, S). 650 651% ?- zdd((ltr_family([[a, b], [c, d]], X), sets(X,S))). 652% ?- zdd((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 653% ?- zdd((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 654% ?- zdd((ltr_family([[a],[a,b]], X), ltr_card(3, X, C), psa(X))). 655% ?- zdd((ltr_family([[], [a],[a,b]], X), ltr_card(2, X, C), psa(X))). 656% ?- zdd((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 657% ?- zdd((X << dnf((a+(-b)+a)), psa(X))). 658% ?- zdd((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 659 660% 661ltr_family(X, Y):- shift(ltr_family(X, Y)). 662% 663ltr_family(X, Y, S):- ltr_family(X, 0, Y, S). 664 665% 666ltr_family([], U, U, _). 667ltr_family([X|Xs], U, V, S):- 668 ltr_append(X, 1, X0, S), 669 ltr_join(X0, U, U0, S), 670 ltr_family(Xs, U0, V, S). 671 672 673% ?- associative_comma((([], [a]), [b]), P, []). 674associative_comma((X, Y), P, Q):-!, associative_comma(X, P, P0), 675 associative_comma(Y, P0, Q). 676associative_comma(X, [X|P], P). 677 678% ?- zdd((X<<{[], [a]}, psa(X), zdd_remove_1(X, Y), psa(Y))). 679% ?- zdd((X<<{[a]}, zdd_remove_1(X, U))). % false 680zdd_remove_1(X, Y):- shift(zdd_remove_1(X, Y)). 681% 682zdd_remove_1(1, 0, _):-!. 683zdd_remove_1(X, Y, S):- X>2, 684 cofact(X, t(A, L, R), S), 685 zdd_remove_1(L, L0, S), 686 cofact(Y, t(A, L0, R), S). 687 688 689% ?- zdd(( (X<< {[a,b,c]}, zdd_choices(X, Y), psa(Y)))). 690% ?- zdd(( (X<< [a,b,c], zdd_choices(X, Y), psa(Y)))). 691% ?- zdd(( (X<< {[a, b], [c, d]}), zdd_choices(X, Y), psa(Y))). 692% ?- zdd(( (X<< {[], [a, b], [c, d]}), zdd_choices(X, Y), psa(Y))). 693% ?- zdd(( (X<< {[a], [c, d]}), zdd_choices(X, Y), psa(Y))). 694% ?- zdd(( X<< {[a,b], [c, d], [e,f]}, zdd_choices(X, Y), psa(Y))). 695% ?- zdd(( X<< {[a,b]}, zdd_choices(X, Y), psa(Y))). 696% ?- zdd(( X<< {[]}, zdd_choices(X, Y), psa(Y))). 697% ?- zdd((X<<([a,b]+[1,2]), zdd_choices(X, Y), psa(Y), card(Y, C))). 698% ?- zdd((A<<charlist(a,z), B<<numlist(1,10), X<<(A+B), 699% zdd_choices(X, Y), card(Y, C))). 700% ?- charlist(a,z, AZ), zdd((A<< AZ, ltr_choices(A, Y), card(Y, C))). 701% ?- zdd((A<<numlist(1, 2), psa(A), zdd_choices(A, Y), card(Y, C))). 702 703zdd_choices(X, Y):- shift(zdd_choices(X, Y)). 704% 705zdd_choices(1, 0, _):-!. 706zdd_choices(0, 1, _):-!. 707zdd_choices(X, Y, S):- memo(zdd_choices(X)-Y, S), 708 ( nonvar(Y) -> true 709 ; zdd_choices(X, [], 1, Y, S) 710 ). 711% 712zdd_choices(0, _, Y, Y, _):-!. 713zdd_choices(1, As, Y0, Y, S):-!, zdd_fold_insert(As, Y0, 0, Y, S). 714zdd_choices(X, As, Y0, Y, S):- cofact(X, t(A, L, R), S), 715 ( L = 0 716 -> zdd_choices(R, [A|As], Y0, Y, S) 717 ; L = 1 718 -> ( As = [] 719 -> Y = 0 720 ; zdd_fold_insert(As, Y0, 0, Y1, S), 721 zdd_choices(R, [A|As], Y1, Y, S) 722 ) 723 ; zdd_choices(L, As, Y0, Y1, S), 724 zdd_choices(R, [A|As], Y1, Y, S) 725 ). 726% 727zdd_fold_insert([], _, Y, Y, _). 728zdd_fold_insert([A|As], Y0, U, Y, S):- 729 zdd_insert(A, Y0, V, S), 730 zdd_join(U, V, U0, S), 731 zdd_fold_insert(As, Y0, U0, Y, S). 732 733% ?- zdd((X<<pow([a,b]), zdd_fold_cons([1,2,3], X, Y), sets(Y, U))), writeln(U). 734% ?- zdd((zdd_singleton([], X), zdd_fold_cons([1,2,3], X, Y), sets(Y, U))), writeln(U). 735% ?- zdd((zdd_list_length(0, [a, b], X), psa(X))). 736% ?- spy(zdd_list_length). 737% ?- zdd((zdd_list_length([a, b], 1, X), psa(X))). 738% ?- zdd((zdd_list_length([a, b, c], 3, X), psa(X))). 739% ?- N=100, numlist(1, N, Ns), zdd((zdd_list_length(Ns, 3, X), card(X, C))). 740% ?- time(( N=50, numlist(1, N, Ns), zdd((zdd_list_length(Ns, 3, X), card(X, C))))). 741%@ % 251,894,470 inferences, 39.500 CPU in 41.508 seconds (95% CPU, 6377136 Lips) 742%@ C = 125000. 743 744zdd_list_length(L, N, X):- shift(zdd_list_length(L, N, X)). 745% 746zdd_list_length(_, 0, X, S):-!, zdd_singleton([], X, S). 747zdd_list_length(L, N, X, S):- N0 is N-1, 748 zdd_list_length(L, N0, X0, S), 749 zdd_fold_cons(L, X0, 0, X, S). 750% 751zdd_fold_cons(L, X, Y):- shift(zdd_fold_cons(L, X, 0, Y)). 752% 753zdd_fold_cons([], _, Y, Y, _). 754zdd_fold_cons([A|As], Y0, U, Y, S):- 755 map_zdd(cons(A), Y0, V, S), 756 zdd_join(U, V, U0, S), 757 zdd_fold_cons(As, Y0, U0, Y, S). 758 759 760% ?- zdd((X<<{[a], [a,b], [b]}, psa(X), 761% select_singleton(X, Y, U), sets(U, SU), 762% select_singleton(U, V, W), sets(W, SW), 763% select_singleton(W, L, M), sets(M, SM))). 764 765% ?- zdd((X<<{[a,b]}, psa(X), 766% select_singleton(X, Y, U))). 767 768% ?- numlist(1, 500, L), numlist(1, 250, M), maplist(pred([I, J]:- 769% J is I+I), M, M0), zdd((X<<pow(M0), zdd_join(X, X, Y))). 770 771% ?- numlist(1, 5, L), zdd((X<<pow(L), card(X, C))). 772 773% ?- numlist(1, 500, L), numlist(1, 250, M), maplist(pred([I, J]:- 774% J is I+I), M, M0), zdd((X<<pow(M0), Y<<pow(L), 775% zdd_join(X, Y, Z), card(X, Cx), card(Y, Cy), card(Z, Cz))).
781zdd_join(X, Y, Z):- shift(zdd_join(X, Y, Z)). 782% 783zdd_join(0, X, X, _):-!. 784zdd_join(X, 0, X, _):-!. 785zdd_join(X, X, X, _):-!. 786zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S). 787zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S). 788zdd_join(X, Y, Z, S):- 789 ( X@<Y -> memo(zdd_join(X,Y)-Z, S) 790 ; memo(zdd_join(Y, X)-Z, S) 791 ), 792 ( nonvar(Z) -> true %, write(.) 793 ; cofact(X, t(A, L, R), S), 794 cofact(Y, t(A0, L0, R0), S), 795 compare(C, A, A0), 796 ( C = (<) 797 -> zdd_join(L, Y, U, S), 798 cofact(Z, t(A, U, R), S) 799 ; C = (=) 800 -> zdd_join(L, L0, U, S), 801 zdd_join(R, R0, V, S), 802 cofact(Z, t(A, U, V), S) 803 ; zdd_join(L0, X, U, S), 804 cofact(Z, t(A0, U, R0), S) 805 ) 806 ). 807 808% ?- zdd((X<<([a]+[b]+[]), psa(X))). 809% ?- zdd((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))).
813zdd_join_1(X, Y):- shift(zdd_join_1(X, Y)). 814% 815zdd_join_1(X, Y, S):- 816 ( X<2 -> Y = 1 817 ; cofact(X, t(A, L, R), S), 818 zdd_join_1(L, L0, S), 819 cofact(Y, t(A, L0, R), S) 820 ). 821 822 823 824% ?- zdd((X<<[a, b], Y<<[a, b], Z << (X*Y), sets(Z, S))). 825% ?- zdd((X<<[a, a], Y<<[a, b], Z << (X*Y), sets(Z, S))). 826% ?- zdd((X<<[a, b], Y<<[a, b], Z << (X&Y), sets(Z, S))). 827% ?- zdd((X<<([a, b]+[c,d]), Y<<([x,y]+[u,v]), Z << (X&Y), sets(Z, S))). 828% ?- trace, zdd(X=[b, a]). 829% ?- zdd((X<<([a, b]+[c,d]), Y<<([x,y]+[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 830% ?- zdd((X<<[b, a], Y<<[a, b], Z <<(X+Y), sets(Z, S))).
835zdd_meet(X, Y, Z):- shift(zdd_meet(X, Y, Z)). 836 837% 838zdd_meet(0, _, 0, _):-!. 839zdd_meet(_, 0, 0, _):-!. 840zdd_meet(1, X, Y, S):-!, zdd_meet_1(X, Y, S). 841zdd_meet(X, 1, Y, S):-!, zdd_meet_1(X, Y, S). 842zdd_meet(X, X, X, _):-!. 843zdd_meet(X, Y, Z, S):- 844 ( X @< Y -> memo(zdd_meet(X,Y)-Z, S) 845 ; memo(zdd_meet(Y,X)-Z, S) 846 ), 847 ( nonvar(Z) -> true 848 ; cofact(X, t(A, L, R), S), 849 cofact(Y, t(A0, L0, R0), S), 850 compare(C, A, A0), 851 ( C = (<) 852 -> zdd_meet(L, Y, Z, S) 853 ; C = (=) 854 -> zdd_meet(L, L0, U, S), 855 zdd_meet(R, R0, V, S), 856 cofact(Z, t(A, U, V), S) 857 ; zdd_meet(R0, X, Z, S) 858 ) 859 ).
864zdd_meet_1(X, Y):- shift(zdd_meet_1(X, Y)). 865% 866zdd_meet_1(X, X, _):- X<2, !. 867zdd_meet_1(X, Y, S):- cofact(X, t(_,L,_), S), 868 zdd_meet_1(L, Y, S).
873% ?- zdd((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 874zdd_subtr(X, Y, Z):-shift(zdd_subtr(X, Y, Z)). 875% 876zdd_subtr(X, X, 0, _):-!. 877zdd_subtr(0, _, 0, _):-!. 878zdd_subtr(X, 0, X, _):-!. 879zdd_subtr(X, 1, Y, S):-!, zdd_subtr_1(X, Y, S). 880zdd_subtr(1, X, Y, S):-!, 881 ( zdd_has_1(X, S) 882 -> Y = 0 883 ; Y = 1 884 ). 885zdd_subtr(X, Y, Z, S):- memo(zdd_subtr(X,Y)-Z, S), 886 ( nonvar(Z) -> true 887 ; cofact(X, t(A, L, R), S), 888 cofact(Y, t(A0, L0, R0), S), 889 compare(C, A, A0), 890 ( C = (<) 891 -> zdd_subtr(L, Y, U, S), 892 cofact(Z, t(A, U, R), S) 893 ; C = (=) 894 -> zdd_subtr(L, L0, U, S), 895 zdd_subtr(R, R0, V, S), 896 cofact(Z, t(A, U, V), S) 897 ; zdd_subtr(L, L0, U, S), 898 cofact(Y, t(A, U, R), S) 899 ) 900 ).
905% ?- zdd((X<<([]+[a]), zdd_subtr_1(X, Y), psa(Y))). 906% ?- zdd((X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y))). 907% ?- zdd((X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y))). 908zdd_subtr_1(X, Y):-shift(zdd_subtr_1(X, Y)). 909% 910zdd_subtr_1(X, 0, _):- X < 2, !. % empty family or singleton of the empty. 911zdd_subtr_1(X, Y, S):- cofact(X, t(A, L, R), S), 912 zdd_subtr_1(L, L0, S), 913 cofact(Y, t(A, L0, R), S). 914 915 /*************** 916 * merge * 917 ***************/
924% ?- zdd(( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 925zdd_merge(X, Y, Z) :- shift(zdd_merge(X, Y, Z)). 926 927% 928zdd_merge(0, _, 0, _):-!. 929zdd_merge(_, 0, 0, _):-!. 930zdd_merge(1, X, X, _):-!. 931zdd_merge(X, 1, X, _):-!. 932zdd_merge(X, Y, Z, S):- 933 ( X@<Y -> memo(zdd_merge(X,Y)-Z, S) 934 ; memo(zdd_merge(Y,X)-Z, S) 935 ), 936 ( nonvar(Z) -> true 937 ; cofact(Y, t(A, L, R), S), 938 zdd_merge(X, R, U, S), 939 zdd_merge(X, L, V, S), 940 zdd_insert(A, U, U0, S), 941 zdd_join(U0, V, Z, S) 942 ). 943 944 /**************** 945 * divide * 946 ****************/
951% ?- spy(zdd_divide). 952% ?- zdd(( X<< 0, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 953% ?- zdd(( X<< 0, Y<< 0, zdd_divide(X, Y, Z), psa(Z))). 954% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 955% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 956% ?- zdd(( X<<{[a,b]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 957% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_divide(X, Y, Z), psa(Z))). 958% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 959% ?- zdd(( X<<1, Y<<1, zdd_divide(X, Y, Z), psa(Z))). 960% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 961% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_divide(X, Y, Z), psa(Z))). 962% ?- zdd(( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_divide(X, Y, Z), psa(Z))). 963% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_divide(X, Y, Z), psa(Z))). 964% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_divide(X, Y, Z), psa(Z))). 965% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_divide(X, Y, Z), psa(Z))). 966% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_divide(X, Y, Z), psa(Z))). 967% ?- zdd(( X<<{[c]}, Y<<{[a, c]}, zdd_divide(X, Y, Z), psa(Z))). 968% ?- zdd(( X<<{[a]}, Y<<{[a, b]}, zdd_divide(X, Y, Z), psa(Z))). 969% ?- zdd(( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_divide(X, Y, Z), psa(Z))). 970% ?- zdd(( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_divide(X, Y, Z), psa(Z))). 971% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_divide(X, Y, Z), psa(Z))). 972% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_divide(X, Y, Z), psa(Z))). 973% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_divide(X, Y, Z), psa(Z))). 974 975zdd_divide(X, Y, Z) :- shift(zdd_divide(X, Y, Z)). 976 977% 978zdd_divide(0, _, 0, _):-!. 979zdd_divide(_, 0, 0, _):-!. 980zdd_divide(1, X, Y, S):-!, 981 ( zdd_has_1(X, S) 982 -> Y = 1 983 ; Y = 0 984 ). 985zdd_divide(X, 1, X, _):-!. 986zdd_divide(X, Y, Z, S):- 987 memo(zdd_divide(X, Y)- Z, S), 988 ( nonvar(Z) -> true 989 ; cofact(X, t(A, L, R), S), 990 cofact(Y, t(A0, L0, R0), S), 991 compare(C, A, A0), 992 ( C = (=) 993 -> zdd_divide(R, R0, Z0, S), 994 zdd_divide(R, L0, Z1, S), 995 zdd_insert(A, Z1, Z2, S), 996 zdd_divide(L, L0, Z3, S), 997 zdd_join(Z0, Z2, Z4, S), 998 zdd_join(Z3, Z4, Z, S) 999 ; C = (<) 1000 -> zdd_divide(R, Y, Z0, S), 1001 zdd_insert(A, Z0, Z1, S), 1002 zdd_divide(L, Y, Z2, S), 1003 zdd_join(Z1, Z2, Z, S) 1004 ; zdd_divide(X, L0, Z, S) 1005 ) 1006 ). 1007 1008% ?- zdd(( X<<{[a, b], [a, c]}, zdd_div_by_list(X, [b], Z), psa(Z))). 1009% ?- zdd(( X<<{[a, b], [c, d]}, zdd_div_by_list(X, [b], Z), psa(Z))). 1010% ?- zdd(( X<<{[a, b, c], [a, b, d]}, zdd_div_by_list(X, [b], Z), psa(Z))). 1011% 1012zdd_div_by_list(X, Y, Z):- shift(zdd_div_by_list(X, Y, Z)). 1013% 1014zdd_div_by_list(X, As, Y, S):- zdd_append(As, 1, D, S), 1015 zdd_divide(X, D, Y, S). 1016 1017 1018 1019 /***************** 1020 * residue * 1021 *****************/ 1022 1023% ?- zdd(( X<< 0, Y<<{[a]}, zdd_residue(X, Y, Z), psa(Z))). 1024% ?- zdd(( X<< 0, Y<< 0, zdd_residue(X, Y, Z), psa(Z))). 1025% ?- zdd(( X<<{[a, b]}, Y<<{[a, c]}, zdd_residue(X, Y, Z), psa(Z))). 1026% ?- zdd(( X<<{[a, b], [b, c]}, Y<<{[a, c]}, zdd_residue(X, Y, Z), psa(Z))). 1027% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a, c]}, zdd_residue(X, Y, Z), psa(Z))). 1028% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_residue(X, Y, Z), psa(Z))). 1029% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_residue(X, Y, Z), psa(Z))). 1030% ?- zdd(( X<<1, Y<<1, zdd_residue(X, Y, Z), psa(Z))). 1031% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_residue(X, Y, Z), psa(Z))). 1032% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_residue(X, Y, Z), psa(Z))). 1033% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_residue(X, Y, Z), psa(Z))). 1034% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_residue(X, Y, Z), psa(Z))). 1035 1036 1037 1038% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_residue(X, Y, Z), psa(Z))). 1039% ?- zdd(( X<<{[a, b]}, Y<<{[a, c]}, zdd_residue(X, Y, Z), psa(Z))). 1040% ?- zdd(( X<<{[a], [b]}, Y<<{[b]}, zdd_residue(X, Y, Z), psa(Z))). 1041% ?- zdd(( X<<{[a, c], [b]}, Y<<{[b]}, zdd_residue(X, Y, Z), psa(Z))). 1042%@ Z = 3. 1043 1044%@ true. 1045%@ zdd.pl qcompiled. 1046 1047zdd_residue(X, Y, Z) :- shift(zdd_residue(X, Y, Z)). 1048 1049% 1050zdd_residue(0, _, 0, _):-!. 1051zdd_residue(_, 1, 0, _):-!. 1052zdd_residue(X, 0, X, _):-!. 1053zdd_residue(X, X, 0, _):-!. 1054zdd_residue(1, _, 1, _):-!. 1055zdd_residue(X, Y, Z, S):- 1056 memo(zdd_residue(X, Y)- Z, S), 1057 ( nonvar(Z) -> true 1058 ; cofact(X, t(A, L, R), S), 1059 cofact(Y, t(A0, L0, R0), S), 1060 compare(C, A, A0), 1061 ( C = (=) 1062 -> zdd_residue(R, R0, Z0, S), 1063 zdd_insert(A, Z0, Z1, S), 1064 zdd_join(L, Z1, Z2, S), 1065 zdd_residue(Z2, L0, Z, S) 1066 ; C = (<) 1067 -> zdd_residue(R, Y, R1, S), 1068 zdd_insert(A, R1, Z0, S), 1069 zdd_residue(L, Y, Z1, S), 1070 zdd_join(Z0, Z1, Z, S) 1071 ; zdd_residue(X, L0, Z, S) 1072 ) 1073 ). 1074 1075zdd_res_by_list(X, Y, Z):- shift(zdd_res_by_list(X, Y, Z)). 1076% 1077zdd_res_by_list(X, As, Y, S):- zdd_append(As, 1, D, S), 1078 zdd_residue(X, D, Y, S). 1079 1080 1081 /********************* 1082 * meta on ZDD * 1083 *********************/ 1084 1085% ?- zdd((X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 1086% ?- zdd((X<<pow([1,2,4,5,6]), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 1087% ?- N=2, numlist(1, N, L), zdd((X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 1088% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 1089% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 1090% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 1091% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N. 1092% ?- N=1000, numlist(1, N, L), zdd((X<<pow(L), 1093% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N.
map_zdd(F, X, Y) works roughly like
maplist(maplist(F), X, Y)) with a list X of lists.
1102:- meta_predicate map_zdd(,,). 1103map_zdd(F, X, Y):- shift(map_zdd(F, X, Y)). 1104:- meta_predicate map_zdd(,,,). 1105map_zdd(F, X, Y, S):- zdd_shift(map_zdd(F, X, Y, S)). 1106 1107:- meta_predicate map_zdd(,,,,). 1108map_zdd(_, X, X, _, _):- X<2, !. 1109map_zdd(F, X, Y, S, M):- memo(map(X,F)-Y, M), 1110 ( nonvar(Y)-> true 1111 ; cofact(X, t(A, L, R), S), 1112 map_zdd(F, L, L0, S, M), 1113 map_zdd(F, R, R0, S, M), 1114 call(F, A, B), 1115 zdd_insert(B, R0, R1, S), 1116 zdd_join(L0, R1, Y, S) 1117 ). 1118 1119% ?- zdd((X<<pow([a,b]), map_zdd0(=, X,Y))). 1120% ?- zdd((X<<pow([a,b]), map_zdd0(==, X,Y), psa(X))).
1125:- meta_predicate map_zdd0(,,). 1126map_zdd0(F, X, Y):- shift(map_zdd0(F, X, Y)). 1127:- meta_predicate map_zdd0(,,,). 1128map_zdd0(F, X, Y, S):-zdd_shift(map_zdd0(F, X, Y, S)). 1129 1130:- meta_predicate map_zdd(,,,,). 1131map_zdd0(_, X, X, _, _):- X<2, !. 1132map_zdd0(F, X, Y, S, M):- memo(map(X,F)-Y, M), 1133 ( nonvar(Y)-> true 1134 ; cofact(X, t(A, L, R), S), 1135 map_zdd0(F, L, L0, S, M), 1136 ( call(F, A, B) 1137 -> map_zdd0(F, R, R0, S, M), 1138 zdd_insert(B, R0, R1, S) 1139 ; R1 = 0 1140 ), 1141 zdd_join(L0, R1, Y, S) 1142 ). 1143 1144 1145 1146% ?- zdd((memo(a-1), setmemo(a-2), memo(a-V))). 1147% ?- zdd((X<<pow([a,b,c,d]), prz(X))). 1148% ?- zdd((X<<pow([a,b,c]), psa(X))). 1149% ?- zdd((prz(1))). 1150% ?- zdd((prz(0))). 1151 1152prz(X):- print_set_at(X). 1153pzm(X):- print_zdd_matrix(X). 1154 1155% 1156psa(X):- print_set_at(X). 1157psa(X, S):- print_set_at(X, S). 1158% 1159print_set_at(X):- shift(print_set_at(X)). 1160print_set_at(0, _):-!, nl, writeln(0). 1161print_set_at(1, _):-!, nl, writeln([]). 1162print_set_at(X, S):- format("\nzdd ~w:", [X]), 1163 forall(set_at(P, X, S), format("\n\t~w", [P])). 1164% 1165 1166% ?- zdd((X<<(set([1-2, 2-3, 3-4])+ set([1-2,2-3])), set_at(U, X))). 1167% ?- zdd((X<<pow([1,2]), set_at(U, X))). 1168set_at(P, X):- shift(set_at(P, X)). 1169% 1170set_at([], 1, _):-!. 1171set_at(P, X, S):- 1172 cofact(X, t(A, L, R), S), 1173 ( set_at(P, L, S) 1174 ; set_at(As, R, S), 1175 P=[A|As] 1176 ). 1177% 1178sets(X, P):- shift(sets(X, P)). 1179 1180sets(X, Y, S):- zdd_sets(X, Y, S). 1181% 1182 1183zdd_sets(1, [[]], _):-!. 1184zdd_sets(0, [], _):-!. 1185zdd_sets(X, P, S):- 1186 cofact(X, t(A,L,R), S), 1187 zdd_sets(L, Y, S), 1188 zdd_sets(R, Z, S), 1189 maplist(cons(A), Z, AZ), 1190 maplist(sort, AZ, AZ0), 1191 sort(AZ0, AZ1), 1192 union(Y, AZ1, P). 1193% 1194ppoly(X):- @(ppoly(X)). 1195 1196ppoly(X, S):- poly_term(X, Poly, S), 1197 writeln(Poly). 1198 1199%@ true. 1200%@ zdd.pl qcompiled. 1201 1202% ?- zdd((X<<pow([a,b]), poly_term(X, P))). 1203% 1204poly_term(X, Poly):- @(poly_term(X, Poly)). 1205% 1206poly_term(X, Poly, S):-zdd_sets(X, Sets, S), 1207 maplist(sort, Sets, Sets0), 1208 sort(Sets0, Sets1), 1209 poly_term0(Sets1, Poly). 1210 1211% ?- poly_term0([], Y). 1212% ?- poly_term0([[]], Y). 1213% ?- poly_term0([[a], [b]], Y). 1214% ?- poly_term0([[a*b], [c]], Y). 1215 1216poly_term0(X, Y):- maplist(mul_term, X, X0), 1217 sum_term(X0, Y). 1218% 1219mul_term([], [[]]):-!. 1220mul_term([X], X):-!. 1221mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 1222% 1223sum_term([], []):-!. 1224sum_term([X], X):-!. 1225sum_term([X, Y|Xs], Z):-sum_term([X+Y|Xs], Z).
1231famset(X, P):- shift(zdd_sets(X, P)).zdd((X<< pow([a,b,c]), zdd_path(X))).
?- zdd((prepare_sat(4), memo(filter(4)-X), zdd_path(X))).1237zdd_path(I) :- shift(zdd_path(I)). 1238% 1239zdd_path(I, S):- get_vector(Vec, S), 1240 ( zdd_path(I, P, [], Vec), 1241 writeln(P), 1242 fail 1243 ; true 1244 ). 1245% 1246zdd_path(true, X, X, _):-!. 1247zdd_path(I, X, Y, Vec):- integer(I), 1248 arg(I, Vec, if(A, L, R)), 1249 ( X = [A|X0], 1250 zdd_path(L, X0, Y, Vec) 1251 ; zdd_path(R, X, Y, Vec) 1252 ). 1253 1254% ?- zdd((X << [a, b, c], zdd_rand_path(X))). 1255% ?- zdd((X << pow([a, b, c]), zdd_rand_path(X))). 1256% ?- zdd((X << {[a], [b], [c]}, zdd_rand_path(X))). 1257% ?- zdd((X << pow([a, b, c, d, e, f, g]), zdd_rand_path(X))).
1261zdd_rand_path(I):- shift(zdd_rand_path(I)). 1262% 1263zdd_rand_path(I, S):- zdd_rand_path(I, P, [], S), writeln(P). 1264% 1265zdd_rand_path(1, X, X, _):-!. 1266zdd_rand_path(I, X, Y, S):- I>1, 1267 cofact(I, t(A, L, R), S), 1268 ( L == 0 1269 -> X = [A|X0], 1270 zdd_rand_path(R, X0, Y, S) 1271 ; random(2) =:= 0 1272 -> X = [A|X0], 1273 zdd_rand_path(R, X0, Y, S) 1274 ; zdd_rand_path(L, X, Y, S) 1275 ). 1276 1277% ?- zdd((X<<[a], zdd_nodes(X, N))). 1278% ?- N=10, numlist(1, N, Ns), zdd((X<<pow(Ns), zdd_nodes(X, U))). 1279% ?- N=10000, numlist(1, N, Ns), time(zdd((X<<pow(Ns), zdd_nodes(X, U)))), length(U, Len). 1280%@ % 350,941,340 inferences, 18.703 CPU in 19.647 seconds (95% CPU, 18763903 Lips)
1286zdd_nodes(X, P):- shift(zdd_nodes(X, P)). 1287% 1288zdd_nodes(X, P, S):- zdd_shift(zdd_nodes(X, P, S)). 1289 1290% 1291zdd_nodes(X, [], _, _):- X<2, !. 1292zdd_nodes(X, P, S, M):- memo(nodes(X)-P, M), 1293 ( nonvar(P) -> true 1294 ; cofact(X, t(_, L, R), S), 1295 zdd_nodes(L, Nl, S, M), 1296 zdd_nodes(R, Nr, S, M), 1297 ord_union([Nl, [X], Nr], P) 1298 ). 1299 1300% ?- zdd((zdd_atoms(1, S))). 1301% ?- zdd((family([[a,b],[b,c]], X), zdd_atoms(X, S))). 1302% ?- N = 10000, time(zdd(({numlist(1, N, L)}, X<<power(L), zdd_atoms(X, S)))). 1303%@ % 200,887,717 inferences, 9.620 CPU in 10.312 seconds (93% CPU, 20883111 Lips)
1308zdd_atoms(X, P):- shift(zdd_atoms(X, P)). 1309 1310zdd_atoms(X, P, S):-zdd_shift(zdd_atoms(X, P, S)). 1311 1312% 1313zdd_atoms(X, [], _, _):- X<2, !. 1314zdd_atoms(X, P, S, M):- memo(atoms(X)-P, M), 1315 ( nonvar(P) -> true 1316 ; cofact(X, t(A, L, R), S), 1317 zdd_atoms(L, Al, S, M), 1318 zdd_atoms(R, Ar, S, M), 1319 ord_union(Al,Ar, P0), 1320 P=[A|P0] 1321 ). 1322 1323% ?- collect(pred([a-_]), [a-b, c-d, a-e], L). 1324 1325% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 1326:- meta_predicate delete(, , ). 1327delete(X, Y, Z):- delete(X, Y, Z, []). 1328 1329:- meta_predicate delete(, , , ). 1330delete(_, [], L, L). 1331delete(Pred, [X|Xs], L, L0):- 1332 ( call(Pred, X) 1333 -> delete(Pred, Xs, L, L0) 1334 ; L = [X|L1], 1335 delete(Pred, Xs, L1, L0) 1336 ). 1337 1338% ?- zdd((zdd_power([a,b], R), sets(R, U))). 1339% ?- zdd((zdd_power(charlist(a-c), R), sets(R, U))). 1340% ?- zdd((R<< pow(charlist(a-d)), card(R, C))). 1341zdd_power(X, Y):- shift(zdd_power(X, Y)). 1342% 1343zdd_power(X, Y, S):- is_list(X), !, 1344 sort(X, X0), 1345 zdd_ord_power(X0, Y, S). 1346% 1347zdd_power(X, Y, S):- callable(X), !, call(X, X0), 1348 zdd_power(X0, Y, S). 1349 1350% ?- concat_atom([a, b], C). 1351% ?- atom_concat(a, b, C). 1352% ?- atomlist(ax(1+1, 3+1), As). 1353% ?- atomlist(ax(1, 3), As). 1354% ?- atomlist(ax(1..3), As). 1355 1356atomlist(X, As):- X=..[A|B], 1357 ( B = [I..J]; B = [I, J] ), !, 1358 I0 is I, 1359 J0 is J, 1360 findall(Y, ( between(I0, J0, K), 1361 atom_concat(A, K, Y) 1362 ), 1363 As). 1364 1365% ?- charlist(a-c, X). 1366charlist(A-B, I):- 1367 findall(X, ( char_type(X, alnum), 1368 X @>= A, 1369 X @=< B 1370 ), 1371 I). 1372% ?- charlist(a, c, X). 1373charlist(A, B, I):- charlist(A-B, I). 1374 1375% 1376zdd_ord_power([], 1, _). 1377zdd_ord_power([X|Xs], P, S):- zdd_ord_power(Xs, Q, S), 1378 cofact(P, t(X, Q, Q), S). 1379 1380% ?- zdd((ltr_sort([-a, a, -b, b], L), ltr_power(L, P), card(P, C))). 1381% ?- zdd((X<<ltr_pow([a,b]), S<<sets(X), C<<card(X))). 1382% ?- zdd((L<<ltr_pow([-a, -b]), C<<card(L))). 1383% ?- zdd((L<<ltr_pow([-a, a, -b, b]), U<<sets(L))). 1384% ?- zdd((L<<ltr_pow([-a, a, -b, b]))). 1385% ?- zdd((L<<ltr_pow([-a, b]), psa(L))). 1386% ?- zdd((L<<ltr_pow([]), psa(L))). 1387 1388% ?- zdd((X<<pow([a,b]), powerzdd(X, Y), powerzdd(Y, Z), card(Z, C))). 1389%% powerzdd(+X, -Y) is det. 1390% Unify Y with the powerZDD of a ZDD X, i.e., 1391% the powerset of nodes of a ZDD X. 1392% powerzdd(X, Y):- powerzdd(X, Y, rozdd). 1393% 1394powerzdd(X, Y):- shift(powerzdd(X, Y)). 1395 1396powerzdd(X, Y, S):- cofact(False, if(p(false), true, true), S), 1397 cofact(A, if(p(true), False, False), S), 1398 powerzdd(X, A, Y, S). 1399 1400% 1401powerzdd(true, Pow, Pow, _):-!. 1402powerzdd(false, Pow, Pow, _):-!. 1403powrzdd(I, Pow, P, S):- memo(pow(I)-P, S), 1404 ( nonvar(P) -> true 1405 ; cofact(I, if(_, L, R), S), 1406 powerzdd(L, Pow, Pow0, S), 1407 powerzdd(R, Pow0, Q, S), 1408 cofact(P, if(p(I), Q, Q), S) 1409 ). 1410 1411% ?- zdd((dnf(A+B, X), get_key(varnum, N), extern(X, Y), X==Y)). 1412% ?- zdd((dnf(X->Y, U), sets(U, V), extern(V, A))).
1417extern(X, Y):-shift(extern(X,Y)). 1418 1419extern(X, Y, S):- get_key(varzip, Zip, S), 1420 subst_opp(X, Y, Zip). 1421 1422% ?- count_atomic_prop(a+b, 0-C, atomic_prop). 1423% ?- count_atomic_prop(a+b+c+a+A, 0-C, atomic_prop). 1424 1425:- meta_predicate count_atomic_prop(, , ). 1426count_atomic_prop(X, Y, Z):- zdd_shift(count_atomic_prop(X, Y, Z)). 1427% 1428count_atomic_prop(X, C-C, _, _):- var(X), !. 1429count_atomic_prop(X, C-D, Pred, S):- call(Pred, X), !, 1430 memo(atomic_prop(X)-B, S), 1431 ( nonvar(B) 1432 -> D = C 1433 ; D is C+1, 1434 B = true 1435 ). 1436count_atomic_prop([], C-C, _, _):-!. 1437count_atomic_prop([X|Y], C-D, Pred, S):-!, 1438 count_atomic_prop(X, C-C0, Pred, S), 1439 count_atomic_prop(Y, C0-D, Pred, S). 1440count_atomic_prop(X, P, Pred, S):- compound(X), !, 1441 X =..[_|As], 1442 count_atomic_prop(As, P, Pred, S). 1443count_atomic_prop(_, C-C, _, _). 1444 1445% ?- term_atoms(a+b=c, L). 1446% ?- term_atoms(a+b, L). 1447% ?- term_atoms(f(a+a), L).
1453term_atoms(X, L):- term_atoms(X, L0, []), 1454 sort(L0, L). 1455 1456% 1457term_atoms(X, L, L):- var(X), !. 1458term_atoms(X, [X|L], L):- atom(X), !. 1459term_atoms([X|Y], L, L0):-!, 1460 term_atoms(X, L, L1), 1461 term_atoms(Y, L1, L0). 1462term_atoms(X, L, L0):- compound(X), !, 1463 X =..[_|As], 1464 term_atoms(As, L, L0). 1465term_atoms(_, L, L). 1466 1467% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 1468% ?- subst_opp(a, X, [b-a]). 1469% ?- subst_opp([a], X, [b-a]). 1470 1471subst_opp(X, Y, L):- memberchk(Y-X, L). 1472subst_opp([X|Y], [X0|Y0], L):-!, 1473 subst_opp(X, X0, L), 1474 subst_opp(Y, Y0, L). 1475subst_opp(X, Y, L):- compound(X), !, 1476 X =..[F|As], 1477 subst_opp(As, Bs, L), 1478 Y =..[F|Bs]. 1479subst_opp(X, X, _). 1480 1481% ?- subst_term(f(a), R, [a-b]). 1482% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 1483% ?- subst_term(f(a), R, [a-X]). 1484% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 1485% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 1486% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
1492subst_term(X, Y, S):- member(X0-Y, S), X0==X, !. 1493subst_term(A, B, S):- compound(A), !, 1494 ( A = [X|Y] 1495 -> B = [X0|Y0], 1496 subst_term(X, X0, S), 1497 subst_term(Y, Y0, S) 1498 ; functor(A, F, N), 1499 functor(B, F, N), 1500 subst_term(N, A, B, S) 1501 ). 1502subst_term(X, X, _). 1503% 1504subst_term(0, _, _, _):-!. 1505subst_term(I, X, Y, S):- 1506 arg(I, X, A), 1507 arg(I, Y, B), 1508 subst_term(A, B, S), 1509 J is I - 1, 1510 subst_term(J, X, Y, S). 1511 1512% ?- all_instances([a,b], [0,1], a+b=b, R). 1513% ?- all_instances([x,y], [0,1], x+y=x, R). 1514%% all_instances(+As, +Vs, +X, -Y) is det. 1515% Unify Y with the list of possible variations P of X, 1516% where P is a variation of X if for each A in As with some 1517% V in Vs which depends on A, P is obtained from X by replacing 1518% all occurrences of A appearing in X with V for A in As. 1519 1520all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 1521 apply_maps(Fs, X, Y, []). 1522% 1523apply_maps([], _, Y, Y). 1524apply_maps([F|Fs], X, [X0|Y], Z):- 1525 subst_term(X, X0, F), 1526 apply_maps(Fs, X, Y, Z). 1527 1528% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 1529% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 1530% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 1531% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 1532%% mod_table(+M, +X, +E, -T) is det. 1533% Unify T with a set of form E' = V where 1534% E' is a possible ground instance of an integer expression E 1535% and V is the value of E' with modulo M, where X is a set of 1536% parameters appearing in E. 1537 1538mod_table(M, Xs, Exp, Table):- M0 is M-1, 1539 numlist(0, M0, V), 1540 all_instances(Xs, V, Exp, Exps), 1541 !, 1542 maplist(mod_arith(M), Exps, Table). 1543% 1544mod_arith(M, Exp, Exp=V):- V is Exp mod M. 1545 1546% 1547unify_all([]). 1548unify_all([_]). 1549unify_all([X,Y|Z]):- zdd:(X=Y), unify_all([Y|Z]). 1550 1551% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1552% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1553% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1554% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1555% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1556% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1561zdd_subfamily(X, Y):- shift(zdd_subfamily(X, Y)). 1562% 1563zdd_subfamily(X, Y, S):-zdd_shift(zdd_subfamily(X, Y, S)). 1564 1565% 1566zdd_subfamily(X, X, _, _):-!. 1567zdd_subfamily(0, _, _, _):-!. 1568zdd_subfamily(_, 0, _, _):-!, fail. 1569zdd_subfamily(1, X, S, _):-!, zdd_has_1(X, S). 1570zdd_subfamily(X, X0, S, M):- memo(subfamily(X, X0)-B, M), 1571 ( nonvar(B) -> true 1572 ; cofact(X, t(A, L, R), S), 1573 cofact(X0, t(A0, L0, R0), S), 1574 compare(C, A, A0), 1575 ( C = (=) 1576 -> zdd_subfamily(L, L0, S, M), 1577 zdd_subfamily(R, R0, S, M), 1578 B = true 1579 ; C = (>), 1580 zdd_subfamily(X, L0, S, M) 1581 ) 1582 ).
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))).1590zdd_appear(A, X):- shift(zdd_appear(A, X)). 1591zdd_appear(A, X, S):- zdd_shift(zdd_appear(A, X, S)). 1592 1593% 1594zdd_appear(A, X, S, M):- X > 1, 1595 memo(visited(X)-B, M), 1596 var(B), 1597 cofact(X, t(U,L,R), S), 1598 compare(C, A, U), 1599 ( C = (=) 1600 -> true 1601 ; C = (>), 1602 ( zdd_appear(A, L, S, M) -> true 1603 ; L < 2 1604 -> zdd_appear(A, R, S, M) 1605 ; memo(visited(L)-true, M), % for earlier fail. 1606 zdd_appear(A, R, S, M) 1607 ) 1608 ).
1614% ?- N=10, time((numlist(1, N, L), zdd((X=pow(L), zdd_count_nodes(X, C))))). 1615zdd_count_nodes(X, C):- shift(zdd_count_nodes(X, C)). 1616 1617zdd_count_nodes(X, C, S):- intermediate_nodes(X, [], L, S), 1618 length(L, C). 1619% 1620intermediate_nodes(I, X, Y, S):-integer(I), !, 1621 ( memberchk(I, X) -> Z = X; Z = [I|X] ), 1622 cofact(I, if(_, L, R), S), 1623 intermediate_nodes(L, Z, Z0, S), 1624 intermediate_nodes(R, Z0, Y, S). 1625intermediate_nodes(_, X, X, _). 1626 1627% 1628map_singleton([], [], _). 1629map_singleton([X|Xs], [Y|Ys], S):- zdd_singleton(X, Y, S), 1630 map_singleton(Xs, Ys, S).
listing(zdd_singleton).1636zdd_singleton(X, P):- shift(zdd_singleton(X, P)). 1637% 1638zdd_singleton(X, P, S):- cofact(P, t(X, 0, 1), S).
1644zdd_meet_t(X, Y):- shift(zdd_meet_t_(X, Y)). 1645% 1646zdd_meet_t_(false, false, _):-!. 1647zdd_meet_t_(true, true, _):-!. 1648zdd_meet_t_(I, K, S):- cofact(I, if(_, _, V), S), 1649 zdd_meet_t_(V, K, S).
1656zdd_meet_t(X, Y, Z):- shift(zdd_meet_t(X, Y, Z)). 1657% 1658zdd_meet_t(_, false, false, _):-!. 1659zdd_meet_t(_, true, true, _):-!. 1660zdd_meet_t(H, I, K, S):- cofact(I, if(J, _, V), S), 1661 ( H @< J -> K = I 1662 ; zdd_meet_t(H, V, K, S) 1663 ).
1670zdd_meet_p(X, Y, Z):- shift(zdd_meet_p(X, Y, Z)). 1671% 1672zdd_meet_p(_, true, false, _). % assuming H is not max. 1673zdd_meet_p(_, false, false, _). 1674zdd_meet_p(H, X, Y, S):- cofact(X, if(I, L, R), S), 1675 ( H @=< I -> zdd_rm_1(R, R0, S), 1676 cofact(Y, if(I, L, R0), S) 1677 ; zdd_meet_p(H, R, Y, S) 1678 ).
1684zdd_has_1(X):- shift(zdd_has_1(X)). 1685% 1686zdd_has_1(1, _):-!. 1687zdd_has_1(X, S):- X>1, 1688 cofact(X, t(_, L, _), S), 1689 zdd_has_1(L, S). 1690 1691 1692% ?- zdd((X<< set([a,b]), Y<<set([]), zdd_merge_line(X, Y, Z), psa(Z))). 1693% ?- zdd((X<< set([a,c]), Y<< set([b, d, e]), zdd_merge_line(X, Y, Z), psa(Z))). 1694% ?- zdd((X<< set([a,b,c]), Y<< set([d,e,f]), psa(X), psa(Y), zdd_merge_line(X, Y, Z), psa(Z))). 1695% ?- zdd((X<<set([a,d,c]), Y<<set([d,b,e]), zdd_merge_line(X, Y, Z), psa(Z))). 1696% ?- zdd((X<<set([c, a, d,c]), Y<<set([d,b,e, d]), zdd_merge_line(X, Y, Z), psa(Z))). 1697 1698% special version of zdd_merge, only for linear ZDD. 1699zdd_merge_line(X, Y, Z):- shift(zdd_merge_line(X, Y, Z)). 1700 1701zdd_merge_line(X, X, X, _):-!. % idempotent (only for line version). 1702zdd_merge_line(0, _, 0, _):-!. 1703zdd_merge_line(_, 0, 0, _):-!. 1704zdd_merge_line(1, X, X, _):-!. 1705zdd_merge_line(X, 1, X, _):-!. 1706zdd_merge_line(X, Y, Z, S):- cofact(X, t(A, _, R), S), 1707 cofact(Y, t(A0, _, R0), S), 1708 compare(C, A, A0), 1709 ( C = (<) 1710 -> zdd_merge_line(R, A0, R0, Z0, S), 1711 cofact(Z, t(A, 0, Z0), S) 1712 ; C = (=) 1713 -> zdd_merge_line(R, R0, Z0, S), 1714 cofact(Z, t(A, 0, Z0), S) 1715 ; zdd_merge_line(R0, A, R, Z0, S), 1716 cofact(Z, t(A0, 0, Z0), S) 1717 ). 1718 1719% 1720zdd_merge_line(0, _, _, 0, _):-!. 1721zdd_merge_line(1, A, R, Z, S):-!, cofact(Z, t(A, 0, R), S). 1722zdd_merge_line(X, A, R, Z, S):- cofact(X, t(B, _, R0), S), 1723 compare(C, A, B), 1724 ( C = (<) 1725 -> zdd_merge_line(R, B, R0, Z0, S), 1726 cofact(Z, t(A, 0, Z0), S) 1727 ; C = (=) 1728 -> zdd_merge_line(R, R0, Z0, S), 1729 cofact(Z, t(A, 0, Z0), S) 1730 ; zdd_merge_line(R0, A, R, Z0, S), 1731 cofact(Z, t(B, 0, Z0), S) 1732 ). 1733 1734 1735% ?- zdd((zdd_line([-a, b], X))). 1736% ?- zdd((X<<zdd(zdd_line([-a, b])), psa(X))). 1737 1738% build line zdd for an unsorted list as it it. 1739zdd_line(X, Y):- shift(zdd_line(X, Y)). 1740% 1741zdd_line([], 1, _). 1742zdd_line([A|As], X, S):- zdd_line(As, X0, S), 1743 cofact(X, t(A, 0, X0), S). 1744 1745 1746 1747% ?- zdd((U<<[x, y, z], P<<[a, b], zdd_subst(a, U, P, Q), psa(Q))). 1748% ?- zdd((U<<pow([a,b]), P<<pow([x,y]), zdd_subst(x, U, P, Q), psa(Q))). 1749zdd_subst(X, U, P, Q):- shift(zdd_subst(X, U, P, Q, [])). 1750% 1751zdd_subst(_, _, false, false, _, _):-!. 1752zdd_subst(_, _, true, true, _, _):-!. 1753zdd_subst(X, U, P, Q, As, S):- 1754 cofact(P, if(Y, L, R), S), 1755 ( X == Y 1756 -> zdd_merge(U, L, UL, S), 1757 zdd_join(UL, R, ULR, S), 1758 zdd_inserts(As, ULR, Q, S) 1759 ; zdd_subst(X, U, L, L0, [Y|As], S), 1760 zdd_subst(X, U, R, R0, As, S), 1761 zdd_join(L0, R0, Q, S) 1762 ). 1763 /*********************** 1764 * product on zdd * 1765 ***********************/ 1766 1767 1768% ?- zdd((X<<[a,b], Y<<[c,d], Z<<(X**Y), card(Z, C), sets(Z, S))). 1769% ?- zdd((X<<[a], Y<<([c]+[e]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1770% ?- zdd((X<<[a], Y<<[c], Z<<(X**Y), card(Z, C), sets(Z, S))). 1771% ?- zdd((X << 0, Y<<[c], Z<<(X**Y), card(Z, C), sets(Z, S))). 1772% ?- zdd((X<<[a], Y<<0, Z<<(X**Y), card(Z, C), sets(Z, S))). 1773% ?- zdd((X<<[a,b], Y<<([c]+[e]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1774% ?- zdd((X<<[a,b], Y<<([c,d]+[e,f]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1775% ?- zdd((X<<{[1, 2],[3,4]}, Y<<([c,d]+[e,f]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1776% ?- zdd((X<<[a], Y<<([c,d]+[e,f]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1777% ?- zdd((X<<pow([a,b]), Y<<pow([c,d]), Z<<(X**Y), card(Z, C), sets(Z, S))). 1778% ?- numlist(1, 16, R), time(zdd((X<<pow(R), Y<<pow(R), Z<<(X**Y), card(Z, C)))) 1779% ?- call_with_time_limit(100, (numlist(1, 10, R), time(zdd((X<<pow(R), Y<<pow(R), Z<<(X**Y), card(Z, C)))))). 1780 1781 1782% ?- call_with_time_limit(120, (numlist(1, 16, R), 1783% time(zdd((X<<pow(R), Z<<(X**X), card(Z, C)))))). 1784%@ % 134,889,120 inferences, 9.751 CPU in 9.754 seconds (100% CPU, 13832978 Lips) 1785 1786%@ X = 17, 1787%@ Z = 4369, 1788%@ C = 1048561. 1789 1790zdd_product(X, Y, Z):- shift(zdd_product(X, Y, Z)). 1791% 1792zdd_product(X, Y, 0, _):- (X<2; Y<2), !. 1793zdd_product(X, Y, Z, S):- memo(prod(X, Y)-Z, S), 1794 ( nonvar(Z) -> true 1795 ; fold_product(X, Y, [], Lpath, 0, Z0, S), 1796 attach_handle(X, Lpath, Z1, S), 1797 zdd_join(Z0, Z1, Z, S) 1798 ). 1799% 1800fold_product(_, X, P, P, Z, Z, _):- X<2, !. 1801fold_product(X, Y, P, Q, U, V, S):- cofact(Y, t(B, L, R), S), 1802 zdd_product(X, L, L0, S), 1803 zdd_join(L0, U, U0, S), 1804 fold_product(X, R, [B|P], Q, U0, V, S). 1805% 1806attach_handle(X, _, X, _):- X<2, !. 1807attach_handle(X, P, U, S):- cofact(X, t(A, L, R), S), 1808 attach_handle(R, P, R0, S), 1809 attach_handle(L, P, L0, S), 1810 pairs_insert(A, P, R0, R1, S), 1811 zdd_join(L0, R1, U, S). 1812 1813% 1814pairs_insert(_, [], U, U, _):-!. 1815pairs_insert(A, [B|Bs], U, V, S):- 1816 zdd_insert((A,B), U, U0, S), 1817 pairs_insert(A, Bs, U0, V, S). 1818 1819 /************************* 1820 * Quotient on ZDD * 1821 *************************/ 1822 1823% ?- zdd((X= {[1,2],[3,4]}, zdd_unify(X, [1=2, 3=4, 3=2], Y), sets(Y, S))). 1824% ?- zdd((X= {[1,2],[2,3]}, zdd_unify(X, [3=2], Y), sets(Y, S))).
1830zdd_quotient(X, Y, Z):- shift(zdd_quotient(X, Y, Z)). 1831 1832zdd_quotient(X, _, X, _):- X<2, !. 1833zdd_quotient(X, [], X, _):- !. 1834zdd_quotient(X, Q, Y, S):- cofact(X, t(A, L, R), S), 1835 zdd_quotient(L, Q, L0, S), 1836 zdd_quotient(R, Q, R0, S), 1837 representative(A, Q, A0), 1838 zdd_insert(A0, L0, L1, S), 1839 zdd_join(L1, R0, Y, S). 1840 1841% ?- representative(b, [[a,b]], R). 1842representative(A, Q, R):- 1843 ( member(B, Q), 1844 memberchk(A, B), 1845 B = [R|_] 1846 -> true 1847 ; R = A 1848 ). 1849 1850% ?- zdd((zdd_map([a], [0,1], M), sets(M, S))). 1851% ?- zdd((zdd_map([a,b], [0], M), sets(M, S))). 1852% ?- zdd((zdd_map([a,b], [0,1], M), sets(M, S))). 1853% ?- zdd((zdd_map([], [0,1], M), sets(M, S))). 1854% ?- zdd((zdd_map([a], [], M), sets(M, S))). 1855% ?- zdd((zdd_map([], [], M), sets(M, S))). 1856% ?- zdd((N = 3, numlist(1, N, L), time(map(L, L, M)))). 1857% ?- N = 1000, numlist(1, N, L), time(zdd(zdd_map(L, L, M))).
1863zdd_map(X, Y, Z):- shift(zdd_map(X, Y, Z)). 1864 1865zdd_map([], _, true, _). 1866zdd_map([X|Xs], R, Y, S):- zdd_map(Xs, R, Z, S), 1867 zdd_map(R, X, Z, Y, S). 1868% 1869zdd_map([], _, _, false, _). 1870zdd_map([V|Vs], X, Z, Y, S):- 1871 zdd_map(Vs, X, Z, Y0, S), 1872 cofact(Y, if(X-V, Z, Y0), S).
zdd((zdd_insert(a, true, X), zdd_insert(b, X, X1), prz(X1))).
?- zdd((X<<pow([a,b,c]), zdd_insert(x, X, X1), prz(X1))).1879zdd_insert(X, Y, Z):- shift(zdd_insert(X, Y, Z)). 1880 1881% 1882zdd_insert(A, 1, J, S):-!, zdd_singleton(A, J, S). 1883zdd_insert(_, 0, 0, _):-!. 1884zdd_insert(A, I, J, S):- memo(zdd_insert(A, I)-J, S), 1885 ( nonvar(J) -> true 1886 ; cofact(I, t(X, L, R), S), 1887 compare(C, A, X), 1888 ( C = (=) 1889 -> zdd_join(L, R, K, S), 1890 cofact(J, t(X, 0, K), S) 1891 ; C = (<) 1892 -> cofact(J, t(A, 0, I), S) 1893 ; zdd_insert(A, L, L0, S), 1894 zdd_insert(A, R, R0, S), 1895 cofact(J, t(X, L0, R0), S) 1896 ) 1897 ). 1898 1899% ?- zdd((family([[a, b],[b]], X), sets(X, Sx), 1900% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))). 1901%% zdd_insert_atoms(+As:sorted list, +X:zdd, -Y:zdd) det. 1902% Insert all atoms in As to X to get the result Y. 1903 1904zdd_insert_atoms(As, X, Y):- shift(zdd_insert_atoms(As, X, Y)). 1905% 1906zdd_insert_atoms([], X, X, _):-!. 1907zdd_insert_atoms([A|As], X, Y, S):- zdd_insert_atoms(As, X, X0, S), 1908 zdd_insert(A, X0, Y, S). 1909 1910% ?- zdd((ord_linear_zdd([c, d, e], Y), sets(Y, Sy))). 1911ord_linear_zdd(X, Y):- shift(ord_linear_zdd(X,Y)). 1912ord_linear_zdd([], 1, _). 1913ord_linear_zdd([A|As], X, S):- ord_linear_zdd(As, X0, S), 1914 cofact(X, t(A, 0, X0), S). 1915% 1916zdd_ord_filter(A, OrdList, F, S):- zdd_ord_power(OrdList, P, S), 1917 zdd_insert(A, P, F, S). 1918% 1919zdd_meet_list([A], A, _):-!. 1920zdd_meet_list([A|As], B, S):- zdd_meet_list(As, A, B, S). 1921% 1922zdd_meet_list([], X, X, _). 1923zdd_meet_list([A|As], X, Y, S):- zdd_meet(A, X, X0, S), 1924 zdd_meet_list(As, X0, Y, S). 1925% 1926zdd_join_list([], X, X, _):-!. 1927zdd_join_list([A|As], X, Y, S):- zdd_join(A, X, X0, S), 1928 zdd_join_list(As, X0, Y, S). 1929 1930 1931% ?- zdd((X<<[a], zdd_disj_filter([b], X, Y), sets(Y, S))). 1932% ?- zdd((X<<([a]+[b]), zdd_disj_filter([-a,-b], X, Y), sets(Y, S))). 1933% ?- zdd((X<<pow([a,b,c]), zdd_disj_filter([a], X, Y), sets(Y, S))). 1934% ?- numlist(1, 10, Ns), 1935% zdd((X<<pow(Ns), zdd_disj_filter([1,2,3], X, Y), card(Y, S))). 1936% ?- numlist(1, 1000, Ns), zdd((X<<pow(Ns), 1937% time(zdd_disj_filter([1,2,3], X, Y)), card(Y, S))). 1938% ?- numlist(1, 3, Ns), zdd((X<<pow(Ns), 1939% time(zdd_disj_filter([1,2,3], X, Y)), card(Y, S))). 1940 1941zdd_disj_filter(L, X, Y):- shift(zdd_disj_filter(L, X, 0, Y)). 1942% 1943zdd_disj_filter([], _, Y, Y, _):-!. 1944zdd_disj_filter(_, 0, Y, Y, _):-!. 1945zdd_disj_filter([-A|As], X, Y0, Y, S):-!, 1946 zdd_proper_ideal(A, X, U, S), 1947 zdd_join(U, Y0, Y1, S), 1948 zdd_disj_filter(As, X, Y1, Y, S). 1949zdd_disj_filter([A|As], X, Y0, Y, S):- 1950 zdd_proper_filter(A, X, U, S), 1951 zdd_join(U, Y0, Y1, S), 1952 zdd_disj_filter(As, X, Y1, Y, S). 1953 1954% ?- numlist(1, 1000, Ns), zdd((X<<pow(Ns), 1955% zdd_proper_filter(1000, X, Y), zdd_proper_filter(1, X, Y0), card(Y, C), card(Y0, C0), 1956% C=C0)). 1957%@ 1958% ?- zdd((X << pow([a,b]), zdd_proper_filter(b, X, Y), card(Y, C))). 1959% ?- zdd((X << {[a]}, zdd_proper_filter(b, X, Y), card(Y, C))). 1960 1961zdd_proper_filter(A, X, Y):- shift(zdd_proper_filter(A, X, Y)). 1962% 1963zdd_proper_filter(A, X, Y, S):-zdd_shift(zdd_proper_filter(A, X, Y, S)). 1964 1965% 1966zdd_proper_filter(_, X, 0, _, _):- X<2, !. 1967zdd_proper_filter(A, X, Y, S, M):- memo(zdd_proper_filter(X)-Y, M), 1968 ( nonvar(Y) -> true 1969 ; cofact(X, t(B, L, R), S), 1970 compare(C, A, B), 1971 ( C = (=) 1972 -> cofact(Y, t(A, 0, R), S) 1973 ; C = (<) 1974 -> Y = 0 1975 ; zdd_proper_filter(A, L, L0, S, M), 1976 zdd_proper_filter(A, R, R0, S, M), 1977 cofact(Y, t(B, L0, R0), S) 1978 ) 1979 ). 1980 1981% ?- zdd((X<<[a], zdd_proper_ideal([b], X, Y), sets(Y, S))). 1982% ?- zdd((X<<([a]+[b]), zdd_proper_ideal(a, X, Y), sets(Y, S))). 1983% ?- zdd((X<<pow([a,b,c]), zdd_proper_ideal(a, X, Y), sets(Y, S))). 1984% ?- numlist(1, 10, Ns), 1985% zdd((X<<pow(Ns), zdd_proper_ideal(1, X, Y), card(Y, S))), 1986% S is 2^9. 1987% ?- numlist(1, 1000, Ns), zdd((X<<pow(Ns), 1988% time(zdd_proper_ideal(1000, X, Y)), card(Y, S))), 1989% S is 2^999. 1990 1991zdd_proper_ideal(A, X, Y):- shift(zdd_proper_ideal(A, X, Y)). 1992% 1993zdd_proper_ideal(A, X, Y, S):- zdd_shift(zdd_proper_ideal(A, X, Y, S)). 1994 1995% 1996zdd_proper_ideal(_, X, X, _, _):- X<2, !. 1997zdd_proper_ideal(A, X, Y, S, M):- memo(zdd_proper_ideal(X)-Y, M), 1998 ( nonvar(Y) -> true 1999 ; cofact(X, t(B, L, R), S), 2000 compare(C, A, B), 2001 ( C = (=) 2002 -> Y = L 2003 ; C = (<) 2004 -> Y = X 2005 ; zdd_proper_ideal(A, L, L0, S, M), 2006 zdd_proper_ideal(A, R, R0, S, M), 2007 cofact(Y, t(B, L0, R0), S) 2008 ) 2009 ). 2010 2011% ?- zdd((zdd_conj_filter([b], 0, Y), sets(Y, S))). 2012% ?- zdd((zdd_conj_filter([-b], 0, Y), sets(Y, S))). 2013% ?- zdd((X<<([a]+[b]), zdd_conj_filter([-a], X, Y), sets(Y, S))). 2014% ?- zdd((X<<([a]+[b]), zdd_conj_filter([-a, -b], X, Y), sets(Y, S))). 2015% ?- zdd((X<<pow([a,b,c]), zdd_conj_filter([a,b], X, Y), sets(Y, S))). 2016% ?- numlist(1, 10, Ns), zdd((X<<pow(Ns), zdd_conj_filter([1,2,3], X, Y), card(Y, S))), S =:= 2^(10-3). 2017% ?- numlist(1, 1000, Ns), zdd((X<<pow(Ns), zdd_conj_filter([1,2,3], X, Y), card(Y, S))), S =:= 2^(1000-3). 2018% ?- numlist(1, 1000, Ns), numlist(1, 998, L), 2019% zdd((X<<pow(Ns), zdd_conj_filter(L, X, Y), card(Y, S))). 2020 2021zdd_conj_filter(L, X, Y):- shift(zdd_conj_filter(L, X, Y)). 2022% 2023% 2024zdd_conj_filter([], X, X, _):-!. 2025zdd_conj_filter(_, 0, 0, _):-!. 2026zdd_conj_filter([-A|As], X, Y, S):- zdd_proper_ideal(A, X, X0, S), 2027 zdd_conj_filter(As, X0, Y, S). 2028zdd_conj_filter([A|As], X, Y, S):- zdd_proper_filter(A, X, X0, S), 2029 zdd_conj_filter(As, X0, Y, S). 2030 2031 2032 /********************* 2033 * remove atom * 2034 *********************/ 2035 2036% ?- zdd((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2037% sets(Y, Sy))). 2038%% zdd_remove(+A, +X, -Y, +G) is det. 2039% Remove an atom A from each set in a ZDD X, 2040% and unify Y with the result. 2041 2042zdd_remove(X, Y, Z):- shift(zdd_remove(X, Y, Z)). 2043 2044zdd_remove(X, Y, Z, S):- zdd_shift(zdd_remove(X, Y, Z, S)). 2045 2046% 2047zdd_remove(_, X, X, _, _):- X<2, !. 2048zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2049 ( nonvar(J) -> true 2050 ; cofact(I, t(Ai, Li, Ri), S), 2051 compare(C, A, Ai), 2052 ( C = (<) -> J = I 2053 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2054 zdd_remove(A, Ri, Ria, S, M), 2055 cofact(J, t(Ai, Lia, Ria), S) 2056 ; zdd_join(Li, Ri, J, S) 2057 ) 2058 ). 2059 2060% For developing. 2061dump_args(List):- nl, 2062 writeln('** Completed Options:'), 2063 maplist(writeln, List). 2064% 2065update_hit_count :- 2066 ( nb_current(count_hit, C), integer(C) 2067 -> true 2068 ; C = 0 2069 ), 2070 C0 is C + 1, 2071 b_setval(count_hit, C0). 2072% 2073print_hit_count :- (nb_current(count_hit, N) -> N0 = N; N0 = 0), 2074 format("~n~w", [count_hit = N0]). 2075% 2076newvars(Vars):- b_getval(boole_zip, Zip), 2077 length(Zip, N), 2078 I is N + 1, 2079 length(Vars, J), 2080 K is I + J - 1, 2081 ( K =<0 -> Vars = [] 2082 ; numlist(I, K, Vars) 2083 ), 2084 zip(Vars, Vars, Zip0), 2085 append(Zip, Zip0, Zip1), 2086 b_setval(boole_zip, Zip1). 2087% 2088new_root_zdds(Zdds):- length(Zdds, N), 2089 length(Vars, N), 2090 newvars(Vars), 2091 maplist(var_to_zdd, Vars, Zdds). 2092% 2093var_to_zdd(I, X):- memo(truth(I)-X). 2094 2095% ?- new_variables(1+2+A+B, [A], V). 2096new_variables(A, OldVs, NewVs):- term_variables(A, V0), 2097 subtract_by_memq(V0, OldVs, NewVs). 2098 2099% ?- update_zip_by_term(A+B, [1-A], R), update_zip_by_term(A+B+C+D, R, S). 2100update_zip_by_term(A, OldZip, NewZip):- zip(_, Vs, OldZip), 2101 new_variables(A, Vs, NewVars), 2102 length(OldZip, Len), 2103 update_zip_by_term(NewVars, Len, OldZip, NewZip). 2104% 2105update_zip_by_term([], _, Z, Z). 2106update_zip_by_term([V|Vs], I, Z, NewZ):- 2107 I0 is I + 1, 2108 update_zip_by_term(Vs, I0, [I0-V|Z], NewZ). 2109 2110% ?- subtract_by_memq([X, A, Y, B], [Y, X], U). 2111subtract_by_memq([], _, []). 2112subtract_by_memq([A|B], C, D):- memq(A, C), !, 2113 subtract_by_memq(B, C, D). 2114subtract_by_memq([A|B], C, [A|D]):- 2115 subtract_by_memq(B, C, D). 2116% 2117union_by_memq([], X, X). 2118union_by_memq([A|As], X, Y) :- memq(A, X), !, 2119 union_by_memq(As, X, Y). 2120union_by_memq([A|As], X, [A|Y]) :- 2121 union_by_memq(As, X, Y). 2122% 2123union_by_memq([], []). 2124union_by_memq([A|B], C) :- union_by_memq(B, C0), 2125 union_by_memq(A, C0, C). 2126 2127% ?- solve([sat(a,X)]), zout(X). 2128zout_zip([]):-!. 2129zout_zip([I-Z|R]):-!, zdd_to_prop(Z, Z0), 2130 writeln(I-Z0), 2131 zout(R). 2132% 2133zout(X):- integer(X), !, 2134 zdd_to_prop(X, Y), 2135 writeln(node(X)=Y). 2136zout(X):- writeln(X). 2137 2138% 2139zout(A, V):-!, zdd_to_prop(V, V0), 2140 format("~w: ~w", [A, V0]). 2141 2142% 2143zdd_to_prop(X, Y):- zdd_to_prop(X, Y, [slim_boole(true)]). 2144% 2145zdd_to_prop(X, Y, Options):- zdd_to_tree(X, T), 2146 tree_to_prop(T, Y0), 2147 ( memberchk(slim_boole(true), Options) 2148 -> slim_boole(Y0, Y) 2149 ; Y=Y0 2150 ). 2151% 2152ztree([]):-!. 2153ztree([[X-Y]|R]):- !, ztree(X, Y), ztree(R). 2154ztree(X):- zdd_to_tree(X, Y), writeln(Y). 2155 2156% 2157ztree(X, Y):- zdd_to_tree(Y, Y0), 2158 format("~w = ~w\n",[X, Y0]). 2159 2160% 2161zdd_to_tree(I, if(X, L, R)):- integer(I), !, 2162 cofact(I, if(X, L0, R0)), 2163 zdd_to_tree(L0, L), 2164 zdd_to_tree(R0, R). 2165zdd_to_tree(X, X). 2166 2167% ?- tree_to_prop(if(1, truth(1), false), P, 1). 2168tree_to_prop(X, Y):- varnum(N), tree_to_prop(X, Y, N). 2169% 2170tree_to_prop(false, false, _):-!. 2171tree_to_prop(true, true, _):-!. 2172tree_to_prop(if(X, L, R), X*L0 + -(X)*R0, N):- 2173 tree_to_prop(L, TL, N), 2174 tree_to_prop(R, TR, N), 2175 depth(L, A, N), 2176 depth(R, B, N), 2177 X0 is X + 1, 2178 conj_of_negs(X0, A, TL, L0), 2179 conj_of_negs(X0, B, TR, R0). 2180 2181% 2182depth(if(I,_,_), I, _):-!. 2183depth(_, N, N). 2184 2185% ?- conj_of_negs(1, 3, A). 2186conj_of_negs(I, J, A):- I=<J, conj_of_negs(I, J, -(J), A). 2187 2188% ?- conj_of_negs(3, 1, a, X). 2189% ?- conj_of_negs(1, 3, a, X). 2190conj_of_negs(I, J, A, A):- I>=J, !. 2191conj_of_negs(I, J, A, B):- J0 is J - 1, 2192 conj_of_negs(I, J0, -(J0)*A, B). 2193 2194% ?- zdd((X<<pow([a,b]), card(X, C))).
2200card(X, Y):- shift(card(X, Y)). 2201% 2202card(X, Y, S):- zdd_shift(card(X, Y, S)). 2203% 2204card(I, I, _, _):- I < 2, !. 2205card(I, C, S, M):- memo(I-C, M), 2206 ( nonvar(C) -> true 2207 ; cofact(I, t(_, L, R), S), 2208 card(R, Cr, S, M), 2209 card(L, Cl, S, M), 2210 C is Cl + Cr 2211 ). 2212 2213% ?- gf2_count([1,1,1], X). 2214% ?- gf2_count([2,2,2], X). 2215% ?- gf2_count([1, 2, 3, 4], X). 2216% ?- numlist(1, 100, Ns), gf2_count(Ns, C). 2217gf2_count(X, Y):- gf2_count(X, 1, Y). 2218 2219gf2_count([], X, X). 2220gf2_count([N|Ns], X, Y):- X0 is X*(2^N - 1), 2221 gf2_count(Ns, X0, Y). 2222 2223 2224% ?- sat_count(((a=b)=c)=(a=(b=c)), X). 2225% ?- zdd((even_odd_power([1-1], X, Y), gf2_sat_count([Y-1], 0, V))). 2226% ?- zdd((even_odd_power([1-1, 2-1], X, Y), gf2_sat_count([Y-1], 0, V))). 2227% ?- zdd((even_odd_power([1-1, 2-1, 3-1], X, Y), gf2_sat_count([Y-1], 0, V))). 2228% ?- zdd((even_odd_power([1-1, 2-2, 3-3], X, Y), gf2_sat_count([Y-1], 0, C))). 2229 2230% 2231gf2_sat_count(X, Y, Z):- shift(gf2_sat_count(X, Y, Z)). 2232% 2233gf2_sat_count([], U, U, _):-!. 2234gf2_sat_count([P-C|As], U, V, S):- gf2_sat_count(P, C, As, U, V, S). 2235 2236% 2237gf2_sat_count(1, C, As, U, V, S):-!, U0 is U + C, 2238 gf2_sat_count(As, U0, V, S). 2239gf2_sat_count(0, _, As, U, V, S):-!, gf2_sat_count(As, U, V, S). 2240gf2_sat_count(P, C, As, U, V, S):- cofact(P, t(_-J, L, R), S), 2241 C0 is C * (2^J-1), 2242 gf2_sat_count(R, C0, [L-C|As], U, V, S). 2243 2244% ?- zdd((even_odd_power([1,2,3], X, Y), psa(X), psa(Y))). 2245% ?- zdd((even_odd_power([1,2,3], X, Y), Z<<pow([1,2,3]), 2246% zdd_join(X, Y, Z))). 2247 2248even_odd_power(X, Y, Z):- shift(even_odd_power(X, Y, Z)). 2249% 2250even_odd_power([], 1, 0, _). 2251even_odd_power([X|Xs], Ev, Od, S):- 2252 even_odd_power(Xs, Ev0, Od0, S), 2253 zdd_insert(X, Ev0, X_Od, S), 2254 zdd_insert(X, Od0, X_Ev, S), 2255 zdd_join(X_Od, Od0, Od, S), 2256 zdd_join(X_Ev, Ev0, Ev, S). 2257 2258% ?- zdd((X<<set([a,b]), card(X, D), even_odd_card(X, C))). 2259% ?- zdd((X<<set([a]), card(X, D), even_odd_card(X, C))). 2260% ?- zdd((X<<pow([a,b]), card(X, D), even_odd_card(X, C))). 2261% ?- zdd((X<<pow([a,b,c]), card(X, D), even_odd_card(X, C))). 2262% ?- zdd((X<<pow([a,b,c,d]), card(X, D), even_odd_card(X, C))). 2263% ?- zdd((X<<pow([a,b,c,d,e]), card(X, D), even_odd_card(X, C))). 2264 2265even_odd_card(X, C):- shift(even_odd_card(X, C)). 2266% 2267even_odd_card(X, C, S):- zdd_shift(even_odd_card(X, C, S)). 2268% 2269even_odd_card(1, 1-0, _, _):-!. 2270even_odd_card(0, 0-0, _, _):-!. 2271even_odd_card(I, C, S, M):- memo(I-C, M), 2272 ( nonvar(C) -> true 2273 ; cofact(I, t(_, L, R), S), 2274 even_odd_card(L, Cl, S, M), 2275 even_odd_card(R, Cr, S, M), 2276 Cr = (Er-Or), 2277 Cl = (El-Ol), 2278 E is El + Or, 2279 O is Ol + Er, 2280 C = (E-O) 2281 ). 2282 2283 % 2284zip([], [], []). 2285zip([X|Xs], [Y|Ys], [X-Y|Zs]) :- zip(Xs, Ys, Zs). 2286% 2287unify_zip([]). 2288unify_zip([X-X|R]):- unify_zip(R). 2289 2290% For debugging. 2291zdd_snap(X):- zdd_to_prop(X, X0), 2292 writeln(zdd_snap(X0)). 2293 2294 2295% 2296% ?- zdd((zdd_append([a,b,c], 1, X), cofact0(X, A, B), card(X, C), psa(X))). 2297% ?- zdd((zdd_append([a,b,c], 0, X), psa(X))).
2302zdd_append(X, Y, Z):- shift(zdd_append(X, Y, Z)). 2303% 2304zdd_append(_, [], [], _S):-!. 2305zdd_append([], X, X, _S). 2306zdd_append([A|As], X, Y, S):- zdd_append(As, X, X0, S), 2307 cofact0(Y, A, X0, S). 2308 2309 2310 /****************************************** 2311 * Oprations on clauses of literals * 2312 ******************************************/ 2313 2314% ?- ltr_compare(C, a, -a). 2315% ?- ltr_compare(C, -(a), a). 2316% ?- ltr_compare(C, -(b), a). 2317% ?- ltr_compare(C, -(a), b). 2318% ?- ltr_compare(C, -(a), -(b)). 2319% ?- ltr_compare(C, -(a), -(a)).
2326ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 2327ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 2328 ( C0 == (=) -> C =(<) 2329 ; C0 = C 2330 ). 2331ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 2332 ( C0 == (=) -> C = (>) 2333 ; C0 = C 2334 ). 2335ltr_compare(C, X, Y):- compare(C, X, Y). 2336 2337% ?- ltr_sort([b, b, a], X). 2338% ?- ltr_sort([-b, b,-b, -a], X).
2343ltr_sort(X, Y):- predsort(ltr_compare, X, Y). 2344 2345% ?- zdd((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). 2346% ?- zdd((X << pow([a, -b, c]), ltr_has_set([a, b], X))). 2347% ?- zdd((X << ltr_power([a, -b, c]), ltr_has_set([a, b], X))). 2348 2349ltr_memberchk(L, Z):- shift(ltr_memberchk(L, Z)). 2350% 2351ltr_memberchk(L, Z, S):- ltr_sort(L, L0), 2352 ltr_ord_memberchk(L0, Z, S). 2353% 2354ltr_ord_memberchk([], Z, S):- !, zdd_has_1(Z, S). 2355ltr_ord_memberchk([A|As], Z, S):- Z > 1, 2356 cofact(Z, t(B, L, R), S), 2357 ltr_compare(C, A, B), 2358 ( C = (=) -> ltr_ord_memberchk(As, R, S) 2359 ; ltr_ord_memberchk([A|As], L, S) 2360 ).
zdd((a_big_cnf(1, X), ltr_card(1, X, C))).
?- zdd((a_big_cnf(2, X), ltr_card(2, X, C))).
?- zdd((a_big_cnf(3, X), ltr_card(3, X, C))).
?- zdd((a_big_cnf(10, X), ltr_card(10, X, C))).
?- zdd((a_big_cnf(20, X), ltr_card(20, X, C))).
?- time(zdd((a_big_cnf(100, X), ltr_card(100, X, C)))), C =:= 2^100.
@ % 2,392,546 inferences, 0.290 CPU in 0.409 seconds (71% CPU, 8246121 Lips)
@ X = 30001,
@ C = 1267650600228229401496703205376 .
?- zdd((a_big_cnf(10, X), ltr_refute(X))).
?- time(zdd((a_big_cnf(20, X), ltr_refute(X)))).
?- call_with_time_limit(100, time(zdd((a_big_cnf(30, X), ltr_refute(X))))).
2377a_big_cnf(X, Y):- shift(a_big_cnf(X, Y)). 2378a_big_cnf(0, 1, _). 2379a_big_cnf(N, X, S):- N>0, 2380 N0 is N-1, 2381 a_big_cnf(N0, X0, S), 2382 ltr_insert(N, X0, R, S), 2383 ltr_insert(-N, X0, L, S), 2384 zdd_join(L, R, X, S). 2385 2386% ?- numlist(1, 3, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), card(Y, C))). 2387% ?- time((numlist(1, 20, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), card(Y, C))))). 2388%@ % 143,146,953 inferences, 9.734 CPU in 9.756 seconds (100% CPU, 14705180 Lips) 2389%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2390%@ X = 41, 2391%@ Y = 60, 2392%@ C = 1. 2393% ?- zdd((boole_to_dnf((a*b)+c, X), ltr_choices(X, Y), ltr_choices(Y, Z), 2394% ltr_choices(Z, U), psa(X), nl, psa(Y), nl, psa(Z), nl, psa(U))), U=Y. 2395% ?- zdd((X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 2396% ltr_choices(Z, U), psa(X), nl, psa(Y), nl, psa(Z), nl, psa(U))), U=Y. 2397% ?- zdd((X<< ( [b,d]+[a,d]+[a,b,d] ), ltr_choices(X, Y), 2398% ltr_choices(Y, Z), ltr_choices(Z, U), ltr_choices(U, V), 2399% psa(X), nl, psa(Y), nl, psa(Z), nl, psa(U), nl, psa(V))). 2400% ?- zdd(( (X<< {[a,b]}), ltr_choices(X, Y), psa(X), nl, psa(Y))). 2401% ?- zdd(( (X<< {[a,b,c]}), ltr_choices(X, Y), psa(X), nl, psa(Y))). 2402% ?- zdd(( (X<< {[a, b], [c, d]}), ltr_choices(X, Y), psa(Y))). 2403% ?- zdd(( (X<< {[], [a, b], [c, d]}), ltr_choices(X, Y), psa(Y))). 2404% ?- zdd(( (X<< {[a], [c, d]}), ltr_choices(X, Y), psa(Y))). 2405% ?- zdd(( X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y))). 2406% ?- zdd(( X<< {[a,b]}, ltr_choices(X, Y), psa(Y))). 2407% ?- zdd(( X<< {[]}, ltr_choices(X, Y), psa(Y))). 2408 2409% 2410ltr_choices(X, Y):- shift(ltr_choices(X, Y)). 2411 2412ltr_choices(1, 1, _):-!. 2413ltr_choices(0, 1, _):-!. 2414 2415% ltr_choices(1, 0, _):-!. 2416% ltr_choices(0, 1, _):-!. 2417 2418ltr_choices(X, Y, S):- memo(ltr_choices(X)-Y, S), 2419 ( nonvar(Y) -> true 2420 ; ltr_choices(X, [], 1, Y, S) 2421 ). 2422% 2423 2424ltr_choices(0, _, Y, Y, _):-!. 2425ltr_choices(1, As, Y0, Y, S):-!, ltr_fold_insert(As, Y0, 0, Y, S). 2426ltr_choices(X, As, Y0, Y, S):- cofact(X, t(A, L, R), S), 2427 ( L = 0 2428 -> ltr_choices(R, [A|As], Y0, Y, S) 2429 ; L = 1 2430 -> ( As = [] 2431 -> Y = 0 2432 ; ltr_fold_insert(As, Y0, 0, Y1, S), 2433 ltr_choices(R, [A|As], Y1, Y, S) 2434 ) 2435 ; ltr_choices(L, As, Y0, Y1, S), 2436 ltr_choices(R, [A|As], Y1, Y, S) 2437 ). 2438% 2439ltr_fold_insert([], _, Y, Y, _). 2440ltr_fold_insert([A|As], Y0, U, Y, S):- 2441 ltr_insert(A, Y0, V, S), 2442 ltr_join(U, V, U0, S), 2443 ltr_fold_insert(As, Y0, U0, Y, S). 2444 2445% ?- sat(-(true)). 2446%@ false. 2447% ?- sat(-(a + -a)). 2448%@ false. 2449% ?- sat(a). 2450%@ true. 2451% ?- sat(or(a, b)), sat_count(C). 2452%@ C = 3. 2453% ?- sat(xor(a, b)), sat_count(C). 2454%@ C = 1. 2455% ?- sat(exor(a, b)), sat_count(C). 2456%@ C = 2. 2457% ?- sat(e_x_o_r(a, b)), sat_count(C). 2458%@ C = 1. 2459% ?- sat(a), sat(-a). 2460%@ false. 2461% ?- sat(a), sat(a+b), sat_count(C). 2462%@ C = 2. 2463% ?- sat(a(1)+a(2)), sat_count(C). 2464%@ C = 3. 2465% ?- sat(A+a(2)), sat_count(C). 2466%@ C = 3. 2467% ?- sat(A + B), sat_count(C). 2468% ?- sat(a+b+c+d), sat_count(C). 2469%@ C = 15. 2470% ?- sat(a+b), sat(c+d), sat_count(C). 2471%@ C = 9. 2472% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 2473%@ C = 2. 2474% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 2475%@ C = 4. 2476% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). 2477%@ false. 2478% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). 2479%@ false. 2480% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 2481%@ E = (a=b)*(b=c)*(c=a), 2482%@ C = 2. 2483% ?- sat(A + B), sat_count(C). 2484%@ C = 3. 2485% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 2486%@ Vs = [A, B], 2487%@ C = 3 . 2488% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 2489%@ Vs = [A, B], 2490%@ C = 4 . 2491% ?- sat(a=<(b=<a)), sat_count(Count). 2492 2493sat(X):- 2494 ( nb_current(sat_state, S), S \== [] -> true 2495 ; open_state(S0, [extra([root-1, varnum-0, varzip-[]])]), 2496 b_setval(sat_state, S0) 2497 ), 2498 b_getval(sat_state, State), 2499 get_key(root, Root, State), 2500 dnf(X, Y, State), 2501 ltr_merge(Y, Root, Root0, State), 2502 set_key(root, Root0, State), 2503 Root0 \== 0. 2504 2505 2506% ?- fos(a*b), fos_count(C). 2507% ?- fos(a), fos_count(C). 2508% ?- fos(pow([a, b])/a), fos_count. 2509% ?- fos(pow([a, b])//a), fos_count. 2510% ?- fos((a+b)*(x+Y)), fos_count. 2511% ?- fos((a+b)&(x+Y)), fos_count. 2512% ?- fos((a+b)&(a+c)), fos_count. 2513 2514fos(X):- 2515 ( nb_current(fos_state, S), S \== [] -> true 2516 ; open_state(S0, [extra([root-0, varnum-0, varzip-[]])]), 2517 b_setval(fos_state, S0) 2518 ), 2519 b_getval(fos_state, State), 2520 get_key(root, Root, State), 2521 fos(X, Y, State), 2522 zdd_join(Y, Root, Root0, State), 2523 set_key(root, Root0, State). 2524% 2525sat_count(C):- b_getval(sat_state, S), 2526 get_key(varnum, N, S), 2527 get_key(root, X, S), 2528 ltr_card(N, X, C, S). 2529% 2530fos_count(C):- b_getval(fos_state, S), 2531 get_key(root, R, S), 2532 card(R, C, S). 2533% 2534fos_count :- fos_count(C), writeln(C). 2535 2536% ?- sat_count(a=<(b=<a), C). 2537% ?- sat_count(a->(b->a), C). 2538sat_count(F, C):- zdd(( 2539 dnf(F, X), 2540 get_key(varnum, N), 2541 ltr_card(N, X, C))). 2542 2543fos_count(F, C):- zdd(( 2544 fos(F, X), 2545 card(X, C))). 2546 2547sat0(X):- 2548 ( nb_current(sat_state, S), S \== [] -> true 2549 ; open_state(S0, [extra([root-1, varnum-0, varzip-[]])]), 2550 b_setval(sat_state, S0) 2551 ), 2552 b_getval(sat_state, State), 2553 get_key(root, Root, State), 2554 dnf0(X, Y, State), 2555 ltr_merge(Y, Root, Root0, State), 2556 set_key(root, Root0, State), 2557 Root0 \== 0. 2558% 2559sat_count0(C):- b_getval(sat_state, S), 2560 get_key(root, R, S), 2561 get_key(varnum, N, S), 2562 ltr_card(N, R, C, S). 2563% 2564sat_count0(F, C):- zdd(( 2565 dnf0(F, X), 2566 get_key(varnum, N), 2567 ltr_card(N, X, C))). 2568 2569 2570print_root:- b_getval(sat_state, S), get_key(root, R, S), psa(R, S). 2571% 2572sat_clear:- nb_setval(sat_state, []). 2573 2574 2575% ?- zdd((dnf(a->b, Y), psa(Y))). 2576% ?- zdd((dnf(a+b, X), dnf(b+c, Y), ltr_merge(Y, X, Z), ltr_card(3, Z, C))). 2577% ?- zdd((dnf(a+b+c, X), ltr_card(3, X, Count))). 2578% ?- zdd((dnf(A+b+c, X), ltr_card(3, X, Count))). 2579% ?- zdd((dnf(A+B+C, X), ltr_card(3, X, Count))). 2580% ?- zdd((dnf(a+b, X), sat(b+c, Y), ltr_join(X, Y, Z), ltr_card(3, Z, C))). 2581% ?- zdd((dnf(a+b, X), dnf(b+c, Y), ltr_merge(X, Y, Z), ltr_card(3, Z, C))). 2582% ?- zdd((dnf((a+b)*(b+c), X), ltr_card(3, X, C))). 2583% ?- zdd((dnf(A->B, X), dnf(B->C, Y), ltr_merge(Y, X, Z), 2584% ltr_card(3, Z, Count))). 2585% ?- zdd((dnf((A->B)*(B->C), X), ltr_card(3, X, Count))). 2586% ?- zdd((dnf(a=b, X), dnf(b=c, Y), ltr_merge(X, Y, Z), ltr_card(3, Z, Count))). 2587% ?- zdd((dnf(x+y, F), ltr_card(2, F, C), dnf(-(x), D), ltr_card(2, D, E))). 2588% ?- zdd((dnf(x, F), ltr_card(2, F, C))). 2589% ?- zdd((dnf(x, F), ltr_card(3, F, C))). 2590% ?- zdd((dnf(-x, F), ltr_card(3, F, C))). 2591% ?- zdd((dnf(true, F), ltr_card(3, F, C))). 2592% ?- zdd((dnf(false, F), ltr_card(3, F, C))). 2593% ?- zdd((dnf(x=y, F), ltr_card(2, F, C))). 2594% ?- zdd((dnf(x=y, F), ltr_card(3, F, C))). 2595% ?- zdd((dnf(x + y, F), ltr_card(2, F, C))). 2596% ?- zdd((dnf(-(x + y), F), ltr_card(2, F, C))). 2597% ?- zdd((dnf(x + y + z, F), ltr_card(3, F, C))). 2598% ?- zdd((dnf(-(x + y + z), F), ltr_card(3, F, C))). 2599 2600% ?- zdd(prove_by_refutation((a->b)->(b->a))). 2601% ?- zdd(prove_by_refutation((a->b)->(a->b))). 2602% ?- zdd(prove_by_refutation((a->b)->(b->a))). 2603% ?- zdd(prove_by_refutation((a->b))). 2604% ?- zdd(prove_by_refutation((a))). 2605% ?- spy(boole_to_cnf), prove_by_refutation((a->b)->b). 2606% ?- prove_by_refutation(a->a). 2607% ?- prove_by_refutation(-(-(a->a))). 2608% ?- prove_by_refutation((-(a->a))). 2609% ?- prove_by_refutation((a)). 2610% ?- prove_by_refutation(-a). 2611% ?- N = 10, numlist(1, N, Ns), zdd((X<<(pow(Ns)), ltr_card(N, X, C))). 2612% ?- N = 1000, numlist(1, N, Ns), zdd((X<<(pow(Ns)-1), ltr_card(N, X, C))). 2613 2614% ?- forall(valid_formula(F, N), (expand_boole_macro(F, F0), 2615% zdd((boole_to_dnf(F0, D), psa(D), 2616% ltr_card(N, D, C), writeln(F), writeln(F0), 2617% writeln(ltr_card(N, D, C)))))). 2618 2619% valid_formula/2 with the number of variables. 2620valid_formula(-(-a)->a, 1). 2621valid_formula(a -> a, 1). 2622valid_formula(a -> (b -> a), 2). 2623valid_formula((a->b)->((b->c)->(a->c)), 3). 2624valid_formula(a->((a->b)->b), 2). 2625valid_formula((a*(a->b))->b, 2). 2626valid_formula((a->b)->(-b -> -a), 2). 2627valid_formula((a->b)->((b->c)->(a->c)), 3). 2628 2629% ?- time(forall(valid_formula(A), prove_by_refutation(A))). 2630% valid_formula/1.v 2631valid_formula(-(-a)->a). 2632valid_formula(a -> a). 2633valid_formula(a -> (b -> a)). 2634valid_formula((a->b)->((b->c)->(a->c))). 2635valid_formula(a->((a->b)->b)). 2636valid_formula((a*(a->b))->b). 2637valid_formula((a->b)->(-b -> -a)). 2638valid_formula((a->b)->((b->c)->(a->c))). 2639 2640% ?- time(forall(non_valid_formula(A), prove_by_refutation(A))). 2641non_valid_formula(a). 2642non_valid_formula((a->b)->a). 2643non_valid_formula((a->b)->(b->a)). 2644non_valid_formula(a -> (b -> c)). 2645 2646% ?- zdd(prove_by_refutation((a->b)->(b->a))). 2647% ?- zdd(prove_by_refutation(a->b)). 2648% ?- zdd(prove_by_refutation(a)). 2649% ?- zdd(prove_by_refutation(a->a)). 2650% ?- zdd((ltr_complement_toplevel(0, X))). 2651% ?- zdd((ltr_complement_toplevel(1, X))). 2652% ?- zdd((ltr_choices(1, X))). 2653% ?- zdd((ltr_choices(0, X))). 2654 2655% 2656prove_by_refutation(X):- % writeln(X), 2657 zdd((cnf(X, X1), % psa(X1), 2658 ltr_complement_toplevel(X1, X2), % nl, nl, psa(X2), 2659 ltr_choices(X2, X3), % nl, nl, psa(X3), 2660 ( ltr_refute(X3) 2661 -> writeln('VALID.') 2662 ; writeln('NOT VALID.') 2663 ))). 2664 2665% ?- spy(ltr_refute). 2666% ?- zdd((X<<dnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))), 2667% psa(X), ltr_refute(X))). 2668% ?- zdd((X<<cnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))), 2669% psa(X), ltr_refute(X))). 2670 2671% ?- zdd((X<<dnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))), psa(X))). 2672% ?- spy(ltr_refute). 2673% ?- zdd((X<<cnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))), 2674% psa(X), ltr_refute(X))). 2675% ?- zdd((X<< cnf(-a * a), psa(X), ltr_refute(X))). 2676% ?- zdd((boole_to_cnf(-a * a, X), psa(X), ltr_refute(X))). 2677% ?- zdd((boole_to_cnf(-a + a, X), psa(X), ltr_refute(X))). 2678% ?- zdd((cnf(-a + a, X), psa(X), ltr_refute(X))). 2679% ?- zdd((cnf((-a )*(a), X), psa(X), ltr_refute(X))). 2680% ?- zdd((dnf(-a + a, X), psa(X), ltr_refute(X))). 2681% ?- zdd((boole_to_cnf(a, X), psa(X), ltr_refute(X))). 2682 2683ltr_refute(X):- shift(ltr_refute(X)). 2684% 2685ltr_refute(X, S) :- zdd_has_1(X, S), !. 2686ltr_refute(X, S) :- X > 1, 2687 cofact(X, t(A, L, R), S), 2688 ( L = 0 2689 -> ( R > 2, 2690 ltr_refute(R, S) % pure literal 2691 ) 2692 ; cofact(L, t(B, L0, R0), S), 2693 ( B = -(A) 2694 -> ltr_merge(R0, R, Y0, S), % resolution 2695 ltr_join(L0, Y0, Y, S), 2696 ltr_refute(Y, S) 2697 ; R = 1 2698 -> ltr_refute(L, S) % unit 2699 ; ltr_join(L, R, Y, S), % pure literal 2700 ltr_refute(Y, S) 2701 ) 2702 ). 2703 2704% ?- zdd((dnf(-a * a, X), psa(X), ltr_refute(X))). 2705% ?- zdd((dnf(a->a, X), psa(X), ltr_refute(X))). 2706% ?- zdd((dnf(-a * a, X), psa(X), ltr_refute(X))). % 0 2707% ?- zdd((dnf( a + a, X), psa(X), ltr_refute(X))). 2708% ?- zdd((dnf( a + a, X), psa(X), ltr_card(1, X, C))). 2709% ?- zdd((dnf(-a * a, X), psa(X), ltr_refute(X))). 2710% ?- zdd((boole_to_cnf(a->a, X), psa(X), ltr_refute(X))). 2711% ?- zdd((boole_to_dnf(-a * a, X), psa(X), ltr_refute(X))). % 0 2712% ?- zdd((boole_to_dnf( a + a, X), psa(X), ltr_refute(X))). 2713% ?- zdd((dnf(1, X), ltr_card(1, X, C))). 2714% ?- zdd((dnf(0, X), ltr_card(1, X, C))). 2715% ?- zdd((dnf(a, X), ltr_card(1, X, C))). 2716% ?- zdd((dnf(a+b, X), ltr_card(2, X, C))). 2717% ?- zdd((dnf(-(a+b), X), ltr_card(2, X, C))). 2718% ?- zdd((dnf(-a * a, X), psa(X))). 2719% ?- zdd((dnf(a, X), psa(X))). 2720% ?- zdd((dnf(-a, X), psa(X))). 2721% ?- zdd((dnf(a+b+(-c), X), psa(X))). 2722% ?- zdd((dnf(-a * a, X), psa(X))). 2723% ?- zdd((dnf(+([2,3,4]), X), ltr_card(3, X, C))). 2724% ?- zdd((dnf(+([2,3,4]), X), ltr_card(X, C))). 2725% ?- zdd((dnf(*([2,3,4]), X), ltr_card(3, X, C))). 2726% ?- zdd((dnf(*([2,3,4]), X), ltr_card(X, C))). 2727% ?- zdd((dnf(*([2,3,4]), X), ltr_card(X, C))). 2728% ?- zdd((dnf(A+b, X), ltr_card(X, C))). 2729% ?- zdd((dnf(A+B+c+A+B, X), ltr_card(X, C))). 2730% ?- zdd((dnf(A+B+c+A+B, X), 2731% ?- sat_count(A+B+c+A+B, C). 2732 2733dnf(X, Y):- shift(dnf(X,Y)). 2734 2735dnf(X, Y, S):- intern(X, Z, S), 2736 boole_to_dnf(Z, Y, S). 2737 2738dnf0(X, Y):- shift(dnf0(X,Y)). 2739 2740dnf0(X, Y, S):- intern(X, Z, S), 2741 simple_boole(Z, Z0), 2742 boole_to_dnf(Z0, Y, S). 2743 2744 2745% ?- zdd((zdd:intern(A, B), extern(B, E))). 2746% ?- zdd((zdd:intern(A+B, X), extern(X, E))). 2747 2748intern(X, Y):- shift(intern(X, Y)). 2749 2750intern(X, Z, S):- memo(atomic_prop_memo - M, S), 2751 ( nonvar(M)-> true 2752 ; open_state(M, []) 2753 ), 2754 getmemo(varnum-NewCount, OldCount, M), 2755 ( var(OldCount) -> OldCount=0; true ), 2756 count_atomic_prop(X, OldCount-Count, atomic_prop, M), 2757 term_variables(X, Vs), 2758 ( Vs = [] 2759 -> Z = X, 2760 Ws = Vs 2761 ; copy_term(X-Vs, Z-Ws) 2762 ), 2763 zip(Vs, Ws, Varzip), 2764 getmemo(varzip-NewVarzip, OldVarzip, M), 2765 ( var(OldVarzip) -> OldVarzip=[]; true), 2766 numbering_prop_var(Varzip, OldVarzip, OldVarzip, 2767 NewVarzip, Count, NewCount), 2768 set_key(varnum, NewCount, S), 2769 set_key(varzip, NewVarzip, S). 2770 2771% 2772qfind_key(K-V, [K0-V|_]):- K==K0, !. 2773qfind_key(P, [_|Z]):- qfind_key(P, Z). 2774 2775% 2776numbering_prop_var([], _, Zip, Zip, C, C). 2777numbering_prop_var([P|Z], Zip0, Zip1, Zip2, C, D):- 2778 ( qfind_key(P, Zip0) 2779 -> numbering_prop_var(Z, Zip0, Zip1, Zip2, C, D) 2780 ; C0 is C + 1, 2781 P=(X-Y), 2782 Y= $(C0), 2783 numbering_prop_var(Z, Zip0, [X-Y|Zip1], Zip2, C0, D) 2784 ). 2785 2786 /********************* 2787 * bool to dnf * 2788 *********************/ 2789 2790% ?- simple_boole((c*b), X). 2791% ?- simple_boole((c*b)*a, X). 2792%@ X = c*(a*b). 2793 2794% ?- simple_boole((c=:=b)=:=a, X). 2795simple_boole(X, Y):- boole_rule(X, X0), !, 2796 simple_boole(X0, Y). 2797simple_boole(X, X). 2798 2799 2800boole_rule(X, Y):-boole_AND(X, Y). 2801boole_rule(X, Y):-boole_OR(X, Y). 2802boole_rule(X, Y):-boole_IMPLY(X, Y). 2803boole_rule(X, Y):-boole_EQ(X, Y). 2804boole_rule(X, Y):-boole_NOT(X, Y). 2805 2806% 2807boole_NOT(-(-X), X). 2808boole_NOT(-(1), 0). 2809boole_NOT(-(0), 1). 2810boole_NOT(-(X), -(Y)):-boole_rule(X, Y). 2811 2812% 2813boole_AND(X*X, X). 2814boole_AND(0*_, 0). 2815boole_AND(_*0, 0). 2816boole_AND(1*X, X). 2817boole_AND(X*1, X). 2818boole_AND((X*Y)*Z, X*(Y*Z)). 2819boole_AND(X*Y, Y*X):-Y@<X. 2820boole_AND(X*(Y*Z), (Y*(X*Z))):-Y@<X. 2821boole_AND(X*Y, X0*Y):- boole_rule(X, X0). 2822boole_AND(X*Y, X*Y0):- boole_rule(Y, Y0). 2823 2824% 2825boole_OR(X+X, X). 2826boole_OR(0+X, X). 2827boole_OR(X+0, X). 2828boole_OR(1+_, 1). 2829boole_OR(_+1, 1). 2830boole_OR((X+Y)+Z, X+(Y+Z)). 2831boole_OR(X+Y, Y+X):-Y@<X. 2832boole_OR(X+(Y+Z), (Y+(X+Z))):-Y@<X. 2833boole_OR(X+Y, X0+Y):- boole_rule(X, X0). 2834boole_OR(X+Y, X+Y0):- boole_rule(Y, Y0). 2835 2836% 2837boole_EQ(X=:=X, 1). 2838boole_EQ(X=:=1, X). 2839boole_EQ(1=:=X, X). 2840boole_EQ(X=X, 1). 2841boole_EQ(1=X, X). 2842boole_EQ(X=1, X). 2843boole_EQ(X=:=Y, Y=:=X):-Y@<X. 2844boole_EQ(X=Y, Y=X):-Y@<X. 2845boole_EQ(X=:=Y, X0=:=Y):- boole_rule(X, X0). 2846boole_EQ(X=:=Y, X=:=Y0):- boole_rule(Y, Y0). 2847boole_EQ(X=Y, X0=Y):- boole_rule(X, X0). 2848boole_EQ(X=Y, X=Y0):- boole_rule(Y, Y0). 2849 2850% 2851boole_IMPLY(1->Y, Y). 2852boole_IMPLY(0->_, 1). 2853boole_IMPLY(X->Y, X0->Y):- boole_rule(X, X0). 2854boole_IMPLY(X->Y, X->Y0):- boole_rule(Y, Y0). 2855 2856 2857% ?- zdd((boole_to_dnf(dnf([[a]]), Y), psa(Y))). 2858% ?- zdd((boole_to_dnf(dnf([[a, b]]), Y), psa(Y))). 2859% ?- zdd((boole_to_dnf(dnf([[a, a]]), Y), psa(Y))). 2860% ?- zdd((boole_to_dnf(dnf([[a, -a]]), Y), psa(Y))). 2861% ?- zdd((boole_to_dnf(dnf([[a, b], [a, c]]), Y), psa(Y))). 2862% ?- zdd((boole_to_dnf(x*dnf([[a, b], [a, c]]), Y), psa(Y))). 2863 2864%@ true. 2865%@ zdd.pl qcompiled. 2866 2867% 2868boole_to_dnf(X, Y):- simple_boole(X, X0), 2869 shift(boole_to_dnf(X0,Y)). 2870% 2871boole_to_dnf(X, Y, S):- make_boole_canonical(X, X0), 2872 canonical_boole_to_dnf(X0, Y, S). 2873% 2874canonical_boole_to_dnf(1, 1, _):-!. 2875canonical_boole_to_dnf(0, 0, _):-!. 2876canonical_boole_to_dnf(X * Y, Z, S):-!, 2877 boole_to_dnf(X, U, S), 2878 boole_to_dnf(Y, V, S), 2879 ltr_merge(U, V, Z, S). 2880canonical_boole_to_dnf(X + Y, Z, S):-!, boole_to_dnf(X, U, S), 2881 boole_to_dnf(Y, V, S), 2882 ltr_join(U, V, Z, S). 2883canonical_boole_to_dnf(+(V), Y, S):- fold_join_list(V, 0, Y, S). 2884canonical_boole_to_dnf(*(V), Y, S):-!, ltr_append(V, 1, Y, S). 2885canonical_boole_to_dnf(dnf(V), Y, S):-!, ltr_read_dnf(V, 0, Y, S). 2886canonical_boole_to_dnf(X, Y, S):-!, zdd_singleton(X, Y, S). 2887% 2888ltr_read_dnf(X, Y, Z):- shift(ltr_read_dnf(X, Y, Z)). 2889% 2890ltr_read_dnf([], Y, Y, _). 2891ltr_read_dnf([C|Cs], Y, Z, S):- ltr_append(C, 1, C0, S), 2892 ltr_join(C0, Y, Y0, S), 2893 ltr_read_dnf(Cs, Y0, Z, S). 2894 2895% 2896fold_join_list([], Y, Y, _). 2897fold_join_list([X|Xs], Y0, Y, S):- 2898 fold_join_list(Xs, Y0, Y1, S), 2899 ( integer(X), 2900 X<2 2901 -> A = X 2902 ; zdd_singleton(X, A, S) 2903 ), 2904 ltr_join(A, Y1, Y, S).
2910ltr_join(X, Y, Z):- shift(ltr_join(X, Y, Z)). 2911% 2912ltr_join(X, X, X, _):-!. 2913ltr_join(0, X, X, _):-!. 2914ltr_join(X, 0, X, _):-!. 2915ltr_join(1, _, 1, _):-!. 2916ltr_join(_, 1, 1, _):-!. 2917ltr_join(X, Y, Z, S):- 2918 ( X@<Y -> memo(ltr_join(X,Y)-Z, S) 2919 ; memo(ltr_join(Y,X)-Z, S) 2920 ), 2921 ( nonvar(Z) -> true %, write(.) 2922 ; cofact(X, t(A, L, R), S), 2923 cofact(Y, t(A0, L0, R0), S), 2924 ltr_compare(C, A, A0), 2925 ( C = (<) -> ltr_join(L, Y, U, S), 2926 ltr_cofact(Z, t(A, U, R), S) 2927 ; C = (=) -> ltr_join(R, R0, U, S), 2928 ltr_join(L, L0, V, S), 2929 ltr_cofact(Z, t(A, V, U), S) 2930 ; ltr_join(L0, X, U, S), 2931 ltr_cofact(Z, t(A0, U, R0), S) 2932 ) 2933 ). 2934 2935% ?- zdd((cnf(a, X), S<<sets(X))). 2936% ?- zdd((X<<cnf(-a), Y<<sets(X))). 2937% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 2938% ?- zdd((X<<cnf(+([a,b,c])), Y<<sets(X))). 2939% ?- zdd((X<<cnf(*([a,b,c])), Y<<sets(X))). 2940% ?- zdd((X<<dnf(+([a,b,c])), Y<<sets(X))). 2941% ?- zdd((X<<dnf(*([a,b,c])), Y<<sets(X))). 2942% ?- zdd((cnf(a, X), psa(X))). 2943% ?- zdd((cnf(-a, X), psa(X))). 2944% ?- zdd((cnf(a+b, X), psa(X))). 2945% ?- zdd((cnf(a+b+(-c), X), psa(X))). 2946% ?- zdd((cnf(-a * a, X), psa(X), ltr_refute(X))). 2947% ?- zdd((boole_to_cnf(a->a, X), psa(X), ltr_refute(X))). 2948% ?- zdd((boole_to_cnf(-a * a, X), psa(X))). 2949% ?- zdd((boole_to_cnf( a + a, X), psa(X))). 2950% ?- zdd((cnf(-(a*b), X), psa(X))). 2951% ?- zdd((cnf(*([a,b,c]), X), psa(X))). 2952% ?- N = 10, numlist(2, N, Ns), zdd((cnf(*(Ns), X), psa(X))). 2953% ?- N = 100, numlist(2, N, Ns), zdd((cnf(*(Ns), X))). 2954% ?- N = 10000, numlist(2, N, Ns), zdd((cnf(*(Ns), X), ltr_card(10000, X, C))). 2955% ?- N = 10, numlist(2, N, Ns), zdd((cnf(*(Ns), X), ltr_card(9, X, C))). 2956% ?- N = 10, numlist(2, N, Ns), zdd((cnf(+(Ns), X), ltr_card(9, X, C))). 2957% ?- zdd((cnf(2+3+4+5, X), ltr_card(4, X, C))). 2958% ?- zdd((cnf(2+3+4+5, X), ltr_card(X, C))). 2959 2960cnf(X, Y):- shift(cnf(X,Y)). 2961 2962cnf(X, Y, S):- intern(X, Z, S), boole_to_cnf(Z, Y, S). 2963 2964cnf0(X, Y):- shift(cnf(X,Y)). 2965 2966cnf0(X, Y, S):- intern(X, Z, S), 2967 simple_boole(Z, Z0), 2968 boole_to_cnf(Z0, Y, S). 2969 2970% 2971boole_to_cnf(X, Y):- shift(boole_to_cnf(X,Y)). 2972% 2973boole_to_cnf(X, Y, S):- make_boole_canonical(X, X0), 2974 canonical_boole_to_cnf(X0, Y, S). 2975 2976% 2977canonical_boole_to_cnf(1, 0, _):-!. 2978canonical_boole_to_cnf(0, 1, _):-!. 2979canonical_boole_to_cnf(X * Y, Z, S):-!, 2980 boole_to_cnf(X, U, S), 2981 boole_to_cnf(Y, V, S), 2982 ltr_join(U, V, Z, S). 2983canonical_boole_to_cnf(X + Y, Z, S):-!, boole_to_cnf(X, U, S), 2984 boole_to_cnf(Y, V, S), 2985 ltr_merge(U, V, Z, S). 2986canonical_boole_to_cnf(+(V), Y, S):- ltr_append(V, 1, Y, S). 2987canonical_boole_to_cnf(*(V), Y, S):-!, fold_join_list(V, 0, Y, S). 2988canonical_boole_to_cnf(cnf(V), Y, S):-!, ltr_read_cnf(V, 1, Y, S). 2989canonical_boole_to_cnf(X, Y, S):-!, zdd_singleton(X, Y, S). 2990 2991ltr_read_cnf([], X, X, _). 2992ltr_read_cnf([X|Xs], Y, Z, S):- ltr_append(X, 1, X0, S), 2993 ltr_join(X0, Y, Y0, S), 2994 ltr_read_cnf(Xs, Y0, Z, S). 2995 2996% ?- zdd((ltr_append([-b, a, -d, c], 1, X), psa(X))). 2997% ?- zdd((ltr_append([-b, 0, -d, c], 1, X), psa(X))). 2998% ?- zdd((ltr_append([-b, 1, -d, c], 1, X), psa(X))). 2999 3000ltr_append(X, Y, Z):- shift(ltr_append(X, Y, Z)). 3001% 3002ltr_append([], X, X, _). 3003ltr_append([A|As], X, Y, S):- ltr_append(As, X, X0, S), 3004 ( A = 1 -> Y = X0 3005 ; A = 0 -> Y = 0 3006 ; ltr_insert(A, X0, Y, S) 3007 ). 3008 3009% ?- zdd((X<<(ltr_set([a])+ltr_set([b])), psa(X))). 3010% ?- zdd((X<<(ltr_set([-a])+ltr_set([b])), psa(X))). 3011% ?- zdd((X<<(ltr_set([-a])+ltr_set([a])), psa(X))). 3012 3013ltr_set(X, Y):- shift(ltr_set(X, Y)). 3014% 3015ltr_set(X, Y, S):- ltr_append(X, 1, Y, S).
3022% ?- zdd((X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y))). 3023% ?- zdd((X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), 3024% nl, nl, psa(Y))). 3025 3026ltr_complement(X, Y):- shift(ltr_complement(X, Y)). 3027% 3028ltr_complement(X, X, _):- X<2, !. 3029ltr_complement(I, Y, S):- memo(ltr_complement(I)-Y, S), 3030 ( nonvar(Y) -> true 3031 ; cofact(I, t(A, L, R), S), 3032 ltr_complement(L, L0, S), 3033 ltr_complement(R, R0, S), 3034 ltr_invert(A, NA), 3035 ltr_insert(NA, R0, R1, S), 3036 ltr_join(L0, R1, Y, S) 3037 ).
3041ltr_invert(-A, A):-!. 3042ltr_invert(A, -A). 3043 3044% ?- complementary(a, -a). 3045% ?- complementary(-a, b).
3049complementary(-(A), A):-!. 3050complementary(A, -(A)).
3054% Change 0 and 1 at toplevel. Note that in CNF, 3055% toplevel 3056% 0 ( set- theoretically empty {} ) is true as a set of clauses, 3057% 1 ( set- theoretically singleton {{}} ) is false as a set of clauses, 3058% that is, unstisfiable.) 3059% In DNF, toplevel 0 and 1 are consistent with false and true, respectively. 3060 3061ltr_complement_toplevel(X, Y):- shift(ltr_complement_toplevel(X, Y)). 3062% 3063ltr_complement_toplevel(1, 0, _). 3064ltr_complement_toplevel(0, 1, _). 3065ltr_complement_toplevel(X, Y, S):- ltr_complement(X, Y, S). 3066 3067% ?- zdd((boole_to_cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S))). 3068%@ X = 4, 3069%@ Y = 7, 3070%@ S = [[b, c], [a, c]]. 3071% ?- zdd((boole_to_dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S))). 3072% ?- zdd((ltr_insert(a, 1, X), sets(X, S))). 3073% ?- zdd((ltr_insert(a, 1, X), 3074% ltr_insert(b, X, Y), sets(Y, S))). 3075% ?- zdd((ltr_insert(a, 1, X), 3076% ltr_insert(b, X, Y), 3077% ltr_insert(-b, Y, Z), 3078% sets(Z, S))). 3079% ?- zdd((ltr_insert(a, 1, X), 3080% ltr_insert(b, X, Y), 3081% ltr_insert(-b, Y, Z), 3082% sets(Z, S))).
3088ltr_insert(X, Y, Z):- shift(ltr_insert(X, Y, Z)). 3089% 3090ltr_insert(_, 0, 0, _):-!. 3091ltr_insert(A, 1, J, S):-!, zdd_singleton(A, J, S). 3092ltr_insert(A, I, J, S):- memo(ltr_insert(A,I)-J, S), 3093 ( nonvar(J) -> true 3094 ; cofact(I, t(X, L, R), S), 3095 ltr_compare(C, A, X), 3096 ( C = (=) -> zdd_join(L, R, U, S), 3097 ltr_cofact(J, t(A, 0, U), S) 3098 ; C = (<) -> ltr_cofact(J, t(A, 0, I), S) 3099 ; C = (>) -> ltr_insert(A, L, L0, S), 3100 ltr_insert(A, R, R0, S), 3101 ltr_cofact(J, t(X, L0, R0), S) 3102 ) 3103 ). 3104 3105% % simple version. 3106% ltr_merge(X, Y, Z):- shift(ltr_merge(X, Y, Z)). 3107% % 3108% ltr_merge(0, _, 0, _):-!. 3109% ltr_merge(_, 0, 0, _):-!. 3110% ltr_merge(1, X, X, _):-!. 3111% ltr_merge(X, 1, X, _):-!. 3112% ltr_merge(X, Y, Z, S):- 3113% ( X@<Y -> memo(ltr_merge(X,Y)-Z, S) 3114% ; memo(ltr_merge(Y,X)-Z, S) 3115% ), 3116% ( nonvar(Z) -> true 3117% ; cofact(Y, t(A, L, R), S), 3118% ltr_merge(X, R, U, S), 3119% ltr_merge(X, L, V, S), 3120% ltr_insert(A, U, U0, S), 3121% ltr_join(V, U0, Z, S) 3122% ). 3123 3124% 3125% longer version. (which is more efficient longer or shorter version) 3126 3127ltr_merge(X, Y, Z):- shift(ltr_merge(X, Y, Z)). 3128 3129% 3130ltr_merge(0, _, 0, _):-!. 3131ltr_merge(_, 0, 0, _):-!. 3132ltr_merge(1, X, X, _):-!. 3133ltr_merge(X, 1, X, _):-!. 3134ltr_merge(X, Y, Z, S):- 3135 ( X@<Y -> memo(ltr_merge(X,Y)-Z, S) 3136 ; memo(ltr_merge(Y,X)-Z, S) 3137 ), 3138 ( nonvar(Z) -> true 3139 ; cofact(X, t(A, L, R), S), 3140 cofact(Y, t(A0, L0, R0), S), 3141 ltr_compare(C, A, A0), 3142 ( C = (=) 3143 -> ltr_merge(L, L0, L_L0, S), 3144 ltr_merge(L, R0, L_R0, S), 3145 ltr_merge(L0, R, L0_R, S), 3146 ltr_merge(R, R0, R_R0, S), 3147 ltr_join(L_R0, L0_R, U, S), 3148 ltr_join(R_R0, U, V, S), 3149 ltr_cofact(Z, t(A, L_L0, V), S) 3150 ; C = (<) 3151 -> ltr_merge(L, Y, L_Y, S), 3152 ltr_merge(R, Y, R_Y, S), 3153 ltr_cofact(Z, t(A, L_Y, R_Y), S) 3154 ; ltr_merge(L0, X, L0_X, S), 3155 ltr_merge(R0, X, R0_X, S), 3156 ltr_cofact(Z, t(A0, L0_X, R0_X), S) 3157 ) 3158 ). 3159 3160% ?- zdd((X<<[a,c], Y<<[b, d, e], ltr_merge_line(X, Y, Z), psa(Z))). 3161% ?- zdd((X<<[a,b], Y<<[], ltr_merge_line(X, Y, Z), psa(Z))). 3162% ?- zdd((X<<[a,c], Y<<[b, d, e], ltr_merge_line(X, Y, Z), psa(Z))). 3163% ?- zdd((X<<[a,b], Y<<[-a, c], ltr_merge_line(X, Y, Z), psa(Z))). 3164% ?- zdd((X<<[a,c], Y<<[b, d, e], ltr_merge_line(X, Y, Z), psa(Z))). 3165% ?- zdd((zdd_line([-a,b], X), Y<<[a, b, c], ltr_merge_line(X, Y, Z), psa(Z))). 3166% special version of ltre_merge. 3167ltr_merge_line(X, Y, Z):- shift(ltr_merge_line(X, Y, Z)). 3168 3169ltr_merge_line(X, X, X, _):-!. % idempotent 3170ltr_merge_line(0, _, 0, _):-!. 3171ltr_merge_line(_, 0, 0, _):-!. 3172ltr_merge_line(1, X, X, _):-!. 3173ltr_merge_line(X, 1, X, _):-!. 3174ltr_merge_line(X, Y, Z, S):- cofact(X, t(A, _, R), S), 3175 cofact(Y, t(A0, _, R0), S), 3176 ( complementary(A, A0) 3177 -> Z = 0 3178 ; ltr_compare(C, A, A0), 3179 ( C = (<) 3180 -> ltr_merge_line(R, A0, R0, Z0, S), 3181 cofact(Z, t(A, 0, Z0), S) 3182 ; C = (=) 3183 -> ltr_merge_line(R, R0, Z0, S), 3184 cofact(Z, t(A, 0, Z0), S) 3185 ; ltr_merge_line(R0, A, R, Z0, S), 3186 cofact(Z, t(A0, 0, Z0), S) 3187 ) 3188 ). 3189 3190% 3191ltr_merge_line(0, _, _, 0, _):-!. 3192ltr_merge_line(1, A, R, Z, S):-!, cofact(Z, t(A, 0, R), S). 3193ltr_merge_line(X, A, R, Z, S):- cofact(X, t(B, _, R0), S), 3194 ( complementary(A, B) 3195 -> Z = 0 3196 ; compare(C, A, B), 3197 ( C = (<) 3198 -> ltr_merge_line(R, B, R0, Z0, S), 3199 cofact(Z, t(A, 0, Z0), S) 3200 ; C = (=) 3201 -> ltr_merge_line(R, R0, Z0, S), 3202 cofact(Z, t(A, 0, Z0), S) 3203 ; ltr_merge_line(R0, A, R, Z0, S), 3204 cofact(Z, t(B, 0, Z0), S) 3205 ) 3206 ). 3207 3208 3209% ?- zdd((cofact(B, t(-b, 1, 1)), 3210% cofact(C, t(a, 1, 1)), 3211% ltr_cofact(A, t(-a, C, B)), 3212% psa(C), psa(B), 3213% psa(A))). 3214% ?- zdd((cofact(B, t(-b, 1, 1)), 3215% cofact(C, t(-a, 1, 1)), 3216% ltr_cofact(A, t(a, C, B)), 3217% psa(C), psa(B), 3218% psa(A))). 3219 3220% Designed so that complentary pair does not appear in any clause. 3221ltr_cofact(X, Y):- shift(ltr_cofact(X, Y)). 3222 3223% 3224ltr_cofact(Z, FOS, S):- nonvar(Z), !, cofact(Z, FOS, S). 3225ltr_cofact(Z, t(A, V, U), S):- U > 1, !, 3226 cofact(U, t(B, L, _), S), 3227 ( complementary(A, B) 3228 -> ltr_cofact(Z, t(A, V, L), S) 3229 ; cofact(Z, t(A, V, U), S) 3230 ). 3231ltr_cofact(Z, T, S):- cofact(Z, T, S). 3232 3233% ?- zdd((X<<[a], ltr_insert(b, X, Y), psa(Y))). 3234% ?- zdd((X<<[b], ltr_insert(a, X, Y), psa(Y))). 3235% ?- zdd((X<<[a], ltr_insert(-a, X, Y), psa(Y))). 3236% ?- zdd((X<<[-a], ltr_insert(a, X, Y), psa(Y))). 3237% ?- zdd((X<<([a,b,c]+[u,v]), ltr_insert(-b, X, Y), psa(Y))). 3238% ?- zdd((X<<[a,b,c], ltr_insert(-b, X, Y), psa(Y))). 3239% ?- zdd((X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y))). 3240% ?- zdd((X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y))). 3241% ?- zdd((zdd_append([-a, b],1, X), psa(X), ltr_remove(-a, X, Y), psa(Y))). 3242% ?- zdd((X<<(set([-a, -b])+set([a, b, c])), psa(X), ltr_remove(b, X, Y), psa(Y))). 3243 3244ltr_remove(X, Y, Z):- shift(ltr_remove(X, Y, Z)). 3245% 3246ltr_remove(X, Y, Z, S):- zdd_shift(ltr_remove(X, Y, Z, S)). 3247 3248% 3249ltr_remove(_, I, I, _, _):- I<2, !. 3250ltr_remove(A, I, J, S, M):- memo(ltr_remove(I)-J, M), 3251 ( nonvar(J) -> true 3252 ; cofact(I, t(X, L, R), S), 3253 ltr_compare(C, A, X), 3254 ( C = (=) 3255 -> ltr_join(L, R, J, S) 3256 ; C = (<) 3257 -> J = I 3258 ; ltr_remove(A, L, L0, S), 3259 ltr_remove(A, R, R0, S), 3260 ltr_cofact(J, t(X, L0, R0), S) 3261 ) 3262 ). 3263 3264% ?- zdd((X<<{[]}, ltr_card(1, X, C))). 3265% ?- zdd((X<<{[]}, ltr_card(2, X, C))). 3266% ?- zdd((X<<{[a]}, ltr_card(1, X, C))). 3267% ?- zdd((X<<{[a]}, ltr_card(2, X, C))). 3268% ?- zdd((boole_to_dnf(a + (-a), X), ltr_card(1, X, C))). 3269% ?- zdd((boole_to_dnf(a + -a, X), ltr_card(2, X, C))). 3270% ?- zdd((boole_to_dnf(a + b, X), ltr_card(2, X, C))). 3271% ?- zdd((boole_to_dnf(a + b + c, X), ltr_card(3, X, C))). 3272% ?- zdd((boole_to_dnf(a + b + c + d, X), ltr_card(4, X, C))). 3273% ?- zdd((boole_to_dnf(-(a + b + c + d), X), ltr_card(4, X, C))). 3274% ?- zdd((boole_to_dnf(a + b + c + -d, X), ltr_card(4, X, C))). 3275% ?- zdd((boole_to_dnf(a * b, X), ltr_card(2, X, C))). 3276% ?- zdd((boole_to_dnf(a * b, X), ltr_card(3, X, C))). 3277% ?- zdd((boole_to_dnf(-(a * b), X), ltr_card(2, X, C))). 3278% ?- zdd((boole_to_dnf(-a * a, X), ltr_card(1, X, C))). 3279% ?- zdd((boole_to_dnf(-a * a, X), ltr_card(2, X, C))). 3280 3281% problematic 3282% ?- zdd((boole_to_dnf(a + -a, X), ltr_card(2, X, C))). 3283% ?- zdd((boole_to_dnf(a + -a, X), ltr_card(X, C))). 3284 3285 3286% ?- zdd((boole_to_dnf(a + b + -a, X), ltr_card(2, X, C))). 3287% ?- zdd((boole_to_dnf(a + b + -a, X), psa(X), ltr_card(2, X, C))). 3288% ?- zdd((boole_to_dnf(a + b + -a + -b, X), psa(X), ltr_card(2, X, C))). 3289% ?- zdd((boole_to_dnf(a + b + c + -a + -b + -c, X), psa(X), ltr_card(3, X, C))). 3290% ?- zdd((boole_to_dnf(a + c + -a + -b + -c, X), psa(X), ltr_card(3, X, C))). 3291 3292positive(-(_)):-!, fail. 3293positive(_). 3294 3295% ?- zdd(( X<<pow([a,b]), ltr_card(X, C))). 3296% ?- zdd(( dnf(a+b, X), psa(X), varnum(N), ltr_card(X, C))). 3297% ?- zdd(( dnf(A+B, X), ltr_card(X, C))). 3298% ?- zdd(( dnf(a, X), psa(X), ltr_card(X, C))). 3299 3300ltr_card(X, Y):- shift(ltr_card0(X, Y)). 3301 3302ltr_card0(X, Y, S):- memo(atomic_prop_memo-M, S), 3303 memo(varnum-N, M), 3304 ltr_card(N, X, Y, S). 3305 3306 3307ltr_card(N, X, Y):- shift(ltr_card(N, X, Y)). 3308% 3309ltr_card(N, X, Y, S):- zdd_shift(ltr_card(N, X, Y, S)). 3310ltr_card(_, 0, 0, _, _):-!. 3311ltr_card(N, 1, C, _, _):-!, C is 2^N. 3312ltr_card(N, X, C, S, M):- memo(path_count(N, X)-C, M), 3313 ( nonvar(C) -> true 3314 ; cofact(X, t(A, L, R), S), 3315 N0 is N-1, 3316 ( L > 1, 3317 positive(A), 3318 cofact(L, t(B, L0, R0), S), 3319 complementary(A, B) 3320 -> ltr_join(R, L0, U, S), % for not counting multple time. 3321 ltr_join(R0, L0, V, S), 3322 ltr_card(N0, U, C_U, S, M), 3323 ltr_card(N0, V, C_V, S, M), 3324 C is C_U + C_V 3325 ; ltr_card(N0, L, C_L, S, M), 3326 ltr_card(N0, R, C_R, S, M), 3327 C is C_L + C_R 3328 ) 3329 ). 3330 3331 3332% Remark. % 1 is "true", 0 is "false", but 2 is a basic proposition. 3333% ?- zdd((dnf(X+2+1, A), psa(A), ltr_card(2, A, C))). 3334% ?- zdd((dnf(X+2+0, A), psa(A), ltr_card(2, A, C))). 3335% ?- zdd((dnf(a(1)+ a(2), A),ltr_card(2, A, C))). 3336% ?- zdd((dnf(a+b+true, A), psa(A), ltr_card(2, A, C))). 3337% ?- zdd((dnf(a+b+false, A), psa(A), ltr_card(2, A, C))). 3338% ?- zdd((dnf(nand(a,b)+ exor(a, b), A), psa(A), ltr_card(2, A, C))). 3339% ?- zdd((dnf(a_nand(a,b)+ exor(a, b), A), psa(A), ltr_card(3, A, C))). 3340% ?- zdd((dnf(a_nand(a,b)+ b_exor(a, b), A), psa(A), ltr_card(2, A, C))).
3344atomic_prop(X) :- var(X), !. 3345atomic_prop(X) :- integer(X), X>1, !. 3346atomic_prop($(_)) :-!. % generated internally for prolog variable. 3347atomic_prop(X):- callable(X), 3348 \+ reserved_boole_symbol(X), 3349 functor(X, F, _), 3350 atom_codes(F, [C|_]), 3351 char_type(C, lower). 3352% 3353reserved_boole_symbol(1). 3354reserved_boole_symbol(0). 3355reserved_boole_symbol($(_)). 3356reserved_boole_symbol(true). 3357reserved_boole_symbol(false). 3358reserved_boole_symbol(not(_)). 3359reserved_boole_symbol(and(_,_)). 3360reserved_boole_symbol(or(_,_)). 3361reserved_boole_symbol(exor(_,_)). 3362reserved_boole_symbol(nand(_,_)). 3363reserved_boole_symbol(imply(_,_)). 3364reserved_boole_symbol(iff(_,_)). 3365reserved_boole_symbol(equiv(_,_)). 3366 3367% ?- zdd((dnf(-a, X), psa(X))). 3368% ?- zdd((dnf(A+B, X), ltr_card(2, X, C))). 3369 3370% ?- zdd((dnf(-(a+b), X), psa(X))). 3371% ?- zdd((dnf(-(a*b), X), psa(X))). 3372 3373% ?- collect_basics(f(1, A, a(2), A, 1, 2), R). 3374% ?- collect_basics(9+ a(1)+b(I)*x(3), R). 3375%% collect_basics(+A, -B) is det. 3376% Unify B with a list of basic boolean subterms appearing in A. 3377collect_basics(A, B):- collect_basics(A, B, atomic_prop). 3378% 3379collect_basics(A, B, Pred):- collect_basics(A, B0, [], Pred), 3380 sort(B0, B). 3381% 3382collect_basics([], L, L, _):- !. 3383collect_basics(X, [X|L], L, Pred):- call(Pred, X), !. 3384collect_basics([X|Y], L, L0, Pred):- !, 3385 collect_basics(X, L, L1, Pred), 3386 collect_basics(Y, L1, L0, Pred). 3387collect_basics(X, L, L0, Pred):- compound(X), !, 3388 X =..[_|As], 3389 collect_basics(As, L, L0, Pred). 3390collect_basics(_, L, L, _). 3391 3392% ?- make_boole_canonical(a->(b->c), R). 3393% ?- make_boole_canonical(a=b, R). 3394% ?- make_boole_canonical(+([a, b]), R). 3395% ?- make_boole_canonical(-(+([a, b])), R). 3396% ?- make_boole_canonical(-(*([a, b])), R). 3397% ?- make_boole_canonical(-(a+b), X). 3398% ?- make_boole_canonical(-(a+ -b), X). 3399% ?- make_boole_canonical(-(a = -b), X). 3400% ?- make_boole_canonical(-(-a = - -b), X). 3401% ?- make_boole_canonical(-(-(0) = - (-(0))), X). 3402% ?- make_boole_canonical(-(0), X). 3403% ?- make_boole_canonical(-(-(0)), X). 3404% ?- make_boole_canonical(p(1,1), X). 3405% ?- make_boole_canonical(true, X). 3406% ?- make_boole_canonical(false, X). 3407% ?- make_boole_canonical(-false, X). 3408% ?- make_boole_canonical(-true, X). 3409% ?- make_boole_canonical(- - -true, X). 3410% ?- make_boole_canonical(exor(a, b), X). 3411% ?- make_boole_canonical(nand(a, b), X). 3412% ?- make_boole_canonical(- nand(a, b), X). 3413% ?- make_boole_canonical(- #(a, b), X). 3414 3415make_boole_canonical(X, Y):- make_boole_canonical(X, Y, boole_macro). 3416% 3417:- meta_predicate make_boole_canonical(, , ). 3418% 3419make_boole_canonical(-(-(X)), Y, Pred):-!, 3420 make_boole_canonical(X, Y, Pred). 3421make_boole_canonical(-(X), Y, Pred):- make_boole_canonical(X, X0, Pred), !, 3422 ( de_morgan(X0, Y) -> true 3423 ; Y = -(X0) 3424 ). 3425make_boole_canonical(X, Y, Pred):- default_boole_macro(X, X0),!, 3426 make_boole_canonical(X0, Y, Pred). 3427make_boole_canonical(X, Y, Pred):- call(Pred, X, X0), !, 3428 make_boole_canonical(X0, Y, Pred). 3429make_boole_canonical(X, X, _). 3430 3431% ?- X= (a<-b). 3432 3433% 3434default_boole_macro(X->Y, -X + Y). 3435default_boole_macro(X=Y, (X->Y)*(Y->X)). 3436default_boole_macro(nand(X,Y), -(X*Y)). 3437default_boole_macro(exor(X,Y), (X + Y) * (-(X * Y))). 3438% 3439canonical_boole(X):- integer(X). 3440canonical_boole(+(_,_)). 3441canonical_boole(*(_,_)). 3442canonical_boole(-(_)). 3443canonical_boole(+(X)):- is_list(X). 3444canonical_boole(*(X)):- is_list(X). 3445 3446% 3447boole_macro(true, 1). 3448boole_macro(false, 0). 3449boole_macro(X =:= Y, X = Y). 3450boole_macro(X =\= Y, -(X = Y)). 3451boole_macro(X <=> Y, X = Y). 3452boole_macro(X \= Y, -(X = Y)). 3453boole_macro(X =\= Y, -(X = Y)). 3454boole_macro(X >= Y, Y -> X). % in harmony arithmetic > 3455boole_macro(X =< Y, X -> Y). % in harmony arithmetic < 3456boole_macro(X ~ Y, X = Y). 3457boole_macro(X <-> Y, X = Y). 3458boole_macro(\/(X,Y), +(X,Y)). 3459boole_macro(\(X), -(X)). 3460boole_macro(/\(X, Y), *(X,Y)). 3461boole_macro((X; Y), +(X,Y)). 3462boole_macro(\+(X), -(X)). 3463boole_macro((X, Y), *(X,Y)). 3464boole_macro(#(X, Y), exor(X,Y)). 3465boole_macro(exor(X, Y), (X + Y)*(-X + -Y)). 3466boole_macro(nand(X, Y), -(X * Y)). 3467boole_macro(equiv(X, Y), X = Y). 3468boole_macro(imply(X, Y), -(X) + Y). 3469boole_macro(not(X), -(X)). 3470boole_macro(and(X, Y), *(X,Y)). 3471boole_macro(or(X, Y), +(X,Y)). 3472 3473% 3474de_morgan(1, 0). 3475de_morgan(0, 1). 3476de_morgan(-(X), X). % double negation. 3477de_morgan(*(X, Y), (-X) + (-Y)). % de Morgan 3478de_morgan(+(X, Y), (-X) * (-Y)). % de Morgan 3479de_morgan(*(X), +(Y)):- maplist(negate_macro, X, Y). 3480de_morgan(+(X), *(Y)):- maplist(negate_macro, X, Y). 3481 3482% 3483pred_plus(A, U, A + U). 3484pred_mul(A, U, A * U). 3485% 3486negate_macro(X, -(X)). 3487 3488% ?- univ_to_binary(+([X,Y,Z]), R). 3489% ?- univ_to_binary(*([X,Y,Z]), R). 3490univ_to_binary(U, B):- U=..[F, L], univ_to_binary(L, F, B). 3491% 3492univ_to_binary([X], _, X):-!. 3493univ_to_binary([X,Y|Z], F, B):- univ_to_binary([Y|Z], F, B0), 3494 B=..[F, X, B0]