1:- module(zmod, 2 [ (<<)/2, (<<)/3, fetch_state/1, fetch_state/2 3 , card/3 4 , ltr_join/4, ltr_join_list/3, ltr_join_list/4 5 , ltr_merge/4, ltr_card/3 6 , card_filter_gte/4, card_filter_lte/4, card_filter_between/5 7 , max_length/3 8 , sat/1, sat_count/1, sat_count/2 9 , set_at/3 10 , obj_id/3 11 , dnf/3, cnf/3, nnf_dnf/3, nnf_cnf/3 12 , all_fun/4, s_map/3, s_map/4 13 , all_mono/4, all_epi/4, merge_funs/3 14 , bdd_list/3, bdd_list_raise/4, bdd_append/4, bdd_interleave/4 15 , opp_compare/3 16 , (zdd)/1, zdd0/1, zdd_eval/3, zdd_eval/4, (ltr_zdd)/1 17 , zdd_append/4 18 , zdd_insert/4, zdd_insert/5, zdd_insert_atoms/3, zdd_cons/4 19 , l_cons/4 20 , zdd_insert_atoms/4 21 , zdd_ord_insert/4, zdd_reorder/4 22 , zdd_has_1/2 23 , zdd_memberchk/2, zdd_memberchk/3 24 , zdd_family/3 25 , zdd_subfamily/3 26 , zdd_join/4, zdd_join_1/3, zdd_join_list/3, zdd_join_list/4 27 , zdd_singleton/3 28 , zdd_merge/4 29 , zdd_merge_list/4 30 , zdd_meet/4 31 , zdd_subtr/4, zdd_subtr_1/3, zdd_xor/4 32 , zdd_div/4, zdd_mod/4, zdd_divmod/5, zdd_div_div/5 33 , zdd_mod_by_list/4, zdd_div_by_list/4, zdd_divisible_by_list/4 34 , zdd_power/3, zdd_ord_power/4 35 , zdd_rand_path/2, zdd_rand_path/3, zdd_rand_path/4 36 , ltr_meet_filter/4, ltr_join_filter/4 37 , get_extra/1, get_extra/2 38 , get_key/3, atom_index/2 39 , set_key/3, update_key/4, bump_up/3 40 , set_pred/2, set_pred/3, set_pred/2, set_pred/3 41 , zdd_compare/4 42 , zdd_sort/3 43 , open_key/3, close_key/2 44 , set_compare/1, set_compare/2, get_compare/2 45 , use_zdd/1, use_zdd/2, pred_zdd/2, pred_zdd/3 46 , zdd_sort_rev/2, zdd_sort_rev/3 47 , map_zdd/4, zdd_find/4 48 , psa/2, psa/0, psa/3, mp/2, mp/3 49 , sets/3, ppoly/2, poly_term/2, poly_term/3 50 , eqns/3 51 , zdd_list/3, zdd_lift/3 52 , significant_length/3 53 , charlist/2, charlist/3, atomlist/2 54 , op(900, xfx, <<) 55 , op(1150, fy, zdd) 56 , op(1150, fy, ltr_zdd) 57 ]). 58 59 60% :- doc_server(7000). 61% :- use_module(library(pldoc/doc_library)). 62% :- doc_load_library. 63% :- doc_browser. 64 65:- use_module(library(apply)). 66:- use_module(library(apply_macros)). 67:- use_module(library(clpfd)). 68:- use_module(library(statistics)). 69:- use_module(zdd('zdd-array')). 70:- use_module(util(math)). 71:- use_module(util(meta2)). 72:- use_module(pac(basic)). 73:- use_module(pac(meta)). 74:- use_module(util(misc)). 75:- use_module(pac('expand-pac')). % For the kind block. 76:- use_module(pac(op)). 77:- use_module(zdd('path-count-by-mate-frontier')). 78 79:- set_prolog_flag(stack_limit, 10_200_147_483_648). 80 81attr_unify_hook(V, Y):- 82 ( get_attr(Y, zdd, A) 83 -> zdd_unify(V, A) 84 ; zdd_unify(V, Y) 85 ). 86 87 :- op(800, xfy, &). 88 :- op(820, fy, \). % NOT 89 :- op(830, xfy, /\). % AND 90 :- op(840, xfy, \/). % OR 91 :- op(860, xfy, ~). % equivalence 92 :- op(860, xfy, #). % exor 93 :- op(860, xfy, <->). % equivalence 94 :- op(860, xfy, <=> ). % equivalence 95 :- op(870, yfx, <-). 96 97% for pac query. 98term_expansion --> pac:expand_pac. 99 100% ?- zdd udg_path_count(a, b, [a-b,b-c,a-c], C). 101% ?- zdd C<< :(!udg_path_count(a, b, [a-b,b-c,a-c])). 102% ?- udg_path_count(a, b, [a-b,b-c,a-c], C, S). 103% ?- (zdd true). 104% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), Z<< (X+Y), U<< card(Z). 105% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), Z<< :arith(X+Y). 106% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), { Z is X+Y }. 107% ?- numlist(1, 16, L), zdd((X<< pow(L), card(X, C))). 108%@ L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 109%@ X = 17, 110%@ C = 65536. 111% ?- numlist(1, 16, L), zdd((X<< pow(L))). 112% ?- numlist(1, 10000, L), zdd((X<< pow(L), card(X, C))). 113% ?- numlist(1, 16, L), 114% zdd((X<< pow(L), Y<<pow(L), Z << (X+Y), U<< (X*Y), card(X, C))). 115% ?- time((numlist(1, 40, L), 116% zdd((X << pow(L), Y<<pow(L), Z << merge(X, Y), card(Z, C))))). 117% ?- zdd((set_memo(a-1))). 118% ?- zdd((set_memo(a-1), set_memo(a-2), memo(a-V))). 119% ?- zdd set_memo(a-1), set_memo(a-2), memo(a-V). 120% ?- zdd X<<{[1,1]}, psa(X). 121% ?- zdd X<< pow(:numlist(0,1)), psa(X). 122% ?- zdd((X<<pow([1,2,3]), psa(X))). 123% ?- zdd((X<< *([1,2,3,1]), psa(X))). 124% ?- zdd((X<< +([1,2,3,1]), psa(X))). 125% ?- zdd((X<< family([[1],[1,2], [1]]), psa(X))). 126% ?- zdd((X<< family([[a-b, b-c]]), prz(X))). 127% ?- zdd memo(a-1), memo(a-X). 128 129% ?- zdd(use_zdd(use_zdd((#memo(a-1), #memo(a-X))))). 130% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))}, sets(X, Sx))). 131% ?- zdd((X<<pow([1,2]), {zdd((Y<<pow([a,b]), sets(Y, Sy)))}, 132% sets(X, Sx), sets(Y, Sy1))). 133% ?- zdd((set_key(root, hello), get_key(root, R))). 134% ?- zdd((all_fun([a],[b], F), psa(F))). 135% ?- zdd((all_fun([],[b], F), psa(F))). 136% ?- zdd((all_fun([a],[], F), psa(F))). 137% ?- zdd((all_fun([a,b],[c,d], F), psa(F), card(F, C))). 138% ?- N = 20, numlist(1, N, A), raise_list(A, 2, A2), zdd((all_fun(A2, A, F), card(F, C))). 139% ?- time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 140% zdd((all_fun(Ns, Ms, F), card(F, C))))). 141 142% Cardinality # of Y^X = { f | f: X-> Y }. 143% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 144 145% ?- I=1, J=1, K=1, L=1, 146% numlist(1, I, X), numlist(1, K, Y), 147% raise_list(X, J, Xj), 148% raise_list(Y, L, Yl), 149% time( ( call_with_time_limit(200, ( 150% zdd((all_fun(Xj, Yl, F), card(F, C))))), 151% C =:= (K^L)^(I^J), 152% significant_length(C, Keta, 10))). 153 154% ?- I=3, J=5, K=3, L=5, 155% numlist(1, I, X), numlist(1, K, Y), 156% raise_list(X, J, Xj), 157% raise_list(Y, L, Yl), 158% time( ( call_with_time_limit(200, ( 159% zdd((all_fun(Xj, Yl, F), card(F, C))))), 160% C =:= (K^L)^(I^J), 161% significant_length(C, Keta, 10))). 162 163significant_length(0, 0, _):-!. 164significant_length(X, 1, Radix):- X < Radix, !. 165significant_length(X, L, Radix):- Y is X // Radix, 166 significant_length(Y, L0, Radix), 167 L is L0+1. 168% 169zdd_atom(X):- shift(zdd_atom(X)). 170% 171zdd_atom(X, S):- get_key(is_atom, Pred, S), !, call(Pred, X). 172zdd_atom(X, _):- (atomic(X); dvar(X)), !.
obj_id([a,b,c], Id)
, obj_id(Obj, Id)
.177obj_id(X, Id, S):- cofact(Id, t(X, 0, 1), S). 178% 179hyphen(X, Y, X-Y). 180comma(X, Y, (X,Y)). 181equality(X, Y, (X=Y)). 182dvar('$VAR'(_)). 183 184 /***************************************** 185 * all_fun/all_mono/all_epi in ZDD * 186 *****************************************/
190% ?- zdd all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F). 191% ?- zdd all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C). 192% ?- N = 100, numlist(1, N, Ns), (zdd all_fun(Ns, Ns, F), card(F, C)). 193% ?- numlist(1, 5, Ns), numlist(6, 10, Ms), 194% (zdd 195% all_fun(Ns, Ns, F), 196% all_fun(Ms, Ms, G), 197% zdd_merge(F, G, H), 198% card(H, C) 199% ), 200% C =:= 5^5 * 5^5. 201 202all_fun(D, R, F, S):- zdd_sort(D, D0, S), 203 zdd_sort(R, R0, S), 204 length(D0, I), 205 length(R0, J), 206 ( I > 0, J = 0 -> F = 0 207 ; zdd_append(D0, 1, D1, S), 208 findall_fun(D1, R0, F, S) 209 ). 210% 211findall_fun(X, _, X, _):- X < 2, !. 212findall_fun(X, Rng, Y, S):- memo(findall_fun(X)-Y, S), 213 ( nonvar(Y) -> true % , write(.) % many hits. 214 ; cofact(X, t(A, L, R), S), 215 findall_fun(L, Rng, L0, S), 216 findall_fun(R, Rng, R1, S), 217 join_for_alt_val(A, Rng, R1, 0, R0, S), 218 zdd_join(L0, R0, Y, S) 219 ). 220% 221join_for_alt_val(_, [], _, V, V, _). 222join_for_alt_val(A, [B|Bs], F, F0, F1, S):- 223 zdd_cons(F2, A-B, F, S), 224 zdd_join(F0, F2, F3, S), 225 join_for_alt_val(A, Bs, F, F3, F1, S).
230% ?- zdd all_mono([1],[a], Is), psa(Is). 231% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is). 232% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is). 233% ?- zdd all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C). 234% ?- zdd all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C). 235% ?- time((numlist(1, 10, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)), factorial(10, C))). 236% ?- time((numlist(1, 12, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)))). 237% ?- N =10, numlist(1, N, Ns), time((zdd all_mono(Ns, Ns, F), card(F, C))), factorial(N, C). 238 239all_mono(D, R, F, S):- zdd_sort(D, D0, S), 240 zdd_sort(R, R0, S), 241 length(D0, I), length(R0, J), 242 ( I @=< J -> 243 zdd_append(D0, 1, D1, S), 244 findall_mono(D1, R0, F, S) 245 ; F = 0 246 ). 247 248% ?- zdd zdd_append([], 1, X), findall_mono(X, [a], Y). 249% ?- zdd zdd_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y). 250% ?- zdd { N=14, numlist(1, N, Ns)}, zdd_append(Ns, 1, X), 251% findall_mono(X, Ns, Y), card(Y, C), 252% { factorial(14, D), ( D=:=C -> writeln("OK")) }. 253 254findall_mono(X, _, X, _):- X < 2, !. 255findall_mono(X, Rng, Y, S):- memo(findall_mono(X,Rng)-Y, S), 256 ( nonvar(Y) -> true % , write(.) % many hits. 257 ; cofact(X, t(A, L, R), S), 258 findall_mono(L, Rng, L0, S), 259 findall_mono(A, R, Rng, R0, S), 260 zdd_join(L0, R0, Y, S) 261 ). 262% 263findall_mono(A, R, Rng, R0, S):- findall(B-U, select(B, Rng, U), Cases), 264 findall_mono(Cases, A, R, 0, R0, S). 265% 266findall_mono([], _A, _R, V, V, _). 267findall_mono([B-Rng|Cases], A, R, U, V, S):- 268 findall_mono(R, Rng, U0, S), 269 cofact(U1, t(A-B, 0, U0), S), 270 zdd_join(U, U1, U2, S), 271 findall_mono(Cases, A, R, U2, V, S).
277% ?- zdd all_epi([],[], F). 278% ?- zdd all_epi([a],[1], F), psa(F). 279% ?- zdd all_epi([a,b],[1], F), psa(F). 280% ?- zdd all_epi([a],[1,2], F), psa(F). 281% ?- zdd all_epi([a,b,c],[1,2], F), psa(F). 282% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (zdd all_epi(Ns, Ms, F)). 283% ?- time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (zdd all_epi(Ns, Ms, F)))). 284 285all_epi(D, R, F, S):- 286 zdd_sort(D, D0, S), 287 zdd_sort(R, R0, S), 288 length(D0, I), length(R0, J), 289 ( I @>= J -> 290 zdd_append(D0, 1, D1, S), 291 findall_epi(D1, R0-R0, F, S) 292 ; F = 0 293 ).
298% ?- N=2, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 299% ?- N=3, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 300% ?- N=10, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 301% ?- N=11, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 302% ?- N=14, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 303% ?- N=15, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C))))X. 304% ?- N=16, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 305%@ % 185,729,299 inferences, 205.838 CPU in 207.237 seconds (99% CPU, 902308 Lips) 306% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R), 307% length(R, L). 308 309all_perm(D, P, S):- zdd_sort(D, D0, S), 310 findall_perm(D0, P, S). 311% 312findall_perm([], 1, _):-!. 313findall_perm(D, X, S):- memo(perm(D)-X, S), 314 ( nonvar(X) -> true % , write(.) % many hits. 315 ; 316 findall(I-D0, select(I, D, D0), U), 317 join_perm_for_selection(U, 0, X, S)). 318% 319join_perm_for_selection([], X, X, _). 320join_perm_for_selection([I-D|U], X, Y, S):- 321 findall_perm(D, X0, S), 322 zdd_cons(X1, I, X0, S), 323 zdd_join(X1, X, X2, S), 324 join_perm_for_selection(U, X2, Y, S). 325 326 /************************************************* 327 * terms in ZDD based on families of lists * 328 *************************************************/
337% ?- zdd coalgebra_for_signature([x], [f/1], [x], E), psa(E). 338% ?- zdd coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E). 339% ?- time((zdd coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2], 340% [x,y,z,u,v,0,1], E), card(E, C))). 341%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips) 342%@ E = 173825, 343%@ C = 68641485507. 344 345coalgebra_for_signature(D, Sgn, As, E, S):- 346 signature(Sgn, As, T, S), 347 signature_map(D, T, E, S). 348% 349signature_map([], _, 1, _):-!. 350signature_map([X|Xs], T, E, S):- 351 signature_map(Xs, T, E0, S), 352 extend_signature_map(X, T, E0, E, S). 353% 354extend_signature_map(_, 0, _, 0, _):-!. 355extend_signature_map(_, 1, E, E, _):-!. 356extend_signature_map(X, T, E, F, S):- cofact(T, t(A, L, _), S), 357 extend_signature_map(X, L, E, E0, S), 358 l_cons(X->A, E, E1, S), 359 zdd_join(E0, E1, F, S).
364% ?- zdd term_path(a, R), psa(R), term_path(A, R). 365term_path(X, Y, S):- 366 ( nonvar(X) -> term_to_path(X, Y, S) 367 ; path_to_term(Y, X, S) 368 ).
373% ?- zdd term_to_path(a, R), psa(R). 374% ?- zdd term_to_path(f(a, b), R), psa(R). 375% ?- zdd term_to_path(f(g(a, b), h(c, d)), R), psa(R). 376% ?- zdd term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R). 377term_to_path(X, Y, S):- functor(X, F, N), 378 ( N = 0 -> zdd_singleton(X, Y, S) 379 ; functor(X, F, N), 380 arg_path(F/N, 1, X, Y, S) 381 ). 382% 383arg_path(_/N, J, _, 0, _):- J>N, !. 384arg_path(F, I, X, Y, S):- J is I + 1, 385 arg(I, X, A), 386 term_to_path(A, U, S), 387 arg_path(F, J, X, V, S), 388 cofact(Y, t(arg(F, I), V, U), S).
394% ?- zdd term_to_path(a, X), path_to_term(X, R). 395% ?- zdd term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R). 396% ?- zdd term_to_path(f(1,2), X), path_to_term(X, R). 397% ?- T=f(h(a), 3, g(b,2), 5), 398% (zdd term_to_path(T, X), path_to_term(X, R)), T = R. 399 400path_to_term(X, Y, S):- X>1, cofact(X, t(A, L, R), S), 401 ( R = 1 -> Y = A 402 ; A = arg(F/_, _), 403 path_to_term(R, R0, S), 404 path_to_term(L, L0, [], S), 405 Y =..[F, R0|L0] 406 ). 407% 408path_to_term(X, U, U, _):- X<2, !. 409path_to_term(X, [R0|U], V, S):- cofact(X, t(_, L, R), S), 410 path_to_term(R, R0, S), 411 path_to_term(L, U, V, S).
compare(C, U, V)
is performed.418% ?- X=f(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 419% term_path_compare(C0, T, U)), compare(C, X, Y). 420% ?- X=g(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 421% term_path_compare(C0, T, U)), compare(C, X, Y). 422% ?- X=g(a,b,c), Y=f(a,b), (zdd term_path(X, T), term_path(Y, U), 423% term_path_compare(C0, T, U)), compare(C, X, Y). 424 425term_path_compare(=, X, X, _):-!. 426term_path_compare(<, 0, _, _):-!. 427term_path_compare(>, _, 0, _):-!. 428term_path_compare(<, 1, _, _):-!. 429term_path_compare(>, _, 1, _):-!. 430term_path_compare(C, X, Y, S):- cofact(X, t(A, L, R), S), 431 cofact(Y, t(B, L0, R0), S), 432 arity_compare(C0, A, B), 433 ( C0 = (=) -> 434 term_path_compare(C1, R, R0, S), 435 ( C1 = (=) -> 436 left_branch_compare(C, L, L0, S) 437 ; C = C0 438 ) 439 ; C = C0 440 ). 441 442% Left branches are for argument lists of the ame length. 443left_branch_compare(=, 0, 0, _):-!. 444left_branch_compare(C, X, Y, S):- 445 cofact(X, t(_, L, R), S), 446 cofact(Y, t(_, L0, R0), S), 447 term_path_compare(C0, R, R0, S), 448 ( C0 = (=) -> 449 left_branch_compare(C, L, L0, S) 450 ; C = C0 451 ). 452 453% 454arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G). 455arity_compare(C, A, B):-!, compare(C, A, B).
462% ?- zdd zdd_lift(1, X). 463% ?- zdd X<< pow([1,2]), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D), psa(Y). 464% ?- N=15, numlist(1, N, Ns), 465% time((zdd X<< pow(Ns), card(X, C), zdd_lift(X, Y), card(Y, D))). 466%@ C = D, D = 32768, 467%@ Y = 131040. 468 469zdd_lift(X, X, _):- X<2, !. 470zdd_lift(X, Y, S):- memo(zdd_lift(X)-Y, S), 471 ( nonvar(Y) -> true %, write(.) % So so hits. 472 ; cofact(X, t(A, L, R), S), 473 zdd_lift(L, L0, S), 474 zdd_lift(R, R0, S), 475 l_cons(A, R0, R1, S), 476 zdd_join(L0, R1, Y, S) 477 ).
483% ?- zdd X<< pow([a,b]), card(X, C), zdd_lift(X, Y), card(Y, D), zdd_univ(Y, Z), psa(Z). 484 485zdd_univ(X, X, _):- X<2, !. 486zdd_univ(X, Y, S):- cofact(X, t(A, L, _), S), 487 zdd_univ(L, L0, S), 488 U=..A, 489 cofact(Y, t(U, L0, 1), S). 490 491% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 492zdd_univ(0, _, 0, _):-!. 493zdd_univ(1, Stack, X, S):-!, reverse(Stack, Stack0), 494 U =.. Stack0, 495 zdd_singleton(U, X, S). 496zdd_univ(X, Stack, Y, S):- cofact(X, t(A, L, R), S), 497 zdd_univ(L, Stack, L0, S), 498 zdd_univ(R, [A|Stack], R0, S), 499 zdd_join(L0, R0, Y, S).
g(a1, ..., an)
where G=g/n and ai in As.505% ?- zdd arity_term(f/2, [1, x, y], T), psa(T). 506arity_term(F/N, As, T, S):- memo((F/N)-T, S), 507 ( nonvar(T) -> true 508 ; all_list(N, As, X, S), 509 l_cons(F, X, T0, S), 510 zdd_univ(T0, [], T, S) 511 ).
519% ?- N=10, numlist(1, N, Ns), 520% time((zdd X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))). 521% ?- zdd X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y). 522% ?- N=100, numlist(1, N, Ns), 523% time((zdd X<<pow(Ns), l_cons(f, X, Y), card(Y, C))). 524% ?- N=100, numlist(1, N, Ns), 525% time((zdd X<<pow(Ns), distribute_cons([f, g, h], X, Y), card(Y, C))). 526 527zdd_functor(F, X, Y, S):- zdd_functor(F, X, [], Y, S). 528% 529zdd_functor(_, 0, _, 0, _):-!. 530zdd_functor(F, 1, St, Y, S):-!, T =..[F|St], 531 zdd_singleton(T, Y, S). 532zdd_functor(F, X, St, Y, S):-cofact(X, t(A, L, R), S), 533 zdd_functor(F, L, St, Y0, S), 534 zdd_functor(F, R, [A|St], Y1, S), 535 zdd_join(Y0, Y1, Y, S).
f(a1, ..., an)
with f/n in G and ai in As.541% ?- zdd signature([f/1, g/2], [1, x, y], U), psa(U). 542% ?- time((zdd signature([f/2, g/2, h/3, i/4, k/5], 543% [0, 1, 2, x, y, z, u, v, w], U), card(U, C))). 544 545signature([], _, 0, _):-!. 546signature([G|Gs], As, T, S):- 547 arity_term(G, As, T0, S), 548 signature(Gs, As, T1, S), 549 zdd_join(T0, T1, T, S).
555% ?- spy(power_list). 556% ?- zdd power_list(0, [a,b], P). 557% ?- zdd power_list(1, [a,b], P). 558% ?- N = 100, numlist(1, N, _Ns), 559% time(((zdd power_list(N, _Ns, X), card(X, _Count)))), 560% _Count > 100^100, writeln(_Count). 561%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips) 562%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101 563%@ N = 100, 564%@ X = 515002. 565 566power_list(N, As, P, S):- obj_id(As, Id, S), 567 power_list_with_id(N, Id, P, S). 568% 569power_list_with_id(0, Id, 1, S):-!, memo(power_list(0, Id)-1, S). 570power_list_with_id(N, Id, Y, S):- 571 N0 is N - 1, 572 power_list_with_id(N0, Id, Y0, S), 573 all_list_with_id(N, Id, Y1, S), 574 zdd_join(Y0, Y1, Y, S).
580% ?- zdd all_list(0, [a], X), psa(X). 581% ?- zdd all_list(1, [a], X), psa(X). 582% ?- N=10, numlist(1, N, Ns), (zdd all_list(4, Ns, X), card(X, C)). 583% ?- N=100, numlist(1, N, Ns), time(((zdd all_list(100, Ns, X), card(X, C)))). 584%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips) 585 586all_list(N, As, Y, S):- obj_id(As, Id, S), 587 all_list_with_id(N, Id, Y, S). 588% 589all_list_with_id(0, Id, 1, S):-!, memo(all_list(0, Id)-1, S). 590all_list_with_id(N, Id, Y, S):- memo(all_list(N, Id)-Y, S), 591 ( nonvar(Y) -> true 592 ; N0 is N-1, 593 all_list_with_id(N0, Id, Y0, S), 594 obj_id(As, Id, S), 595 distribute_cons(As, Y0, 0, Y, S) 596 ).
601singleton_family([], 0, _):-!. 602singleton_family([A|As], X, S):- 603 singleton_family(As, X0, S), 604 zdd_singleton(A, U, S), 605 zdd_join(U, X0, X, S).
610distribute_cons(F, X, Y, S):- distribute_cons(F, X, 0, Y, S). 611% 612distribute_cons([], _, Y, Y, _). 613distribute_cons([A|As], Y, U, V, S):- 614 l_cons(A, Y, V0, S), 615 zdd_join(U, V0, U0, S), 616 distribute_cons(As, Y, U0, V, S).
621% ?- zdd X<<pow([1,2]), l_cons(a, X, Y), psa(Y). 622l_cons(A, Y, U, S):- cofact(U, t(A, 0, Y), S).
append(L, U, M)
with U in X.
?- zdd X<<pow([1,2])
, l_append([a,b], X, Y)
, psa(Y)
.629l_append([], X, X, _). 630l_append([A|As], X, Y, S):- 631 l_append(As, X, X0, S), 632 l_cons(A, X0, Y, S). 633 634% ?- zdd zdd_append([], 1, X), findall_epi(X, [a]-[a], Y). 635% ?- zdd zdd_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 636% ?- zdd zdd_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 637% ?- zdd zdd_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C). 638% ?- zdd zdd_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y). 639% ?- N = 2, (zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 640% ?- N = 3, (zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 641% ?- N = 10,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), 642% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 643% ?- N = 11,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), 644% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 645% ?- N = 12,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), 646% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 647% ?- N = 13,(zdd {numlist(1, N, Ns)}, zdd_append(Ns, 1, X), 648% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 649 650select_target(Range, U, B, V):- member(B, Range), 651 ( select(B, U, V) -> true 652 ; V = U 653 ). 654 655%! 656findall_epi(0, _, 0, _):-!. 657findall_epi(1, _-U, X, _):-!, 658 ( U=[] -> X = 1 659 ; X = 0 660 ). 661findall_epi(X, RngU, Y, S):- memo(findall_epi(X, RngU)-Y, S), 662 ( nonvar(Y) -> true % , write(.) % many hits. 663 ; cofact(X, t(A, L, R), S), 664 findall_epi(L, RngU, L0, S), 665 findall_epi(A, R, RngU, R0, S), 666 zdd_join(L0, R0, Y, S) 667 ). 668% 669findall_epi(A, R, Rng-U, R0, S):- 670 findall(B-(Rng-V), select_target(Rng, U, B, V), Cases), 671 findall_epi(Cases, A, R, 0, R0, S). 672% 673findall_epi([], _, _, V, V, _). 674findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V, S):- 675 findall_epi(R, Rng-Rng0, U0, S), 676 cofact(U1, t(A-B, 0, U0), S), 677 zdd_join(U, U1, U2, S), 678 findall_epi(Cases, A, R, U2, V, S). 679 680% ?- zdd merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X). 681merge_funs(Fs, X, S):- fold_merge_funs(Fs, 1, X, S). 682% 683fold_merge_funs([], X, X, _). 684fold_merge_funs([G|Fs], X, Y, S):- 685 fun_block(G, X0, S), 686 zdd_merge(X, X0, X1, S), 687 fold_merge_funs(Fs, X1, Y, S). 688% 689fun_block(G, X, S):- 690 ( G = mono(D-R) -> all_mono(D, R, X, S) 691 ; G = epi(D-R) -> all_epi(D, R, X, S) 692 ; G = fun(D-R), 693 all_fun(D, R, X, S) 694 ). 695 696% ?- N=2, numlist(1, N, Ns), 697% (zdd set_compare(opp_compare), 698% X<<pow(Ns), psa(X), set_compare(compare), 699% zdd_normalize(X, Y), psa(Y)). 700 701zdd_normalize(X, X, _):- X<2, !. 702zdd_normalize(X, Y, S):- memo(normalize(X)-Y, S), 703 ( nonvar(Y) -> true % , write(.) % Many hits. 704 ; cofact(X, t(A, L, R), S), 705 zdd_normalize(L, L0, S), 706 zdd_normalize(R, R1, S), 707 zdd_insert(A, R1, R0, S), 708 zdd_join(L0, R0, Y, S) 709 ). 710 711% ?- N = 1000, numlist(1, N, Ns), 712% time(zdd((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C)))). 713 714% ?- N = 1000, numlist(1, N, Ns), 715% time(zdd(( X<<pow(Ns), 716% get_family_of_rank(500, X, Y), 717% card(Y, C)))).
722get_family_of_rank(Order, X, F):- shift(get_family_of_rank(Order, X, F)). 723% 724get_family_of_rank(Order, X, F, S):- rank_family_by_card(X, _, S), 725 memo(family_with_card(Order)-F, S). 726 727% ?- zdd X<<set([a]), rank_family_by_card(X, P), 728% memo(family_with_card(0)-L), sets(L, Sl), 729% memo(family_with_card(1)-M), sets(M, Sm).
734rank_family_by_card(X, Y):- shift(rank_family_by_card(X, Y)). 735% 736rank_family_by_card(0, 0, _):-!. 737rank_family_by_card(1, 0, S):-!, memo(family_with_card(0)-1, S). 738rank_family_by_card(I, P, S):- memo(rank_family_by_card_done(I)-B, S), 739 ( nonvar(B) -> true 740 ; cofact(I, t(A, L, R), S), 741 rank_family_by_card(L, Pl, S), 742 rank_family_by_card(R, Pr, S), 743 max(Pl, Pr, P0), 744 insert_one_to_family(A, P0, New, S), 745 P is P0 + 1, 746 memo(family_with_card(P)-New, S), 747 B = true 748 ). 749% 750insert_one_to_family(A, 0, G, S):-!, memo(family_with_card(0)-F, S), 751 zdd_insert(A, F, G, S). 752insert_one_to_family(A, P, G, S):- P0 is P-1, 753 insert_one_to_family(A, P0, G0, S), 754 memo(family_with_card(P)-Fp, S), 755 zdd_insert(A, Fp, G, S), 756 zdd_join(Fp, G0, Gp, S), 757 set_memo(family_with_card(P)-Gp, S). 758 759 /********************** 760 * State access * 761 **********************/ 762 763get_extra(Extra):- shift(get_extra(Extra)). 764get_extra(Extra, S):- arg(2, S, Extra). 765% 766set_extra(Extra):- shift(set_extra(Extra)). 767set_extra(Extra, S):- setarg(2, S, Extra). 768 769% ?- zdd bump_up(a, N), bump_up(a, K). 770bump_up(Key, N, S):- arg(2, S, Extra), 771 ( select(Key-N0, Extra, Extra0) -> true 772 ; N0 = 0, 773 Extra0 = Extra 774 ), 775 N is N0 + 1, 776 setarg(2, S, [Key-N|Extra0]). 777% 778:- meta_predicate set_compare( ). 779:- meta_predicate set_compare( , ). 780set_compare(Compare):- shift(set_compare(Compare)). 781set_compare(Compare, S):- setarg(3, S, Compare). 782 783% ?- zdd0((zdd_compare(C, a->b, a-b))). 784% ?- zdd((zdd_compare(C, a, b))). 785% ?- zdd0((zdd_compare(C, a, b))). 786 787get_compare(Compare, S):- arg(3, S, Compare). 788% 789% 790zdd_compare(C, X, Y, S):- arg(3, S, F), call(F, C, X, Y). 791 792% ?- zdd((zdd_sort([1->1, 1->2, 1-1, 2-2], X))). 793% 794zdd_sort(X, Y, S):- get_compare(Comp, S), 795 predsort(Comp, X, Y). 796 797% ?- zdd get_key(a, V), set_key(a, 1), get_key(a, W). % fail. 798% ?- zdd set_key(a, 1), get_key(a, W). 799get_key(K, V, S):- arg(2, S, Assoc), memberchk(K-V, Assoc). 800% 801set_key(K, V, S) :- arg(2, S, Assoc), 802 ( select(K-_, Assoc, Assoc0) 803 -> setarg(2, S, [K-V|Assoc0]) 804 ; setarg(2, S, [K-V|Assoc]) 805 ). 806 807:- meta_predicate set_pred( , ). 808set_pred(K, V):- shift(set_key(K, V)). 809 810:- meta_predicate set_pred( , , ). 811set_pred(K, V, S) :- set_key(K, V, S). 812 813% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]}, 814% get_key(a, Z), close_key(a))). 815% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]}, 816% get_key(a, Z), close_key(a), get_key(a, U))). % false 817 818update_key(K, New, Old, S):- arg(2, S, Assoc), 819 ( select(K-Old, Assoc, Assoc0) -> true 820 ; Assoc0 = Assoc 821 ), 822 setarg(2, S, [K-New|Assoc0]). 823% 824open_key(K, Val, S):- arg(2, S, Assoc), 825 ( select(K-_, Assoc, Assoc0) -> true 826 ; Assoc0 = Assoc 827 ), 828 setarg(2, S, [K-Val|Assoc0]). 829 830% 831close_key(K, S):- arg(2, S, Extra), 832 ( select(K-_, Extra, Extra0) -> setarg(2, S, Extra0) 833 ; true 834 ). 835 836% ?- zdd((varnum(D), varnum(E))). 837%% varnum(-D, +S) is det. 838% update a global variable varnum with D. 839% 840varnum(D, S):- get_key(varnum, D, S). 841 842% ?- sort([1->1, 1->2, 1-1, 2-2], X). 843% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X). 844% ?- zdd(zdd_sort_rev([1,2,3], X)). 845 846compare_rev(Comp, C, A, B):- call(Comp, C, B, A). 847% 848zdd_sort_rev(X, Y):- shift(zdd_sort_rev(X, Y)). 849zdd_sort_rev(X, Y, S):- get_compare(Comp, S), 850 predsort(compare_rev(Comp), X, Y). 851 852% ?- pred_zdd(path_count:opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)). 853:- meta_predicate pred_zdd( , ). 854pred_zdd(Comp, X):- open_state(S), pred_zdd(Comp, X, S). 855% 856pred_zdd(Comp, X, S):- set_compare(Comp, S), zdd(X, S). 857 858% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c], X))). 859% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([], X))). 860% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
865zdd_memberchk(L, Z):- shift(zdd_memberchk(L, Z)). 866% 867zdd_memberchk(L, Z, S):- zdd_sort(L, L0, S), 868 zdd_ord_memberchk(L0, Z, S). 869% 870zdd_ord_memberchk(L, Z):- shift(zdd_ord_memberchk(L, Z)). 871% 872zdd_ord_memberchk([], Z, S):- !, zdd_has_1(Z, S). 873zdd_ord_memberchk([A|As], Z, S):- Z>1, 874 cofact(Z, t(B, L, R), S), 875 ( A == B 876 -> zdd_ord_memberchk(As, R, S) 877 ; A @> B, 878 zdd_ord_memberchk([A|As], L, S) 879 ). 880 881% PASS 882% ?- zdd X<<pow([a,b]), card(X, C). 883% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))). 884% ?- zdd {X=1, Y =2, Z is X + Y}. 885% ?- zdd X<<set([a]), sets(X, U). 886% ?- zdd((X<<pow([a,b]), S<<sets(X))). 887% ?- zdd((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 888% ?- zdd(((X<< *(:append([a,b], [c,d]))), sets(X, Y))). 889% ?- zdd((X<<(*[a,b]& *[c,d]), S<<sets(X))). 890% ?- zdd((X<<{[a],[b],[c]}, sets(X,S))). 891% ?- zdd((X<<{[a],[b, c]}, sets(X,S))). 892% ?- zdd((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 893% ?- zdd((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 894% ?- I =1000, J =2000, 895% time( (zdd 896% { numlist(1, I, L), 897% numlist(1, J, M)}, 898% X << pow(L), 899% Y << pow(M), 900% Z << (Y - X), 901% card(Z, C), 902% {C =:= 2^J-2^I} )). 903 904 905% PASS 906% ?- zdd((X<<cnf(0), Y<<sets(X))). 907% ?- zdd((X<<cnf(1), Y<<sets(X))). 908% ?- zdd((X<<cnf(2), Y<<sets(X))). 909% ?- zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 910% ?- ltr_zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 911% ?- zdd((X<<cnf(a), Y<<sets(X))). 912% ?- zdd((X<<cnf(-a), Y<<sets(X))). 913% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 914% ?- zdd((X<<cnf(-(a+b)), Y<<sets(X))). 915% ?- zdd((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 916% ?- zdd((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 917% ?- zdd((X<<cnf(-(-a + -b)), Y<<sets(X))). 918% ?- zdd((X<<dnf(a), Y<<sets(X), extern(Y, Y0))). 919% ?- zdd((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))). 920% ?- zdd((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))). 921% ?- zdd((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))). 922% ?- zdd((X<<dnf(a+b), Y<<sets(X))). 923% ?- zdd((X<<dnf(-(a+b)), Y<<sets(X))). 924% ?- zdd((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 925% ?- zdd((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 926% ?- zdd((X<<dnf(-(-a + -b)), Y<<sets(X))). 927% ?- zdd((X<<dnf((-a + a)), Y<<sets(X))). 928% ?- zdd((X<<dnf(-(-a + a)), Y<<sets(X))). 929% ?- zdd(X << *(:append([a,b], [c,d]))). 930% ?- zdd((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))). 931% ?- zdd((X << *[a,b], sets(X, S))). 932% ?- zdd((X << +[a,b], sets(X, S))). 933% ?- zdd((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 934% ?- zdd((zdd_list_to_singletons([], X), prz(X))). 935% ?- zdd((zdd_list_to_singletons([a], X), prz(X))). 936% ?- zdd((zdd_list_to_singletons([a,b], X), prz(X))). 937% ?- zdd((zdd_list_to_singletons([c, a, b], X), prz(X))). 938 939 940% ERROR (intentional) 941% ?- I =1000, J is I + 1, numlist(1, I, L), 942% prepare_ltr_list(L, L0), 943% time(zdd(( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
951zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 952% 953zdd_list_to_singletons([], 1, _). 954zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 955 zdd_singleton(A, Y0, S), 956 zdd_join(Y0, Y, X, S). 957 958% PASS. 959% ?- zdd((zdd_partial_choices([], X), prz(X))). 960% ?- zdd((zdd_partial_choices([[a], [b]], X), prz(X))). 961% ?- zdd((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 962% ?- zdd((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 963% ?- zdd((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 964% ?- zdd((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 965% ?- zdd((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))). 966% ?- zdd((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 967% ?- zdd((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 968% ?- findall([I], between(1, 10000, I), Ls), 969% zdd((zdd_partial_choices(Ls, X), 970% card(X, C))), !, C =:= 2^10000.
975zdd_partial_choices(X, Y):- shift(zdd_partial_choices(X, Y)). 976% 977zdd_partial_choices([], 1, _):-!. 978zdd_partial_choices([L|Ls], X, S):- zdd_partial_choices(Ls, X0, S), 979 sw_fold_insert(zdd, L, X0, 0, X1, S), 980 zdd_join(X0, X1, X, S).
985:- meta_predicate s_map( , , , ). 986% 987s_map(_, [], [], _):-!. 988s_map(F, [X|Xs], [Y|Ys], S):- call(F, X, Y, S), !, s_map(F, Xs, Ys, S).
993:- meta_predicate s_map( , , ). 994% 995s_map(_, [], _):-!. 996s_map(F, [X|Xs], S):- call(F, X, S), !, s_map(F, Xs, S). 997 998 999:- meta_predicate zdd_find( , , , ).
1004% ?- zdd X<< pow([a,b,c]), zdd_find(=(c), X, Y). 1005% ?- zdd X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y). 1006% ?- zdd X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y). 1007 1008zdd_find(F, X, Y, S):- X>1, 1009 cofact(X, t(A, L, R), S), 1010 ( call(F, A), Y = A 1011 ; zdd_find(F, L, Y, S) 1012 ; zdd_find(F, R, Y, S) 1013 ). 1014 1015% PASS. 1016% 1017% ?- zdd((P<<pow([1,2,3]), {X=1;X=2}, card(P,C))). 1018 1019% ?- zdd((P<<pow([1,2,3]), card(P,C))). 1020% ?- zdd P<<pow([1,2,3]), card(P,C). 1021% ?- zdd((P << (set([1,2,3,2,3])+set([4, 2,4])), psa(P))). 1022% ?- zdd({append([a,b], [c,d], X)}). 1023% ?- zdd(X << :append([a,b], [c,d])). 1024% ?- zdd(zdd(X << :append([a,b], [c,d]))). 1025% ?- zdd(zdd(zdd((X << :append([a,b], [c,d]))))). 1026% ?- zdd(zdd(zdd(((X<<pow([1,2]), true, true))))). 1027% ?- zdd(zdd(zdd((X<<pow([1,2]), true, true, card(X, C))))). 1028% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), card(X, C)). 1029 1030 1031fetch_state(S):- setup_state_for_query(S, '$zdd'). % for short. 1032% 1033fetch_state(S, G):- setup_state_for_query(S, G). % for short.
1040setup_state_for_query(S, Gv):-
1041 ( var(S) ->
1042 ( nb_current(Gv, S), S\==[] -> true
1043 ; open_state(S),
1044 b_setval(Gv, S)
1045 )
1046 ; b_setval(Gv, S)
1047 ).
1052:-meta_predicate ltr_zdd( ). 1053ltr_zdd(M:G):- ltr_open_state(S), 1054 fetch_state(S), 1055 zdd_solve(G, S, M).
1059:- meta_predicate zdd( ). % zdd(0) does not work. 1060zdd(M:G):- fetch_state(S), 1061 set_key(atom_index, 0, S), 1062 set_compare(compare, S), 1063 zdd_solve(G, S, M). 1064 1065% 1066:- meta_predicate zdd( , ). 1067zdd(M:A, S):- zdd_solve(A, S, M).
1073:- meta_predicate zdd0( ). 1074zdd0(X):- zdd((set_compare(opp_compare), X)).
opp_compare(C, Y, X)
.1079% PASS. 1080% ?- zdd((zdd_sort([a-b,a->b, b-c, b->c], X))). 1081% ?- zdd0((zdd_sort([a-b,a->b, b-c, b->c], X))). 1082% ?- opp_compare(C, 1, 2). 1083% ?- opp_compare(C, a->b, b). 1084% ?- opp_compare(C, p(0,0), p(1,0)). 1085% ?- opp_compare(C, p(1,0)-p(0,0), p(1,0)-p(1,0)). 1086 1087opp_compare(<, -(_,_), ->(_,_)):-!. 1088opp_compare(>, ->(_,_), -(_,_)):-!. 1089opp_compare(C, X, Y):- compare(C, Y, X). % reverse order 1090 1091% PASS. 1092% ?- zdd((set_key(a, 1), get_key(a, X))). 1093:- meta_predicate use_zdd( ). 1094use_zdd(X):- use_zdd(X, [hash_size(128)]). 1095 1096:- meta_predicate use_zdd( , ). 1097use_zdd(X, Options):- 1098 setup_call_cleanup( 1099 open_state(S, Options), 1100 zdd(X, S), 1101 close_state(S)). 1102 1103% ?- zdd X<< @(abc), psa(X). 1104% ?- zdd X<<pow([1,2]), memo(a-X), card(X, C).
call(G, S)
(Deprecated)
M:G Solve G in module M
true true
{G} call(G)
with G as a plain prolog goal.
A call(M:A, S)
. Call an atomic goal A with S in M.1121% ?- zdd X<< +[ *[a,b], *[c, d]], psa(X). 1122% ?- zdd X<< +[ *[a,b], *[c, d]], #(psa(X)). 1123% ?- zdd <<(X, +[*[a,b], *[c,d]]), psa(X). 1124 1125% ?- zdd X<<1, Y<<2. 1126% ?- zdd X<< card(pow([1,2])+pow([a,b])). 1127 1128:- meta_predicate <<( , ). 1129<<(X, E) :- setup_state_for_query(S), zdd_eval(E, X, S).
1134:- meta_predicate <<( , , ). 1135<<(X, E, S) :- setup_state_for_query(S), zdd_eval(E, X, S).
1140% ?- zdd X<< *[0, 1, 2, 3], psa(X). 1141% ?- zdd X<< *[*[]], psa(X). 1142% ?- zdd X<< *[[]], psa(X). 1143% ?- zdd X<< *[+[]], psa(X). 1144% ?- zdd X<< +[ *[1,2], *[3,4]], psa(X). 1145% ?- zdd X<<pow(:numlist(1, 100)), card(X, C). 1146% ?- zdd X<< :numlist(1, 100). 1147%@ X = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]. 1148 1149% 1150zdd_solve(true, _, _) :-!. 1151zdd_solve(M:G, S, _) :-!, zdd_solve(G, S, M). 1152zdd_solve({G}, _, M) :-!, call(M:G). 1153% zdd_solve(#(G), S, M) :-!, zdd_solve(G, S, M). % Dropped. 1154zdd_solve(X<<E, S, M) :-!, zdd_numbervars(E, S), zdd_eval(E, X, S, M). 1155zdd_solve((A,B), S, M) :-!, zdd_solve(A, S, M), zdd_solve(B, S, M). 1156zdd_solve((A;B), S, M) :-!, (zdd_solve(A, S, M); zdd_solvde(B, S, M)). 1157zdd_solve((A->B), S, M) :-!, (zdd_solve(A, S, M) -> zdd_solve(B, S, M)). 1158zdd_solve(G, S, M):- call(M:G, S).
--- only basic expressions follow ---
x x if x is nummber, string, or list. $E E (quote). @(a) {{a}} as a singleton family of a.
:E eval E as prolog term with last argument as output. #E eval E as zdd term using state. !E apply E without evaluating args.
--- zdd expression ---
X + Y join (union) of X and Y
X - Y subtract Y from X
X \ Y subtract Y from X
X & Y intersection of X and Y
merge(X, Y)
merge/multiply X and Y
X * Y merge/multiply X and Y
X // Y quotient X by Y.
X / Y remainder of X by Y.
prod(X, YO)
product of X and Y
X ** Y product of X and Y
pow(X)
powerset of X
power(X)
powerset of X
set(L)
read L a singleton family {L}.
sets(X, S)
convet X in S to list of lists
*E merge all elements of a list E.
+E join all elements of a list E.
{A,B,..} family of sets [A, B, ...]
--- Boolean terms ---
cnf(F, X) X is CNF of F. dnf(F, X) X is DNF of F,
1197% Pass. 1198% ?- zdd((X<<dnf(a*b), psa(X))). 1199% ?- zdd((X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C))). 1200% ?- zdd((X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))). 1201% ?- zdd((X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C))). 1202 1203% Pass. 1204% ?- zdd X<< @a. 1205% ?- zdd X<< a, psa(X). 1206% ?- zdd X<<pow([a,b]), card(X, C). 1207% ?- zdd X<<pow([a,b])-pow([a]), card(X, C). 1208% ?- zdd X<< set(:(append([1,2],[3,4]))), psa(X). 1209% ?- zdd((X<< +(:append([1,2],[3,4])), psa(X))). 1210% ?- zdd((X<< (@a + @b), psa(X))). 1211% ?- zdd((X<< ((@a + @b)* @c), psa(X))). 1212% ?- zdd((X<< [a,b])). 1213% ?- zdd((X<< set(:(append([a,b],[c,d]))), psa(X))). 1214% ?- zdd((X<< set(!append([a,b],[c,d])), psa(X))). % error 1215% ?- zdd(X<< card(pow([a,b]))). 1216% ?- zdd(X<< card(pow(:numlist(1, 100)))). 1217% ?- zdd((X<< set([1]), Y<< (X+X), psa(X))). 1218% ?- zdd((X<< set([1]), psa(X))). 1219% ?- zdd((X<< set([]))). 1220% ?- zdd((X << {[a], [b], [c]}, psa(X))). 1221% ?- zdd((X << {[a], [b], [c]}, card(X, C))). 1222 1223% PASS. 1224% ?- zdd((X << card(pow(:append(numlist(1,3), numlist(4,5)))))). 1225% ?- zdd((X << set(:append(numlist(1,2), numlist(4,5))))). 1226% ?- zdd((X << set(:append(numlist(1,10), numlist(11,20))))). 1227% ?- zdd { numlist(1,10,A), numlist(11,20, B)}, X<< pow( :append(A, B)), 1228% card(X, C). 1229% ?- zdd((X << pow(:(numlist(1,2))), card(X, C))). 1230% ?- zdd((X << pow(:(! charlist(a,z))), card(X, C))). 1231% ?- zdd((X << pow(:(! charlist(a-z))), card(X, C))). 1232% ?- zdd((X << pow([a,b]))). 1233% ?- zdd((X << *[a, b, c])). 1234% ?- zdd((X << (*[a, b, c] + *[a,b,c]), psa(X))). 1235% ?- zdd((X << (*[a, b, c] + *[2, 3]), psa(X))). 1236% ?- zdd((C << card(pow([a,b,c,1,2,3])))). 1237% ?- zdd((C << card(pow(:append([a,b,c], [1,2,3]))))). 1238% ?- zdd((C << pow(:numlist(1, 3)))). 1239% ?- zdd((C << @(a), psa(C))). 1240 1241% Pass. 1242% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))). 1243% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))). 1244% ?- zdd((U << +(:(append([a,b,c], [d,e,f]))), psa(U))). 1245% ?- zdd((U << *(:(append([a,b,c], [d,e,f]))), psa(U))). 1246% ?- zdd((U << +(:(append(:append([a,b,c], [x,y,z]), [1, 2]))), psa(U))). 1247% ?- zdd((U << +[ *[a,b], *[c,d]], psa(U))). 1248% ?- zdd((U << *[ +[a,b], +[c,d]], psa(U))). 1249% ?- zdd((U << *[ *[a,b], *[c,d]], psa(U))). 1250% ?- zdd((U << *[ *[a,b], +[c,d]], psa(U))). 1251% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1252% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1253% ?- zdd((U << #(card(pow([a]))))). 1254% ?- zdd((U << :succ(#(card(pow([a])))))). 1255% ?- zdd((U << card(pow([a])))). 1256 1257% Pass. 1258% ?- zdd((U << :(=(3)))). 1259% ?- zdd((U << *([1,2,3]), psa(U))). 1260% ?- zdd((U << :plus(#(card(pow([a,b]))), #(card(pow([1,2])))))). 1261% ?- zdd((U << @a)). % singleton. 1262% ?- zdd((U << @2)). 1263% ?- zdd((U << [a,b])). 1264% ?- zdd((U << *[a,b], psa(U))). 1265% ?- zdd((U << +[a,b], psa(U))). 1266% ?- zdd((U << +[*[a,b], *[c,d]], psa(U))). 1267% ?- zdd((U << +[+[a,b], +[c,d]], psa(U))). 1268% ?- zdd((U << *[+[a,b], +[c,d]], psa(U))). 1269% ?- zdd((U << *[*[a,b], *[c,d]], psa(U))). 1270% ?- zdd((U << :(!call(=, hello)))). 1271% ?- zdd((U << :(call($(=), :append([a,b],[c,d]))))). 1272% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< zdd_join(X, Y), psa(Z). 1273% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< (X+Y), psa(Z). 1274% 1275basic_type(X):- number(X); 1276 string(X); 1277 is_list(X); 1278 var(X).
1283zdd_eval(X, Y, S):- context_module(M), 1284 zdd_numbervars(X, S), 1285 zdd_eval(X, Y, S, M). 1286 1287% illegal use of pragma. 1288% ?- zdd((U << @(=(3)))). % Error 1289% ?- zdd((U << #append([a], [b]))). % Error 1290% ?- zdd((U << +(!append([a], [b])))), psa(U). % Error 1291% ?- zdd((U << #(get_compare), psa(U))). % Error 1292% ?- zdd( #(get_compare, X)). % Error 1293 1294% Normal use of pragmas, though meaningless. 1295% ?- zdd((U << (@a+ @b+ @c), psa(U))). 1296% ?- zdd((U << :append([a], [b]))). 1297% ?- zdd((U << get_compare)). 1298% ?- zdd((U << +(:append([[a]], [[b]])), psa(U))). 1299% ?- zdd(U << get_compare). 1300% ?- zdd( get_compare(X)). 1301% ?- zdd( U << :arith(1+2)). 1302% ?- zdd( U << :plus(arith(1+2), arith(3+4))). 1303% ?- zdd((U << (@A+ @B+ @C), psa(U))). 1304% ?- zdd((U << (@A), psa(U))).
1309% Note that intgeger is used as a unique name of a ZDD. 1310% use indicator `@` as `@(3)` for 3 as an atom. 1311 1312zdd_eval(X, X, _, _) :- basic_type(X), !. 1313zdd_eval(@(X), Y, S, _) :-!, zdd_singleton(X, Y, S). 1314zdd_eval({}, 0, _, _) :-!. % The empty family of sets. 1315zdd_eval({X}, Y, S, _) :-!, associative_comma(X, U, []), zdd_family(U, Y, S). 1316zdd_eval($(X), X, _, _) :-!. 1317zdd_eval(!(X), Y, S, M) :-!, call(M:X, Y, S). 1318zdd_eval(:(X), Y, S, M) :-!, prolog_eval(X, Y, S, M). 1319zdd_eval(#(X), Y, S, M) :-!, zdd_eval(X, Y, S, M). 1320zdd_eval(M:X, Y, S, _) :-!, zdd_eval(X, Y, S, M). 1321zdd_eval(X, Y, S, M) :- 1322 ( zdd_apply(X, Y, S, M) -> true 1323 ; zdd_atom(X, S) -> zdd_singleton(X, Y, S) 1324 ; zdd_eval_args(X, X0, S, M), 1325 zdd_apply0(X0, Y, S, M) 1326 ). 1327% 1328zdd_eval_args(A, A, _, _):- atomic(A), !. 1329zdd_eval_args(A, B, S, M):- 1330 functor(A, Fa, Na), 1331 functor(B, Fa, Na), 1332 zdd_eval_args(1, A, B, S, M). 1333% 1334zdd_eval_args(I, A, B, S, M):- arg(I, A, U), !, 1335 zdd_eval(U, V, S, M), 1336 arg(I, B, V), 1337 J is I+1, 1338 zdd_eval_args(J, A, B, S, M). 1339zdd_eval_args(_, _, _, _, _).
1345prolog_eval(X, X, _, _) :- basic_type(X), !. 1346prolog_eval($(X), X, _, _) :-!. 1347prolog_eval(!(X), Y, _, M) :-!, call(M:X, Y). 1348prolog_eval(:(X), Y, S, M) :-!, prolog_eval(X, Y, S, M). 1349prolog_eval(#(X), Y, S, M) :-!, zdd_eval(X, Y, S, M). 1350prolog_eval(M:X, Y, S, _) :-!, prolog_eval(X, Y, S, M). 1351prolog_eval(arith(X), Y, _, _) :-!, Y is X. 1352prolog_eval(X, Y, S, M) :- prolog_eval_args(X, X0, S, M), 1353 call(M:X0, Y). 1354% 1355prolog_eval_args(A, A, _, _):- atomic(A), !. 1356prolog_eval_args(A, B, S, M):- 1357 functor(A, Fa, Na), 1358 functor(B, Fa, Na), 1359 prolog_eval_args(1, A, B, S, M). 1360% 1361prolog_eval_args(I, A, B, S, M):- arg(I, A, U),!, 1362 prolog_eval(U, V, S, M), 1363 arg(I, B, V), 1364 J is I+1, 1365 prolog_eval_args(J, A, B, S, M). 1366prolog_eval_args(_, _, _, _, _). 1367 1368 /********************************* 1369 * zdd vecrtor expressions * 1370 *********************************/
1375% ?- zdd((X<< *(: (=([[a,b],[c,d]]))), psa(X))). 1376% ?- zdd((X<< +(: (=([[a,b],[c,d]]))), psa(X))). 1377% ?- zdd((X<< +(: (=([*[a,b], *[c,d]]))), psa(X))). 1378% ?- zdd((X<< +[[1,2],[a,b]], psa(X), card(X, C))). 1379% ?- zdd((X<< *[[1,2],[a,b]], psa(X), card(X, C))). 1380% ?- zdd((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))). 1381% ?- zdd((X<< +[*[1,2],*[a,b]], psa(X), card(X, C))). 1382% ?- zdd((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))). 1383% ?- zdd((X<< *[1,2], psa(X), card(X, C))). 1384% ?- zdd((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))). 1385% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1386% ?- zdd zdd_vector_exp(+[[a],*[b,c]], X), psa(X). 1387% ?- zdd zdd_vector_exp(+[a,b,c], X), psa(X). 1388% ?- zdd zdd_vector_exp(*[a,b,c], X), psa(X). 1389% ?- zdd zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X). 1390% ?- zdd zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X). 1391% ?- zdd zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X). 1392% ?- zdd X<< *[a, b], psa(X). 1393% ?- zdd X<< +[a, b], psa(X). 1394% ?- zdd X<< *[A, B], psa(X). 1395% ?- zdd X<< *[*[0, 1], *[2,3]], psa(X). 1396% ?- zdd X<< *[*[], *[2,3]], psa(X). 1397% ?- zdd X<< *[0, 1, *[2,3]], psa(X). 1398 1399zdd_vector_exp(*(X), Y, S):-!, zdd_vector_exp(*, X, Y, S). 1400zdd_vector_exp(+(X), Y, S):-!, zdd_vector_exp(+, X, Y, S). 1401% zdd_vector_exp(X, X, _):- (X = 0; X=1),!. 1402zdd_vector_exp(X, Y, S):- zdd_singleton(X, Y, S). 1403 1404% 1405zdd_vector_exp(*, [], 1, _):-!. 1406zdd_vector_exp(+, [], 0, _):-!. 1407zdd_vector_exp(F, [A|As], R, S):-!, % F in [*,+]. 1408 zdd_vector_exp(A, U, S), 1409 zdd_vector_exp(F, As, V, S), 1410 apply_binary_basic(F, U, V, R, S). 1411 1412% 1413apply_binary_basic(*, X, Y, Z, S):-!, zdd_merge(X, Y, Z, S). 1414apply_binary_basic(+, X, Y, Z, S):- zdd_join(X, Y, Z, S). 1415 1416% 1417zdd_fold_join([], Z, Z, _). 1418zdd_fold_join([X|Xs], Z, Z0, S):- 1419 zdd_join(X, Z, Z1, S), 1420 zdd_fold_join(Xs, Z1, Z0, S). 1421% 1422zdd_fold_merge([], Z, Z, _). 1423zdd_fold_merge([X|Xs], Z, Z0, S):- 1424 zdd_merge(X, Z, Z1, S), 1425 zdd_fold_merge(Xs, Z1, Z0, S). 1426% 1427fold_singleton_join([], X, X, _). 1428fold_singleton_join([A|As], X, Y, S):- 1429 zdd_singleton(A, U, S), 1430 zdd_join(U, X, X0, S), 1431 fold_singleton_join(As, X0, Y, S). 1432 1433 /*********************************************** 1434 * Currently reserved names of operations. * 1435 ***********************************************/
1440zdd_apply(@(A), Y, S, _) :-!, zdd_singleton(A, Y, S). 1441zdd_apply(X, Y, S, _) :- dvar(X), !, zdd_singleton(X, Y, S). 1442zdd_apply(ltr_set(L), Y, S, _) :-!, ltr_append(L, 1, Y, S). 1443zdd_apply(dnf(A), X, S, _) :-!, dnf(A, X, S). 1444zdd_apply(cnf(A), X, S, _) :-!, cnf(A, X, S). 1445zdd_apply(gf2(A), X, S, _) :-!, gf2(A, X, S). 1446zdd_apply(qp(A), X, S, _) :-!, mqp(A, X, S). 1447zdd_apply(cofact(A, L, R), X, S, _) :-!, cofact(X, t(A, L, R), S). 1448zdd_apply(cofact(X), Y, S, _) :-!, integer(X), X>1, cofact(X, Y, S). 1449zdd_apply(fact(X), Y, S, _) :- integer(X), X>1, cofact(X, Y, S). 1450zdd_apply(+(X), Y, S, _) :-!, zdd_vector_exp(+(X), Y, S). 1451zdd_apply(*(X), Y, S, _) :-!, zdd_vector_exp(*(X), Y, S). 1452 1453 1454% 1455zdd_apply0(X + Y, Z, S, _) :-!, zdd_join(X, Y, Z, S). 1456zdd_apply0(X * Y, Z, S, _) :-!, zdd_merge(X, Y, Z, S). 1457zdd_apply0(merge(X, Y), Z, S, _) :-!, zdd_merge(X, Y, Z, S). 1458zdd_apply0(X - Y, Z, S, _) :-!, zdd_subtr(X, Y, Z, S). 1459zdd_apply0(\(X,Y), Z, S, _) :-!, zdd_subtr(X, Y, Z, S). 1460zdd_apply0((X // Y), Z, S, _):-!, zdd_div(X, Y, Z, S). 1461zdd_apply0((X / Y), Z, S, _) :-!, zdd_mod(X, Y, Z, S). 1462zdd_apply0((X mod Y), Z, S, _) :-!, zdd_mod(X, Y, Z, S). 1463zdd_apply0(&(X, Y), Z, S, _) :-!, zdd_meet(X, Y, Z, S). 1464zdd_apply0(prod(X, Y), Z, S, _) :-!, zdd_product(X, Y, Z, S). 1465zdd_apply0(**(X, Y), Z, S, _):-!, zdd_product(X, Y, Z, S). 1466zdd_apply0(pow(X), Z, S, _) :-!, zdd_sort(X, Y, S), zdd_power(Y, Z, S). 1467zdd_apply0(power(X), Z, S, _):-!, zdd_sort(X, Y, S), zdd_power(Y, Z, S). 1468zdd_apply0(sets(X), Z, S, _) :-!, sets(X, Z, S). 1469zdd_apply0(X, Y, S, M) :- call(M:X, Y, S). 1470 1471% ?- zdd X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X). 1472% ?- zdd X<< +[*[a,b]] + +[*[c,d]], psa(X). 1473% ?- zdd((X<<pow([1,2,3,4]), Y<<pow([1,2,3]), 1474% card(X, C), card(Y, D), Z<<(X-Y), card(Z, E))). 1475zdd_super_power([], P, P, _). 1476zdd_super_power([A|As], P, Q, S):- 1477 zdd_super_power(As, P, Q0, S), 1478 zdd_insert(A, Q0, Q, S). 1479 1480% 1481set(L, Y, S) :-!, zdd_append(L, 1, Y, S). 1482 1483% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 1484family(X, Y, S):- zdd_numbervars(X, S), 1485 zdd_family(X, Y, S).
1491zdd_family(X, Y, S):- zdd_numbervars(X, S), 1492 zdd_family(X, 0, Y, S). 1493 1494% ?- zdd zdd_family([[a],[a,b]], X), card(X, C), psa(X). 1495% ?- zdd zdd_family([[], [a,a],[a,b]], X), psa(X). 1496zdd_family([], U, U, _). 1497zdd_family([X|Xs], U, V, S):- 1498 zdd_insert_atoms(X, 1, X1, S), 1499 zdd_join(X1, U, U0, S), 1500 zdd_family(Xs, U0, V, S). 1501 1502% ?- zdd((ltr_family([[a, b], [c, d]], X), sets(X,S))). 1503% ?- zdd((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 1504% ?- zdd((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 1505% ?- zdd((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 1506% ?- zdd((X << dnf((a+(-b)+a)), psa(X))). 1507% ?- zdd((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 1508% ?- zdd((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))). 1509% ?- ltr_zdd ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X). 1510% ?- ltr_zdd ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X). 1511% ?- ltr_zdd ltr_family([[a],[-b, -a,-c]], X), psa(X). 1512% 1513% 1514ltr_family(X, Y, S):- ltr_family(X, 0, Y, S). 1515 1516% 1517ltr_family([], U, U, _). 1518ltr_family([X|Xs], U, V, S):- 1519 ltr_append(X, 1, X0, S), 1520 ltr_join(X0, U, U0, S), 1521 ltr_family(Xs, U0, V, S). 1522 1523 /************************ 1524 * choices * 1525 ************************/ 1526 1527% ?- zdd X<< pow([a,b]), card(X, C). 1528%! zdd_choices(+X, -Y, +S) is det. 1529% Y = { W | U in W iff all A in U some V in X such that A in X }. 1530 1531% ?- zdd X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y). 1532% ?- N=10, numlist(1, N, Ns), (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1533% zdd_choices(X, Y), card(Y, C)). 1534% ?- N=1000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1535% zdd_choices(X, Y), card(Y, C))). 1536 1537zdd_choices(0, 1, _):-!. 1538zdd_choices(1, 0, _):-!. 1539zdd_choices(X, Y, S):- memo(choices(X)-Y, S), 1540 ( nonvar(Y)->true %, write(+) % many hits when X has the empty set. 1541 ; cofact(X, t(A, L, R), S), 1542 zdd_choices(L, L0, S), 1543 zdd_choices(R, R0, S), 1544 cofact(R1, t(A, R0, 1), S), 1545 zdd_merge(L0, R1, Y, S) 1546 ). 1547 1548 1549 /************************************************* 1550 * Operation on zdd join/merge/meet/subtr/cons * 1551 *************************************************/
1556% 1557zdd_join(0, X, X, _):-!. 1558zdd_join(X, 0, X, _):-!. 1559zdd_join(X, X, X, _):-!. 1560zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S). 1561zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S). 1562zdd_join(X, Y, Z, S):- 1563 ( X@<Y -> memo(zdd_join(X,Y)-Z, S) 1564 ; memo(zdd_join(Y, X)-Z, S) 1565 ), 1566 ( nonvar(Z) -> true %, write(.) 1567 ; cofact(X, t(A, L, R), S), 1568 cofact(Y, t(A0, L0, R0), S), 1569 zdd_compare(C, A, A0, S), 1570 ( C = (<) -> 1571 zdd_join(L, Y, U, S), 1572 cofact(Z, t(A, U, R), S) 1573 ; C = (=) -> 1574 zdd_join(L, L0, U, S), 1575 zdd_join(R, R0, V, S), 1576 cofact(Z, t(A, U, V), S) 1577 ; zdd_join(L0, X, U, S), 1578 cofact(Z, t(A0, U, R0), S) 1579 ) 1580 ).
cofact(Z, t(X, 0, Y), S)
.
Having analogy Z = [X|Y] in mind.1586% ?- zdd zdd_cons(X, a, 1), zdd_cons(X, A, B). 1587% ?- zdd zdd_cons(X, a, 0), zdd_cons(X, A, B). % false 1588 1589zdd_cons(X, Y, Z, S):- ( var(X); X>1 ), !, cofact(X, t(Y, 0, Z), S). 1590 1591% ?- zdd((X<<(*[a]+ *[b]+ []), psa(X))). % false for []. 1592% ?- zdd((X<<(*[a]+ *[b]+ 1), psa(X))). 1593% ?- zdd((X<<(*[a]+ *[b]+ 0), psa(X))). 1594% ?- zdd((X<<(*[a]+ *[b]), psa(X))). 1595% ?- zdd((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))). 1596 1597% zdd_join_1(+X, -Y, +G) is det. 1598% Y is the union of X and 1 (the singleton {{}}). 1599 1600% ?- numlist(1,100, Ns), (zdd X<<pow(Ns), {fetch_state(S), time(repeat(100, zdd_join_1(X,_,S)))}). 1601zdd_join_1(X, X, S):- zdd_has_1(X, S), !. 1602zdd_join_1(X, Y, S):- zdd_add_1(X, Y, S). 1603% 1604zdd_add_1(0, 1, _):-!. 1605zdd_add_1(X, Y, S):- cofact(X, t(A, L, R), S), 1606 zdd_add_1(L, L0, S), 1607 cofact(Y, t(A, L0, R), S). 1608 1609% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1610% ?- zdd((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1611% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))). 1612% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))). 1613% ?- trace, zdd(X=[b, a]). 1614% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 1615% ?- zdd((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
1620zdd_meet(0, _, 0, _):-!. 1621zdd_meet(_, 0, 0, _):-!. 1622zdd_meet(1, X, Y, S):-!, zdd_meet_1(X, Y, S). 1623zdd_meet(X, 1, Y, S):-!, zdd_meet_1(X, Y, S). 1624zdd_meet(X, X, X, _):-!. 1625zdd_meet(X, Y, Z, S):- 1626 ( X @< Y -> memo(zdd_meet(X,Y)-Z, S) 1627 ; memo(zdd_meet(Y,X)-Z, S) 1628 ), 1629 ( nonvar(Z) -> true 1630 ; cofact(X, t(A, L, R), S), 1631 cofact(Y, t(A0, L0, R0), S), 1632 zdd_compare(C, A, A0, S), 1633 ( C = (<) -> zdd_meet(L, Y, Z, S) 1634 ; C = (=) -> 1635 zdd_meet(L, L0, U, S), 1636 zdd_meet(R, R0, V, S), 1637 cofact(Z, t(A, U, V), S) 1638 ; zdd_meet(L0, X, Z, S) 1639 ) 1640 ).
1645zdd_meet_1(X, 1, S):- zdd_has_1(X, S), !. 1646zdd_meet_1(_, 0, _).
1651% ?- zdd((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 1652% ?- zdd0((X<<pow([a,b,c]), Y<<pow([a,b]), zdd_subtr(X, Y, Z), card(Z, C))). 1653% 1654zdd_subtr(X, X, 0, _):-!. 1655zdd_subtr(0, _, 0, _):-!. 1656zdd_subtr(X, 0, X, _):-!. 1657zdd_subtr(X, 1, Y, S):-!, zdd_subtr_1(X, Y, S). 1658zdd_subtr(1, X, Y, S):-!, 1659 ( zdd_has_1(X, S) -> Y = 0 1660 ; Y = 1 1661 ). 1662zdd_subtr(X, Y, Z, S):- memo(zdd_subtr(X,Y)-Z, S), 1663 ( nonvar(Z) -> true 1664 ; cofact(X, t(A, L, R), S), 1665 cofact(Y, t(A0, L0, R0), S), 1666 zdd_compare(C, A, A0, S), 1667 ( C = (<) -> 1668 zdd_subtr(L, Y, U, S), 1669 cofact(Z, t(A, U, R), S) 1670 ; C = (=) -> 1671 zdd_subtr(L, L0, U, S), 1672 zdd_subtr(R, R0, V, S), 1673 cofact(Z, t(A, U, V), S) 1674 ; zdd_subtr(X, L0, Z, S) 1675 ) 1676 ).
1681% ?- zdd((X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y))). 1682% ?- zdd((X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y))). 1683% ?- zdd((X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y))). 1684% 1685zdd_subtr_1(X, 0, _):- X < 2, !. % empty family or singleton of the empty. 1686zdd_subtr_1(X, Y, S):- cofact(X, t(A, L, R), S), 1687 zdd_subtr_1(L, L0, S), 1688 cofact(Y, t(A, L0, R), S).
1693% ?- zdd X<<{[a]}, Z << zdd_xor(X, X). 1694% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z). 1695% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms), 1696% time((zdd X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))). 1697% ?- time((zdd Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))). 1698zdd_xor(X, Y, Z, S):-zdd_subtr(X, Y, A, S), 1699 zdd_subtr(Y, X, B, S), 1700 zdd_join(A, B, Z, S). 1701 1702 1703% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S), 1704% zdd_meet(X, Y, B, S), 1705% zdd_subtr(A, B, Z, S).
Remark. The merge is associative and commutative, but not idempotent.
1714% ?- zdd(( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 1715% ?- time(zdd(( X<<pow(!charlist(a-z)), Y<<pow(:numlist(1, 26))))). 1716% ?- time(zdd(( X<<pow(:charlist($(a-z))), Y<<pow(:numlist(1, 26)), 1717% zdd_merge(X, Y, Z), U << zdd_meet(X, Z), card(X, C)))), C is 2^26. 1718% 1719zdd_merge(0, _, 0, _):-!. 1720zdd_merge(_, 0, 0, _):-!. 1721zdd_merge(1, X, X, _):-!. 1722zdd_merge(X, 1, X, _):-!. 1723zdd_merge(X, Y, Z, S):- 1724 ( X > Y -> memo(zdd_merge(Y, X)-Z, S) 1725 ; memo(zdd_merge(X, Y)-Z, S) 1726 ), 1727 ( nonvar(Z) -> true 1728 ; cofact(X, t(A, L, R), S), 1729 zdd_merge(L, Y, L0, S), 1730 zdd_merge(R, Y, R0, S), 1731 zdd_insert(A, R0, R1, S), 1732 zdd_join(L0, R1, Z, S) 1733 ). 1734% 1735 1736zdd_merge_list([], X, X, _). 1737zdd_merge_list([A|As], X, Y, S):- 1738 ( integer(A) -> zdd_merge(A, X, X0, S) 1739 ; zdd_insert(A, X, X0, S) % atom case 1740 ), 1741 zdd_merge_list(As, X0, Y, S). 1742 1743% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1744%@ X = 7, 1745%@ Y = 3. 1746% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1747%@ false. 1748% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1749% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1750% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1751% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1756zdd_subfamily(X, X, _):-!. 1757zdd_subfamily(0, _, _):-!. 1758zdd_subfamily(_, 0, _):-!, fail. 1759zdd_subfamily(1, X, S):-!, zdd_has_1(X, S). 1760zdd_subfamily(X, X0, S):- 1761 cofact(X, t(A, L, R), S), 1762 cofact(X0, t(A0, L0, R0), S), 1763 zdd_compare(C, A, A0, S), 1764 ( C = (=) -> 1765 zdd_subfamily(L, L0, S), 1766 zdd_subfamily(R, R0, S) 1767 ; C = (>), 1768 zdd_subfamily(X, L0, S) 1769 ). 1770 1771 /********************************* 1772 * division/residue in ZDD * 1773 *********************************/
zdd_divmod(X, Y, D, M, S)
,
psa(X, S)
, psa(D, S)
, psa(M, S)
.
1781zdd_divmod(X, Y, D, M, S):-
1782 zdd_div_div(X, Y, D1, D, S),
1783 zdd_subtr(X, D1, M, S).
1789% ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S), 1790% psa(X, S), psa(D, S), psa(M, S). 1791zdd_divmod0(X, Y, D, M, S):- 1792 zdd_divisible(X, Y, D, S), 1793 zdd_subtr(X, D, M, S).
1799% ?- zdd X<< +[b], zdd_div_div(X, 1, D, M, S), 1800% psa(X, S), psa(D, S), psa(M, S). 1801% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M, S), 1802% psa(X, S), psa(Y, S), psa(D, S), psa(M, S). 1803% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M, S), 1804% psa(X, S), psa(Y, S), psa(D, S), psa(M, S). 1805% ?- zdd X<< +[*[a,b]], Y<< +[*[b]], psa(X, S), psa(Y, S), zdd_div_div(X, Y, D, M, S), psa(D, S), psa(M, S). 1806% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]], 1807% zdd_div_div(X, Y, D, D1, S), 1808% psa(D, S), psa(D1, S). 1809 1810zdd_div_div(0, _, 0, 0, _):-!. 1811zdd_div_div(1, X, Y, Y, S):-!, 1812 ( zdd_has_1(X, S) -> Y = 1 1813 ; Y = 0 1814 ). 1815zdd_div_div(_, 0, 0, 0, _):-!. 1816zdd_div_div(X, 1, X, X, _):-!. 1817zdd_div_div(X, Y, Z, U, S):- memo(div_div(X, Y)- P, S), 1818 ( nonvar(P) -> P = (Z, U) 1819 ; cofact(X, t(A, L, R), S), 1820 zdd_div_div(L, Y, L0, U0, S), 1821 zdd_div_div(A, R, Y, R0, V0, S), 1822 zdd_join(L0, R0, Z, S), 1823 zdd_join(U0, V0, U, S), 1824 P = (Z, U) 1825 ). 1826% 1827zdd_div_div(_, 0, _, 0, 0, _):-!. 1828zdd_div_div(_, 1, 0, 0, 0, _):-!. % ??? 1829zdd_div_div(A, 1, 1, Z, Z, S):-!, zdd_singleton(A, Z, S). 1830zdd_div_div(_, _, 0, 0, 0, _):-!. 1831zdd_div_div(A, X, 1, Z, Z, S):-!, cofact(Z, t(A, 0, X), S). 1832zdd_div_div(A, X, Y, Z, U, S):- cofact(Y, t(B, L, R), S), 1833 zdd_compare(C, A, B, S), 1834 ( C = (<) -> 1835 zdd_div_div(X, Y, Z0, U0, S), 1836 zdd_insert(A, Z0, Z, S), 1837 zdd_insert(A, U0, U, S) 1838 ; C = (=) -> 1839 zdd_div_div(X, L, Z0, U0, S), 1840 zdd_insert(A, Z0, Z1, S), 1841 zdd_insert(A, U0, U1, S), 1842 zdd_div_div(X, R, Z2, U2, S), 1843 zdd_insert(A, Z2, Z3, S), % A is absorbed due to hit (A=B). 1844 zdd_join(Z1, Z3, Z, S), 1845 zdd_join(U1, U2, U, S) 1846 ; zdd_div_div(A, X, L, Z, U, S) 1847 ).
1853% ?- zdd(( X<< {[a]}, zdd_div(X, X, Z), psa(Z))). 1854% ?- zdd(( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1855% ?- zdd(( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))). 1856% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1857% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1858% ?- zdd(( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1859% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1860% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1861% ?- zdd(( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1862% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1863% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))). 1864% ?- zdd(( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1865% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1866% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1867% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))). 1868% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1869% ?- zdd(( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))). 1870% ?- zdd(( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1871% ?- zdd(( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1872% ?- zdd(( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))). 1873% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))). 1874% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1875% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1876 1877% 1878zdd_div(0, _, 0, _):-!. 1879zdd_div(1, X, Y, S):-!, 1880 ( zdd_has_1(X, S) -> Y = 1 1881 ; Y = 0 1882 ). 1883zdd_div(X, Y, Z, S):- memo(zdd_div(X, Y)- Z, S), 1884 ( nonvar(Z) -> true 1885 ; cofact(X, t(A, L, R), S), 1886 zdd_div(L, Y, L0, S), 1887 zdd_div(A, R, Y, R0, S), 1888 zdd_join(L0, R0, Z, S) 1889 ). 1890% 1891zdd_div(_, _, 0, 0, _):-!. 1892zdd_div(A, X, 1, Z, S):-!, cofact(Z, t(A, 0, X), S). 1893zdd_div(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S), 1894 zdd_compare(C, A, B, S), 1895 ( C = (<) -> 1896 zdd_div(X, Y, Z0, S), 1897 cofact(Z, t(A, 0, Z0), S) 1898 ; C = (=) -> 1899 zdd_div(X, L, L0, S), 1900 zdd_div(X, R, R0, S), 1901 cofact(Z, t(A, R0, L0), S) 1902 ; zdd_div(A, X, L, Z, S) 1903 ).
1909% ?- zdd {N=10, numlist(1, N, Ns), numlist(1, 10, Js)}, X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z). 1910% ?- zdd X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1911% ?- zdd X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1912% ?- zdd X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1913% ?- zdd X<<pow([a, b, c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z). 1914 1915zdd_divisible(0, _, 0, _):-!. 1916zdd_divisible(1, X, Y, S):-!, 1917 ( zdd_has_1(X, S) -> Y = 1 1918 ; Y = 0 1919 ). 1920zdd_divisible(X, Y, Z, S):- memo(zdd_divisible(X, Y)- Z, S), 1921 ( nonvar(Z) -> true 1922 ; cofact(X, t(A, L, R), S), 1923 zdd_divisible(L, Y, L0, S), 1924 zdd_divisible(A, R, Y, R0, S), 1925 zdd_join(L0, R0, Z, S) 1926 ). 1927% 1928zdd_divisible(_, _, 0, 0, _):-!. 1929zdd_divisible(A, X, 1, Z, S):-!, cofact(Z, t(A, 0, X), S). 1930zdd_divisible(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S), 1931 zdd_compare(C, A, B, S), 1932 ( C = (<) -> 1933 zdd_divisible(X, Y, Z0, S), 1934 cofact(Z, t(A, 0, Z0), S) 1935 ; C = (=) -> 1936 zdd_divisible(X, L, L0, S), 1937 zdd_divisible(X, R, R0, S), 1938 zdd_join(L0, R0, Z0, S), 1939 cofact(Z, t(A, 0, Z0), S) 1940 ; zdd_divisible(A, X, L, Z, S) 1941 ).
1946% ?- zdd X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1947% ?- zdd X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1948% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S). 1949% ?- zdd X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S). 1950% ?- N = 300, zdd numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns], 1951% time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S). 1952 1953% ?- zdd X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z). 1954 1955zdd_divisible_by_all(X, Y, X, _):-Y<2, !. % It was hard to find this. 1956zdd_divisible_by_all(X, _, 0, _):-X<2, !. % It was a little bit hard to find this. 1957zdd_divisible_by_all(X, Y, Z, S):- memo(div_by_all(X, Y)-Z, S), 1958 ( nonvar(Z) -> true 1959 ; cofact(X, t(A, L, R), S), 1960 zdd_divisible_by_all(L, Y, L0, S), 1961 zdd_divisible_by_all(A, R, Y, R0, S), 1962 zdd_join(L0, R0, Z, S) 1963 ). 1964% 1965zdd_divisible_by_all(A, X, Y, Z, S):- Y<2, !, 1966 cofact(Z, t(A, 0, X), S). 1967zdd_divisible_by_all(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S), 1968 zdd_compare(C, A, B, S), 1969 ( C = (<) -> 1970 zdd_divisible_by_all(X, Y, Z0, S), 1971 zdd_insert(A, Z0, Z, S) 1972 ; C = (=) -> 1973 zdd_divisible_by_all(X, R, R1, S), 1974 zdd_insert(A, R1, R0, S), 1975 zdd_divisible_by_all(R0, L, Z, S) 1976 ; Z = 0 % It was hard to find this. 1977 ).
1981zdd_mod(X, Y, Z, S) :- zdd_divisible(Y, X, X0, S),
1982 zdd_subtr(X, X0, Z, S).
1987% ?- zdd zdd_list(X, [[a]], S), zdd_list(Y, [[a,c],[a,d]], S), 1988% zdd_multiple(X, Y, Z, S), psa(Z, S). 1989% ?- zdd zdd_list(X, [[a,b]], S), zdd_list(Y, [[a,c],[a,d]], S), 1990% zdd_multiple(X, Y, Z, S), psa(Z, S). 1991% ?- zdd zdd_list(X, [[a,b]], S), Y<<pow([a,b,c]), 1992% zdd_multiple(X, Y, Z, S), psa(Z, S). 1993% ?- zdd Y<<pow([a,b,c]), zdd_multiple(0, Y, Z, S), psa(Z, S). 1994% ?- zdd Y<<pow([a,b]), zdd_multiple(1, Y, Z, S), psa(Z, S). 1995 1996zdd_multiple(0, _, 0, _):-!. 1997zdd_multiple(1, Y, Y, _):-!. 1998zdd_multiple(_, Y, 0, _):-Y<2, !. 1999zdd_multiple(X, Y, Z, S):-memo(multiple(X, Y)-Z, S), 2000 ( nonvar(Z) -> true 2001 ; cofact(X, t(A, L, R), S), 2002 zdd_multiple(L, Y, L0, S), 2003 zdd_multiple(A, R, Y, R0, S), 2004 zdd_join(L0, R0, Z, S) 2005 ). 2006% 2007zdd_multiple(_, _, Y, 0, _):- Y<2, !. 2008zdd_multiple(A, X, Y, Z, S):- cofact(Y, t(B, L, R), S), 2009 zdd_multiple(A, X, L, L0, S), 2010 zdd_compare(C, A, B, S), 2011 ( C = (<) -> R0 = 0 2012 ; C = (=) -> 2013 zdd_multiple(X, R, R1, S), 2014 zdd_insert(A, R1, R0, S) 2015 ; zdd_multiple(A, X, R, R1, S), 2016 zdd_insert(B, R1, R0, S) 2017 ), 2018 zdd_join(L0, R0, Z, S). 2019 2020 /********************************* 2021 * division/resudue in List * 2022 *********************************/
zdd_list(Y, U, Z)
, zdd_mod_by_list(X, U, Z, S)
.2028% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a], Y), psa(Y))). 2029% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [], Y), psa(Y))). 2030% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a, b], Y), psa(Y))). 2031% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [b,c], Y), psa(Y))). 2032% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [a,c], Y), psa(Y))). 2033% ?- zdd((X<<pow([a]), zdd_mod_by_list(X, [c], Y), psa(Y))). 2034% ?- N=100, numlist(1, N, Ns), numlist(1, N, Js), zdd((X<<pow(Ns), zdd_mod_by_list(X, Js, Z), card(Z, C))). 2035 2036zdd_mod_by_list(X, Y, Z, S):- zdd_divisible_by_list(X, Y, Z0, S), 2037 zdd_subtr(X, Z0, Z, S).
zdd_sets(U, [X], Z, S)
, zdd_div(Y, U, Z, S)
.2043% ?- zdd((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 2044% ?- zdd((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 2045 2046zdd_div_by_list(X, [], X, _):-!. 2047zdd_div_by_list(X, F, Y, S):- F=[A|As], 2048 ( X<2 -> Y = 0 2049 ; cofact(X, t(B, L, R), S), 2050 zdd_div_by_list(L, F, L0, S), 2051 zdd_compare(C, B, A, S), 2052 ( C = (>) -> R0 = 0 2053 ; C = (=) -> 2054 zdd_div_by_list(R, As, R0, S) 2055 ; zdd_div_by_list(R, F, R1, S), 2056 zdd_insert(B, R1, R0, S) 2057 ), 2058 zdd_join(L0, R0, Y, S) 2059 ).
zdd_sets(U, [X], S)
, zdd_divisible(Y, U, Z, S)
.2065% ?- zdd((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 2066% ?- zdd((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 2067 2068zdd_divisible_by_list(X, [], X, _):-!. 2069zdd_divisible_by_list(X, F, Y, S):- F=[A|As], 2070 ( X<2 -> Y = 0 2071 ; cofact(X, t(B, L, R), S), 2072 zdd_divisible_by_list(L, F, L0, S), 2073 zdd_compare(C, B, A, S), 2074 ( C = (>) -> R0 = 0 2075 ; C = (=) -> zdd_divisible_by_list(R, As, R0, S) 2076 ; zdd_divisible_by_list(R, F, R0, S) 2077 ), 2078 cofact(Y, t(B, L0, R0), S) 2079 2080 ). 2081 2082 2083 2084 /********************* 2085 * meta on ZDD * 2086 *********************/ 2087 2088% ?- zdd((X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2089% ?- zdd((X<<pow([1,2,4,5,6]), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2090% ?- N=2, numlist(1, N, L), zdd((X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2091% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2092% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2093% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2094% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N. 2095% ?- N=1000, numlist(1, N, L), zdd((X<<pow(L), 2096% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N.
map_zdd(F, X, Y)
works roughly like
maplist(maplist(F), X, Y)
) with a list X of lists.
2105:- meta_predicate map_zdd( , , , ). 2106 2107map_zdd(_, X, X, _):- X<2, !. 2108map_zdd(F, X, Y, S):- memo(map(X,F)-Y, S), 2109 ( nonvar(Y)-> true 2110 ; cofact(X, t(A, L, R), S), 2111 map_zdd(F, L, L0, S), 2112 map_zdd(F, R, R0, S), 2113 call(F, A, B), 2114 zdd_insert(B, R0, R1, S), 2115 zdd_join(L0, R1, Y, S) 2116 ). 2117 2118% ?- zdd((memo(a-1), set_memo(a-2), memo(a-V))). 2119% ?- zdd((X<<pow([a,b,c,d]), prz(X))). 2120% ?- zdd((X<<pow([a,b,c]), psa(X))). 2121% ?- zdd((prz(1))). 2122% ?- zdd((prz(0))). 2123% ?- zdd((mp(hello, 1))). 2124% ?- zdd((mp(hello, 0))).
2128prz(X, S):- print_set_at(X, S).
pow([a])
, psa(X)
.
?- zdd X<<{[a]}, psa(X)
.2135psa(M, X, S):- writeln(M), 2136 print_set_at(X, S), 2137 writeln('-------------------'). 2138 2139psa(X, S):- print_set_at(X, S), 2140 writeln('-------------------'). 2141% 2142psa :- sat_fetch(S), get_key(root, R, S), 2143 psa(R, S). 2144% 2145mp(M, X) :- shift(mp(M, X)).
2149mp(M, X, S) :- format("~w\n", [M]), print_set_at(X, S).
2153print_set_at(0, _):-!, format("\szid = 0\n\t0\n"). 2154print_set_at(1, _):-!, format("\szid = 1\n\t[]\n"). 2155print_set_at(X, S):- format("\szid = ~w\n", [X]), 2156 forall(set_at(P, X, S), format("\t~w\n", [P])). 2157 2158% ?- zdd((X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X))). 2159% ?- zdd((X<<pow([1,2]), set_at(U, X))). 2160% ?- zdd((X<<pow([1,2]), mp(powerset, X))). 2161 2162set_at([], 1, _):-!. 2163set_at(P, X, S):- X>1, 2164 cofact(X, t(A, L, R), S), 2165 ( set_at(P, L, S) 2166 ; set_at(As, R, S), 2167 P=[A|As] 2168 ). 2169 2170% set_at(P, X, S):- X>1, 2171% cofact(X, t(A, L, R), S), 2172% ( set_at(P, L, S) 2173% ; set_at(As, R, S), 2174% P=[A|As] 2175% ). 2176 2177% ?- zdd zdd_singleton(a, X), show_fos(X). 2178% ?- zdd X<< {[a,b], [b,c]}, show_fos(X). 2179% ?- zdd X<< pow([a,b]), show_fos(X).
2183show_fos(X, S):- X > 1, 2184 accessible_nodes(X, Ns, S), 2185 forall( member(M, Ns), 2186 ( cofact(M, T, S), 2187% cofact_intern(T, T0), 2188 writeln(M->T))). 2189% 2190accessible_nodes(X, Ns, S):- 2191 accessible_nodes(X, Ns0, [], S), 2192 sort(Ns0, Ns1), 2193 reverse(Ns1, Ns). 2194% 2195accessible_nodes(X, A, A, _):- X<2, !. 2196accessible_nodes(X, [X|A], B, S):- 2197 cofact(X, t(_, L, R), S), 2198 accessible_nodes(L, A, A0, S), 2199 accessible_nodes(R, A0, B, S).
2205% ?- zdd((X<<pow([a,b,c]), zdd_list(X, Y), zdd_list(X0, Y))). 2206% ?- powerset([a,b,c], Y), zdd((zdd_list(X, Y), zdd_list(X, Y0), zdd_list(X0, Y0))), 2207% maplist(sort, Y, Y1), sort(Y1, Y2). 2208% 2209zdd_list(X, Y, S):- nonvar(X), !, zdd_sets(X, Y, S). 2210zdd_list(X, Y, S):- zdd_family(Y, X, S). 2211 2212% ?- zdd((X<<pow([a,b,c]), sets(X, P))). 2213% ?- zdd((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))). 2214% ?- zdd((X<<pow([]), sets(X, P))). 2215% ?- zdd((X<<pow([a]), sets(X, P))). 2216% ?- zdd((X<<pow(:numlist(1,3)), sets(X, Y))). 2217% ?- zdd((X<<pow([a,b,c]), sets(X, Y))). 2218% ?- zdd((X<<pow(:charlist($a, $c)), sets(X, Y))). 2219% ?- zdd((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))), sets(X, Y))).
2224sets(X, Y, S):- zdd_sets(X, Y0, S), zdd_sort(Y0, Y, S). 2225% 2226zdd_sets(1, [[]], _):-!. 2227zdd_sets(0, [], _):-!. 2228zdd_sets(X, P, S):- 2229 cofact(X, t(A,L,R), S), 2230 zdd_sets(L, Y, S), 2231 zdd_sets(R, Z, S), 2232 maplist(cons(A), Z, AZ), 2233 append(AZ, Y, P). 2234 2235% ?- open_state(S), zdd_eval(pow([a, b, c, d, e, f]), I, S), eqns(I, X, S), 2236% maplist(writeln, X). 2237% 2238eqns(X, Y, S):- zdd_eqns(X, Y, S). 2239 2240basic_zdd(0). 2241basic_zdd(1). 2242 2243% ?- zdd X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es). 2244% ?- zdd X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es). 2245 2246zdd_eqns(I, Es, S):- nonvar(I), var(Es), !, 2247 zdd_to_eqns(I, Es, [], S). 2248zdd_eqns(I, Es, S):- var(I), nonvar(Es), !, 2249 ( check_eqns_for_zdd(Es, S) 2250 -> Es = [X=_|_], 2251 eqns_to_zdd(Es, X, I, S) 2252 ; throw('Violating-underlying-ordering-on-atoms.'(Es)) 2253 ). 2254% 2255zdd_to_eqns(I, X, S):- zdd_to_eqns(I, X, [], S), 2256 zdd_sort(X, X1, S), 2257 reverse(X1, X). 2258% 2259zdd_to_eqns(I, X, X, _):- I<2, !. 2260zdd_to_eqns(I, X, Y, S):- memo(visited(I)-F, S), 2261 ( nonvar(F) -> Y = X 2262 ; F = true, 2263 cofact(I, t(A, L, R), S), 2264 X = [I=t(A, L, R)|X0], 2265 zdd_to_eqns(L, X0, X1, S), 2266 zdd_to_eqns(R, X1, Y, S) 2267 ). 2268% 2269check_eqns_for_zdd(Es, S):- are_eqns_closed(Es, Es, S), 2270 sort(Es, Fs), 2271 has_unique_left(Fs), 2272 sort(2, @=<, Es, Gs), 2273 has_unique_right(Gs). 2274% 2275are_eqns_closed([], _, _). 2276are_eqns_closed([_ = t(A, L, R)|Rest], Es, S):- 2277 ( basic_zdd(L) -> true 2278 ; memberchk(L = t(B, _, _), Es), 2279 zdd_compare(<, A, B, S) 2280 ), 2281 ( basic_zdd(R) -> true 2282 ; memberchk(L = t(C, _, _), Es), 2283 zdd_compare(<, A, C, S) 2284 ), 2285 are_eqns_closed(Rest, Es, S). 2286% 2287eqns_to_zdd(_, 0, 0, _):-!. 2288eqns_to_zdd(_, 1, 1, _):-!. 2289eqns_to_zdd(Es, X, I, S):- memo(solve(X)-I, S), 2290 ( nonvar(I) -> true 2291 ; memberchk(X = t(A, L, R), Es), 2292 eqns_to_zdd(Es, L, L0, S), 2293 eqns_to_zdd(Es, R, R0, S), 2294 cofact(I, t(A, L0, R0), S) 2295 ).
is_function([a-1,b-2,c-3])
.
?- is_function([a-1,b-2,a-3])
.2301is_function(X):- sort(X, Y), has_unique_left(Y). 2302% 2303has_unique_left([X,Y|Z]):-!, 2304 ( arg(1, X, A), arg(1, Y, A) -> false 2305 ; has_unique_left([Y|Z]) 2306 ). 2307has_unique_left(_).
2312% ?- check_one_to_one([a-1,b-2,c-3]). 2313% ?- check_one_to_one([a-1,b-2,c-1]). % false 2314 2315check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y). 2316% 2317has_unique_right([X,Y|Z]):-!, 2318 ( arg(2, X, A), arg(2, Y, A) -> false 2319 ; has_unique_right([Y|Z]) 2320 ). 2321has_unique_right(_).
2325ppoly(X, S):- poly_term(X, Poly, S), 2326 writeln(Poly). 2327 2328% ?- zdd((X<<pow([a,b]), poly_term(X, P))). 2329% ?- zdd((X<<pow([a,b,c]), poly_term(X, P))). 2330% ?- zdd((X<<(@a + @b), psa(X))). 2331% 2332poly_term(X, Poly):- shift(poly_term(X, Poly)). 2333% 2334poly_term(X, Poly, S):- zdd_sets(X, Sets, S), 2335 get_compare(Pred, S), 2336 maplist(predsort(Pred), Sets, Sets0), 2337 predsort(Pred, Sets0, Sets1), 2338 poly_term0(Sets1, Poly). 2339 2340% ?- poly_term0([], Y). 2341% ?- poly_term0([[]], Y). 2342% ?- poly_term0([[a], [b]], Y). 2343% ?- poly_term0([[a*b], [c]], Y). 2344 2345poly_term0(X, Y):- maplist(mul_term, X, X0), 2346 sum_term(X0, Y). 2347% 2348mul_term([], 1):-!. 2349mul_term([X], X):-!. 2350mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 2351% 2352sum_term([], 0):-!. 2353sum_term([X], X):-!. 2354sum_term([X, Y|Xs], Z):-sum_term([X+Y|Xs], Z).
?- zdd((X << pow([a, b, c]), zdd_rand_path(X)))
.
?- zdd((X << {[a], [b], [c]}, zdd_rand_path(X)))
.
?- zdd((X << pow([a, b, c, d, e, f, g]), zdd_rand_path(X)))
.
@ [a,c,e,f]
@ X = 8.
2366zdd_rand_path(I, S):- zdd_rand_path(I, P, [], S), writeln(P). 2367% 2368zdd_rand_path(I, P, S):- zdd_rand_path(I, P, [], S). 2369% 2370zdd_rand_path(1, X, X, _):-!. 2371zdd_rand_path(I, X, Y, S):- I>1, 2372 cofact(I, t(A, L, R), S), 2373 ( L == 0 -> 2374 X = [A|X0], 2375 zdd_rand_path(R, X0, Y, S) 2376 ; random(2) =:= 0 -> 2377 X = [A|X0], 2378 zdd_rand_path(R, X0, Y, S) 2379 ; zdd_rand_path(L, X, Y, S) 2380 ).
zdd((zdd_atoms(1, S)))
.
?- zdd((family([[a,b],[b,c]], X), zdd_atoms(X, S)))
.
?- N = 10000, time(zdd(({numlist(1, N, L)}, X<<pow(L), zdd_atoms(X, S))))
.
?- zdd X<<pow([a,b,c,d])
, zdd_atoms(X, U)
.2389zdd_atoms(X, [], _):- X<2, !. 2390zdd_atoms(X, P, S):- memo(atoms(X)-P, S), 2391 ( nonvar(P) -> true 2392 ; cofact(X, t(A, L, R), S), 2393 zdd_atoms(L, Al, S), 2394 zdd_atoms(R, Ar, S), 2395 ord_union(Al, Ar, P0), 2396 P=[A|P0] 2397 ). 2398 2399% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 2400:- meta_predicate delete( , , ). 2401delete(X, Y, Z):- delete(X, Y, Z, []). 2402 2403:- meta_predicate delete( , , , ). 2404delete(_, [], L, L). 2405delete(Pred, [X|Xs], L, L0):- 2406 ( call(Pred, X) 2407 -> delete(Pred, Xs, L, L0) 2408 ; L = [X|L1], 2409 delete(Pred, Xs, L1, L0) 2410 ). 2411 2412% ?- zdd((zdd_power([a,b], R), sets(R, U))). 2413% ?- zdd((X<< zdd_power(:charlist($(a-c))), sets(X, U))). 2414% ?- zdd((R<< pow(: !charlist(a-d)), card(R, C))). 2415%% 2416zdd_power(X, Y, S):- zdd_sort(X, X0, S), 2417 zdd_ord_power(X0, 1, Y, S).
zdd_ord_power([a,b], 1, X)
, psa(X)
.2422zdd_ord_power([], P, P, _). 2423zdd_ord_power([X|Xs], P, Q, S):- zdd_ord_power(Xs, P, R, S), 2424 cofact(Q, t(X, R, R), S).
a(e0,e1)
, where a is an atom,
e0 and e1 are integer expressions.
A is the list of atoms ai with suffix i (j=<i=<k),
where j and k is the value of e0 and e1.2432% ?- atomlist(ax(1+1, 3+1), As). 2433% ?- atomlist(ax(1, 3), As). 2434atomlist(X, As):- X=..[A, I, J], 2435 I0 is I, 2436 J0 is J, 2437 findall(Y, ( between(I0, J0, K), 2438 atom_concat(A, K, Y) 2439 ), 2440 As).
2446% ?- charlist(a-c, X). 2447charlist(A-B, I):- 2448 findall(X, ( char_type(X, alnum), 2449 X @>= A, 2450 X @=< B 2451 ), 2452 I).
charlist(A-B, X)
.
?- charlist(a, c, X)
.
@ X = [a, b, c].2458charlist(A, B, I):- charlist(A-B, I). 2459 2460% ?- term_atoms(a+b=c, L). 2461% ?- term_atoms(a+b, L). 2462% ?- term_atoms(f(a+a), L).
2468term_atoms(X, L):- term_atoms(X, L0, []), 2469 sort(L0, L). 2470 2471% 2472term_atoms(X, L, L):- var(X), !. 2473term_atoms(X, [X|L], L):- atom(X), !. 2474term_atoms([X|Y], L, L0):-!, 2475 term_atoms(X, L, L1), 2476 term_atoms(Y, L1, L0). 2477term_atoms(X, L, L0):- compound(X), !, 2478 X =..[_|As], 2479 term_atoms(As, L, L0). 2480term_atoms(_, L, L). 2481 2482% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 2483% ?- subst_opp(a, X, [b-a]). 2484% ?- subst_opp([a], X, [b-a]). 2485 2486subst_opp(X, Y, L):- memberchk(Y-X, L). 2487subst_opp([X|Y], [X0|Y0], L):-!, 2488 subst_opp(X, X0, L), 2489 subst_opp(Y, Y0, L). 2490subst_opp(X, Y, L):- compound(X), !, 2491 X =..[F|As], 2492 subst_opp(As, Bs, L), 2493 Y =..[F|Bs]. 2494subst_opp(X, X, _). 2495 2496% ?- subst_term(f(a), R, [a-b]). 2497% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 2498% ?- subst_term(f(a), R, [a-X]). 2499% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2500% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2501% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
2507subst_term(X, Y, S):- member(X0-Y, S), X0==X, !. 2508subst_term(A, B, S):- compound(A), !, 2509 ( A = [X|Y] -> 2510 B = [X0|Y0], 2511 subst_term(X, X0, S), 2512 subst_term(Y, Y0, S) 2513 ; functor(A, F, N), 2514 functor(B, F, N), 2515 subst_term(N, A, B, S) 2516 ). 2517subst_term(X, X, _). 2518% 2519subst_term(0, _, _, _):-!. 2520subst_term(I, X, Y, S):- 2521 arg(I, X, A), 2522 arg(I, Y, B), 2523 subst_term(A, B, S), 2524 J is I - 1, 2525 subst_term(J, X, Y, S). 2526 2527% ?- all_instances([a,b], [0,1], a+b=b, R). 2528% ?- all_instances([x,y], [0,1], x+y=x, R). 2529%! all_instances(+As, +Vs, +X, -Y) is det. 2530% Unify Y with the list of possible variations P of X, 2531% where P is a variation of X if for each A in As with some 2532% V in Vs which depends on A, P is obtained from X by replacing 2533% all occurrences of A appearing in X with V for A in As. 2534 2535all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 2536 apply_maps(Fs, X, Y, []). 2537% 2538apply_maps([], _, Y, Y). 2539apply_maps([F|Fs], X, [X0|Y], Z):- 2540 subst_term(X, X0, F), 2541 apply_maps(Fs, X, Y, Z). 2542 2543% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 2544% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 2545% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 2546% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 2547%! mod_table(+M, +X, +E, -T) is det. 2548% Unify T with a set of form E' = V where 2549% E' is a possible ground instance of an integer expression E 2550% and V is the value of E' with modulo M, where X is a set of 2551% parameters appearing in E. 2552 2553mod_table(M, Xs, Exp, Table):- M0 is M-1, 2554 numlist(0, M0, V), 2555 all_instances(Xs, V, Exp, Exps), 2556 !, 2557 maplist(mod_arith(M), Exps, Table). 2558% 2559mod_arith(M, Exp, Exp=V):- V is Exp mod M. 2560 2561% 2562unify_all([]). 2563unify_all([_]). 2564unify_all([X,Y|Z]):- zdd:(X=Y), unify_all([Y|Z]). 2565 2566% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 2567% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 2568% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 2569% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 2570% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 2571% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
zdd((X <<{[a,b], [a,c]}, zdd_appear(e, X)))
. % false
?- zdd((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X)
)). % false
?- zdd((X <<(*[a,b]+ *[a,c]), psa(X)
, zdd_appear(c, X)
)).
?- numlist(1, 10000, Ns)
, zdd((X<<pow(Ns), zdd_appear(10000, X)))
.
?- zdd X<<pow(:numlist(1, 10000)
), zdd_appear(10000, X)
.2581zdd_appear(A, X, S):- open_memo(S), 2582 get_child(S, M), 2583 zdd_appear(A, X, S, M), 2584 close_memo(S). 2585% 2586zdd_appear(A, X, S, M):- X > 1, 2587 memo(visited(X)-B, M), 2588 var(B), 2589 cofact(X, t(U,L,R), S), 2590 zdd_compare(C, A, U, S), 2591 ( C = (=) 2592 -> true 2593 ; C = (>), 2594 ( zdd_appear(A, L, S, M) -> true 2595 ; L < 2 2596 -> zdd_appear(A, R, S, M) 2597 ; memo(visited(L)-true, M), % for earlier fail. 2598 zdd_appear(A, R, S, M) 2599 ) 2600 ).
2605zdd_singleton(X, P, S):- cofact(P, t(X, 0, 1), S).
zdd0((X<<pow([a,b,c]), zdd_subtr(1, X, Y), card(Y, C)))
.2611zdd_has_1(1, _):-!. 2612zdd_has_1(X, S):- X>1, 2613 cofact(X, t(_, L, _), S), 2614 zdd_has_1(L, S).
zdd((U<<{[a]}, P<<pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q)))
.2625zdd_subst(_, _, X, X, _):- X<2, !. 2626zdd_subst(X, U, P, Q, S):- memo(zdd_subst(X, U, P)-Q, S), 2627 ( nonvar(Q) -> true 2628 ; cofact(P, t(Y, L, R), S), 2629 zdd_subst(X, U, L, L0, S), 2630 zdd_compare(C, X, Y, S), 2631 ( C = (=) -> zdd_merge(U, R, R0, S) 2632 ; C = (<) -> zdd_cons(R0, Y, R, S) 2633 ; zdd_subst(X, U, R, R1, S), 2634 zdd_insert(Y, R1, R0, S) 2635 ), 2636 zdd_join(L0, R0, Q, S) 2637 ). 2638 2639 /*********************** 2640 * product on zdd * 2641 ***********************/ 2642 2643% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))). 2644% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y))). 2645% ?- zdd((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))). 2646% ?- zdd((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))). 2647% ?- time(zdd((X<<pow(@numlist(1,16)), Z<<(X**X), card(Z, C)))). 2648% ?- call_with_time_limit(120, (numlist(1, 16, R), 2649% time(zdd((X<<pow(R), Z<<(X**X), card(Z, C)))))). 2650 2651zdd_product(X, Y, Z):- shift(zdd_product(X, Y, Z)). 2652% 2653zdd_product(X, Y, 0, _):- (X<2; Y<2), !. 2654zdd_product(X, Y, Z, S):- memo(prod(X, Y)-Z, S), 2655 ( nonvar(Z) -> true % , write(.) % hits found. 2656 ; zdd_product(X, Y, [], Bs, 0, Z0, S), 2657 append_pairs_list(X, Bs, Z1, S), 2658 zdd_join(Z0, Z1, Z, S) 2659 ). 2660% 2661zdd_product(_, X, Bs, Bs, Z, Z, _):- X<2, !. 2662zdd_product(X, Y, Bs, Q, U, V, S):- cofact(Y, t(B, L, R), S), 2663 zdd_product(X, L, L0, S), 2664 zdd_join(L0, U, U0, S), 2665 zdd_product(X, R, [B|Bs], Q, U0, V, S). 2666% 2667append_pairs_list(X, _, X, _):- X<2, !. 2668append_pairs_list(X, Bs, U, S):- cofact(X, t(A, L, R), S), 2669 append_pairs_list(R, Bs, R0, S), 2670 append_pairs_list(L, Bs, L0, S), 2671 insert_pairs(A, Bs, R0, R1, S), 2672 zdd_join(L0, R1, U, S). 2673 2674% 2675insert_pairs(_, [], U, U, _):-!. 2676insert_pairs(A, [B|Bs], U, V, S):- 2677 zdd_insert((A-B), U, U0, S), 2678 insert_pairs(A, Bs, U0, V, S). 2679 2680 /************************* 2681 * Quotient on ZDD * 2682 *************************/
?- zdd((zdd_insert(a, 1, X), zdd_insert(b, X, X1), prz(X1)))
.
?- zdd((X<<pow([a,b,c]), zdd_insert(x, X, X1), psa(X1)))
.
2691zdd_insert(_, 0, 0, _):-!. 2692zdd_insert(A, 1, J, S):-!, zdd_singleton(A, J, S). 2693zdd_insert(A, I, J, S):- memo(insert(A, I)-J, S), 2694 ( nonvar(J) -> true 2695 ; cofact(I, t(X, L, R), S), 2696 zdd_compare(C, A, X, S), 2697 ( C = (=) -> 2698 zdd_join(L, R, K, S), 2699 cofact(J, t(X, 0, K), S) 2700 ; C = (<) -> 2701 cofact(J, t(A, 0, I), S) 2702 ; zdd_insert(A, L, L0, S), 2703 zdd_insert(A, R, R0, S), 2704 cofact(J, t(X, L0, R0), S) 2705 ) 2706 ). 2707 2708% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), 2709% psa(X, S), psa(Y, S), 2710% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S). 2711 2712% ?- zdd X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S), 2713% psa(Y, S). 2714% ?- listing(zdd_insert). 2715 2716:- meta_predicate zdd_insert( , , , , ). 2717zdd_insert(_, _, 0, 0, _):-!. 2718zdd_insert(_, A, 1, Y, S):-!, zdd_singleton(A, Y, S). 2719zdd_insert(F, A, X, Y, S):- memo(zdd_insert(X, A, F)-Y, S), 2720 ( nonvar(Y) -> true % , write(.) % many hits 2721 ; cofact(X, t(B, L, R), S), 2722 zdd_insert(F, A, L, L0, S), 2723 call(F, C, A, B), 2724 ( C = (=) -> zdd_cons(R0, A, R, S) 2725 ; C = (<) -> bdd_append([A, B], R, R0, S) 2726 ; zdd_insert(F, A, R, R1, S), 2727 zdd_cons(R0, B, R1, S) 2728 ), 2729 zdd_join(L0, R0, Y, S) 2730 ). 2731 2732% ?- zdd((family([[a, b],[b]], X), sets(X, Sx), 2733% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
2738% ?- numlist(1, 10000, Ns), zdd((zdd_insert_atoms(Ns, 1, X), psa(X))). 2739zdd_insert_atoms(As, X, Y):- shift(zdd_insert_atoms(As, X, Y)). 2740 2741% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))). 2742% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))). 2743zdd_insert_atoms(X, Y, Z, S):- zdd_sort(X, X0, S), 2744 zdd_ord_insert(X0, Y, Z, S). 2745% 2746zdd_ord_insert(_, 0, 0, _):-!. 2747zdd_ord_insert([], X, X, _):-!. 2748zdd_ord_insert(As, 1, Y, S):-!, zdd_ord_append(As, 1, Y, S). 2749zdd_ord_insert(As, X, Y, S):- memo(ord_insert(X, As)-Y, S), 2750 ( nonvar(Y) -> true % , write(.) % many hits. 2751 ; As = [A|U], 2752 cofact(X, t(B, L, R), S), 2753 zdd_compare(C, A, B, S), 2754 ( C = (<) -> 2755 zdd_ord_insert(U, X, Y0, S), 2756 cofact(Y, t(A, 0, Y0), S) 2757 ; C = (=) -> 2758 zdd_ord_insert(U, L, L1, S), 2759 zdd_ord_insert(U, R, R1, S), 2760 zdd_join(R1, L1, Y0, S), 2761 cofact(Y, t(A, 0, Y0), S) 2762 ; zdd_ord_insert(As, L, L1, S), 2763 zdd_ord_insert(As, R, R1, S), 2764 cofact(Y, t(B, L1, R1), S) 2765 ) 2766 ).
2772% ?- numlist(1, 100, Ns), zdd((X<<pow(Ns), card(X, C))). 2773% ?- numlist(1, 100, Ns), zdd((X<<pow(Ns))). 2774 2775% ?- zdd((zdd_append([c, a, b,c], 1, Z), psa(Z))). 2776zdd_append(X, Y, Z, S):- zdd_sort(X, X0, S), 2777 zdd_ord_append(X0, Y, Z, S). 2778% 2779zdd_ord_append([], X, X, _). 2780zdd_ord_append([A|As], X, Y, S):- 2781 zdd_ord_append(As, X, Y0, S), 2782 cofact(Y, t(A, 0, Y0), S). 2783 2784% ?- zdd X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y, S), psa(Y, S). 2785:- meta_predicate zdd_reorder( , , , ). 2786zdd_reorder(_, X, X, _):- X<2, !. 2787zdd_reorder(F, X, Y, S):- cofact(X, t(A, L, R), S), 2788 zdd_reorder(F, L, L0, S), 2789 zdd_reorder(F, R, R1, S), 2790 zdd_insert(F, A, R1, R0, S), 2791 zdd_join(L0, R0, Y, S). 2792 2793 2794 /***************** 2795 * filters * 2796 *****************/ 2797 2798% ?- zdd X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y, S), psa(Y, S). 2799% ?- zdd X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y, S), psa(Y, S). 2800% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y, S), psa(Y, S). 2801% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, 3], X, Y, S), psa(Y, S). 2802% ?- zdd numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y, S), psa(Y, S). 2803% ?- zdd numlist(1, 1000, Ns), X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y, S), card(Y, C, S), 2804% card(X, D, S), compare(E, C, D), U is D-C. 2805% 2806ltr_meet_filter([], X, X, _):-!. 2807ltr_meet_filter([A|F], X, Y, S):- 2808 ltr_filter(A, X, X0, S), 2809 ltr_meet_filter(F, X0, Y, S). 2810 2811% ?- zdd X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y, S), psa(Y, S). 2812% ?- zdd X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y, S), psa(Y, S). 2813ltr_join_filter(F, X, Y, S):- 2814 ltr_join_filter(F, X, 0, Y, S). 2815% 2816ltr_join_filter([], _, Y, Y, _):-!. 2817ltr_join_filter([P|F], X, Y, Y0, S):-!, 2818 ltr_filter(P, X, Y1, S), 2819 zdd_join(Y, Y1, Y2, S), 2820 ltr_join_filter(F, X, Y2, Y0, S). 2821 2822% 2823ltr_filter(-A, X, Y, S):-!, ltr_filter_negative(A, X, Y, S). 2824ltr_filter(A, X, Y, S):- ltr_filter_positive(A, X, Y, S). 2825 2826% 2827ltr_filter_negative(_, X, X, _):- X<2, !. 2828ltr_filter_negative(A, X, Y, S):- memo(letral_neg(X, A)-Y, S), 2829 ( nonvar(Y) -> true 2830 ; cofact(X, t(B, L, R), S), 2831 ltr_filter_negative(A, L, L0, S), 2832 zdd_compare(C, A, B, S), 2833 ( C = (=) -> R0 = 0 2834 ; C = (<) -> R0 = R 2835 ; ltr_filter_negative(A, R, R0, S) 2836 ), 2837 cofact(Y, t(B, L0, R0), S) 2838 ). 2839% 2840ltr_filter_positive(_, X, 0, _):- X<2, !. 2841ltr_filter_positive(A, X, Y, S):- memo(ltr_pos(X, A)-Y, S), 2842 ( nonvar(Y) -> true 2843 ; cofact(X, t(B, L, R), S), 2844 ltr_filter_positive(A, L, L0, S), 2845 zdd_compare(C, A, B, S), 2846 ( C = (=) -> R0 = R 2847 ; C = (<) -> R0 = 0 2848 ; ltr_filter_positive(A, R, R0, S) 2849 ), 2850 cofact(Y, t(B, L0, R0), S) 2851 ). 2852 2853% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[-b,-c]], X, Y)), psa(Y))). 2854% ?- zdd((X<<pow([a,b]), shift(dnf_filter([[b]], X, Y)), psa(Y))). 2855% ?- zdd((X<<pow([a,b]), shift(dnf_filter([[a,b]], X, Y)), psa(Y))). 2856% ?- zdd((X<<pow([a,b]), shift(dnf_filter([], X, Y)), psa(Y))). 2857% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[c]], X, Y)), psa(Y))). 2858% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([], X, Y)), psa(Y))). 2859% ?- zdd((X<<pow([a,b,c]), shift(dnf_filter([[a],[-c]], X, Y)), psa(Y))). 2860dnf_filter(DNF, X, Y, S):- dnf_filter(DNF, X, 0, Y, S). 2861% 2862dnf_filter([], _, Y, Y, _). 2863dnf_filter([F|Fs], X, Y, Z, S):- 2864 ltr_meet_filter(F, X, X0, S), 2865 zdd_join(X0, Y, Y0, S), 2866 dnf_filter(Fs, X, Y0, Z, S). 2867 2868% ?- zdd((X<<pow([a,b,c]), shift(cnf_filter([[-b,-c]], X, Y)), psa(Y))). 2869% ?- zdd((X<<pow([a,b,c]), shift(cnf_filter([[-a, -b, -c]], X, Y)), psa(Y))). 2870cnf_filter([], X, X, _). 2871cnf_filter([F|Fs], X, Y, S):- 2872 ltr_join_filter(F, X, X0, S), 2873 cnf_filter(Fs, X0, Y, S). 2874 2875% 2876zdd_meet_list([A], A, _):-!. 2877zdd_meet_list([A|As], B, S):- zdd_meet_list(As, A, B, S). 2878% 2879zdd_meet_list([], X, X, _). 2880zdd_meet_list([A|As], X, Y, S):- zdd_meet(A, X, X0, S), 2881 zdd_meet_list(As, X0, Y, S). 2882% 2883zdd_join_list([], 0, _):-!. 2884zdd_join_list([X|Xs], Y, S):- zdd_join_list(Xs, X, Y, S). 2885% 2886zdd_join_list([], X, X, _):-!. 2887zdd_join_list([A|As], X, Y, S):- zdd_join(A, X, X0, S), 2888 zdd_join_list(As, X0, Y, S). 2889 2890% 2891ltr_join_list([], 0, _):-!. 2892ltr_join_list([X|Xs], Y, S):-ltr_join_list(Xs, X, Y, S). 2893% 2894ltr_join_list([], X, X, _):-!. 2895ltr_join_list([A|As], X, Y, S):- zdd_join(A, X, X0, S), 2896 ltr_join_list(As, X0, Y, S). 2897 2898 /********************* 2899 * remove atom * 2900 *********************/
2906% ?- zdd((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2907% sets(Y, Sy))). 2908zdd_remove(X, Y, Z, S):- setup_call_cleanup( 2909 open_state(M, [hash_size(256)]), 2910 zdd_remove(X, Y, Z, S, M), 2911 close_state(M)). 2912% 2913zdd_remove(_, X, X, _, _):- X<2, !. 2914zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2915 ( nonvar(J) -> true 2916 ; cofact(I, t(Ai, Li, Ri), S), 2917 zdd_compare(C, A, Ai, S), 2918 ( C = (<) -> J = I 2919 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2920 zdd_remove(A, Ri, Ria, S, M), 2921 cofact(J, t(Ai, Lia, Ria), S) 2922 ; zdd_join(Li, Ri, J, S) 2923 ) 2924 ). 2925 2926 2927 /********************* 2928 * Cardinality * 2929 *********************/
2934% ?-N = 10000, numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:= 2^N. 2935%@ % 1,298,553 inferences, 0.105 CPU in 0.114 seconds (92% CPU, 12364110 Lips) 2936%@ N = 10000, 2937%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2938%@ X = 10001. 2939 2940% 2941card(X, Y, S):- setup_call_cleanup( 2942 open_state(M), 2943 card_with_memo(X, Y, S, M), 2944 close_state(M)). 2945 2946% 2947card_with_memo(I, I, _, _):- I < 2, !. 2948card_with_memo(I, C, S, M):- memo(I-C, M), 2949 ( nonvar(C) -> true 2950 ; cofact(I, t(_, L, R), S), 2951 card_with_memo(R, Cr, S, M), 2952 card_with_memo(L, Cl, S, M), 2953 C is Cl + Cr 2954 ).
2959max_length(X, Max, S):- 2960 setup_call_cleanup( 2961 open_memo(S), 2962 max_length_with_memo(X, Max, S), 2963 close_memo(S)). 2964% 2965max_length_with_memo(X, 0, _):- X<2, !. 2966max_length_with_memo(X, Max, S):- 2967 memo(max(X)-Max, S), 2968 cofact(X, t(_, L, R), S), 2969 ( nonvar(Max) -> true 2970 ; max_length_with_memo(L, ML, S), 2971 max_length_with_memo(R, MR, S), Max is max(1 + MR, ML) 2972 ). 2973 2974 /*********************** 2975 * Handy helpers * 2976 ***********************/ 2977 2978% 2979unify_zip([]). 2980unify_zip([X-X|R]):- unify_zip(R). 2981 2982 2983 /****************************************** 2984 * Oprations on clauses of literals * 2985 ******************************************/ 2986 2987% ?- ltr_compare(C, a, -a). 2988% ?- ltr_compare(C, -(a), a). 2989% ?- ltr_compare(C, -(b), a). 2990% ?- ltr_compare(C, -(a), b). 2991% ?- ltr_compare(C, -(a), -(b)). 2992% ?- ltr_compare(C, -(a), -(a)).
2999ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 3000ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 3001 ( C0 == (=) -> C =(<) 3002 ; C0 = C 3003 ). 3004ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 3005 ( C0 == (=) -> C = (>) 3006 ; C0 = C 3007 ). 3008ltr_compare(C, X, Y):- compare(C, X, Y). 3009 3010% ?- zdd {ltr_compare(C, a, b)}. 3011% ?- zdd {ltr_compare(C, -a, a)}. 3012% ?- zdd {ltr_compare(C, a, -a)}. 3013% ?- zdd {ltr_compare(C, -a, b)}. 3014ltr_compare(C, X, Y, S):- get_compare(F, S), 3015 call(F, C, X, Y).
3020% ?- ltr_sort([b, b, a], X). 3021% ?- ltr_sort([-b, b,-b, -a], X). 3022 3023% ?- zdd(shift(ltr_sort([-c, a, -b, -a, b, c], X))). 3024ltr_sort(X, Y):- predsort(ltr_compare, X, Y).
3028ltr_sort(X, Y, S):- get_compare(F, S), 3029 predsort(F, X, Y). 3030 3031 3032% ?- zdd((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false 3033% ?- zdd((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))). 3034% 3035ltr_memberchk(L, Z, S):- ltr_sort(L, L0, S), 3036 ltr_ord_memberchk(L0, Z, S). 3037% 3038ltr_ord_memberchk([], Z, S):- !, zdd_has_1(Z, S). 3039ltr_ord_memberchk([A|As], Z, S):- Z > 1, 3040 cofact(Z, t(B, L, R), S), 3041 ltr_compare(C, A, B), 3042 ( C = (=) -> ltr_ord_memberchk(As, R, S) 3043 ; ltr_ord_memberchk([A|As], L, S) 3044 ). 3045 3046% ?- call_with_time_limit(100, time(zdd((big_normal_form(30, X), resolve(X))))). 3047% ?- zdd((big_normal_form(1, X), ltr_card(X, C))). 3048% ?- zdd((big_normal_form(2, X), ltr_card(X, C))). 3049% ?- zdd((big_normal_form(3, X), ltr_card(X, C))). 3050% ?- zdd((big_normal_form(10, X), ltr_card(X, C))). 3051% ?- zdd((big_normal_form(20, X), ltr_card(X, C))). 3052% ?- time(zdd((big_normal_form(100, X), ltr_card(X, C)))). 3053% ?- N=10, time(zdd((big_normal_form(N, X), ltr_card(X, C)))), C=:=2^N. 3054% ?- N=300, time(zdd((big_normal_form(N, X), ltr_card(X, C, N)))), C=:=2^N. 3055 3056big_normal_form(X, Y):- shift(big_normal_form(X, Y)). 3057% 3058big_normal_form(0, 1, _). 3059big_normal_form(N, X, S):- N>0, 3060 N0 is N-1, 3061 big_normal_form(N0, X0, S), 3062 ltr_insert(N, X0, R, S), 3063 ltr_insert(-N, X0, L, S), 3064 zdd_join(L, R, X, S). 3065 3066% ?- numlist(1, 3, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), psa(X), psa(Y), card(Y, C))). 3067% ?- time((numlist(1, 20, Ns), zdd((X<<(pow(Ns)-1), ltr_choices(X, Y), card(Y, C))))). 3068% ?- zdd((X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y))). 3069% ?- zdd((X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 3070% ltr_choices(Z, U), psa(X), psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V))). 3071% ?- zdd(( (X<< {[a,b]}), ltr_choices(X, Y), psa(X), {nl}, psa(Y))). 3072% ?- zdd(( (X<< {[a,b,c]}), ltr_choices(X, Y), psa(X), {nl}, psa(Y))). 3073% ?- zdd(( (X<< {[a, b], [c, d]}), ltr_choices(X, Y), psa(Y))). 3074% ?- zdd(( (X<< {[], [a, b], [c, d]}), ltr_choices(X, Y), psa(Y))). 3075% ?- zdd(( (X<< {[a], [c, d]}), ltr_choices(X, Y), psa(Y))). 3076% ?- zdd(( X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y))). 3077% ?- zdd(( X<< {[a,b]}, ltr_choices(X, Y), psa(Y))). 3078% ?- zdd(( X<< {[]}, ltr_choices(X, Y), psa(Y))). 3079% ?- zdd(( cnf(a, X), ltr_choices(X, Y), psa(Y))). 3080% ?- zdd(( cnf(a*b, X), ltr_choices(X, Y), psa(Y))). 3081% ?- zdd(( cnf(a* (-a), X), ltr_choices(X, Y), psa(Y))). 3082 3083% ?- N=10, numlist(2, 10, Ns), zdd((sample_cnf(Ns, X), card(X, C))). 3084% ?- N=100, numlist(2, N, Ns), time(zdd((sample_cnf(Ns, X), card(X, C), resolve(X)))). 3085%@ 3086 3087sample_cnf([], 1, _). 3088sample_cnf([J|Js], X, S):- sample_cnf(Js, Y, S), 3089 ltr_insert(J, Y, Z, S), 3090 ltr_insert(-J, Y, U, S), 3091 ltr_join(Z, U, X, S). 3092 3093% test sat. PASSED. [2023/11/09] 3094% ?- sat(-true). % false 3095% ?- sat(a+b), sat_count(C). 3096% ?- sat(a), sat(b). 3097% ?- sat(-(a + -a)). % false 3098% ?- sat(a), sat(b), sat_count(C). 3099% ?- sat(or(a, b)), sat_count(C). 3100% ?- sat(b), sat_count(C). 3101% ?- sat(xor(a, b)), sat_count(C). 3102% ?- sat(exor(a, b)), sat_count(C). 3103% ?- sat(e_x_o_r(a, b)), sat_count(C). 3104% ?- sat(a), sat(-a). % false. 3105% ?- sat(a), sat(a+b), sat_count(C). 3106% ?- sat(a(1)+a(2)), sat_count(C). 3107% ?- sat(A+a(2)), sat_count(C). 3108% ?- sat(A + B), sat_count(C). 3109% ?- sat(a+b+c+d), sat_count(C). 3110% ?- sat(a+b), sat(c+d), sat_count(C). 3111% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 3112% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 3113% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false. 3114% ?- sat(*[p(1),p(2)]), sat_count(C). 3115% ?- sat(+[p(1),p(2)]), sat_count(C). 3116% ?- N=10, findall(p(I, J), 3117% (between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C). 3118% ?- N=10, findall(p(I, J), 3119% (between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C). 3120% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false 3121% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 3122% ?- sat(A + B), sat_count(C). 3123% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 3124% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 3125% ?- sat(a=<(b=<a)), sat_count(Count). 3126% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3127% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3128% ?- Prop = 3129% ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)), 3130% sat(Prop), sat_count(C). 3131% ?- sat(a+b), sat(b+c), b_getval(sat_state, S), 3132% get_key(root, R, S), ltr_card(R, C, S). 3133% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false 3134% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false 3135 3136% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa. 3137% ?- sat(A=:=B), psa, sat(B=:=C), psa. 3138sat(X):- 3139 sat_fetch(S), 3140 get_key(root, Root, S), 3141 dnf(X, Y, S), 3142 ltr_merge(Y, Root, Root0, S), 3143 set_key(root, Root0, S), 3144 !, 3145 Root0 \== 0. 3146% 3147sat_fetch(S):- 3148 ( nb_current(sat_state, S), S \== [] -> true 3149 ; open_state(S, [extra([root-1, varnum-0, atom_index-0])]), 3150 set_compare(ltr_compare, S), 3151 b_setval(sat_state, S) 3152 ). 3153 3154sat_close:- sat_fetch(S), 3155 close_state(S), 3156 b_setval(sat_state, S). % nb_setval ? 3157 3158% ?- Prop = 3159% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3160% sat(Prop), 3161% sat_count(Count). 3162 3163% ?- Prop = 3164% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3165% sat(-Prop), 3166% sat_count(Count). 3167 3168zdd_numbervars(X, S):- get_key(varnum, N, S), 3169 numbervars(X, N, N0), 3170 set_key(varnum, N0, S). 3171 3172% ?- sat(a). 3173% ?- sat(a->(b->a)), sat(a->(b->a)), sat_count(C). 3174% ?- sat(A->(B->A)), sat(A->(B->A)), sat_count(C). 3175% ?- sat(a), sat(b), sat_count(C). 3176% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3177% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3178% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3179% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3180% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3181% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C). 3182 3183sat_count(C):- sat_fetch(S), 3184 get_key(root, X, S), 3185 ltr_card(X, C, S). 3186 3187% ?- sat(a), b_getval(sat_state, S), write(S), 3188% get_key(root, R, S), 3189% psa(R, S), get_key(atom_index, A, S), ltr_card(R, C, S). 3190sat_count(F, C):-sat(F), sat_count(C). 3191 3192% 3193print_root :- sat_fetch(S), 3194 get_key(root, R, S), 3195 psa(R, S). 3196% 3197sat_clear:- sat_fetch(S), 3198 close_state(S), 3199 b_setval(sat_state, []). 3200 3201% ?- time(forall(valid_formula(A), prove(A))). 3202% ?- time(forall(invalid_formula(A), prove(A))). 3203 3204% ?- heavy_valid_formula(H), prove(H). % Take time. Should be wrapped 3205% with call_with_time_limit/1. 3206 3207heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10) 3208<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3209<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10) 3210<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3211<=> p2) <=> p1) <=> p0)). 3212 3213% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y). 3214% ?- mk_left_assoc_term(=, 1, X), prove(X). 3215 3216% ?- ltr_zdd X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3217% ?- run(1, 100). 3218% ?- run(2, 100). 3219% ?- run(5, 100). 3220% ?- run(1-9, 100). 3221% ?- run(11, 100). 3222%@ 3223%@ Propositions: p(0) ... p(11). 3224%@ % 447,630,303 inferences, 47.959 CPU in 49.907 seconds (96% CPU, 9333572 Lips) 3225%@ true. 3226% ?- run(12, 360). 3227%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips) 3228% imac 3229% on M1 mbp pro 32 GB, timeout. 3230 3231% ?- mk_left_assoc_term(==, 1, F), prove(F). 3232 3233 3234run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3235 ( mk_left_assoc_term(==, K, F), 3236 format("~nPropositions: p(0) ... p(~w).~n", [K]), 3237 call_with_time_limit(T_limit, time(prove(F))))). 3238% run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3239% ( mk_left_assoc_term(==, K, F), 3240% format("~nPropositions: p(0) ... p(~w).~n", [K]), 3241% call_with_time_limit(T_limit, time(seq:seq_prove(F))))). 3242 3243% 3244run(N, T) :- run(N-N, T). 3245 3246% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X). 3247% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X). 3248 3249mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L), 3250 append(L, L, L2), 3251 reverse(L2, R), 3252 apply_left_assoc(Bop, R, Ex). 3253% 3254apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex). 3255% 3256apply_left_assoc(_, X, [], X):-!. 3257apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X], 3258 apply_left_assoc(Bop, V, Y, W). 3259 3260demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3261 3262demorgan1( ((a * b) -> -((-a + -b)))). 3263demorgan2(-((-a + -b)) -> (a * b)). 3264 3265% ?- forall(valid_formula(A), prove(A)). 3266% Valid formulae. 3267valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)). 3268valid_formula((-(-a) -> a) * (a -> -(-a))). % Double Negation 3269valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3270valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b). 3271valid_formula(a + -a). 3272valid_formula(((a -> b) -> a) -> a). % Peirce’s Law 3273valid_formula(-(-a)->a). 3274valid_formula(a -> a). 3275valid_formula(a -> (b -> a)). 3276valid_formula((a->b)->((b->c)->(a->c))). 3277valid_formula(a->((a->b)->b)). 3278valid_formula((a*(a->b))->b). 3279valid_formula((a->b)->(-b -> -a)). 3280valid_formula((a->b)->((b->c)->(a->c))). 3281valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)). 3282 3283% ?- forall(invalid_formula(A), prove(A)). 3284invalid_formula(a). 3285invalid_formula((a->b)->a). 3286invalid_formula((a->b)->(b->a)). 3287invalid_formula(a -> (b -> c)). 3288invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)). 3289invalid_formula( -((-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f))).
3294% ?- prove(a). 3295% ?- prove(a*b->a). 3296% ?- prove(a*a->a). 3297% ?- prove((-a) + a). 3298% ?- prove((-A) + A). 3299% ?- prove(A -> (p(B)->A)). 3300% ?- prove(-(a->a)). 3301% ?- prove(a->a). 3302% ?- prove((a->b)->(b->a)). 3303% ?- prove((a->b)->(a->b)). 3304% ?- prove((a->b)->(a)). 3305% ?- prove(a->(b->a)). 3306% ?- prove((-(a) * a)). 3307% ?- prove(-(-(a) * a)). 3308% ?- prove(a+ (-a)). 3309% ?- prove((-true)*true). 3310% ?- prove(true*true). 3311% ?- prove(true*false). 3312% ?- prove(false*true). 3313% ?- prove(false*false). 3314% ?- prove(true+true). 3315% ?- prove(true+false). 3316% ?- prove(false+true). 3317% ?- prove(false+false). 3318% ?- prove((a->b)*(b->c) -> (a->c)). 3319% ?- prove((a->b) -> ((b->c) -> (a->c))). 3320 3321prove(X):- 3322 ltr_open_state(S), 3323 ( prove(X, S) 3324 -> writeln('VALID') 3325 ; writeln('INVALID') 3326 ), 3327 close_state(S). 3328% 3329prove(X, S):- cnf(-X, CNF, S), 3330 get_key(atom_index, N, S), 3331 ( CNF = 0 -> N = 0 3332 ; CNF = 1 -> N > 0 3333 ; resolve(CNF, S) 3334 ).
3340% ?- ltr_open_state(S), ltr_pow([a,b,c], P, S), resolve(P, S), psa(P, S). 3341% ?- open_state(S), numlist(1, 10, L), ltr_pow(L, P, S), card(P, C, S). 3342% ?- open_state(S), numlist(1, 100, L), ltr_pow(L, P, S), card(P, C, S). 3343% ?- N = 100000, time((ltr_open_state(S), numlist(1, N, L), ltr_pow(L, P, S), 3344% resolve(P, S))). 3345 3346resolve(X, S):- zdd_has_1(X, S), !. % The empty clause found. 3347resolve(X, S):- X > 1, 3348 cofact(X, t(A, L, R), S), 3349 ( L = 0 -> fail % Pure literal rule. 3350 ; A = -(_) -> resolve(L, S) % Negative pure literal rule. 3351 ; ( cofact(L, t(B, U, V), S), % Pure literal rule. 3352 ( B = -(A) 3353 -> ltr_merge(V, R, M, S), % Resolution + Tautology rule. 3354 ltr_join(U, M, W, S), 3355 resolve(W, S) % Updated set of clauses. 3356 ; resolve(L, S) % Posituve pure literal rule. 3357 ) 3358 ) 3359 ). 3360 3361% ?- N=100, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3362% ?- N = 100, (zdd {numlist(1, N, L)}, ltr_pow(L, P), 3363% A << set(L), zdd_subtr(P, A, Q), card(Q, C), 3364% {writeln(C)}, resolve(Q)). % false 3365 3366% ?- N = 40, time((open_state(S), numlist(1, N, L), ltr_pow(L, P, S), 3367% zdd_eval(set(L), A, S), zdd_subtr(P, A, Q, S), card(Q, C, S), 3368% writeln(C), resolve(Q, S))). % false 3369% ?- N = 100000, time((ltr_open_state(S), numlist(1, N, _L), ltr_pow(_L, P, S), 3370% card(P, _C, S))), _C=:= 2^N. 3371 3372atom_index(X, S):- memo(atom_index(X)-Y, S), 3373 ( nonvar(Y) -> true 3374 ; get_key(atom_index, Y, S), 3375 memo(index_atom(Y)-X, S), 3376 Y0 is Y + 1, 3377 set_key(atom_index, Y0, S) 3378 ). 3379 3380 3381% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_zdd nnf_cnf(Y, Z), psa(Z)). 3382 3383boole_nnf(X, Y):- % numbervars_index(X, S), 3384 basic_boole(X, Z), 3385 once(neg_normal(Z, Y)). 3386 3387% ?- basic_boole(a, A). 3388% ?- basic_boole(@(a), A). 3389% ?- basic_boole(0, A). 3390% ?- basic_boole(1, A). 3391% ?- basic_boole(true, A). 3392% ?- basic_boole(a+b, A). 3393% ?- basic_boole(a+b+c, A). 3394% ?- basic_boole(-a + b + c, A). 3395% ?- basic_boole(a -> b -> c, A). 3396% ?- basic_boole((a -> b) -> c, A). 3397% ?- basic_boole(*[(a -> b), c], A). 3398% ?- basic_boole(*[(0 -> 1)->2], A). 3399 3400basic_boole(A, BoolConst):-atomic(A), 3401 boole_op(0, [], Fs, BoolConst), 3402 memberchk(A, Fs), 3403 !. 3404basic_boole(I, @(I)):- integer(I), !. 3405basic_boole(@(I), @(I)):-!. 3406basic_boole(*(L), F):-!, basic_boole_vector(L, *, F). 3407basic_boole(+(L), F):-!, basic_boole_vector(L, +, F). 3408basic_boole(X, Y):- X=..[F|Xs], 3409 length(Xs, N), 3410 boole_op(N, As, Fs, Y), 3411 memberchk(F, Fs), 3412 !, 3413 basic_boole_list(Xs, As). 3414basic_boole(X, @(X)). 3415 3416% 3417basic_boole_list([], []). 3418basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y), 3419 basic_boole_list(Xs, Ys). 3420% 3421basic_boole_vector([], +, false):-!. 3422basic_boole_vector([], *, true):-!. 3423basic_boole_vector([X|Xs], F, Y):- 3424 basic_boole(X, X0), 3425 Y=..[F, X0, Z], 3426 basic_boole_vector(Xs, F, Z). 3427 3428% Remark [2023/11/13]: 3429% Use of 0/1 as Boolean constants has been dropped. 3430% Any integer is now usable for a boolean variable, which 3431% may be useful or (nested) vectors of integers *[...], +[...]. 3432% 0/1 as boolean is error prone because ZDD must use 0/1 internally 3433% as basic constant similar, but not exactly the same, 3434% to true/flase. They are different. 3435% This decision was hard because 0/1 is traditionally useful 3436% as boolean constrants, but clear separation and simplicity 3437% were preferred. 3438 3439boole_op(0, [], [false, ff], false). % 0 for false dropped. 3440boole_op(0, [], [true, tt], true). % 1 for true dropped. 3441boole_op(1, [X], [-, ~, \+, not], -(X)). 3442boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y). 3443boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y). 3444boole_op(2, [X, Y], [->, imply], -X + Y). 3445boole_op(2, [X, Y], [<-], Y->X). 3446boole_op(2, [X, Y], [iff, ==, =, =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y). 3447boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)). % -(X==Y) = xor(X, Y) 3448boole_op(2, [X, Y], [nand], -(X) + (-Y)). 3449 3450 3451% ?- neg_normal(-(true + b), X). 3452% ?- neg_normal(-(a), X). 3453% ?- neg_normal(-(a), X). 3454% ?- neg_normal(-(a), X). 3455neg_normal(true, true). 3456neg_normal(false, false). 3457neg_normal(-(false), true). 3458neg_normal(-(true), false). 3459neg_normal(-(-X), Z) :- neg_normal(X, Z). 3460neg_normal(-(X+Y), Z) :- neg_normal(-X* -Y, Z). 3461neg_normal(-(X*Y), Z) :- neg_normal(-X+ -Y, Z). 3462neg_normal(-(X), -(Y)) :- neg_normal(X, Y). 3463neg_normal(X+Y, X0+Y0) :- neg_normal(X, X0), 3464 neg_normal(Y, Y0). 3465neg_normal(X*Y, X0*Y0) :- neg_normal(X, X0), 3466 neg_normal(Y, Y0). 3467neg_normal(@(X), @(X)):-!. 3468neg_normal(X, @(X)):-!. 3469 3470% ?- zdd((intern(-(a;b;c), X), boole_to_dnf(X, Z), sets(Z, U), extern(U, Y))). 3471%% extern(+X, -Y) is det. 3472% Convert an internal form X into an external one 3473% in order to unify Y with the result. 3474 3475extern(X, Y):-shift(extern(X, Y)). 3476% 3477extern(X, Y, S):-integer(X), !, 3478 ( X < 2 -> Y = X 3479 ; memo(index_atom(X)-Y, S) 3480 ). 3481extern(X, X, _):- atomic(X), !. 3482extern(X, Y, S):- X =.. [F|Xs], 3483 extern_list(Xs, Ys, S), 3484 Y =..[F|Ys]. 3485% 3486extern_list([], [], _). 3487extern_list([X|Xs], [Y|Ys], S):- extern(X, Y, S), 3488 extern_list(Xs, Ys, S). 3489 3490 /********************************************* 3491 * Cofact/insert/join/merge on literals * 3492 *********************************************/
t(A, L, R)
such that
A is the minimum literal in X w.r.t. specified literal compare predicate,
L = { U in X | not ( A in U ) },
R = { V \ {A} | V in X, A in V }.
If Y is given then
X = union of L and A*R = { unionf of U and {A} | U in R }.
Due to ltr_cofact/3 and itr_insert/4, it is guaranteed that
every clause is complentary-free ( no complementary pair ).3507ltr_cofact(Z, Y, S):- nonvar(Z), !, cofact(Z, Y, S). 3508ltr_cofact(Z, t(A, V, U), S):- U > 1, !, 3509 cofact(U, t(B, L, _), S), 3510 ( ltr_invert(A, B) 3511 -> ltr_cofact(Z, t(A, V, L), S) 3512 ; cofact(Z, t(A, V, U), S) 3513 ). 3514ltr_cofact(Z, T, S):- cofact(Z, T, S).
3523% PASS. 3524% ?- ltr_zdd cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S). 3525% ?- ltr_zdd dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S). 3526% ?- ltr_zdd ltr_insert(a, 1, X), sets(X, S). 3527% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), sets(Y, S). 3528% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), 3529% ltr_insert(-b, Y, Z), sets(Z, S). 3530% ?- ltr_zdd X<<set([a]), ltr_insert(b, X, Y), psa(Y). 3531% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3532% ?- ltr_zdd X<<set([b]), ltr_insert(a, X, Y), psa(Y). 3533% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3534% ?- ltr_zdd X<<set([-a]), ltr_insert(a, X, Y), psa(Y))). 3535% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y). 3536% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y). 3537% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y). 3538% ?- ltr_zdd X<<{[a]}, ltr_insert(a, X, Y), psa(Y). 3539% ?- ltr_zdd X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y). 3540% ?- ltr_zdd X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y). 3541% ?- ltr_zdd X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y). 3542% ?- ltr_zdd X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y). 3543% ?- ltr_zdd X<< dnf(a), ltr_insert(b, X, Y), psa(Y). 3544% ?- ltr_zdd X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y). 3545% ?- ltr_zdd X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y). 3546% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3547% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3548% ?- sat((x=\=y)*x*y). % false 3549% ?- sat((a * -a)). % false 3550% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y). 3551 3552% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y). 3553% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y). 3554% ?- ltr_zdd dnf((-a)*b, X), psa(X). 3555% ?- ltr_zdd cnf((-a)*b, X). 3556% ?- ltr_zdd cnf((a), X). 3557% ?- spy(cnf). 3558% ?- spy(atom_index). 3559% 3560ltr_insert(_, 0, 0, _):-!. 3561ltr_insert(A, 1, J, S):-!, zdd_singleton(A, J, S). 3562ltr_insert(A, I, J, S):- memo(ltr_insert(A,I)-J, S), 3563 ( nonvar(J) -> true 3564 ; cofact(I, t(B, L, R), S), 3565 zdd_compare(C, A, B, S), 3566 ( C = (<) -> 3567 ( complementary(A, B) -> 3568 cofact(J, t(A, 0, L), S) 3569 ; cofact(J, t(A, 0, I), S) 3570 ) 3571 ; C = (=) -> 3572 ( negative(A) -> 3573 ltr_join(L, R, K, S), 3574 cofact(J, t(A, 0, K), S) 3575 ; ltr_insert_aux(J, A, L, R, S) 3576 ) 3577 ; ( complementary(A, B) -> ltr_insert(A, L, J, S) 3578 ; ltr_insert(A, L, L0, S), 3579 ltr_insert(A, R, R0, S), 3580 cofact(J, t(B, L0, R0), S) 3581 ) 3582 ) 3583 ). 3584 3585% for suppressing use of cofact/3 and ltr_insert/4 3586ltr_insert_aux(J, A, L, R, S):- % A is positive. R has no -A. 3587 ( L < 2 -> cofact(J, t(A, L, R), S) 3588 ; cofact(L, t(B, L0, _), S), 3589 ( complementary(A, B)-> 3590 ltr_join(L0, R, K, S), 3591 cofact(J, t(A, 0, K), S) 3592 ; ltr_join(L, R, K, S), 3593 cofact(J, t(A, 0, K), S) 3594 ) 3595 ).
3601% 3602ltr_join(X, X, X, _):-!. % idemopotent law of logical disjunction (OR) 3603ltr_join(0, X, X, _):-!. 3604ltr_join(X, 0, X, _):-!. 3605ltr_join(1, _, 1, _):-!. 3606ltr_join(_, 1, 1, _):-!. 3607ltr_join(X, Y, Z, S):- 3608 ( X=<Y -> memo(ltr_join(X,Y)-Z, S) 3609 ; memo(ltr_join(Y,X)-Z, S) 3610 ), 3611 ( nonvar(Z) -> true %, write(.) 3612 ; cofact(X, t(A, L, R), S), 3613 cofact(Y, t(A0, L0, R0), S), 3614 zdd_compare(C, A, A0, S), 3615 ( C = (=) -> 3616 ltr_join(R, R0, U, S), 3617 ltr_join(L, L0, V, S), 3618 cofact(Z, t(A, V, U), S) 3619 ; C = (<) -> 3620 ltr_join(L, Y, U, S), 3621 cofact(Z, t(A, U, R), S) 3622 ; ltr_join(L0, X, U, S), 3623 cofact(Z, t(A0, U, R0), S) 3624 ) 3625 ).
3633ltr_merge(X, X, X, _):-!. % idempotent law of logical conjunction (AND). 3634ltr_merge(0, _, 0, _):-!. 3635ltr_merge(_, 0, 0, _):-!. 3636ltr_merge(1, X, X, _):-!. 3637ltr_merge(X, 1, X, _):-!. 3638ltr_merge(X, Y, Z, S):- 3639 ( X =< Y -> memo(ltr_merge(X,Y)-Z, S) 3640 ; memo(ltr_merge(Y,X)-Z, S) 3641 ), 3642 ( nonvar(Z) -> true 3643 ; cofact(Y, t(A, L, R), S), 3644 ltr_merge(X, R, U, S), 3645 ltr_merge(X, L, V, S), 3646 ltr_insert(A, U, U0, S), 3647 ltr_join(V, U0, Z, S) 3648 ). 3649 3650 /****************************************** 3651 * Auxiliary operations on literals * 3652 ******************************************/
3656complementary(-(A), A):-!. 3657complementary(A, -(A)). 3658% 3659negative(-(_)).
3668% ?- ltr_zdd ltr_pow([a], X), card(X, C), psa(X). 3669% ?- ltr_zdd ltr_pow([a, b], X), card(X, C), psa(X). 3670% ?- ltr_zdd {numlist(1, 100, L)}, ltr_pow(L, X), card(X, C). 3671ltr_pow([], 1, _). 3672ltr_pow([A|As], P, S):- ltr_pow(As, Q, S), 3673 ltr_insert(A, Q, R, S), 3674 ltr_insert(-A, Q, L, S), 3675 ltr_join(L, R, P, S).
3683% ?- ltr_zdd ltr_append([-b, a, -d, c], 1, X), psa(X). 3684% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3685% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3686% ?- ltr_zdd X<<dnf(a->a), ltr_card(X, C), psa(X). 3687ltr_append(X, Y, Z):- shift(ltr_append(X, Y, Z)). 3688% 3689ltr_append([], X, X, _). 3690ltr_append([A|As], X, Y, S):- ltr_append(As, X, X0, S), 3691 ltr_insert(A, X0, Y, S).
ltr_append(X, 1, Y, S)
.
?- ltr_zdd X<<(ltr_set([a])
+ltr_set([b])
), psa(X)
)).
?- ltr_zdd X<<(ltr_set([-a])
+ltr_set([b])
), psa(X)
)).
?- ltr_zdd X<<(ltr_set([-a])
+ltr_set([a])
), psa(X)
)).3699ltr_set(X, Y):- shift(ltr_set(X, Y)). 3700% 3701ltr_set(X, Y, S):- ltr_append(X, 1, Y, S).
3708% ?- zdd((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))). 3709% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))). 3710% ?- zdd((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))). 3711% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3712% ?- zdd((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3713 3714% ?- ltr_zdd X<<dnf(a), ltr_negate(X, Y), psa(Y). 3715% ?- ltr_zdd ltr_negate(0, Y), psa(Y). 3716% ?- ltr_zdd ltr_negate(1, Y), psa(Y). 3717 3718ltr_negate(X, Y):- shift(ltr_negate(X, Y)). 3719% 3720ltr_negate(X, Y, S):- ltr_complement(X, X0, S), 3721 ltr_choices(X0, Y, S).
3730% ?- zdd X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y). 3731% ?- zdd X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y). 3732% 3733ltr_complement(X, X, _):- X<2, !. 3734ltr_complement(I, Y, S):- memo(ltr_complement(I)-Y, S), 3735 ( nonvar(Y) -> true 3736 ; cofact(I, t(A, L, R), S), 3737 ltr_complement(L, L0, S), 3738 ltr_complement(R, R0, S), 3739 complementary(A, NA), 3740 ltr_insert(NA, R0, R1, S), 3741 ltr_join(L0, R1, Y, S) 3742 ). 3743 3744 /************************************ 3745 * Convert Boolean Form to DNF/CNF * 3746 ************************************/
3751% ?- boole_nnf(-(a+b), X). 3752% ?- zdd dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V). 3753% ?- zdd((dnf(-(a=:=b), X), psa(X))). 3754% ?- zdd((dnf((a=\=b), X), psa(X))). 3755% ?- zdd((dnf((0), X), psa(X))). 3756% ?- zdd((dnf(*[1,3,2,3], X), psa(X))). 3757% ?- zdd dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I). 3758% ?- zdd((dnf(*[@(1),3,2,3], X), psa(X))). 3759 3760dnf(X, Y, S):- zdd_numbervars(X, S), 3761 boole_nnf(X, Z), 3762 nnf_dnf(Z, Y, S).
3771% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y). 3772% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U). 3773% ?- ltr_zdd big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D). 3774 3775dnf_cnf(X, Y, S):- nonvar(X), !, ltr_choices(X, Y, S). 3776dnf_cnf(X, Y, S):- ltr_choices(Y, X, S). 3777% 3778cnf_dnf(X, Y, S):- dnf_cnf(X, Y, S). 3779 3780% ?- ltr_zdd X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y). 3781%@ * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug 3782% ?- ltr_zdd X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y). 3783% ?- ltr_zdd X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y). 3784% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3785% ?- ltr_zdd X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y). 3786% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3787% ?- ltr_zdd X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y). 3788% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3789% dnf_cnf(Z, Y), psa(X), psa(Y). 3790 3791% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3792% dnf_cnf(Z, Y), psa(X), psa(Y). 3793 3794% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3795% dnf_cnf(Z, Y). 3796 3797% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), 3798% dnf_cnf(Z, U). 3799 3800% ?- N=100, time((ltr_zdd big_normal_form(N, X), 3801% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3802%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips) 3803%@ N = 100, 3804%@ X = 39901, 3805%@ Y = D, D = 0, % <== CORRECT. 3806%@ C = 1267650600228229401496703205376 . 3807 3808% ?- N=1000, time((ltr_zdd big_normal_form(N, X), 3809% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3810%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips) 3811%@ N = 1000, 3812%@ X = 3999001, 3813%@ Y = D, D = 0, % <== CORRECT. 3814%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
3828ltr_choices(0, 1, _):-!. 3829ltr_choices(1, 0, _):-!. 3830ltr_choices(X, Y, S):- memo(ltr_choices(X)-Y, S), 3831 ( nonvar(Y)->true %, write(.) % many hits. 3832 ; cofact(X, t(A, L, R), S), 3833 ltr_choices(L, L0, S), 3834 ltr_choices(R, R0, S), 3835 cofact(R1, t(A, R0, 1), S), 3836 ltr_merge(L0, R1, Y, S) 3837 ).
3842nnf_dnf(false * _, 0, _):-!. 3843nnf_dnf(_ * false, 0, _):-!. 3844nnf_dnf(true * X, Y, S):-!, nnf_dnf(X, Y, S). 3845nnf_dnf(X * true, Y, S):-!, nnf_dnf(X, Y, S). 3846nnf_dnf(X * Y, Z, S):-!, memo(dnf(X*Y)-Z, S), 3847 ( nonvar(Z) -> true 3848 ; nnf_dnf(X, U, S), 3849 nnf_dnf(Y, V, S), 3850 ltr_merge(U, V, Z, S) 3851 ). 3852nnf_dnf(false + X, Y, S):-!, nnf_dnf(X, Y, S). 3853nnf_dnf(X + false, Y, S):-!, nnf_dnf(X, Y, S). 3854nnf_dnf(true + X, Y, S):-!, nnf_dnf(X, Z, S), 3855 ltr_join(1, Z, Y, S). 3856nnf_dnf(X + true, Y, S):-!, nnf_dnf(X, Z, S), 3857 ltr_join(1, Z, Y, S). 3858nnf_dnf(X + Y, Z, S):-!, memo(dnf(X+Y)-Z, S), 3859 ( nonvar(Z) -> true 3860 ; nnf_dnf(X, U, S), 3861 nnf_dnf(Y, V, S), 3862 ltr_join(U, V, Z, S) 3863 ). 3864nnf_dnf(@(X), I, S):-!, atom_index(X, S), 3865 zdd_singleton(X, I, S). 3866nnf_dnf(-(@(X)), I, S):- atom_index(X, S), 3867 zdd_singleton(-(X), I, S).
3873% ?- zdd((cnf(a, X), S<<sets(X))). 3874% ?- ltr_zdd((cnf(a*b, X), S<<sets(X))). 3875% ?- zdd((X<<cnf(-a), Y<<sets(X))). 3876% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 3877% ?- zdd((X<<cnf(+([a,b,c])), Y<<sets(X))). 3878% ?- zdd((X<<cnf(*([a,b,c])), Y<<sets(X))). 3879% ?- zdd((X<<dnf(+([a,b,c])), Y<<sets(X))). 3880% ?- zdd((X<<dnf(*([a,b,c])), Y<<sets(X))). 3881% ?- zdd((cnf(a, X), psa(X))). 3882% ?- zdd((cnf(-a, X), psa(X))). 3883% ?- zdd((cnf(a+b, X), psa(X))). 3884% ?- zdd((cnf(a+b+(-c), X), psa(X))). 3885% ?- zdd((cnf(-a * a, X), psa(X))). 3886% ?- zdd((cnf(a->a, X), psa(X))). 3887% ?- zdd((cnf(-a * a, X), psa(X))). 3888% ?- zdd((cnf( a + a, X), psa(X))). 3889% ?- zdd((cnf( A + A, X), psa(X))). 3890% ?- zdd((cnf(-(a*b), X), psa(X))). 3891% ?- zdd((cnf(*([a,b,c]), X), psa(X))). 3892% ?- zdd {N = 10, numlist(2, N, Ns)}, cnf(*(Ns), X), ltr_card(X, C, K). 3893% ?- ltr_zdd((dnf(a, X), psa(X))). 3894% ?- ltr_zdd((cnf(-(a->b), X), psa(X))). 3895% ?- ltr_zdd((cnf(a, X), psa(X))). 3896% ?- boole_nnf(-(*[0,1,2]), X). 3897% ?- ltr_zdd {mk_left_assoc_term(==, 1, F)}, cnf(F, X), psa(X). 3898cnf(X, Y, S):- zdd_numbervars(X, S), 3899 boole_nnf(X, Z), 3900 nnf_cnf(Z, Y, S). 3901% 3902nnf_cnf(true, 1, _):-!. 3903nnf_cnf(false, 0, _):-!. 3904nnf_cnf(false * _, 0, _):-!. 3905nnf_cnf(_ * false, 0, _):-!. 3906nnf_cnf(true * X, Y, S):-!, nnf_cnf(X, Y, S). 3907nnf_cnf(X * true, Y, S):-!, nnf_cnf(X, Y, S). 3908nnf_cnf(X * X, Y, S):-!, nnf_cnf(X, Y, S). 3909nnf_cnf(X * Y, Z, S):-!, memo(cnf(X*Y)-Z, S), 3910 ( nonvar(Z)->true %, write(.) % many hits. 3911 ; nnf_cnf(X, U, S), 3912 nnf_cnf(Y, V, S), 3913 ltr_join(U, V, Z, S) 3914 ). 3915nnf_cnf(false + X, Y, S):-!, nnf_cnf(X, Y, S). 3916nnf_cnf(X + false, Y, S):-!, nnf_cnf(X, Y, S). 3917nnf_cnf(true + _, 1, _):-!. 3918nnf_cnf(_ + true, 1, _):-!. 3919nnf_cnf(X + X, Y, S):-!, nnf_cnf(X, Y, S). 3920nnf_cnf(X + Y, Z, S):-!, memo(cnf(X+Y)-Z, S), 3921 ( nonvar(Z)->true %, write(+) % many hits. 3922 ; nnf_cnf(X, U, S), 3923 nnf_cnf(Y, V, S), 3924 ltr_merge(U, V, Z, S) 3925 ). 3926nnf_cnf(@(X), I, S):-!, atom_index(X, S), 3927 zdd_singleton(X, I, S). 3928nnf_cnf(-(@(X)), I, S):- atom_index(X, S), 3929 zdd_singleton(-(X), I, S). 3930 3931 3932 /***************************************************** 3933 * ltr_card/[3,4] Counting solutions of a DNF. * 3934 *****************************************************/ 3935 3936 3937% ?- sat_count_by_collect_atoms(a, C). 3938% ?- sat_count_by_collect_atoms(a+b, C). 3939% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C). 3940% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 3941sat_count_by_collect_atoms(X, C):- sat_fetch(S), 3942 dnf(X, Y, S), 3943 sat_count_by_collect_atoms(Y, C, S), 3944 sat_close. 3945% 3946sat_count_by_collect_atoms(X, C, S):- 3947 zdd_boole_atoms(Us, S), 3948 zdd_sort(Us, Vs, S), 3949 expand_dnf(Vs, X, Y, S), 3950 card(Y, C, S). 3951 3952% ?- ltr_zdd X<<dnf(b+a), zdd_boole_atoms(Us). 3953zdd_boole_atoms(Us, S):- 3954 ( get_key(atom_index, N, S) -> 3955 collect_boole_atoms(0, N, Us, S) 3956 ; Us = [] 3957 ). 3958 3959% 3960collect_boole_atoms(I, N, [], _):- I>=N, !. 3961collect_boole_atoms(I, N, [A|U], S):- memo(index_atom(I)-A, S), 3962 J is I+1, 3963 collect_boole_atoms(J, N, U, S). 3964 3965 /****************************** 3966 * find_counter_example * 3967 ******************************/
3971% ?- findall_counter_examples(a, X, S), psa(X, S). 3972% ?- findall_counter_examples((a->b)->a, X, S), psa(X, S). 3973% ?- findall_counter_examples((a->b)->(b->a), X, S), psa(X, S). 3974% ?- findall_counter_examples(a->b, X, S), psa(X, S). 3975% ?- findall_counter_examples((a->b)->(b->a), X, S), psa(X, S). 3976% ?- findall_counter_examples(a->b, Out, S), psa(Out,S). 3977findall_counter_examples(In, Out, S):- 3978 ltr_open_state(S), 3979 dnf(In, InZ, S), 3980 zdd_boole_atoms(Us, S), 3981 zdd_sort(Us, Vs, S), 3982 expand_prefix_dnf(Vs, 1, All, S), 3983 expand_dnf(Vs, InZ, Y, S), 3984 zdd_subtr(All, Y, Out, S).
open_state(S)
and set ltr_compare/3 in S as the compare predicate.
3989ltr_open_state(S):- open_state(S),
3990 set_compare(ltr_compare, S),
3991 set_key(varnum, 0, S),
3992 set_key(atom_index,0, S).
3998% ?- ltr_zdd X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 3999% ?- ltr_zdd X<< dnf(a), psa(X), ltr_card(X, C). 4000% ?- ltr_zdd X<< dnf(a->a), ltr_card(X, C). 4001% ?- ltr_zdd X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4002% ?- ltr_zdd X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C). 4003% ?- findall(p(J), between(1, 100, J), Ps), 4004% time(ltr_zdd((X<< dnf(+Ps), ltr_card(X, C)))). 4005% ?- N = 1000, findall(p(J), between(1, N, J), Ps), 4006% time((ltr_zdd X<< dnf(+Ps),ltr_card(X, C))), 4007% C =:= 2^1000 - 1. 4008 4009ltr_card(In, Out, S):- 4010 zdd_boole_atoms(Us, S), 4011 zdd_sort(Us, Vs, S), 4012 expand_dnf(Vs, In, Y, S), 4013 card(Y, Out, S). 4014 4015% ?- ltr_var(-(5), X). 4016ltr_var(-(V), V):-!. 4017ltr_var(V, V).
4024% ?- ltr_zdd((X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y))). 4025% ?- ltr_zdd((X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), card(Y, C))). 4026% ?- ltr_zdd((X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C))). 4027% ?- ltr_zdd((X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y))). 4028% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 4029% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 4030% ?- ltr_zdd((X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 4031 4032expand_dnf([], X, X, _):-!. 4033expand_dnf(_, 0, 0, _):-!. 4034expand_dnf(Vs, 1, Y, S):-!, expand_prefix_dnf(Vs, 1, Y, S). 4035expand_dnf(Vs, X, Y, S):- memo(expand_dnf(X,Vs)-Y, S), 4036 ( nonvar(Y) -> true %, write(.) % Many hits. 4037 ; cofact(X, t(A, L, R), S), 4038 ltr_var(A, K), 4039 divide_ord_list(Vs, K, [], Us, Ws), 4040 expand_dnf(Us, R, R0, S), 4041 ltr_insert(A, R0, R1, S), 4042 expand_left_dnf(K, Us, L, L0, S), 4043 ltr_join(L0, R1, X0, S), 4044 expand_prefix_dnf(Ws, X0, Y, S) 4045 ).
divide_ord_list([a,b,c,d,e], c, [u], T, W)
.
?- divide_ord_list([a,b,c, d], e, [], X, Y)
. % false4053divide_ord_list([V|Vs], V, Us, Vs, Us):-!. 4054divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U), 4055 divide_ord_list(Vs, U, [V|Us], Ws, Ps).
4062% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))). 4063expand_prefix_dnf(Vs, X, Y, S):- zdd_sort(Vs, OrdVs, S), 4064 expand_ord_prefix_dnf(OrdVs, X, Y, S). 4065 4066% 4067expand_ord_prefix_dnf([], X, X, _):-!. 4068expand_ord_prefix_dnf([V|Vs], X, Y, S):- 4069 expand_ord_prefix_dnf(Vs, X, X0, S), 4070 ltr_insert(V, X0, X1, S), 4071 ltr_insert(-V, X0, X2, S), 4072 ltr_join(X1, X2, Y, S).
4082expand_left_dnf(_, _, 0, 0, _):-!. 4083expand_left_dnf(K, Us, 1, Y, S):-!, expand_prefix_dnf([K|Us], 1, Y, S). 4084expand_left_dnf(K, Us, X, Y, S):- cofact(X, t(A, L, R), S), 4085 ltr_var(A, J), 4086 ( K = J -> 4087 expand_dnf(Us, R, R0, S), 4088 ltr_insert(A, R0, R1, S) 4089 ; divide_ord_list([K|Us], J, [], Vs, Ws), 4090 expand_dnf(Vs, R, R0, S), 4091 ltr_insert(A, R0, Q, S), 4092 expand_prefix_dnf(Ws, Q, R1, S) 4093 ), 4094 expand_dnf([K|Us], L, L0, S), 4095 ltr_join(L0, R1, Y, S). 4096 4097 /******************************* 4098 * Filter on cardinality * 4099 *******************************/
4105% ?- zdd((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))). 4106card_filter_gte(0, X, X, _):- !. % gte: greater than or equal 4107card_filter_gte(1, X, Y, S):- !, zdd_subtr(X, 1, Y, S). 4108card_filter_gte(_, X, 0, _):- X<2, !. 4109card_filter_gte(N, X, Y, S):- memo(filter_gte(N,X)-Y, S), 4110 ( nonvar(Y) -> true % many hits. 4111 ; cofact(X, t(A, L, R), S), 4112 N0 is N - 1, 4113 card_filter_gte(N, L, L0, S), 4114 card_filter_gte(N0, R, R0, S), 4115 cofact(Y, t(A, L0, R0), S) 4116 ).
4122% ?- zdd((X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y))). 4123card_filter_lte(0, X, Y, S):- % lte: less than or equal 4124 ( zdd_has_1(X, S) -> Y = 1 4125 ; Y = 0 4126 ). 4127card_filter_lte(_, X, X, _):- X<2, !. 4128card_filter_lte(N, X, Y, S):- memo(filter_lte(N,X)-Y, S), 4129 ( nonvar(Y) -> true % many hits. 4130 ; cofact(X, t(A, L, R), S), 4131 N0 is N - 1, 4132 card_filter_lte(N, L, L0, S), 4133 card_filter_lte(N0, R, R0, S), 4134 cofact(Y, t(A, L0, R0), S) 4135 ).
4140% ?- time(( N = 100, numlist(1, N, Ns), zdd((X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))))). 4141card_filter_between(I, J, X, Y, S):- 4142 card_filter_gte(I, X, Z, S), 4143 card_filter_lte(J, Z, Y, S). 4144 4145% ?- time(( N = 100, numlist(1, N, Ns), zdd((X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))))). 4146card_filter_between_by_meet(I, J, X, Y, S):- 4147 card_filter_gte(I, X, Z, S), 4148 card_filter_lte(J, X, U, S), 4149 zdd_meet(Z, U, Y, S). 4150 4151 4152 /********************************************************* 4153 * Solve boolean equations and verify the solution * 4154 *********************************************************/ 4155% Recovered [2023/11/14] 4156%! dnf_subst(+V, +T, +X, -Y, +S) is det. 4157% Y is the ZDD obtained by substituting each 4158% occurrence of atom V in X with T. 4159 4160% ?-ltr_zdd X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4161% ?-ltr_zdd X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4162% ?-ltr_zdd X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4163 4164dnf_subst(_, _, X, X, _):- X < 2, !. 4165dnf_subst(V, D, X, Y, S):- 4166 cofact(X, t(A, L, R), S), 4167 dnf_subst(V, D, L, L0, S), 4168 once( A = -(U); U = A ), 4169 ltr_compare(C, V, U), 4170 ( C = (<) -> Y = X 4171 ; ( C = (=) -> 4172 ( A = (-V) -> 4173 ltr_negate(D, D0, S), 4174 ltr_merge(D0, R, R0, S) 4175 ; A = V -> 4176 ltr_merge(D, R, R0, S) 4177 ) 4178 ; dnf_subst(V, D, R, R1, S), 4179 ltr_insert(A, R1, R0, S) 4180 ), 4181 ltr_join(L0, R0, Y, S) 4182 ).
4190% exists x s.t. C0*(L,-x) + C1*x = 1 4191% if and only if 4192% C0 + C1 = 1 satisfiable 4193% x = a*C1 + (-C0). 4194 4195% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S). 4196% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S). 4197% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S). 4198 4199solve_boole_with_check(Exp, Xs, Ps, S):- ltr_open_state(S), 4200 dnf(Exp, E, S), 4201 solve_boolean_equations(E, Xs, Ps, Sols, S), 4202 eliminate_variables(E, Sols, Cond, S), 4203 !, 4204 dnf_valid_check(Cond, S). 4205 4206% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), 4207% solutions_to_sets(Sols, Sols0). 4208% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0). 4209 4210solve_boolean_equations(_, [], _, [], _):-!. 4211solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols], S):- 4212 solve_boolean_equations_basic(E, X, A, Sol0, E0, S), 4213 solve_boolean_equations(E0, Xs, As, Sols, S), 4214 dnf_subst_list(Sols, Sol0, Sol, S). 4215 4216% ?- ltr_zdd E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond). 4217solve_boolean_equations_basic(E, X, A, Sol, Cond, S):- 4218 dnf_subst(X, 1, E, C1, S), 4219 dnf_subst(X, 0, E, C0, S), 4220 ltr_join(C0, C0, Cond, S), 4221 ltr_negate(C0, NC0, S), 4222 ltr_insert(A, C1, AC1, S), 4223 ltr_join(NC0, AC1, Sol, S). 4224% 4225dnf_subst_list([], E, E, _). 4226dnf_subst_list([X=A|Eqs], E, F, S):- 4227 dnf_subst(X, A, E, E0, S), 4228 dnf_subst_list(Eqs, E0, F, S). 4229% 4230solutions_to_sets([], [], _). 4231solutions_to_sets([X = E|Sols], [X = E0|Sols0], S):- 4232 sets(E, E0, S), 4233 solutions_to_sets(Sols, Sols0, S). 4234 4235% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check). 4236 4237% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check), psa(Cond), dnf_valid_check(Cond). 4238 4239% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), solutions_to_sets(Sols, Sols0), eliminate_variables(E, Sols, Cond), sets(Cond, Check), psa(Cond). 4240 4241eliminate_variables(Exp, Eqns, Cond, S):- 4242 apply_subst_list(Eqns, Exp, Cond, S). 4243% 4244apply_subst_list([], E, E, _). 4245apply_subst_list([X=U|Eqns], E, E0, S):- 4246 dnf_subst(X, U, E, E1, S), 4247 dnf_subst_list(Eqns, E1, E0, S). 4248% 4249dnf_valid_check(X, S):- 4250 ltr_atoms_by_scan(X, As, S), 4251 ltr_sort(As, Bs), 4252 expand_dnf(Bs, X, Y, S), 4253 card(Y, C, S), 4254 length(Bs, N), 4255 ( C =:= (1<< N) -> writeln('Solved and Verified.') 4256 ; writeln('Solved but NOT verified.') 4257 ). 4258 4259% ?- ltr_zdd X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), {sort(As, Bs)}. 4260ltr_atoms_by_scan(X, [], _):- X<2, !. 4261ltr_atoms_by_scan(X, P, S):- memo(ltr_atoms(X)-P, S), 4262 ( nonvar(P) -> true 4263 ; cofact(X, t(A, L, R), S), 4264 ltr_atoms_by_scan(L, Al, S), 4265 ltr_atoms_by_scan(R, Ar, S), 4266 ltr_var(A, A0), 4267 union([A0|Al], Ar, P) 4268 ). 4269 4270 /********************************* 4271 * operations on reducible zdd * 4272 *********************************/ 4273 4274% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y). 4275% ?- zdd bdd_append([x, a, y, b], 0, Y), psa(Y). 4276% ?- zdd bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z). 4277 4278bdd_append([], Z, Z, _). 4279bdd_append([X|Y], Z, U, S):- 4280 bdd_append(Y, Z, Z0, S), 4281 cofact(U, t(X, 0, Z0), S). 4282 4283% ?- zdd bdd_list([b, b], Y), zdd_append([b,b], Y, Z), psa(Z). 4284% ?- zdd bdd_list([b, b], Y), bdd_list(X, Y). 4285bdd_list(List, X, S):- var(X), !, bdd_append(List, 1, X, S). 4286bdd_list(List, X, S):- get_bdd_list(X, List, S). 4287 4288% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L). 4289% ?- zdd bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L). 4290get_bdd_list(1, [], _):-!. 4291get_bdd_list(X, [A|As], S):- X>1, zdd_cons(X, A, X0, S), 4292 get_bdd_list(X0, As, S). 4293 4294% ?- zdd bdd_append([a,a,b,b], 1, X), 4295% bdd_append([1,1,2,2], 1, Y), 4296% bdd_zip(X, Y, Z), psa(Z). 4297bdd_zip(0, _, 0, _):-!. 4298bdd_zip(_, 0, 0, _):-!. 4299bdd_zip(1, _, 1, _):-!. 4300bdd_zip(_, 1, 1, _):-!. 4301bdd_zip(X, Y, Z, S):- zdd_cons(X, A, X0, S), 4302 zdd_cons(Y, B, Y0, S), 4303 bdd_zip(X0, Y0, Z0, S), 4304 zdd_cons(Z, A-B, Z0, S). 4305 4306% ?- zdd bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y). 4307bdd_normal(X, X, _):- X<2, !. 4308bdd_normal(X, Y, S):- cofact(X, t(A, L, R), S), 4309 bdd_normal(L, L0, S), 4310 bdd_normal(R, R1, S), 4311 zdd_insert(A, R1, R0, S), 4312 zdd_join(L0, R0, Y, S). 4313 4314% ?- zdd bdd_append([a,b,a,b], 1, X), 4315% bdd_append([a,b, c, a,b, c], 1, Y), 4316% bdd_append([b, a, b, a, a,b ], 1, Z), 4317% bdd_list_normal([X, Y, Z], R), psa(R). 4318 4319bdd_list_normal([], 0, _). 4320bdd_list_normal([A|As], R, S):- bdd_list_normal(As, R0, S), 4321 bdd_normal(A, A0, S), 4322 zdd_join(A0, R0, R, S). 4323 4324% 4325bdd_insert(_, 0, 0, _):-!. 4326bdd_insert(A, 1, X, S):-!, zdd_singleton(A, X, S). 4327bdd_insert(A, X, Y, S):- cofact(X, t(B, L, R), S), 4328 bdd_insert(A, L, L0, S), 4329 bdd_append([A,B], R, R0, S), 4330 zdd_join(L0, R0, Y, S).
4339% ?- zdd bdd_list_raise([], 0, X). 4340% ?- zdd bdd_list_raise([a], 0, X). 4341% ?- zdd bdd_list_raise([a], 1, X), psa(X). 4342% ?- zdd bdd_list_raise([a,b], 1, X), psa(X). 4343% ?- zdd {N = 1, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X), card(X, C). 4344% ?- zdd {N = 15, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X),card(X, C). 4345 4346bdd_list_raise(_, 0, 1, _):-!. 4347bdd_list_raise(L, N, X, S):- N0 is N-1, 4348 bdd_list_raise(L, N0, X0, S), 4349 bdd_map_insert(L, X0, X, S). 4350% 4351bdd_map_insert([], _, 0, _). 4352bdd_map_insert([A|As], X, Y, S):- 4353 bdd_insert(A, X, X0, S), 4354 bdd_map_insert(As, X, Y0, S), 4355 zdd_join(X0, Y0, Y, S). 4356 4357% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert, 4358% also work for bddered zdd. 4359 4360% ?- zdd X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U), 4361% psa(X), psa(Y), psa(Z), psa(U). 4362% ?- zdd X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z), 4363% psa(Z, S), card(Z, C). 4364% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4365% card(Z, C). 4366% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z), 4367% card(Z, C), card(X, D). 4368 4369bdd_merge(0, _, 0, _):-!. 4370bdd_merge(_, 0, 0, _):-!. 4371bdd_merge(1, X, X, _):-!. 4372bdd_merge(X, 1, X, _):-!. 4373bdd_merge(X, Y, Z, S):- memo(bdd_merge(X, Y)-Z, S), 4374 ( nonvar(Z) -> true % , write(.) % So so frequently hits. 4375 ; cofact(X, t(A, L, R), S), 4376 bdd_merge(L, Y, L0, S), 4377 bdd_merge(R, Y, R1, S), 4378 zdd_cons(R0, A, R1, S), 4379 zdd_join(L0, R0, Z, S) 4380 ). 4381 4382 /**************n*************************** 4383 * Interleave bddered atoms in BDD * 4384 ******************************************/
length(M)
= length(A)
+length(B)
, and both A and B are sublists of M.
A list U is a sublist of a list V if U is a subsequence of V,
provided that a list is viewed as a sequence.4393% ?- zdd X<< +[*[a,b], *[x,y]], Y<< +[*[1]], 4394% bdd_interleave(X, Y, Z), psa(Z). 4395% ?- zdd X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z). 4396% ?- zdd X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z). 4397 4398bdd_interleave(0, _, 0, _):-!. 4399bdd_interleave(_, 0, 0, _):-!. 4400bdd_interleave(1, X, X, _):-!. 4401bdd_interleave(X, 1, X, _):-!. 4402bdd_interleave(X, Y, Z, S):- % memo is useless here. 4403 cofact(Y, t(B, L, R), S), 4404 ( L < 2 -> L0 = 0 4405 ; bdd_interleave(X, L, L0, S) 4406 ), 4407 bdd_interleave(X, B, R, R0, S), 4408 zdd_join(L0, R0, Z, S). 4409% 4410bdd_interleave(0, _, _, 0, _):-!. 4411bdd_interleave(1, B, Y, Z, S):-!, cofact(Z, t(B, 0, Y), S). 4412bdd_interleave(X, B, Y, Z, S):- memo(merge(X, Y, B)-Z, S), 4413 ( nonvar(Z) -> true % , write(+) % many hits. 4414 ; cofact(X, t(A, L, R), S), 4415 ( L < 2 -> L0 = 0 4416 ; bdd_interleave(L, B, Y, L0, S) 4417 ), 4418 bdd_interleave(A, R, B, Y, R0, S), 4419 zdd_join(L0, R0, Z, S) 4420 ). 4421% 4422bdd_interleave(A, X, B, Y, Z, S):- % memo is useless here. 4423 bdd_interleave(X, B, Y, U, S), 4424 cofact(Z0, t(A, 0, U), S), 4425 bdd_interleave(Y, A, X, V, S), 4426 cofact(Z1, t(B, 0, V), S), 4427 zdd_join(Z0, Z1, Z, S).
mono(A-B)
, epi(A-B)
, fun(A-B)
,
and operator * (merge), & (interleave).
F is the function space in ZDD built from these parts.
mono(A-B)
means function restricted to A is one-to-one mappings to B.
epi(A-B)
one-to-onto, and fun(A-B)
mapping.4436% ?- zdd bdd_funs(mono([1,2]-[a,b])*mono([3,4]-[c,d]), X), psa(X). 4437% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), psa(X). 4438% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), 4439% zdd_normalize(X, Y), psa(Y). 4440 4441bdd_funs(A*B, F, S):-!, bdd_funs(A, A0, S), 4442 bdd_funs(B, B0, S), 4443 bdd_merge(A0, B0, F, S). 4444bdd_funs(A&B, F, S):-!, bdd_funs(A, A0, S), 4445 bdd_funs(B, B0, S), 4446 bdd_interleave(A0, B0, F, S). 4447bdd_funs(A, F, S):- fun_block(A, F, S). 4448 4449 /************** 4450 * misc * 4451 **************/
4456% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), zdd_flatten(X, Y), psa(Y)). 4457zdd_flatten(X, 0, _):- X<2, !. 4458zdd_flatten(X, Y, S):- memo(flatten(X)-Y, S), 4459 ( nonvar(Y) -> true % Many hits. 4460 ; cofact(X, t(A, L, R), S), 4461 zdd_flatten(L, L0, S), 4462 zdd_flatten(R, R0, S), 4463 zdd_join(L0, R0, Y0, S), 4464 cofact(Y, t(A, Y0, 1), S) 4465 )