1:- module(zmod, 2 [ (<<)/2, zdd/0, zdd_eval/2, zdd_eval/3, ltr/0 3 , card/2 4 , ltr_join/3, ltr_join_list/2, ltr_join_list/3 5 , ltr_merge/3, ltr_card/2 6 , card_filter_gte/3, card_filter_lte/3 7 , card_filter_between/4 8 , max_length/2 9 , sat/0, sat/1, sat_count/1 10 , set_at/2 11 , obj_id/2 12 , dnf/2, cnf/2, nnf_dnf/2, nnf_cnf/2 13 , all_fun/3 14 , all_mono/3, all_epi/3, merge_funs/2 15 , bdd_list/2, bdd_list_raise/3, bdd_append/3, bdd_interleave/3 16 , zdd_div_by_list/3 17 , opp_compare/3 18 , bdd_sort_append/3, bdd_append/3 19 , zdd_insert/3, zdd_insert/4, zdd_insert_atoms/3 20 , bdd_cons/3 21 , l_cons/3 22 , zdd_insert_atoms/3 23 , zdd_ord_insert/3, zdd_reorder/3 24 , zdd_has_1/1 25 , zdd_memberchk/2 26 , zdd_family/2 27 , zdd_subfamily/2 28 , zdd_join/3, zdd_join_1/2, zdd_join_list/2, zdd_singleton/2 29 , zdd_merge/3, zdd_disjoint_merge/3 30 , zdd_merge_list/3 31 , zdd_meet/3 32 , zdd_subtr/3, zdd_subtr_1/2, zdd_xor/3 33 , zdd_div/3, zdd_mod/3, zdd_divmod/4, zdd_div_div/4 34 , zdd_divisible_by_list/3 35 , zdd_power/2, zdd_ord_power/3 36 , zdd_rand_path/1, zdd_rand_path/2, zdd_rand_path/3 37 , ltr_meet_filter/3, ltr_join_filter/3 38 , get_key/2, atom_index/1 39 , set_key/2, update_key/3 40 , set_pred/2, zdd_compare/3 41 , zdd_sort/2 42 , open_key/2, close_key/1 43 , set_compare/1, get_compare/1 44 , map_zdd/3, zdd_find/3 45 , psa/0, psa/1, psa/2, mp/2 46 , sets/2, ppoly/1, poly_term/2 47 , eqns/2 48 , zdd_list/2 49 , significant_length/3 50 , charlist/2, charlist/3, atomlist/2 51 , op(900, xfx, <<) 52 ]). 53 54% ?- zdd. 55% ?- N = 10000, numlist(1, N, Ns), time(((X<<pow(Ns), card(X, _C)))), _C=:=2^N. 56% :- doc_server(7000). 57% :- use_module(library(pldoc/doc_library)). 58% :- doc_load_library. 59% :- doc_browser. 60 61:- use_module(library(apply)). 62:- use_module(library(apply_macros)). 63:- use_module(library(clpfd)). 64:- use_module(library(statistics)). 65:- use_module(zdd('zdd-array')). 66:- use_module(util(math)). 67:- use_module(util(meta2)). 68:- use_module(pac(basic)). 69:- use_module(pac(meta)). 70:- use_module(util(misc)). 71:- use_module(pac('expand-pac')). % For the kind block. 72:- use_module(pac(op)). 73:- use_module(zdd('frontier-vector')). 74:- set_prolog_flag(stack_limit, 10_200_147_483_648). 75:- nb_setval(default_zdd_mode, zdd). 76 77% :- initialization(activate_zdd). % choices: zdd/ltr/sat 78 79activate_zdd:- b_getval(default_zdd_mode, Mode), 80 call(Mode), 81 format( 82 "\n%\s~w mode activated. 83%\sCurrently available modes: zdd/ltr/sat\n", [Mode]). 84 85attr_unify_hook(V, Y):- 86 ( get_attr(Y, zdd, A) 87 -> zdd_unify(V, A) 88 ; zdd_unify(V, Y) 89 ). 90 91 :- op(800, xfy, &). 92 :- op(820, fy, \). % NOT 93 :- op(830, xfy, /\). % AND 94 :- op(840, xfy, \/). % OR 95 :- op(860, xfy, ~). % equivalence 96 :- op(860, xfy, #). % exor 97 :- op(860, xfy, <->). % equivalence 98 :- op(860, xfy, <=> ). % equivalence 99 :- op(870, yfx, <-). 100 101% for pac query. 102term_expansion --> pac:expand_pac. 103 104% ?- zdd. 105% ?- numlist(1, 2, Ns), Y<<pow(Ns), card(Y, C). 106% ?- set_memo(a-1), set_memo(a-2), memo(a-V). 107% ?- X<<{[1,1]}, psa(X). 108% ?- X<< *[ *a, *a, *b,*c], psa(X). 109% ?- set_key(root, hello), get_key(root, R). 110% ?- all_fun([a],[b], F), psa(F). 111% ?- all_fun([],[b], F), psa(F) 112% ?- all_fun([a],[], F), psa(F) 113% ?- all_fun([a,b],[c,d], F), psa(F), card(F, C). 114% ?- N = 20, numlist(1, N, A), raise_list(A, 2, A2), all_fun(A2, A, F), card(F, C). 115% ?- time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 116% all_fun(Ns, Ms, F), card(F, C))). 117 118% Cardinality # of Y^X = { f | f: X-> Y }. 119% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 120 121% ?- I=1, J=1, K=1, L=1, 122% numlist(1, I, X), numlist(1, K, Y), 123% raise_list(X, J, Xj), 124% raise_list(Y, L, Yl), 125% time(call_with_time_limit(200, (all_fun(Xj, Yl, F), card(F, C)))), 126% C =:= (K^L)^(I^J), 127% significant_length(C, Keta, 10). 128 129% ?- I=3, J=5, K=3, L=5, 130% numlist(1, I, X), numlist(1, K, Y), 131% raise_list(X, J, Xj), 132% raise_list(Y, L, Yl), 133% time( ( call_with_time_limit(200, ( 134% (all_fun(Xj, Yl, F), card(F, C)))))), 135% C =:= (K^L)^(I^J), 136% significant_length(C, Keta, 10). 137%@ % 477,828,435 inferences, 56.259 CPU in 58.472 seconds (96% CPU, 8493400 Lips) 138%@ F = 7204222, 139%@ Keta = 580. 140 141% ?- significant_length(020, X, 10). 142significant_length(0, 0, _):-!. 143significant_length(X, 1, Radix):- X < Radix, !. 144significant_length(X, L, Radix):- Y is X // Radix, 145 significant_length(Y, L0, Radix), 146 L is L0+1. 147 148% 149zdd_atom(X):- get_key(is_atom, Pred), !, call(Pred, X). 150zdd_atom(X):- (atomic(X); dvar(X)), !.
obj_id([a,b,c], Id), obj_id(Obj, Id).155obj_id(X, Id):- cofact(Id, t(X, 0, 1)). 156% 157hyphen(X, Y, X-Y). 158comma(X, Y, (X,Y)). 159equality(X, Y, (X=Y)). 160dvar('$VAR'(_)). 161 162 /***************************************** 163 * all_fun/all_mono/all_epi in ZDD * 164 *****************************************/
168% ?- all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F). 169% ?- all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C). 170% ?- N = 100, numlist(1, N, Ns), all_fun(Ns, Ns, F)^, card(F, C). 171% ?- numlist(1, 5, Ns), numlist(6, 10, Ms), 172% all_fun(Ns, Ns, F), 173% all_fun(Ms, Ms, G), 174% zdd_merge(F, G, H), 175% card(H, C), 176% C =:= 5^5 * 5^5. 177 178all_fun(D, R, F):- zdd_sort(D, D0), 179 zdd_sort(R, R0), 180 length(D0, I), 181 length(R0, J), 182 ( I > 0, J = 0 -> F = 0 183 ; bdd_sort_append(D0, 1, D1), 184 findall_fun(D1, R0, F) 185 ). 186% 187findall_fun(X, _, X):- X < 2, !. 188findall_fun(X, Rng, Y):- memo(findall_fun(X)-Y), 189 ( nonvar(Y) -> true % , write(.) % many hits. 190 ; cofact(X, t(A, L, R)), 191 findall_fun(L, Rng, L0), 192 findall_fun(R, Rng, R1), 193 join_for_alt_val(A, Rng, R1, 0, R0), 194 zdd_join(L0, R0, Y) 195 ). 196% 197join_for_alt_val(_, [], _, V, V). 198join_for_alt_val(A, [B|Bs], F, F0, F1):- 199 bdd_cons(F2, A-B, F), 200 zdd_join(F0, F2, F3), 201 join_for_alt_val(A, Bs, F, F3, F1).
206% ?- zdd all_mono([1],[a], Is), psa(Is). 207% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is). 208% ?- zdd all_mono([1,2],[a,b,c], Is), psa(Is). 209% ?- zdd all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C). 210% ?- zdd all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C). 211% ?- time((numlist(1, 10, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)), factorial(10, C))). 212% ?- time((numlist(1, 12, Ns), (zdd all_mono(Ns, Ns, F), card(F, C)))). 213% ?- N =10, numlist(1, N, Ns), time((zdd all_mono(Ns, Ns, F), card(F, C))), factorial(N, C). 214 215all_mono(D, R, F):- zdd_sort(D, D0), 216 zdd_sort(R, R0), 217 length(D0, I), 218 length(R0, J), 219 ( I @=< J -> 220 bdd_sort_append(D0, 1, D1), 221 findall_mono(D1, R0, F) 222 ; F = 0 223 ). 224 225% ?- zdd bdd_sort_append([], 1, X), findall_mono(X, [a], Y). 226% ?- zdd bdd_sort_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y). 227% ?- zdd { N=14, numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 228% findall_mono(X, Ns, Y), card(Y, C), 229% { factorial(14, D), ( D=:=C -> writeln("OK")) }. 230 231findall_mono(X, _, X):- X < 2, !. 232findall_mono(X, Rng, Y):- memo(findall_mono(X,Rng)-Y), 233 ( nonvar(Y) -> true % , write(.) % many hits. 234 ; cofact(X, t(A, L, R)), 235 findall_mono(L, Rng, L0), 236 findall_mono(A, R, Rng, R0), 237 zdd_join(L0, R0, Y) 238 ). 239% 240findall_mono(A, R, Rng, R0):- findall(B-U, select(B, Rng, U), Cases), 241 findall_mono(Cases, A, R, 0, R0). 242% 243findall_mono([], _A, _R, V, V). 244findall_mono([B-Rng|Cases], A, R, U, V):- 245 findall_mono(R, Rng, U0), 246 cofact(U1, t(A-B, 0, U0)), 247 zdd_join(U, U1, U2), 248 findall_mono(Cases, A, R, U2, V).
254% ?- zdd all_epi([],[], F). 255% ?- zdd all_epi([a],[1], F), psa(F). 256% ?- zdd all_epi([a,b],[1], F), psa(F). 257% ?- zdd all_epi([a],[1,2], F), psa(F). 258% ?- zdd all_epi([a,b,c],[1,2], F), psa(F). 259% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (zdd all_epi(Ns, Ms, F)). 260% ?- time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (zdd all_epi(Ns, Ms, F)))). 261 262all_epi(D, R, F):- 263 zdd_sort(D, D0), 264 zdd_sort(R, R0), 265 length(D0, I), length(R0, J), 266 ( I @>= J -> 267 bdd_sort_append(D0, 1, D1), 268 findall_epi(D1, R0-R0, F) 269 ; F = 0 270 ).
275% ?- N=2, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 276% ?- N=3, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 277% ?- N=10, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 278% ?- N=11, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 279% ?- N=14, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 280% ?- N=15, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C))))X. 281% ?- N=16, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 282%@ % 185,729,299 inferences, 205.838 CPU in 207.237 seconds (99% CPU, 902308 Lips) 283% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R), 284% length(R, L). 285 286all_perm(D, P):- zdd_sort(D, D0), 287 findall_perm(D0, P). 288% 289findall_perm([], 1):-!. 290findall_perm(D, X):- memo(perm(D)-X), 291 ( nonvar(X) -> true % , write(.) % many hits. 292 ; 293 findall(I-D0, select(I, D, D0), U), 294 join_perm_for_selection(U, 0, X)). 295% 296join_perm_for_selection([], X, X). 297join_perm_for_selection([I-D|U], X, Y):- 298 findall_perm(D, X0), 299 bdd_cons(X1, I, X0), 300 zdd_join(X1, X, X2), 301 join_perm_for_selection(U, X2, Y). 302 303 /************************************************* 304 * terms in ZDD based on families of lists * 305 *************************************************/
313% ?- zdd coalgebra_for_signature([x], [f/1], [x], E), psa(E). 314% ?- zdd coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E). 315% ?- time((zdd coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2], 316% [x,y,z,u,v,0,1], E), card(E, C))). 317%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips) 318%@ E = 173825, 319%@ C = 68641485507. 320 321coalgebra_for_signature(D, Sgn, As, E):- 322 signature(Sgn, As, T), 323 signature_map(D, T, E). 324% 325signature_map([], _, 1):-!. 326signature_map([X|Xs], T, E):- 327 signature_map(Xs, T, E0), 328 extend_signature_map(X, T, E0, E). 329% 330extend_signature_map(_, 0, _, 0):-!. 331extend_signature_map(_, 1, E, E):-!. 332extend_signature_map(X, T, E, F):- cofact(T, t(A, L, _)), 333 extend_signature_map(X, L, E, E0), 334 l_cons(X->A, E, E1), 335 zdd_join(E0, E1, F).
340% ?- zdd term_path(a, R), psa(R), term_path(A, R). 341term_path(X, Y):- 342 ( nonvar(X) -> term_to_path(X, Y) 343 ; path_to_term(Y, X) 344 ).
349% ?- zdd term_to_path(a, R), psa(R). 350% ?- zdd term_to_path(f(a, b), R), psa(R). 351% ?- zdd term_to_path(f(g(a, b), h(c, d)), R), psa(R). 352% ?- zdd term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R). 353term_to_path(X, Y):- functor(X, F, N), 354 ( N = 0 -> zdd_singleton(X, Y) 355 ; functor(X, F, N), 356 arg_path(F/N, 1, X, Y) 357 ). 358% 359arg_path(_/N, J, _, 0):- J>N, !. 360arg_path(F, I, X, Y):- J is I + 1, 361 arg(I, X, A), 362 term_to_path(A, U), 363 arg_path(F, J, X, V), 364 cofact(Y, t(arg(F, I), V, U)).
370% ?- zdd term_to_path(a, X), path_to_term(X, R). 371% ?- zdd term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R). 372% ?- zdd term_to_path(f(1,2), X), path_to_term(X, R). 373% ?- T=f(h(a), 3, g(b,2), 5), 374% (zdd term_to_path(T, X), path_to_term(X, R)), T = R. 375 376path_to_term(X, Y):- X>1, cofact(X, t(A, L, R)), 377 ( R = 1 -> Y = A 378 ; A = arg(F/_, _), 379 path_to_term(R, R0), 380 path_to_term(L, L0, []), 381 Y =..[F, R0|L0] 382 ). 383% 384path_to_term(X, U, U):- X<2, !. 385path_to_term(X, [R0|U], V):- cofact(X, t(_, L, R)), 386 path_to_term(R, R0), 387 path_to_term(L, U, V).
compare(C, U, V) is performed.394% ?- X=f(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 395% term_path_compare(C0, T, U)), compare(C, X, Y). 396% ?- X=g(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 397% term_path_compare(C0, T, U)), compare(C, X, Y). 398% ?- X=g(a,b,c), Y=f(a,b), (zdd term_path(X, T), term_path(Y, U), 399% term_path_compare(C0, T, U)), compare(C, X, Y). 400 401term_path_compare(=, X, X):-!. 402term_path_compare(<, 0, _):-!. 403term_path_compare(>, _, 0):-!. 404term_path_compare(<, 1, _):-!. 405term_path_compare(>, _, 1):-!. 406term_path_compare(C, X, Y):- cofact(X, t(A, L, R)), 407 cofact(Y, t(B, L0, R0)), 408 arity_compare(C0, A, B), 409 ( C0 = (=) -> 410 term_path_compare(C1, R, R0), 411 ( C1 = (=) -> 412 left_branch_compare(C, L, L0) 413 ; C = C0 414 ) 415 ; C = C0 416 ). 417 418% Left branches are for argument lists of the name length. 419left_branch_compare(=, 0, 0):-!. 420left_branch_compare(C, X, Y):- 421 cofact(X, t(_, L, R)), 422 cofact(Y, t(_, L0, R0)), 423 term_path_compare(C0, R, R0), 424 ( C0 = (=) -> 425 left_branch_compare(C, L, L0) 426 ; C = C0 427 ). 428 429% 430arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G). 431arity_compare(C, A, B):-!, compare(C, A, B).
437% ?- zdd zdd_lift(1, X). 438% ?- zdd X<< pow([1,2]), zdd_lift(X, Y), card(Y, D), psa(Y). 439% ?- zdd X<< pow(numlist(1,10)), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D). 440% ?- N=16, numlist(1, N, Ns), 441% time((zdd X<< pow(Ns), zdd_lift(X, Y), card(Y, D))), D=:=2^N. 442%@ % 19,643,341 inferences, 31.553 CPU in 31.694 seconds (100% CPU, 622559 Lips) 443 444zdd_lift(X, X):- X<2, !. 445zdd_lift(X, Y):- memo(zdd_lift(X)-Y), 446 ( nonvar(Y) -> true %, write(.) % So so hits. 447 ; cofact(X, t(A, L, R)), 448 zdd_lift(L, L0), 449 zdd_lift(R, R0), 450 zdd_lift(A, R0, R1), 451 zdd_join(L0, R1, Y) 452 ). 453% 454zdd_lift(_, 0, 0):-!. 455zdd_lift(A, 1, Y):-!, zdd_singleton([A], Y). 456zdd_lift(A, X, Y):- cofact(X, t(B, L, _)), 457 zdd_singleton([A|B], R0), 458 zdd_lift(A, L, L0), 459 zdd_join(L0, R0, Y).
465% ?- zdd X<< pow([a,b]), card(X, C), zdd_univ(X, Y), psa(Y). 466% ?- zdd X<< pow([a,b]), zdd_univ(X, Y), psa(Y). 467 468zdd_univ(X, X):- X<2, !. 469zdd_univ(X, Y):- cofact(X, t(A, L, R)), 470 zdd_univ(R, [A], R0), 471 zdd_univ(L, L0), 472 zdd_join(L0, R0, Y). 473 474% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 475% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 476 477zdd_univ(0, _, 0):-!. 478zdd_univ(1, Stack, X):-!, reverse(Stack, Stack0), 479 U =.. Stack0, 480 zdd_singleton(U, X). 481zdd_univ(X, Stack, Y):- cofact(X, t(A, L, R)), 482 zdd_univ(L, Stack, L0), 483 zdd_univ(R, [A|Stack], R0), 484 zdd_join(L0, R0, Y).
g(a1, ..., an)
where G=g/n and ai in As.490% ?- zdd arity_term(f/2, [1, x, y], T), psa(T). 491arity_term(F/N, As, T):- memo((F/N)-T), 492 ( nonvar(T) -> true 493 ; all_list(N, As, X), 494 l_cons(F, X, T0), 495 zdd_univ(T0, [], T) 496 ).
504% ?- N=10, numlist(1, N, Ns), 505% time((zdd X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))). 506% ?- zdd X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y). 507% ?- N=100, numlist(1, N, Ns), 508% time((zdd X<<pow(Ns), l_cons(f, X, Y), card(Y, C))). 509% ?- N=10, numlist(1, N, Ns), 510% time((zdd X<<pow(Ns), zdd_mul_list([f, g, h], X, Y), card(Y, C))). 511 512zdd_functor(F, X, Y):- zdd_functor(F, X, [], Y). 513% 514zdd_functor(_, 0, _, 0):-!. 515zdd_functor(F, 1, St, Y):-!, T =..[F|St], 516 zdd_singleton(T, Y). 517zdd_functor(F, X, St, Y):-cofact(X, t(A, L, R)), 518 zdd_functor(F, L, St, Y0), 519 zdd_functor(F, R, [A|St], Y1), 520 zdd_join(Y0, Y1, Y).
f(a1, ..., an)
with f/n in G and ai in As.526% ?- zdd signature([f/1, g/2], [1, x, y], U), psa(U). 527% ?- time((zdd signature([f/2, g/2, h/3, i/4, k/5], 528% [0, 1, 2, x, y, z, u, v, w], U), card(U, C))). 529 530signature([], _, 0):-!. 531signature([G|Gs], As, T):- 532 arity_term(G, As, T0), 533 signature(Gs, As, T1), 534 zdd_join(T0, T1, T).
540% ?- spy(power_list). 541% ?- zdd power_list(0, [a,b], P). 542% ?- zdd power_list(1, [a,b], P). 543% ?- N = 100, numlist(1, N, _Ns), 544% time(((zdd power_list(N, _Ns, X), card(X, _Count)))), 545% _Count > 100^100, writeln(_Count). 546%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips) 547%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101 548%@ N = 100, 549%@ X = 515002. 550 551power_list(N, As, P):- obj_id(As, Id), 552 power_list_with_id(N, Id, P). 553% 554power_list_with_id(0, Id, 1):-!, memo(power_list(0, Id)-1). 555power_list_with_id(N, Id, Y):- 556 N0 is N - 1, 557 power_list_with_id(N0, Id, Y0), 558 all_list_with_id(N, Id, Y1), 559 zdd_join(Y0, Y1, Y).
565% ?- zdd all_list(0, [a], X), psa(X). 566% ?- zdd all_list(1, [a], X), psa(X). 567% ?- N=10, numlist(1, N, Ns), (zdd all_list(4, Ns, X), card(X, C)). 568% ?- N=100, numlist(1, N, Ns), time(((zdd all_list(100, Ns, X), card(X, C)))). 569%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips) 570 571all_list(N, As, Y):- obj_id(As, Id), 572 all_list_with_id(N, Id, Y). 573% 574all_list_with_id(0, Id, 1):-!, memo(all_list(0, Id)-1). 575all_list_with_id(N, Id, Y):- memo(all_list(N, Id)-Y), 576 ( nonvar(Y) -> true 577 ; N0 is N-1, 578 all_list_with_id(N0, Id, Y0), 579 obj_id(As, Id), 580 zdd_mul_list(As, Y0, 0, Y) 581 ).
586singleton_family([], 0):-!. 587singleton_family([A|As], X):- 588 singleton_family(As, X0), 589 zdd_singleton(A, U), 590 zdd_join(U, X0, X).
595distribute_con(F, X, Y):- zdd_mul_list(F, X, 0, Y). 596% 597zdd_mul_list([], _, Y, Y). 598zdd_mul_list([A|As], Y, U, V):- 599 l_cons(A, Y, V0), 600 zdd_join(U, V0, U0), 601 zdd_mul_list(As, Y, U0, V).
606% ?- zdd X<<pow([1,2]), l_cons(a, X, Y), psa(Y). 607 608l_cons(A, Y, U):- cofact(U, t(A, 0, Y)).
append(L, U, M) with U in X.
?- zdd X<<pow([1,2]), l_append([a,b], X, Y), psa(Y).615l_append([], X, X). 616l_append([A|As], X, Y):- 617 l_append(As, X, X0), 618 l_cons(A, X0, Y). 619 620% ?- zdd bdd_sort_append([], 1, X), findall_epi(X, [a]-[a], Y). 621% ?- zdd bdd_sort_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 622% ?- zdd bdd_sort_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 623% ?- zdd bdd_sort_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C). 624% ?- zdd bdd_sort_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y). 625% ?- N = 2, (zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 626% ?- N = 3, (zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 627% ?- N = 10,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 628% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 629% ?- N = 11,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 630% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 631% ?- N = 12,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 632% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 633% ?- N = 13,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 634% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 635 636select_target(Range, U, B, V):- member(B, Range), 637 ( select(B, U, V) -> true 638 ; V = U 639 ). 640 641% 642findall_epi(0, _, 0):-!. 643findall_epi(1, _-U, X):-!, 644 ( U=[] -> X = 1 645 ; X = 0 646 ). 647findall_epi(X, RngU, Y):- memo(findall_epi(X, RngU)-Y), 648 ( nonvar(Y) -> true % , write(.) % many hits. 649 ; cofact(X, t(A, L, R)), 650 findall_epi(L, RngU, L0), 651 findall_epi(A, R, RngU, R0), 652 zdd_join(L0, R0, Y) 653 ). 654% 655findall_epi(A, R, Rng-U, R0):- 656 findall(B-(Rng-V), select_target(Rng, U, B, V), Cases), 657 findall_epi(Cases, A, R, 0, R0). 658% 659findall_epi([], _, _, V, V). 660findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V):- 661 findall_epi(R, Rng-Rng0, U0), 662 cofact(U1, t(A-B, 0, U0)), 663 zdd_join(U, U1, U2), 664 findall_epi(Cases, A, R, U2, V). 665 666% ?- zdd merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X). 667merge_funs(Fs, X):- fold_merge_funs(Fs, 1, X). 668% 669fold_merge_funs([], X, X). 670fold_merge_funs([G|Fs], X, Y):- 671 fun_block(G, X0), 672 zdd_merge(X, X0, X1), 673 fold_merge_funs(Fs, X1, Y). 674% 675fun_block(G, X):- 676 ( G = mono(D-R) -> all_mono(D, R, X) 677 ; G = epi(D-R) -> all_epi(D, R, X) 678 ; G = fun(D-R), 679 all_fun(D, R, X) 680 ). 681 682% ?- N=2, numlist(1, N, Ns), 683% (zdd set_compare(opp_compare), 684% X<<pow(Ns), psa(X), set_compare(compare), 685% zdd_normalize(X, Y), psa(Y)). 686 687zdd_normalize(X, X):- X<2, !. 688zdd_normalize(X, Y):- memo(normalize(X)-Y), 689 ( nonvar(Y) -> true % , write(.) % Many hits. 690 ; cofact(X, t(A, L, R)), 691 zdd_normalize(L, L0), 692 zdd_normalize(R, R1), 693 zdd_insert(A, R1, R0), 694 zdd_join(L0, R0, Y) 695 ). 696 697% ?- N = 1000, numlist(1, N, Ns), 698% time((X<<pow(Ns), rank_family_by_card(X, P), card(P, C))). 699 700% ?- N = 1000, numlist(1, N, Ns), 701% time((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C))). 702 703% ?- N = 1000, numlist(1, N, Ns), 704% time((( X<<pow(Ns), 705% get_family_of_rank(500, X, Y), 706% card(Y, C)))).
711get_family_of_rank(Order, X, F):- rank_family_by_card(X, _), 712 memo(family_with_card(Order)-F). 713 714% ?- X<<pow([1]). 715% ?- X<<set([a]), rank_family_by_card(X, P), 716% memo(family_with_card(0)-L), sets(L, Sl), 717% memo(family_with_card(1)-M), sets(M, Sm).
723rank_family_by_card(0, 0):-!. 724rank_family_by_card(1, 0):-!, memo(family_with_card(0)-1). 725rank_family_by_card(I, P):- memo(rank_family_by_card_done(I)-B), 726 ( nonvar(B) -> true 727 ; cofact(I, t(A, L, R)), 728 rank_family_by_card(L, Pl), 729 rank_family_by_card(R, Pr), 730 max(Pl, Pr, P0), 731 insert_one_to_family(A, P0, New), 732 P is P0 + 1, 733 memo(family_with_card(P)-New), 734 B = true 735 ). 736% 737insert_one_to_family(A, 0, G):-!, memo(family_with_card(0)-F), 738 zdd_insert(A, F, G). 739insert_one_to_family(A, P, G):- P0 is P-1, 740 insert_one_to_family(A, P0, G0), 741 memo(family_with_card(P)-Fp), 742 zdd_insert(A, Fp, G), 743 zdd_join(Fp, G0, Gp), 744 set_memo(family_with_card(P)-Gp). 745 746 /********************** 747 * State access * 748 **********************/ 749 750get_extra(Extra):- b_getval(zdd_extra, Extra). 751% 752set_extra(Extra):- b_setval(zdd_extra, Extra). 753 754% ?- bump_up(a, N), bump_up(a, K). 755bump_up(Key):- b_getval(zdd_extra, Extra), 756 ( select(Key-N0, Extra, Extra0) -> true 757 ; N0 = 0, 758 Extra0 = Extra 759 ), 760 N is N0 + 1, 761 b_setval(zdd_extra, [Key-N|Extra0]). 762 763 764:- meta_predicate set_compare(). 765set_compare(Compare):- nb_setval(zdd_compare, Compare). 766 767% ?- zdd_compare(C, a, b). 768get_compare(Compare):- b_getval(zdd_compare, Compare). 769% 770zdd_compare(C, X, Y):- get_compare(F), call(F, C, X, Y). 771 772% ?- zdd_sort([1->1, 1->2, 1-1, 2-2], X). 773zdd_sort(X, Y):- get_compare(Comp), predsort(Comp, X, Y). 774 775% ?- get_key(a, V), set_key(a, 1), get_key(a, W). % fail. 776% ?- set_key(a, 1), get_key(a, W). 777get_key(K, V):- b_getval(zdd_extra, Assoc), 778 memberchk(K-V, Assoc). 779% 780set_key(K, V) :- b_getval(zdd_extra, Assoc), 781 ( select(K-_, Assoc, Assoc0) 782 -> b_setval(zdd_extra, [K-V|Assoc0]) % nb_linkval not work. 783 ; b_setval(zdd_extra, [K-V|Assoc]) % nb_linkval not work. 784 ). 785% 786nb_set_key(K, V) :- b_getval(zdd_extra, Assoc), 787 ( select(K-_, Assoc, Assoc0) 788 -> nb_setval(zdd_extra, [K-V|Assoc0]) 789 ; nb_setval(zdd_extra, [K-V|Assoc]) 790 ). 791 792:- meta_predicate set_pred(, ). 793set_pred(K, V) :- set_key(K, V). 794 795% ?- open_key(a, []), update_key(a, X, Y), X=[1|Y], 796% get_key(a, Z), close_key(a). 797 798% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]}, 799% get_key(a, Z), close_key(a), get_key(a, U))). % false 800 801% 802open_key(K, Val):- set_key(K, Val). 803% 804update_key(X, Old, New):- b_getval(zdd_extra, Assoc), 805 select(X-Old, Assoc, Assoc0), 806 b_setval(zdd_extra, [X-New|Assoc0]). 807% 808close_key(Key):- b_getval(zdd_extra, Assoc), 809 ( select(Key-_, Assoc, Assoc0) -> 810 b_setval(zdd_extra, Assoc0) 811 ; true 812 ). 813 814% ?- varnum(D), varnum(E).
819varnum(D):- get_key(varnum, D). 820 821% ?- sort([1->1, 1->2, 1-1, 2-2], X). 822% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X). 823% ?- zdd_sort_rev([1,2,3], X). 824 825compare_rev(Comp, C, A, B):- call(Comp, C, B, A). 826% 827zdd_sort_rev(X, Y):- get_compare(Comp), 828 predsort(compare_rev(Comp), X, Y). 829 830% ?- pred_zdd(opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)). 831:- meta_predicate pred_zdd(, ). 832pred_zdd(Comp, X):- set_compare(Comp), call(X). 833 834% ?- X<<pow([a,b,c]), zdd_memberchk([a,c], X). 835% ?- X<<pow([a,b,c]). 836% ?- spy(zdd_ord_power). 837 838 839% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([], X))). 840% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
845zdd_memberchk(L, Z):- zdd_sort(L, L0), zdd_ord_memberchk(L0, Z). 846% 847zdd_ord_memberchk([], Z):- !, zdd_has_1(Z). 848zdd_ord_memberchk([A|As], Z):- Z>1, 849 cofact(Z, t(B, L, R)), 850 ( A == B 851 -> zdd_ord_memberchk(As, R) 852 ; A @> B, 853 zdd_ord_memberchk([A|As], L) 854 ). 855 856% PASS 857% ?- zdd X<<pow([a,b]), card(X, C). 858% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))). 859% ?- zdd {X=1, Y =2, Z is X + Y}. 860% ?- zdd X<<set([a]), sets(X, U). 861% ?- zdd((X<<pow([a,b]), S<<sets(X))). 862% ?- zdd((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 863% ?- zdd(((X<< *(:append([a,b], [c,d]))), sets(X, Y))). 864% ?- zdd((X<<(*[a,b]& *[c,d]), S<<sets(X))). 865% ?- zdd((X<<{[a],[b],[c]}, sets(X,S))). 866% ?- zdd((X<<{[a],[b, c]}, sets(X,S))). 867% ?- zdd((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 868% ?- zdd((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 869% ?- I =1000, J =2000, 870% time( (zdd 871% { numlist(1, I, L), 872% numlist(1, J, M)}, 873% X << pow(L), 874% Y << pow(M), 875% Z << (Y - X), 876% card(Z, C), 877% {C =:= 2^J-2^I} )). 878 879 880% PASS 881% ?- zdd((X<<cnf(0), Y<<sets(X))). 882% ?- zdd((X<<cnf(1), Y<<sets(X))). 883% ?- zdd((X<<cnf(2), Y<<sets(X))). 884% ?- zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 885% ?- ltr_zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 886% ?- zdd((X<<cnf(a), Y<<sets(X))). 887% ?- zdd((X<<cnf(-a), Y<<sets(X))). 888% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 889% ?- zdd((X<<cnf(-(a+b)), Y<<sets(X))). 890% ?- zdd((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 891% ?- zdd((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 892% ?- zdd((X<<cnf(-(-a + -b)), Y<<sets(X))). 893% ?- zdd((X<<dnf(a), Y<<sets(X), extern(Y, Y0))). 894% ?- zdd((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))). 895% ?- zdd((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))). 896% ?- zdd((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))). 897% ?- zdd((X<<dnf(a+b), Y<<sets(X))). 898% ?- zdd((X<<dnf(-(a+b)), Y<<sets(X))). 899% ?- zdd((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 900% ?- zdd((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 901% ?- zdd((X<<dnf(-(-a + -b)), Y<<sets(X))). 902% ?- zdd((X<<dnf((-a + a)), Y<<sets(X))). 903% ?- zdd((X<<dnf(-(-a + a)), Y<<sets(X))). 904% ?- zdd(X << *(:append([a,b], [c,d]))). 905% ?- zdd((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))). 906% ?- zdd((X << *[a,b], sets(X, S))). 907% ?- zdd((X << +[a,b], sets(X, S))). 908% ?- zdd((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 909% ?- zdd((zdd_list_to_singletons([], X), prz(X))). 910% ?- zdd((zdd_list_to_singletons([a], X), prz(X))). 911% ?- zdd((zdd_list_to_singletons([a,b], X), prz(X))). 912% ?- zdd((zdd_list_to_singletons([c, a, b], X), prz(X))). 913% ?- zdd X << *[a,b], psa(X). 914% ?- zdd X << +[a,b], psa(X). 915 916% ?- I =1000, J is I + 1, numlist(1, I, L), 917% prepare_ltr_list(L, L0), 918% time(zdd(( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
926zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 927% 928zdd_list_to_singletons([], 1, _). 929zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 930 zdd_singleton(A, Y0, S), 931 zdd_join(Y0, Y, X, S). 932 933% PASS. 934% ?- zdd((zdd_partial_choices([], X), prz(X))). 935% ?- zdd((zdd_partial_choices([[a], [b]], X), prz(X))). 936% ?- zdd((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 937% ?- zdd((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 938% ?- zdd((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 939% ?- zdd((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 940% ?- zdd((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))). 941% ?- zdd((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 942% ?- zdd((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 943% ?- findall([I], between(1, 10000, I), Ls), 944% zdd((zdd_partial_choices(Ls, X), 945% card(X, C))), !, C =:= 2^10000.
950zdd_partial_choices([], 1):-!. 951zdd_partial_choices([L|Ls], X):- zdd_partial_choices(Ls, X0), 952 sw_fold_insert(zdd, L, X0, 0, X1), 953 zdd_join(X0, X1, X). 954 955:- meta_predicate zdd_find(, , ).
960% ?- zdd X<< pow([a,b,c]), zdd_find(=(c), X, Y). 961% ?- zdd X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y). 962% ?- zdd X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y). 963 964zdd_find(F, X, Y):- X>1, 965 cofact(X, t(A, L, R)), 966 ( call(F, A), Y = A 967 ; zdd_find(F, L, Y) 968 ; zdd_find(F, R, Y) 969 ). 970 971use_table(G):- functor(G, F, N), 972 setup_call_cleanup( 973 table(F/N), % 974 G, 975 untable(F/N) % 976 ). 977 978 979 980% PASS. 981% 982% ?- zdd P<<pow([1,2,3]), {X=1;X=2}, card(P,C). 983% ?- zdd P<<pow([1,2,3]), card(P,C). 984% ?- zdd P<<pow([1,2,3]), card(P,C). 985 986% ?- zdd P << set([1,2,3,2,3]), psa(P). 987 988% ?- zdd P << ({[1,2,3,2,3]} + {[4, 2,4]}), psa(P). 989 990% ?- zdd {append([a,b], [c,d], X)}. 991% ?- zdd X << :append([a,b], [c,d]). 992% ?- zdd (zdd X << :append([a,b], [c,d])). 993% ?- zdd (zdd (zdd X << :append([a,b], [c,d]))). 994% ?- zdd (zdd (zdd ( X<<pow([1,2]), true, true))). 995% ?- zdd (zdd zdd X<<pow([1,2]), true, true, card(X, C)). 996% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), card(X, C)). 997 998 999% ?- show_state. 1000 1001% ?- fetch_state, X<<pow([a,b]), fetch_state, card(X, C). 1002% ?- zdd X<<{[a],[b]}, Y<<{[b], [c]}, zdd_merge(X, Y, Z), psa(Z). 1003% ?- zdd X<<{[a,b],[b,c],[c,d]}, zdd_merge(X, X, Z), psa(Z).
opp_compare(C, 1, 2).
?- opp_compare(C, a->b, b).
?- opp_compare(C, p(0,0), p(1,0)).
?- opp_compare(C, p(1,0)-p(0,0), p(1,0)-p(1,0)).1012opp_compare(<, -(_,_), ->(_,_)):-!. 1013opp_compare(>, ->(_,_), -(_,_)):-!. 1014opp_compare(C, X, Y):- compare(C, Y, X). % reverse order 1015 1016% ?- zdd X<< @(abc), psa(X). 1017% ?- 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.1034% ?- X<< +[ *[a,b], *[c, d]], psa(X). 1035% ?- <<(X, +[*[a,b], *[c,d]]), psa(X). 1036% ?- X<< card(pow([1,2]) + pow([a,b])). 1037% ?- X<< card(pow([1,2])). 1038 1039 1040:- meta_predicate <<(, ). 1041<<(X, E) :- zdd_eval(E, X).
zdd_solve(+G, +S, +M) is det.
Solve goal G with state S and module M.1048% ?- zdd X<< (+[0, 1]), psa(X). 1049% ?- zdd X<< (+[0,1]), {fetch_state, b_getval('$zdd', S0), writeln(S0)}. 1050% ?- zdd X<< *[0, 1, 2, 3], psa(X). 1051% ?- zdd X<< *[*[]], psa(X). 1052% ?- zdd X<< *[[]], psa(X). 1053% ?- zdd X<< *[+[]], psa(X). 1054% ?- zdd X<<pow(:numlist(1, 100)), card(X, C). 1055% ?- zdd X<< :numlist(1, 100). 1056 1057% % 1058% zdd_solve(true, _) :-!. 1059% zdd_solve(M:G, _) :-!, zdd_solve(G, M). 1060% zdd_solve({G}, M) :-!, call(M:G). 1061% zdd_solve(X<<E, M) :-!, zdd_numbervars(E), zdd_eval(E, X, M). 1062% zdd_solve((A,B), M) :-!, zdd_solve(A, M), zdd_solve(B, M). 1063% zdd_solve((A;B), M) :-!, (zdd_solve(A, M); zdd_solvde(B, M)). 1064% zdd_solve((A->B), M) :-!, (zdd_solve(A, M) -> zdd_solve(B, M)). 1065% zdd_solve(G, M):- call(M:G).
--- 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 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,
1102% Pass. 1103% ?- X<<dnf(a*b), psa(X). 1104% ?- X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C). 1105% ?- X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))). 1106% ?- X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C). 1107 1108% Pass. 1109% ?- zdd X<< @a. 1110% ?- zdd X<< a, psa(X). 1111% ?- zdd X<<pow([a,b]), card(X, C). 1112% ?- zdd X<<pow([a,b])-pow([a]), card(X, C). 1113% ?- zdd X<< set(:(append([1,2],[3,4]))), psa(X). 1114% ?- zdd((X<< +(:append([1,2],[3,4])), psa(X))). 1115% ?- zdd((X<< (@a + @b), psa(X))). 1116% ?- zdd((X<< ((@a + @b)* @c), psa(X))). 1117% ?- zdd((X<< [a,b])). 1118% ?- zdd((X<< set(:(append([a,b],[c,d]))), psa(X))). 1119% ?- zdd((X<< set(!append([a,b],[c,d])), psa(X))). % error 1120% ?- zdd(X<< card(pow([a,b]))). 1121% ?- zdd(X<< card(pow(:numlist(1, 100)))). 1122% ?- zdd((X<< set([1]), Y<< (X+X), psa(X))). 1123% ?- zdd((X<< set([1]), psa(X))). 1124% ?- zdd((X<< set([]))). 1125% ?- zdd((X << {[a], [b], [c]}, psa(X))). 1126% ?- zdd((X << {[a], [b], [c]}, card(X, C))). 1127 1128% PASS. 1129% ?- zdd X << card(pow(:append(:numlist(1,3), :numlist(4,5)))). 1130 1131% ?- zdd((X << set(:append(numlist(1,2), numlist(4,5))))). 1132% ?- zdd((X << set(:append(numlist(1,10), numlist(11,20))))). 1133% ?- zdd { numlist(1,10,A), numlist(11,20, B)}, X<< pow( :append(A, B)), 1134% card(X, C). 1135% ?- zdd X << pow(:(numlist(1,2))), card(X, C). 1136% ?- zdd X << pow(:(numlist(1,2))). 1137 1138% ?- zdd((X << pow(:(! charlist(a,z))), card(X, C))). 1139% ?- zdd((X << pow(:(! charlist(a-z))), card(X, C))). 1140% ?- zdd((X << pow([a,b]))). 1141% ?- zdd((X << *[a, b, c])). 1142% ?- zdd((X << (*[a, b, c] + *[a,b,c]), psa(X))). 1143% ?- zdd((X << (*[a, b, c] + *[2, 3]), psa(X))). 1144% ?- zdd((C << card(pow([a,b,c,1,2,3])))). 1145% ?- zdd((C << card(pow(:append([a,b,c], [1,2,3]))))). 1146% ?- zdd((C << pow(:numlist(1, 3)))). 1147% ?- zdd((C << @(a), psa(C))). 1148 1149% Pass. 1150% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))). 1151% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))). 1152% ?- zdd((U << +(:(append([a,b,c], [d,e,f]))), psa(U))). 1153% ?- zdd((U << *(:(append([a,b,c], [d,e,f]))), psa(U))). 1154% ?- zdd((U << +(:(append(:append([a,b,c], [x,y,z]), [1, 2]))), psa(U))). 1155% ?- zdd((U << +[ *[a,b], *[c,d]], psa(U))). 1156% ?- zdd((U << *[ +[a,b], +[c,d]], psa(U))). 1157% ?- zdd((U << *[ *[a,b], *[c,d]], psa(U))). 1158% ?- zdd((U << *[ *[a,b], +[c,d]], psa(U))). 1159% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1160% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1161% ?- zdd((U << #(card(pow([a]))))). 1162% ?- zdd((U << :succ(#(card(pow([a])))))). 1163% ?- zdd((U << card(pow([a])))). 1164% ?- zdd U << card(pow([a])+pow([b])). 1165 1166% ?- zdd((U << :(=(3)))). 1167% ?- zdd((U << *([1,2,3]), psa(U))). 1168% ?- zdd((U << :plus(#(card(pow([a,b]))), #(card(pow([1,2])))))). 1169% ?- zdd((U << @a)). % singleton. 1170% ?- zdd((U << @2)). 1171% ?- zdd((U << [a,b])). 1172% ?- zdd((U << *[a,b], psa(U))). 1173% ?- zdd((U << +[a,b], psa(U))). 1174% ?- zdd((U << +[*[a,b], *[c,d]], psa(U))). 1175% ?- zdd((U << +[+[a,b], +[c,d]], psa(U))). 1176% ?- zdd((U << *[+[a,b], +[c,d]], psa(U))). 1177% ?- zdd((U << *[*[a,b], *[c,d]], psa(U))). 1178% ?- zdd((U << :(!call(=, hello)))). 1179% ?- zdd((U << :(call($(=), :append([a,b],[c,d]))))). 1180% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< zdd_join(X, Y), psa(Z). 1181% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< (X+Y), psa(Z). 1182% 1183basic_type(X):- number(X); 1184 string(X); 1185 is_list(X); 1186 var(X). 1187 1188% ?- X<< p(2,3), psa(X). 1189% ?- X<< pq(2,3), psa(X). % Error. 1190% ?- findall(p(I), between(1,3,I), As), X<< +As, psa(X). 1191 1192default_atom(X):- functor(X, F, _), 1193 atom_chars(F, [A|As]), 1194 char_type(A, alpha), 1195 digit_chars(As). 1196% 1197digit_chars([]). 1198digit_chars([D|Ds]):- char_type(D, digit), 1199 digit_chars(Ds).
1204% Unusual first, but legal samples. 1205% ?- zdd U << @(=(3)), psa(U). 1206% ?- zdd U << +(!append([a], [b])), psa(U). 1207% ?- zdd U << (@a+ @b+ @c), psa(U). 1208% ?- zdd U << append([a], [b]). 1209% ?- zdd U << +(append([[a]], [[b]])), psa(U). 1210% ?- zdd U << get_compare. 1211% ?- zdd get_compare(X). 1212% ?- zdd U << arith(1+2). 1213% ?- zdd U << plus(arith(1+2), arith(3+4)). 1214% ?- zdd U << (@A+ @B+ @C), psa(U). 1215 1216zdd_eval(X, Y):- context_module(M), 1217 zdd_numbervars(X), 1218 zdd_eval(X, Y, M).
1224% Note that intgeger is used as a unique name of a ZDD. 1225% use indicator `@` as `@(3)` for 3 as an atom. 1226 1227zdd_eval(X, X, _) :- basic_type(X), !. 1228zdd_eval({}, 0, _) :-!. % The empty family of sets. 1229zdd_eval({X}, Y, _) :-!, associative_comma(X, U, []), zdd_family(U, Y). 1230zdd_eval($(X), X, _) :-!. 1231zdd_eval(!(X), Y, M) :-!, call(M:X, Y). 1232zdd_eval(M:X, Y, _) :-!, zdd_eval(X, Y, M). 1233zdd_eval(X, Y, _) :- zdd_basic(X, Y), !. 1234zdd_eval(X, Y, M) :- zdd_eval_args(X, X0, M), 1235 ( zdd_apply(X0, Y) -> true 1236 ; call(M:X0, Y) 1237 ). 1238% 1239zdd_eval_args(A, A, _):- atomic(A), !. 1240zdd_eval_args(A, B, M):- 1241 functor(A, Fa, Na), 1242 functor(B, Fa, Na), 1243 zdd_eval_args(1, A, B, M). 1244% 1245zdd_eval_args(I, A, B, M):- arg(I, A, U), !, 1246 zdd_eval(U, V, M), 1247 arg(I, B, V), 1248 J is I+1, 1249 zdd_eval_args(J, A, B, M). 1250zdd_eval_args(_, _, _, _). 1251 1252 /*********************************************** 1253 * Currently reserved names of operations. * 1254 ***********************************************/ 1255zdd_basic(@(A), Y) :-!, zdd_singleton(A, Y). 1256zdd_basic(X, Y) :- default_atom(X), !, zdd_singleton(X, Y). 1257zdd_basic(dnf(A), X) :-!, dnf(A, X). 1258zdd_basic(cnf(A), X) :-!, cnf(A, X). 1259zdd_basic(arith(E), X) :-!, X is E. 1260zdd_basic(X, Y) :- (atom(X); dvar(X)), !, zdd_singleton(X, Y).
1267zdd_apply(ltr_set(L), Y):-!, ltr_append(L, 1, Y). 1268zdd_apply(gf2(A), X) :-!, gf2(A, X). 1269zdd_apply(qp(A), X) :-!, mqp(A, X). 1270zdd_apply(cofact(A, L, R), X) :-!, cofact(X, t(A, L, R)). 1271zdd_apply(cofact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1272zdd_apply(fact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1273zdd_apply(+(X), Y) :-!, zdd_vector_exp(+(X), Y). 1274zdd_apply(*(X), Y) :-!, zdd_vector_exp(*(X), Y). 1275zdd_apply(X + Y, Z) :-!, zdd_join(X, Y, Z). 1276zdd_apply(X * Y, Z) :-!, zdd_merge(X, Y, Z). 1277zdd_apply(merge(X, Y), Z) :-!, zdd_merge(X, Y, Z). 1278zdd_apply(-(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1279zdd_apply(\(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1280zdd_apply((X // Y), Z) :-!, zdd_div(X, Y, Z). 1281zdd_apply((X / Y), Z) :-!, zdd_mod(X, Y, Z). 1282zdd_apply((X mod Y), Z) :-!, zdd_mod(X, Y, Z). 1283zdd_apply(&(X, Y), Z) :-!, zdd_meet(X, Y, Z). 1284zdd_apply(prod(X, Y), Z):-!, zdd_product(X, Y, Z). 1285zdd_apply(**(X, Y), Z) :-!, zdd_product(X, Y, Z). 1286zdd_apply(pow(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1287zdd_apply(power(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1288zdd_apply(set(X), Z) :- bdd_sort_append(X, 1, Z). 1289 1290 1291 /********************************* 1292 * zdd vector expressions * 1293 *********************************/
1298% ?- zdd((X<< +[[1,2],[a,b]], psa(X), card(X, C))). 1299% ?- zdd((X<< *[[1,2],[a,b]], psa(X), card(X, C))). 1300% ?- zdd((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))). 1301% ?- zdd X<< +[*[1,2], *[a,b]], psa(X). 1302% ?- zdd X<< +[*[1,2], *[1]], psa(X). 1303% ?- zdd X<< +[*[1,2], *[a,b]]. 1304% ?- zdd((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))). 1305% ?- zdd((X<< *[1,2], psa(X), card(X, C))). 1306% ?- zdd((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))). 1307% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1308% ?- zdd zdd_vector_exp(+[[a],*[b,c]], X), psa(X). 1309% ?- zdd zdd_vector_exp(+[a,b,c], X), psa(X). 1310% ?- zdd zdd_vector_exp(*[a,b,c], X), psa(X). 1311% ?- zdd zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X). 1312% ?- zdd zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X). 1313% ?- zdd zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X). 1314% ?- zdd X<< *[a, b], psa(X). 1315% ?- zdd X<< +[a, b], psa(X). 1316% ?- zdd X<< *[A, B], psa(X). 1317% ?- zdd X<< *[*[0, 1], *[2,3]], psa(X). 1318% ?- zdd X<< *[*[], *[2,3]], psa(X). 1319% ?- zdd X<< *[0, 1, *[2,3]], psa(X). 1320% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1321% ?- zdd zdd_vector_exp(+[a,b], X), psa(X). 1322 1323zdd_vector_exp(*(X), Y):-!, zdd_vector_exp(*, X, Y). 1324zdd_vector_exp(+(X), Y):-!, zdd_vector_exp(+, X, Y). 1325zdd_vector_exp(X, Y):- zdd_singleton(X, Y). 1326% 1327zdd_vector_exp(*, [], 1):-!. 1328zdd_vector_exp(+, [], 0):-!. 1329zdd_vector_exp(F, [A|As], R):-!, % F in [*,+]. 1330 zdd_vector_exp(A, U), 1331 zdd_vector_exp(F, As, V), 1332 apply_binary_basic(F, U, V, R). 1333zdd_vector_exp(_, A, R):- zdd_singleton(A, R). 1334% 1335apply_binary_basic(*, X, Y, Z):-!, zdd_merge(X, Y, Z). 1336apply_binary_basic(+, X, Y, Z):- zdd_join(X, Y, Z). 1337% 1338zdd_fold_join([], Z, Z). 1339zdd_fold_join([X|Xs], Z, Z0):- 1340 zdd_join(X, Z, Z1), 1341 zdd_fold_join(Xs, Z1, Z0). 1342% 1343zdd_fold_merge([], Z, Z). 1344zdd_fold_merge([X|Xs], Z, Z0):- 1345 zdd_merge(X, Z, Z1), 1346 zdd_fold_merge(Xs, Z1, Z0). 1347% 1348fold_singleton_join([], X, X). 1349fold_singleton_join([A|As], X, Y):- 1350 zdd_singleton(A, U), 1351 zdd_join(U, X, X0), 1352 fold_singleton_join(As, X0, Y). 1353 1354% ?- zdd X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X). 1355% ?- zdd X<< (+[a,b]), psa(X). 1356% ?- zdd X<< +[*[a,b]] + +[*[c,d]], psa(X). 1357% ?- zdd X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X\Y). 1358% ?- zdd X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X-Y). 1359 1360zdd_super_power([], P, P). 1361zdd_super_power([A|As], P, Q):- 1362 zdd_super_power(As, P, Q0), 1363 zdd_insert(A, Q0, Q). 1364% 1365single_set(L, Y) :-!, bdd_sort_append(L, 1, Y). 1366 1367% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 1368family(X, Y):- zdd_numbervars(X), zdd_family(X, Y).
1374zdd_family(X, Y):- zdd_numbervars(X), zdd_family(X, 0, Y). 1375 1376% ?- zdd zdd_family([[a],[a,b]], X), card(X, C), psa(X). 1377% ?- zdd zdd_family([[], [a,a],[a,b]], X), psa(X). 1378zdd_family([], U, U). 1379zdd_family([X|Xs], U, V):- 1380 zdd_insert_atoms(X, 1, X1), 1381 zdd_join(X1, U, U0), 1382 zdd_family(Xs, U0, V). 1383 1384% ?- zdd((ltr_family([[a, b], [c, d]], X), sets(X,S))). 1385% ?- zdd((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 1386% ?- zdd((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 1387% ?- zdd((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 1388% ?- zdd((X << dnf((a+(-b)+a)), psa(X))). 1389% ?- zdd((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 1390% ?- zdd((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))). 1391% ?- ltr_zdd ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X). 1392% ?- ltr_zdd ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X). 1393% ?- ltr_zdd ltr_family([[a],[-b, -a,-c]], X), psa(X). 1394% 1395ltr_family(X, Y):- ltr_family(X, 0, Y). 1396 1397% 1398ltr_family([], U, U). 1399ltr_family([X|Xs], U, V):- 1400 ltr_append(X, 1, X0), 1401 ltr_join(X0, U, U0), 1402 ltr_family(Xs, U0, V). 1403 1404 /************************ 1405 * choices * 1406 ************************/
1411% ?- zdd X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y). 1412% ?- N=10, numlist(1, N, Ns), (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1413% zdd_choices(X, Y), card(Y, C)). 1414% ?- N=1000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1415% zdd_choices(X, Y), card(Y, C))). 1416 1417zdd_choices(0, 1):-!. 1418zdd_choices(1, 0):-!. 1419zdd_choices(X, Y):- memo(choices(X)-Y), 1420 ( nonvar(Y)->true %, write(+) % many hits when X has the empty set. 1421 ; cofact(X, t(A, L, R)), 1422 zdd_choices(L, L0), 1423 zdd_choices(R, R0), 1424 cofact(R1, t(A, R0, 1)), 1425 zdd_merge(L0, R1, Y) 1426 ). 1427 1428 1429 /************************************************* 1430 * Operation on zdd join/merge/meet/subtr/cons * 1431 *************************************************/
1436zdd_join(0, X, X):-!. 1437zdd_join(X, 0, X):-!. 1438zdd_join(X, X, X):-!. 1439zdd_join(1, X, Y):-!, zdd_join_1(X, Y). 1440zdd_join(X, 1, Y):-!, zdd_join_1(X, Y). 1441zdd_join(X, Y, Z):- 1442 ( Y < X -> memo(zdd_join(Y, X)-Z) 1443 ; memo(zdd_join(X, Y)-Z) 1444 ), 1445 ( nonvar(Z) -> true 1446 ; cofact(X, t(A, L, R)), 1447 cofact(Y, t(A0, L0, R0)), 1448 zdd_compare(C, A, A0), 1449 ( C = (<) -> 1450 zdd_join(L, Y, U), 1451 cofact(Z, t(A, U, R)) 1452 ; C = (=) -> 1453 zdd_join(L, L0, U), 1454 zdd_join(R, R0, V), 1455 cofact(Z, t(A, U, V)) 1456 ; zdd_join(L0, X, U), 1457 cofact(Z, t(A0, U, R0)) 1458 ) 1459 ).
cofact(Z, t(X, 0, Y), S).
Having analogy Z = [X|Y] in mind.1465% ?- bdd_cons(X, a, 1), bdd_cons(X, A, B). 1466% ?- bdd_cons(X, a, 0), bdd_cons(X, A, B). % false 1467 1468bdd_cons(X, Y, Z):- ( var(X); X>1 ), !, cofact(X, t(Y, 0, Z)). 1469 1470% ?- zdd((X<<(*[a]+ *[b]+ []), psa(X))). % false for []. 1471% ?- zdd((X<<(*[a]+ *[b]+ 1), psa(X))). 1472% ?- zdd((X<<(*[a]+ *[b]+ 0), psa(X))). 1473% ?- zdd((X<<(*[a]+ *[b]), psa(X))). 1474% ?- zdd((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))). 1475 1476% zdd_join_1(+X, -Y, +G) is det. 1477% Y is the union of X and 1 (the singleton {{}}). 1478 1479% ?- numlist(1,100, Ns), (zdd X<<pow(Ns), {fetch_state(S), time(repeat(100, zdd_join_1(X,_,S)))}). 1480zdd_join_1(X, X):- zdd_has_1(X), !. 1481zdd_join_1(X, Y):- zdd_add_1(X, Y). 1482% 1483zdd_add_1(0, 1):-!. 1484zdd_add_1(X, Y):- cofact(X, t(A, L, R)), 1485 zdd_add_1(L, L0), 1486 cofact(Y, t(A, L0, R)). 1487 1488% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1489%@ * Call: (13) zmod:zdd_solve((zmod:_1185968<<(zmod: *([a, b])), zmod:_1185992<<(zmod: *([a|...])), zmod:_1186004<<(zmod:_1185968*_1185992), zmod:sets(_1186004, _1186012)), zdd43, zmod) ? no debug 1490%@ X = Y, Y = Z, Z = 4, 1491%@ S = [[a, b]]. 1492% ?- zdd((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1493% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))). 1494% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))). 1495% ?- trace, zdd(X=[b, a]). 1496% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 1497% ?- zdd((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
1502zdd_meet(0, _, 0):-!. 1503zdd_meet(_, 0, 0):-!. 1504zdd_meet(1, X, Y):-!, zdd_meet_1(X, Y). 1505zdd_meet(X, 1, Y):-!, zdd_meet_1(X, Y). 1506zdd_meet(X, X, X):-!. 1507zdd_meet(X, Y, Z):- 1508 ( X @< Y -> memo(zdd_meet(X,Y)-Z) 1509 ; memo(zdd_meet(Y,X)-Z) 1510 ), 1511 ( nonvar(Z) -> true 1512 ; cofact(X, t(A, L, R)), 1513 cofact(Y, t(A0, L0, R0)), 1514 zdd_compare(C, A, A0), 1515 ( C = (<) -> zdd_meet(L, Y, Z) 1516 ; C = (=) -> 1517 zdd_meet(L, L0, U), 1518 zdd_meet(R, R0, V), 1519 cofact(Z, t(A, U, V)) 1520 ; zdd_meet(L0, X, Z) 1521 ) 1522 ).
1527zdd_meet_1(X, 1):- zdd_has_1(X), !. 1528zdd_meet_1(_, 0).
1533% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), Z<<(X-Y), psa(Z). 1534% ?- zdd((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 1535% 1536zdd_subtr(X, X, 0):-!. 1537zdd_subtr(0, _, 0):-!. 1538zdd_subtr(X, 0, X):-!. 1539zdd_subtr(X, 1, Y):-!, zdd_subtr_1(X, Y). 1540zdd_subtr(1, X, Y):-!, 1541 ( zdd_has_1(X) -> Y = 0 1542 ; Y = 1 1543 ). 1544zdd_subtr(X, Y, Z):- memo(zdd_subtr(X,Y)-Z), 1545 ( nonvar(Z) -> true 1546 ; cofact(X, t(A, L, R)), 1547 cofact(Y, t(A0, L0, R0)), 1548 zdd_compare(C, A, A0), 1549 ( C = (<) -> 1550 zdd_subtr(L, Y, U), 1551 cofact(Z, t(A, U, R)) 1552 ; C = (=) -> 1553 zdd_subtr(L, L0, U), 1554 zdd_subtr(R, R0, V), 1555 cofact(Z, t(A, U, V)) 1556 ; zdd_subtr(X, L0, Z) 1557 ) 1558 ).
1563% ?- zdd X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y). 1564% ?- zdd X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y). 1565% ?- zdd X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y). 1566% 1567zdd_subtr_1(X, 0):- X < 2, !. % empty family or singleton of the empty. 1568zdd_subtr_1(X, Y):- cofact(X, t(A, L, R)), 1569 zdd_subtr_1(L, L0), 1570 cofact(Y, t(A, L0, R)).
1575% ?- zdd X<<{[a]}, Z << zdd_xor(X, X). 1576% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z). 1577% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms), 1578% time((zdd X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))). 1579% ?- time((zdd Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))). 1580zdd_xor(X, Y, Z):-zdd_subtr(X, Y, A), 1581 zdd_subtr(Y, X, B), 1582 zdd_join(A, B, Z). 1583 1584% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S), 1585% zdd_meet(X, Y, B, S), 1586% zdd_subtr(A, B, Z, S).
Remark. The merge is associative and commutative, but not idempotent.
1595% ?- zdd(( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 1596% ?- time(zdd(( X<<pow(!charlist(a-z)), Y<<pow(:numlist(1, 26))))). 1597% ?- time(zdd(( X<<pow(:charlist($(a-z))), Y<<pow(:numlist(1, 26)), 1598% zdd_merge(X, Y, Z), U << zdd_meet(X, Z), card(X, C)))), C is 2^26. 1599 1600zdd_merge(0, _, 0):-!. 1601zdd_merge(_, 0, 0):-!. 1602zdd_merge(1, X, X):-!. 1603zdd_merge(X, 1, X):-!. 1604zdd_merge(X, Y, Z):- 1605 ( X > Y -> memo(zdd_merge(Y, X)-Z) 1606 ; memo(zdd_merge(X, Y)-Z) 1607 ), 1608 ( nonvar(Z) -> true 1609 ; cofact(X, t(A, L, R)), 1610 zdd_merge(L, Y, L0), 1611 zdd_merge(R, Y, R0), 1612 zdd_insert(A, R0, R1), 1613 zdd_join(L0, R1, Z) 1614 ). 1615% 1616 1617zdd_merge_list([], X, X). 1618zdd_merge_list([A|As], X, Y):- 1619 ( integer(A) -> zdd_merge(A, X, X0) 1620 ; zdd_insert(A, X, X0) % atom case 1621 ), 1622 zdd_merge_list(As, X0, Y).
1630zdd_disjoint_merge(0, _, 0):-!. 1631zdd_disjoint_merge(_, 0, 0):-!. 1632zdd_disjoint_merge(1, X, X):-!. 1633zdd_disjoint_merge(X, 1, X):-!. 1634zdd_disjoint_merge(X, Y, Z):- 1635 ( X @> Y -> memo(disj_merge(Y, X)-Z) 1636 ; memo(disj_merge(X, Y)-Z) 1637 ), 1638 ( nonvar(Z) -> true 1639 ; cofact(X, t(A, L, R)), 1640 cofact(Y, t(A0, L0, R0)), 1641 zdd_compare(C, A, A0), 1642 ( C= (<) -> 1643 zdd_disjoint_merge(L, Y, U), 1644 zdd_disjoint_merge(R, Y, V), 1645 cofact(Z, t(A, U, V)) 1646 ; C = (=) -> 1647 zdd_disjoint_merge(L, L0, U), 1648 zdd_disjoint_merge(L, R0, V), 1649 zdd_disjoint_merge(R, L0, W), 1650 zdd_join(V, W, P), 1651 cofact(Z, t(A, U, P)) 1652 ; zdd_disjoint_merge(X, L0, U), 1653 zdd_disjoint_merge(X, R0, V), 1654 cofact(Z, t(A0, U, V)) 1655 ) 1656 ). 1657 1658 1659% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1660% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1661%@ false. 1662% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1663% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1664% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1665% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1670zdd_subfamily(X, X):-!. 1671zdd_subfamily(0, _):-!. 1672zdd_subfamily(_, 0):-!, fail. 1673zdd_subfamily(1, X):-!, zdd_has_1(X). 1674zdd_subfamily(X, X0):- 1675 cofact(X, t(A, L, R)), 1676 cofact(X0, t(A0, L0, R0)), 1677 zdd_compare(C, A, A0), 1678 ( C = (=) -> 1679 zdd_subfamily(L, L0), 1680 zdd_subfamily(R, R0) 1681 ; C = (>), 1682 zdd_subfamily(X, L0) 1683 ). 1684 1685 /********************************* 1686 * division/residue in ZDD * 1687 *********************************/
zdd_divmod(X, Y, D, M, S),
psa(X, S), psa(D, S), psa(M, S).
1695zdd_divmod(X, Y, D, M):-
1696 zdd_div_div(X, Y, D1, D),
1697 zdd_subtr(X, D1, M).1703% ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S), 1704% psa(X, S), psa(D, S), psa(M, S). 1705zdd_divmod0(X, Y, D, M):- 1706 zdd_divisible(X, Y, D), 1707 zdd_subtr(X, D, M).
1713% ?- zdd X<< +[b], zdd_div_div(X, 1, D, M), psa(X), psa(D), psa(M). 1714% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), psa(X), psa(Y), psa(D), psa(M). 1715% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), 1716% psa(X), psa(Y), psa(D), psa(M). 1717% ?- zdd X<< +[*[a,b]], Y<< +[*[b]], psa(X), psa(Y), zdd_div_div(X, Y, D, M), 1718% psa(D), psa(M). 1719% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]], 1720% zdd_div_div(X, Y, D, D1), 1721% psa(D), psa(D1). 1722 1723zdd_div_div(0, _, 0, 0):-!. 1724zdd_div_div(1, X, Y, Y):-!, 1725 ( zdd_has_1(X) -> Y = 1 1726 ; Y = 0 1727 ). 1728zdd_div_div(_, 0, 0, 0):-!. 1729zdd_div_div(X, 1, X, X):-!. 1730zdd_div_div(X, Y, Z, U):- memo(div_div(X, Y)- P), 1731 ( nonvar(P) -> P = (Z, U) 1732 ; cofact(X, t(A, L, R)), 1733 zdd_div_div(L, Y, L0, U0), 1734 zdd_div_div(A, R, Y, R0, V0), 1735 zdd_join(L0, R0, Z), 1736 zdd_join(U0, V0, U), 1737 P = (Z, U) 1738 ). 1739% 1740zdd_div_div(_, 0, _, 0, 0):-!. 1741zdd_div_div(_, 1, 0, 0, 0):-!. % ??? 1742zdd_div_div(A, 1, 1, Z, Z):-!, zdd_singleton(A, Z). 1743zdd_div_div(_, _, 0, 0, 0):-!. 1744zdd_div_div(A, X, 1, Z, Z):-!, cofact(Z, t(A, 0, X)). 1745zdd_div_div(A, X, Y, Z, U):- cofact(Y, t(B, L, R)), 1746 zdd_compare(C, A, B), 1747 ( C = (<) -> 1748 zdd_div_div(X, Y, Z0, U0), 1749 zdd_insert(A, Z0, Z), 1750 zdd_insert(A, U0, U) 1751 ; C = (=) -> 1752 zdd_div_div(X, L, Z0, U0), 1753 zdd_insert(A, Z0, Z1), 1754 zdd_insert(A, U0, U1), 1755 zdd_div_div(X, R, Z2, U2), 1756 zdd_insert(A, Z2, Z3), % A is absorbed due to hit (A=B). 1757 zdd_join(Z1, Z3, Z), 1758 zdd_join(U1, U2, U) 1759 ; zdd_div_div(A, X, L, Z, U) 1760 ).
1766% ?- zdd(( X<< {[a]}, zdd_div(X, X, Z), psa(Z))). 1767% ?- zdd(( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1768% ?- zdd(( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))). 1769% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1770% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1771% ?- zdd(( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1772% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1773% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1774% ?- zdd(( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1775% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1776% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))). 1777% ?- zdd(( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1778% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1779% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1780% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))). 1781% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1782% ?- zdd(( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))). 1783% ?- zdd(( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1784% ?- zdd(( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1785% ?- zdd(( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))). 1786% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))). 1787% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1788% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1789 1790% 1791zdd_div(0, _, 0):-!. 1792zdd_div(1, X, Y):-!, 1793 ( zdd_has_1(X) -> Y = 1 1794 ; Y = 0 1795 ). 1796zdd_div(X, Y, Z):- memo(zdd_div(X, Y)- Z), 1797 ( nonvar(Z) -> true 1798 ; cofact(X, t(A, L, R)), 1799 zdd_div(L, Y, L0), 1800 zdd_div(A, R, Y, R0), 1801 zdd_join(L0, R0, Z) 1802 ). 1803% 1804zdd_div(_, _, 0, 0):-!. 1805zdd_div(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1806zdd_div(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1807 zdd_compare(C, A, B), 1808 ( C = (<) -> 1809 zdd_div(X, Y, Z0), 1810 cofact(Z, t(A, 0, Z0)) 1811 ; C = (=) -> 1812 zdd_div(X, L, L0), 1813 zdd_div(X, R, R0), 1814 cofact(Z, t(A, R0, L0)) 1815 ; zdd_div(A, X, L, Z) 1816 ).
1822% ?- zdd {N=10, numlist(1, N, Ns), numlist(1, 10, Js)}, X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z). 1823% ?- zdd X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1824% ?- zdd X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1825% ?- zdd X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1826% ?- zdd X<<pow([a, b, c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z). 1827 1828zdd_divisible(0, _, 0):-!. 1829zdd_divisible(1, X, Y):-!, 1830 ( zdd_has_1(X) -> Y = 1 1831 ; Y = 0 1832 ). 1833zdd_divisible(X, Y, Z):- memo(zdd_divisible(X, Y)- Z), 1834 ( nonvar(Z) -> true 1835 ; cofact(X, t(A, L, R)), 1836 zdd_divisible(L, Y, L0), 1837 zdd_divisible(A, R, Y, R0), 1838 zdd_join(L0, R0, Z) 1839 ). 1840% 1841zdd_divisible(_, _, 0, 0):-!. 1842zdd_divisible(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1843zdd_divisible(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1844 zdd_compare(C, A, B), 1845 ( C = (<) -> 1846 zdd_divisible(X, Y, Z0), 1847 cofact(Z, t(A, 0, Z0)) 1848 ; C = (=) -> 1849 zdd_divisible(X, L, L0), 1850 zdd_divisible(X, R, R0), 1851 zdd_join(L0, R0, Z0), 1852 cofact(Z, t(A, 0, Z0)) 1853 ; zdd_divisible(A, X, L, Z) 1854 ).
1859% ?- zdd X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1860% ?- zdd X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1861% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S). 1862% ?- zdd X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S). 1863% ?- N = 300, zdd numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns], 1864% time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S). 1865 1866% ?- zdd X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z). 1867 1868zdd_divisible_by_all(X, Y, X):-Y<2, !. % It was hard to find this. 1869zdd_divisible_by_all(X, _, 0):-X<2, !. % It was a little bit hard to find this. 1870zdd_divisible_by_all(X, Y, Z):- memo(div_by_all(X, Y)-Z), 1871 ( nonvar(Z) -> true 1872 ; cofact(X, t(A, L, R)), 1873 zdd_divisible_by_all(L, Y, L0), 1874 zdd_divisible_by_all(A, R, Y, R0), 1875 zdd_join(L0, R0, Z) 1876 ). 1877% 1878zdd_divisible_by_all(A, X, Y, Z):- Y<2, !, 1879 cofact(Z, t(A, 0, X)). 1880zdd_divisible_by_all(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1881 zdd_compare(C, A, B), 1882 ( C = (<) -> 1883 zdd_divisible_by_all(X, Y, Z0), 1884 zdd_insert(A, Z0, Z) 1885 ; C = (=) -> 1886 zdd_divisible_by_all(X, R, R1), 1887 zdd_insert(A, R1, R0), 1888 zdd_divisible_by_all(R0, L, Z) 1889 ; Z = 0 % It was hard to find this. 1890 ).
1894zdd_mod(X, Y, Z) :- zdd_divisible(Y, X, X0),
1895 zdd_subtr(X, X0, Z).1900% ?- zdd zdd_list(X, [[a]]), zdd_list(Y, [[a,c],[a,d]]), 1901% zdd_multiple(X, Y, Z), psa(Z). 1902% ?- zdd zdd_list(X, [[a,b]]), zdd_list(Y, [[a,c],[a,d]]), 1903% zdd_multiple(X, Y, Z), psa(Z). 1904% ?- zdd zdd_list(X, [[a,b]]), Y<<pow([a,b,c]), 1905% zdd_multiple(X, Y, Z), psa(Z). 1906% ?- zdd Y<<pow([a,b,c]), zdd_multiple(0, Y, Z), psa(Z). 1907% ?- zdd Y<<pow([a,b]), zdd_multiple(1, Y, Z), psa(Z). 1908 1909zdd_multiple(0, _, 0):-!. 1910zdd_multiple(1, Y, Y):-!. 1911zdd_multiple(_, Y, 0):-Y<2, !. 1912zdd_multiple(X, Y, Z):-memo(multiple(X, Y)-Z), 1913 ( nonvar(Z) -> true 1914 ; cofact(X, t(A, L, R)), 1915 zdd_multiple(L, Y, L0), 1916 zdd_multiple(A, R, Y, R0), 1917 zdd_join(L0, R0, Z) 1918 ). 1919% 1920zdd_multiple(_, _, Y, 0):- Y<2, !. 1921zdd_multiple(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1922 zdd_multiple(A, X, L, L0), 1923 zdd_compare(C, A, B), 1924 ( C = (<) -> R0 = 0 1925 ; C = (=) -> 1926 zdd_multiple(X, R, R1), 1927 zdd_insert(A, R1, R0) 1928 ; zdd_multiple(A, X, R, R1), 1929 zdd_insert(B, R1, R0) 1930 ), 1931 zdd_join(L0, R0, Z). 1932 1933 /********************************* 1934 * division/resudue in List * 1935 *********************************/
zdd_list(Y, U, Z), zdd_mod_by_list(X, U, Z, S).1941% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a], Y), psa(Y))). 1942% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [], Y), psa(Y))). 1943% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a, b], Y), psa(Y))). 1944% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [b,c], Y), psa(Y))). 1945% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [a,c], Y), psa(Y))). 1946% ?- zdd((X<<pow([a]), zdd_mod_by_list(X, [c], Y), psa(Y))). 1947% ?- N=100, numlist(1, N, Ns), numlist(1, N, Js), zdd((X<<pow(Ns), zdd_mod_by_list(X, Js, Z), card(Z, C))). 1948 1949zdd_mod_by_list(X, Y, Z):- zdd_divisible_by_list(X, Y, Z0), 1950 zdd_subtr(X, Z0, Z).
zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).1956% ?- zdd((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1957% ?- zdd((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1958 1959zdd_div_by_list(X, [], X):-!. 1960zdd_div_by_list(X, F, Y):- F=[A|As], 1961 ( X<2 -> Y = 0 1962 ; cofact(X, t(B, L, R)), 1963 zdd_div_by_list(L, F, L0), 1964 zdd_compare(C, B, A), 1965 ( C = (>) -> R0 = 0 1966 ; C = (=) -> 1967 zdd_div_by_list(R, As, R0) 1968 ; zdd_div_by_list(R, F, R1), 1969 zdd_insert(B, R1, R0) 1970 ), 1971 zdd_join(L0, R0, Y) 1972 ).
zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).1978% ?- zdd((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1979% ?- zdd((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1980 1981zdd_divisible_by_list(X, [], X):-!. 1982zdd_divisible_by_list(X, F, Y):- F=[A|As], 1983 ( X<2 -> Y = 0 1984 ; cofact(X, t(B, L, R)), 1985 zdd_divisible_by_list(L, F, L0), 1986 zdd_compare(C, B, A), 1987 ( C = (>) -> R0 = 0 1988 ; C = (=) -> zdd_divisible_by_list(R, As, R0) 1989 ; zdd_divisible_by_list(R, F, R0) 1990 ), 1991 cofact(Y, t(B, L0, R0)) 1992 1993 ). 1994 1995 1996 /********************* 1997 * meta on ZDD * 1998 *********************/ 1999% 2000% ?- zdd((X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2001% ?- zdd((X<<pow([1,2,4,5,6]), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2002% ?- N=2, numlist(1, N, L), zdd((X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2003% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2004% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2005% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2006% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N. 2007% ?- N=1000, numlist(1, N, L), zdd((X<<pow(L), 2008% 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.
2017:- meta_predicate map_zdd(,,). 2018 2019map_zdd(_, X, X):- X<2, !. 2020map_zdd(F, X, Y):- memo(map(X,F)-Y), 2021 ( nonvar(Y)-> true 2022 ; cofact(X, t(A, L, R)), 2023 map_zdd(F, L, L0), 2024 map_zdd(F, R, R0), 2025 call(F, A, B), 2026 zdd_insert(B, R0, R1), 2027 zdd_join(L0, R1, Y) 2028 ). 2029 2030% ?- zdd X<< (*[a,b,c]), psa(X). 2031% ?- zdd X<< (+[a,b]), psa(X). 2032% ?- zdd((X<<pow([a,b,c]), psa(X))). 2033% ?- zdd((prz(1))). 2034% ?- zdd((prz(0))). 2035% ?- zdd((mp(hello, 1))). 2036% ?- zdd((mp(hello, 0))).
2040prz(X):- print_set_at(X).2044mp(M, X) :- mpsa(M, X). 2045 2046mpsa(M, X):- writeln(M), 2047 print_set_at(X), 2048 writeln('-------------------'). 2049 2050% ?- sat(a+b), sat(b+c), psa. 2051psa :- b_getval(root, R), psa(R).
pow([a]), psa(X).
?- X<<{[a]}, psa(X).2058psa(X):- print_set_at(X), 2059 writeln('-------------------'). 2060% 2061psa(X, G):- print_set_at(X, G), 2062 writeln('-------------------').
Users/cantor/devel/zdd/prolog/zdd/zdd.pl2067print_set_at(0):-!, format("\szid = 0\n\t0\n"). 2068print_set_at(1):-!, format("\szid = 1\n\t[]\n"). 2069print_set_at(X):- format("\szid = ~w\n", [X]), 2070 forall(set_at(P, X), format("\t~w\n", [P])). 2071% 2072print_set_at(0, _):-!, format("\szid = 0\n\t0\n"). 2073print_set_at(1, _):-!, format("\szid = 1\n\t[]\n"). 2074print_set_at(X, G):- format("\szid = ~w\n", [X]), 2075 forall(set_at(P, X, G), format("\t~w\n", [P])). 2076 2077% ?- X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X). 2078% ?- X<<pow([1,2]), set_at(U, X), psa(X). 2079 2080% ?- zdd((X<<pow([1,2]), mp(powerset, X))). 2081set_at([], 1):-!. 2082set_at(P, X):- X>1, 2083 cofact(X, t(A, L, R)), 2084 ( set_at(P, L) 2085 ; set_at(As, R), 2086 P=[A|As] 2087 ). 2088% 2089set_at([], 1, _):-!. 2090set_at(P, X, G):- X>1, 2091 cofact(X, t(A, L, R), G), 2092 ( set_at(P, L, G) 2093 ; set_at(As, R, G), 2094 P=[A|As] 2095 ). 2096 2097% ?- zdd zdd_singleton(a, X), show_fos(X). 2098% ?- zdd X<< {[a,b], [b,c]}, show_fos(X). 2099% ?- zdd X<< pow([a,b]), show_fos(X).
2103show_fos(X):- X > 1, 2104 accessible_nodes(X, Ns), 2105 forall( member(M, Ns), 2106 ( cofact(M, T), 2107 writeln(M->T))). 2108% 2109accessible_nodes(X, Ns):- 2110 accessible_nodes(X, Ns0, []), 2111 sort(Ns0, Ns1), 2112 reverse(Ns1, Ns). 2113% 2114accessible_nodes(X, A, A):- X<2, !. 2115accessible_nodes(X, [X|A], B):- 2116 cofact(X, t(_, L, R)), 2117 accessible_nodes(L, A, A0), 2118 accessible_nodes(R, A0, B).
2124% ?- zdd((X<<pow([a,b,c]), zdd_list(X, Y), zdd_list(X0, Y))). 2125% ?- powerset([a,b,c], Y), zdd((zdd_list(X, Y), zdd_list(X, Y0), zdd_list(X0, Y0))), 2126% maplist(sort, Y, Y1), sort(Y1, Y2). 2127% 2128zdd_list(X, Y):- nonvar(X), !, zdd_sets(X, Y). 2129zdd_list(X, Y):- zdd_family(Y, X). 2130 2131% ?- zdd((X<<pow([a,b,c]), sets(X, P))). 2132% ?- zdd((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))). 2133% ?- zdd((X<<pow([]), sets(X, P))). 2134% ?- zdd((X<<pow([a]), sets(X, P))). 2135% ?- zdd((X<<pow(:numlist(1,3)), sets(X, Y))). 2136% ?- zdd((X<<pow([a,b,c]), sets(X, Y))). 2137% ?- zdd((X<<pow(:charlist($a, $c)), sets(X, Y))). 2138% ?- zdd((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))), sets(X, Y))).
2143sets(X, Y):- zdd_sets(X, Y0), zdd_sort(Y0, Y). 2144% 2145zdd_sets(1, [[]]):-!. 2146zdd_sets(0, []):-!. 2147zdd_sets(X, P):- 2148 cofact(X, t(A,L,R)), 2149 zdd_sets(L, Y), 2150 zdd_sets(R, Z), 2151 maplist(cons(A), Z, AZ), 2152 append(AZ, Y, P). 2153 2154% ?- zdd zdd_eval(pow([a, b, c, d, e, f]), I), eqns(I, X), 2155% maplist(writeln, X). 2156% 2157eqns(X, Y):- zdd_eqns(X, Y). 2158 2159basic_zdd(0). 2160basic_zdd(1). 2161 2162% % ?- zdd X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es). 2163% % ?- zdd X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es). 2164 2165% zdd_eqns(I, Es):- nonvar(I), var(Es), !, zdd_to_eqns(I, Es, []). 2166% zdd_eqns(I, Es):- var(I), nonvar(Es), !, 2167% ( check_eqns_for_zdd(Es) -> 2168% Es = [X=_|_], 2169% eqns_to_zdd(Es, X, I) 2170% ; throw('Violating-underlying-ordering-on-atoms.'(Es)) 2171% ). 2172% % 2173% zdd_to_eqns(I, X, Y):- zdd_to_eqns(I, X, [], S), 2174% zdd_sort(X, X1, S), 2175% reverse(X1, X). 2176% % 2177% zdd_to_eqns(I, X, X):- I<2, !. 2178% zdd_to_eqns(I, X, Y):- memo(visited(I)-F), 2179% ( nonvar(F) -> Y = X 2180% ; F = true, 2181% cofact(I, t(A, L, R)), 2182% X = [I=t(A, L, R)|X0], 2183% zdd_to_eqns(L, X0, X1), 2184% zdd_to_eqns(R, X1, Y) 2185% ). 2186% % 2187% check_eqns_for_zdd(Es):- are_eqns_closed(Es, Es), 2188% sort(Es, Fs), 2189% has_unique_left(Fs), 2190% sort(2, @=<, Es, Gs), 2191% has_unique_right(Gs). 2192% % 2193% are_eqns_closed([], _). 2194% are_eqns_closed([_ = t(A, L, R)|Rest], Es):- 2195% ( basic_zdd(L) -> true 2196% ; memberchk(L = t(B, _, _), Es), 2197% zdd_compare(<, A, B) 2198% ), 2199% ( basic_zdd(R) -> true 2200% ; memberchk(L = t(C, _, _), Es), 2201% zdd_compare(<, A, C) 2202% ), 2203% are_eqns_closed(Rest, Es). 2204% % 2205% eqns_to_zdd(_, 0, 0):-!. 2206% eqns_to_zdd(_, 1, 1):-!. 2207% eqns_to_zdd(Es, X, I):- memo(solve(X)-I), 2208% ( nonvar(I) -> true 2209% ; memberchk(X = t(A, L, R)), 2210% eqns_to_zdd(Es, L, L0), 2211% eqns_to_zdd(Es, R, R0), 2212% cofact(I, t(A, L0, R0)) 2213% ).
is_function([a-1,b-2,c-3]).
?- is_function([a-1,b-2,a-3]).2219is_function(X):- sort(X, Y), has_unique_left(Y). 2220% 2221has_unique_left([X,Y|Z]):-!, 2222 ( arg(1, X, A), arg(1, Y, A) -> false 2223 ; has_unique_left([Y|Z]) 2224 ). 2225has_unique_left(_).
2230% ?- check_one_to_one([a-1,b-2,c-3]). 2231% ?- check_one_to_one([a-1,b-2,c-1]). % false 2232 2233check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y). 2234% 2235has_unique_right([X,Y|Z]):-!, 2236 ( arg(2, X, A), arg(2, Y, A) -> false 2237 ; has_unique_right([Y|Z]) 2238 ). 2239has_unique_right(_).
ppoly(+X) is det.
Print X in polynomical form.2243ppoly(X):- poly_term(X, Poly), 2244 writeln(Poly). 2245 2246% ?- zdd((X<<pow([a,b]), poly_term(X, P))). 2247% ?- zdd((X<<pow([a,b,c]), poly_term(X, P))). 2248% ?- zdd((X<<(@a + @b), psa(X))). 2249 2250poly_term(X, Poly):- zdd_sets(X, Sets), 2251 get_compare(Pred), 2252 maplist(predsort(Pred), Sets, Sets0), 2253 predsort(Pred, Sets0, Sets1), 2254 poly_term0(Sets1, Poly). 2255 2256% ?- poly_term0([], Y). 2257% ?- poly_term0([[]], Y). 2258% ?- poly_term0([[a], [b]], Y). 2259% ?- poly_term0([[a*b], [c]], Y). 2260 2261poly_term0(X, Y):- maplist(mul_term, X, X0), 2262 sum_term(X0, Y). 2263% 2264mul_term([], 1):-!. 2265mul_term([X], X):-!. 2266mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 2267% 2268sum_term([], 0):-!. 2269sum_term([X], X):-!. 2270sum_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))).
2279zdd_rand_path(I):- zdd_rand_path(I, P, []), writeln(P). 2280% 2281zdd_rand_path(I, P):- zdd_rand_path(I, P, []). 2282% 2283zdd_rand_path(1, X, X):-!. 2284zdd_rand_path(I, X, Y):- I>1, 2285 cofact(I, t(A, L, R)), 2286 ( L == 0 -> 2287 X = [A|X0], 2288 zdd_rand_path(R, X0, Y) 2289 ; random(2) =:= 0 -> 2290 X = [A|X0], 2291 zdd_rand_path(R, X0, Y) 2292 ; zdd_rand_path(L, X, Y) 2293 ).
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).2302zdd_atoms(X, []):- X<2, !. 2303zdd_atoms(X, P):- memo(atoms(X)-P), 2304 ( nonvar(P) -> true 2305 ; cofact(X, t(A, L, R)), 2306 zdd_atoms(L, Al), 2307 zdd_atoms(R, Ar), 2308 ord_union(Al, Ar, P0), 2309 P=[A|P0] 2310 ). 2311 2312% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 2313:- meta_predicate delete(, , ). 2314delete(X, Y, Z):- delete(X, Y, Z, []). 2315 2316:- meta_predicate delete(, , , ). 2317delete(_, [], L, L). 2318delete(Pred, [X|Xs], L, L0):- 2319 ( call(Pred, X) 2320 -> delete(Pred, Xs, L, L0) 2321 ; L = [X|L1], 2322 delete(Pred, Xs, L1, L0) 2323 ). 2324 2325% ?- zdd((zdd_power([a,b], R), sets(R, U))). 2326% ?- zdd((X<< zdd_power(:charlist($(a-c))), sets(X, U))). 2327% ?- zdd((R<< pow(: !charlist(a-d)), card(R, C))). 2328%% 2329zdd_power(X, Y):- zdd_sort(X, X0), 2330 zdd_ord_power(X0, 1, Y).
zdd_ord_power([a,b], 1, X), psa(X).2335zdd_ord_power([], P, P). 2336zdd_ord_power([X|Xs], P, Q):- zdd_ord_power(Xs, P, R), 2337 cofact(Q, t(X, R, R)).
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.2345% ?- atomlist(ax(1+1, 3+1), As). 2346% ?- atomlist(ax(1, 3), As). 2347atomlist(X, As):- X=..[A, I, J], 2348 I0 is I, 2349 J0 is J, 2350 findall(Y, ( between(I0, J0, K), 2351 atom_concat(A, K, Y) 2352 ), 2353 As).
2359% ?- charlist(a-c, X). 2360charlist(A-B, I):- 2361 findall(X, ( char_type(X, alnum), 2362 X @>= A, 2363 X @=< B 2364 ), 2365 I).
charlist(A-B, X).
?- charlist(a, c, X).
@ X = [a, b, c].2371charlist(A, B, I):- charlist(A-B, I). 2372 2373% ?- term_atoms(a+b=c, L). 2374% ?- term_atoms(a+b, L). 2375% ?- term_atoms(f(a+a), L).
2381term_atoms(X, L):- term_atoms(X, L0, []), 2382 sort(L0, L). 2383 2384% 2385term_atoms(X, L, L):- var(X), !. 2386term_atoms(X, [X|L], L):- atom(X), !. 2387term_atoms([X|Y], L, L0):-!, 2388 term_atoms(X, L, L1), 2389 term_atoms(Y, L1, L0). 2390term_atoms(X, L, L0):- compound(X), !, 2391 X =..[_|As], 2392 term_atoms(As, L, L0). 2393term_atoms(_, L, L). 2394 2395% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 2396% ?- subst_opp(a, X, [b-a]). 2397% ?- subst_opp([a], X, [b-a]). 2398 2399subst_opp(X, Y, L):- memberchk(Y-X, L). 2400subst_opp([X|Y], [X0|Y0], L):-!, 2401 subst_opp(X, X0, L), 2402 subst_opp(Y, Y0, L). 2403subst_opp(X, Y, L):- compound(X), !, 2404 X =..[F|As], 2405 subst_opp(As, Bs, L), 2406 Y =..[F|Bs]. 2407subst_opp(X, X, _). 2408 2409% ?- subst_term(f(a), R, [a-b]). 2410% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 2411% ?- subst_term(f(a), R, [a-X]). 2412% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2413% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2414% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
2420subst_term(X, Y):- member(X0-Y), X0==X, !. 2421subst_term(A, B):- compound(A), !, 2422 ( A = [X|Y] -> 2423 B = [X0|Y0], 2424 subst_term(X, X0), 2425 subst_term(Y, Y0) 2426 ; functor(A, F, N), 2427 functor(B, F, N), 2428 subst_term(N, A, B) 2429 ). 2430subst_term(X, X). 2431% 2432subst_term(0, _, _):-!. 2433subst_term(I, X, Y):- 2434 arg(I, X, A), 2435 arg(I, Y, B), 2436 subst_term(A, B), 2437 J is I - 1, 2438 subst_term(J, X, Y). 2439 2440% ?- all_instances([a,b], [0,1], a+b=b, R). 2441% ?- all_instances([x,y], [0,1], x+y=x, R). 2442%! all_instances(+As, +Vs, +X, -Y) is det. 2443% Unify Y with the list of possible variations P of X, 2444% where P is a variation of X if for each A in As with some 2445% V in Vs which depends on A, P is obtained from X by replacing 2446% all occurrences of A appearing in X with V for A in As. 2447 2448all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 2449 apply_maps(Fs, X, Y, []). 2450% 2451apply_maps([], _, Y, Y). 2452apply_maps([F|Fs], X, [X0|Y], Z):- 2453 subst_term(X, X0, F), 2454 apply_maps(Fs, X, Y, Z). 2455 2456% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 2457% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 2458% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 2459% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 2460%! mod_table(+M, +X, +E, -T) is det. 2461% Unify T with a set of form E' = V where 2462% E' is a possible ground instance of an integer expression E 2463% and V is the value of E' with modulo M, where X is a set of 2464% parameters appearing in E. 2465 2466mod_table(M, Xs, Exp, Table):- M0 is M-1, 2467 numlist(0, M0, V), 2468 all_instances(Xs, V, Exp, Exps), 2469 !, 2470 maplist(mod_arith(M), Exps, Table). 2471% 2472mod_arith(M, Exp, Exp=V):- V is Exp mod M. 2473 2474% 2475unify_all([]). 2476unify_all([_]). 2477unify_all([X,Y|Z]):- zdd:(X=Y), unify_all([Y|Z]). 2478 2479% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 2480% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 2481% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 2482% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 2483% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 2484% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
2489% ?- zdd((X <<{[a,b], [a,c]}, zdd_appear(e, X))). % false 2490% ?- zdd((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X))). % false 2491% ?- zdd((X <<(*[a,b]+ *[a,c]), psa(X), zdd_appear(c, X))). 2492% ?- numlist(1, 10000, Ns), zdd((X<<pow(Ns), zdd_appear(10000, X))). 2493% ?- zdd X<<pow(:numlist(1, 10000)), zdd_appear(10000, X). 2494%@ X = 10001. 2495 2496zdd_appear(A, X):- use_memo(zdd_atom_appear(A, X)). 2497 2498zdd_atom_appear(A, X):- X > 1, 2499 memo(visited(X)-B), 2500 var(B), 2501 cofact(X, t(U,L,R)), 2502 zdd_compare(C, A, U), 2503 ( C = (=) -> true 2504 ; C = (>), 2505 ( zdd_atom_appear(A, L) -> true 2506 ; L < 2 -> 2507 zdd_atom_appear(A, R) 2508 ; memo(visited(L)-true), % for earlier fail. 2509 zdd_atom_appear(A, R) 2510 ) 2511 ).
2516zdd_singleton(X, P):- cofact(P, t(X, 0, 1)).2521zdd_has_1(1):-!. 2522zdd_has_1(X):- X>1, 2523 cofact(X, t(_, L, _)), 2524 zdd_has_1(L).
zdd((U<<{[a]}, P<<pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q))).2535zdd_subst(_, _, X, X, _):- X<2, !. 2536zdd_subst(X, U, P, Q):- memo(zdd_subst(X, U, P)-Q), 2537 ( nonvar(Q) -> true 2538 ; cofact(P, t(Y, L, R)), 2539 zdd_subst(X, U, L, L0), 2540 zdd_compare(C, X, Y), 2541 ( C = (=) -> zdd_merge(U, R, R0) 2542 ; C = (<) -> bdd_cons(R0, Y, R) 2543 ; zdd_subst(X, U, R, R1), 2544 zdd_insert(Y, R1, R0) 2545 ), 2546 zdd_join(L0, R0, Q) 2547 ). 2548 2549 /*********************** 2550 * product on zdd * 2551 ***********************/ 2552 2553% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))). 2554% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y))). 2555% ?- zdd((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))). 2556% ?- zdd((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))). 2557% ?- time(zdd((X<<pow(:numlist(1,16)), Z<<(X**X), card(Z, C)))). 2558% ?- N is 10000, time( ( zdd X<<pow(:numlist(1,N)), card(X, _C))), _C =:= 2^N. 2559% ?- call_with_time_limit(120, (numlist(1, 16, R), 2560% time(zdd((X<<pow(R), Z<<(X**X), card(Z, C)))))). 2561 2562% 2563zdd_product(X, Y, 0):- (X<2; Y<2), !. 2564zdd_product(X, Y, Z):- memo(prod(X, Y)-Z), 2565 ( nonvar(Z) -> true % , write(.) % hits found. 2566 ; zdd_product(X, Y, [], Bs, 0, Z0), 2567 append_pairs_list(X, Bs, Z1), 2568 zdd_join(Z0, Z1, Z) 2569 ). 2570% 2571zdd_product(_, X, Bs, Bs, Z, Z):- X<2, !. 2572zdd_product(X, Y, Bs, Q, U, V):- cofact(Y, t(B, L, R)), 2573 zdd_product(X, L, L0), 2574 zdd_join(L0, U, U0), 2575 zdd_product(X, R, [B|Bs], Q, U0, V). 2576% 2577append_pairs_list(X, _, X):- X<2, !. 2578append_pairs_list(X, Bs, U):- cofact(X, t(A, L, R)), 2579 append_pairs_list(R, Bs, R0), 2580 append_pairs_list(L, Bs, L0), 2581 insert_pairs(A, Bs, R0, R1), 2582 zdd_join(L0, R1, U). 2583 2584% 2585insert_pairs(_, [], U, U):-!. 2586insert_pairs(A, [B|Bs], U, V):- 2587 zdd_insert((A-B), U, U0), 2588 insert_pairs(A, Bs, U0, V). 2589 2590 /************************* 2591 * Quotient on ZDD * 2592 *************************/
?- 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))).
2601zdd_insert(_, 0, 0):-!. 2602zdd_insert(A, 1, J):-!, zdd_singleton(A, J). 2603zdd_insert(A, I, J):- memo(insert(A, I)-J), 2604 ( nonvar(J) -> true 2605 ; cofact(I, t(X, L, R)), 2606 zdd_compare(C, A, X), 2607 ( C = (=) -> 2608 zdd_join(L, R, K), 2609 cofact(J, t(X, 0, K)) 2610 ; C = (<) -> 2611 cofact(J, t(A, 0, I)) 2612 ; zdd_insert(A, L, L0), 2613 zdd_insert(A, R, R0), 2614 cofact(J, t(X, L0, R0)) 2615 ) 2616 ). 2617 2618% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), 2619% psa(X, S), psa(Y, S), 2620% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S). 2621 2622% ?- zdd X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S), 2623% psa(Y, S). 2624% ?- listing(zdd_insert). 2625 2626:- meta_predicate zdd_insert(, , , ). 2627zdd_insert(_, _, 0, 0):-!. 2628zdd_insert(_, A, 1, Y):-!, zdd_singleton(A, Y). 2629zdd_insert(F, A, X, Y):- memo(zdd_insert(X, A, F)-Y), 2630 ( nonvar(Y) -> true % , write(.) % many hits 2631 ; cofact(X, t(B, L, R)), 2632 zdd_insert(F, A, L, L0), 2633 call(F, C, A, B), 2634 ( C = (=) -> bdd_cons(R0, A, R) 2635 ; C = (<) -> bdd_append([A, B], R, R0) 2636 ; zdd_insert(F, A, R, R1), 2637 bdd_cons(R0, B, R1) 2638 ), 2639 zdd_join(L0, R0, Y) 2640 ). 2641 2642% ?- zdd((family([[a, b],[b]], X), sets(X, Sx), 2643% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
2648% ?- numlist(1, 10000, Ns), zdd((zdd_insert_atoms(Ns, 1, X), psa(X))). 2649 2650% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))). 2651% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))). 2652zdd_insert_atoms(X, Y, Z):- zdd_sort(X, X0), 2653 zdd_ord_insert(X0, Y, Z). 2654 2655% 2656zdd_ord_insert(_, 0, 0):-!. 2657zdd_ord_insert([], X, X):-!. 2658zdd_ord_insert(As, 1, Y):-!, bdd_append(As, 1, Y). 2659zdd_ord_insert(As, X, Y):- memo(ord_insert(X, As)-Y), 2660 ( nonvar(Y) -> true % , write(.) % many hits. 2661 ; As = [A|U], 2662 cofact(X, t(B, L, R)), 2663 zdd_compare(C, A, B), 2664 ( C = (<) -> 2665 zdd_ord_insert(U, X, Y0), 2666 cofact(Y, t(A, 0, Y0)) 2667 ; C = (=) -> 2668 zdd_ord_insert(U, L, L1), 2669 zdd_ord_insert(U, R, R1), 2670 zdd_join(R1, L1, Y0), 2671 cofact(Y, t(A, 0, Y0)) 2672 ; zdd_ord_insert(As, L, L1), 2673 zdd_ord_insert(As, R, R1), 2674 cofact(Y, t(B, L1, R1)) 2675 ) 2676 ). 2677 2678 2679% ?- X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y), psa(Y). 2680:- meta_predicate zdd_reorder(, , ). 2681zdd_reorder(_, X, X):- X<2, !. 2682zdd_reorder(F, X, Y):- cofact(X, t(A, L, R)), 2683 zdd_reorder(F, L, L0), 2684 zdd_reorder(F, R, R1), 2685 zdd_insert(F, A, R1, R0), 2686 zdd_join(L0, R0, Y). 2687 2688 2689 /***************** 2690 * filters * 2691 *****************/ 2692 2693% ?- zdd X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y), psa(Y). 2694% ?- zdd X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y), psa(Y). 2695% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y), psa(Y). 2696% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([1, 3], X, Y), psa(Y). 2697% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y), psa(Y). 2698% ?- zdd { numlist(1, 1000, Ns) }, X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y), card(Y, C), 2699% card(X, D), zdd_compare(E, C, D), {U is D-C}. 2700 2701% 2702ltr_meet_filter([], X, X):-!. 2703ltr_meet_filter([A|F], X, Y):- 2704 ltr_filter(A, X, X0), 2705 ltr_meet_filter(F, X0, Y). 2706 2707% ?- X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y), psa(Y). 2708% ?- X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y), psa(Y). 2709ltr_join_filter(F, X, Y):- 2710 ltr_join_filter(F, X, 0, Y). 2711% 2712ltr_join_filter([], _, Y, Y):-!. 2713ltr_join_filter([P|F], X, Y, Y0):-!, 2714 ltr_filter(P, X, Y1), 2715 zdd_join(Y, Y1, Y2), 2716 ltr_join_filter(F, X, Y2, Y0). 2717 2718% 2719ltr_filter(-A, X, Y):-!, ltr_filter_negative(A, X, Y). 2720ltr_filter(A, X, Y):- ltr_filter_positive(A, X, Y). 2721 2722% 2723ltr_filter_negative(_, X, X):- X<2, !. 2724ltr_filter_negative(A, X, Y):- memo(letral_neg(X, A)-Y), 2725 ( nonvar(Y) -> true 2726 ; cofact(X, t(B, L, R)), 2727 ltr_filter_negative(A, L, L0), 2728 zdd_compare(C, A, B), 2729 ( C = (=) -> R0 = 0 2730 ; C = (<) -> R0 = R 2731 ; ltr_filter_negative(A, R, R0) 2732 ), 2733 cofact(Y, t(B, L0, R0)) 2734 ). 2735% 2736ltr_filter_positive(_, X, 0):- X<2, !. 2737ltr_filter_positive(A, X, Y):- memo(ltr_pos(X, A)-Y), 2738 ( nonvar(Y) -> true 2739 ; cofact(X, t(B, L, R)), 2740 ltr_filter_positive(A, L, L0), 2741 zdd_compare(C, A, B), 2742 ( C = (=) -> R0 = R 2743 ; C = (<) -> R0 = 0 2744 ; ltr_filter_positive(A, R, R0) 2745 ), 2746 cofact(Y, t(B, L0, R0)) 2747 ). 2748 2749% ?- zdd((X<<pow([a,b,c]), dnf_filter([[-b,-c]], X, Y), psa(Y))). 2750% ?- zdd((X<<pow([a,b]), dnf_filter([[b]], X, Y), psa(Y))). 2751% ?- zdd((X<<pow([a,b]), dnf_filter([[a,b]], X, Y), psa(Y))). 2752% ?- zdd((X<<pow([a,b]), dnf_filter([], X, Y), psa(Y))). 2753% ?- zdd((X<<pow([a,b,c]), dnf_filter([[c]], X, Y), psa(Y))). 2754% ?- zdd((X<<pow([a,b,c]), dnf_filter([], X, Y), psa(Y))). 2755% ?- zdd((X<<pow([a,b,c]), dnf_filter([[a],[-c]], X, Y), psa(Y))). 2756 2757dnf_filter(DNF, X, Y):- dnf_filter(DNF, X, 0, Y). 2758% 2759dnf_filter([], _, Y, Y, _). 2760dnf_filter([F|Fs], X, Y, Z):- 2761 ltr_meet_filter(F, X, X0), 2762 zdd_join(X0, Y, Y0), 2763 dnf_filter(Fs, X, Y0, Z). 2764 2765% ?- zdd((X<<pow([a,b,c]), cnf_filter([[-b,-c]], X, Y), psa(Y))). 2766% ?- zdd((X<<pow([a,b,c]), cnf_filter([[-a, -b, -c]], X, Y), psa(Y))). 2767cnf_filter([], X, X). 2768cnf_filter([F|Fs], X, Y):- 2769 ltr_join_filter(F, X, X0), 2770 cnf_filter(Fs, X0, Y). 2771 2772% 2773zdd_meet_list([A], A):-!. 2774zdd_meet_list([A|As], B):- zdd_meet_list(As, A, B). 2775% 2776zdd_meet_list([], X, X). 2777zdd_meet_list([A|As], X, Y):- zdd_meet(A, X, X0), 2778 zdd_meet_list(As, X0, Y). 2779% 2780zdd_join_list([], 0):-!. 2781zdd_join_list([X|Xs], Y):- zdd_join_list(Xs, X, Y). 2782% 2783zdd_join_list([], X, X):-!. 2784zdd_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2785 zdd_join_list(As, X0, Y). 2786 2787% 2788ltr_join_list([], 0):-!. 2789ltr_join_list([X|Xs], Y):-ltr_join_list(Xs, X, Y). 2790% 2791ltr_join_list([], X, X):-!. 2792ltr_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2793 ltr_join_list(As, X0, Y). 2794 2795 2796 /********************* 2797 * remove atom * 2798 *********************/
2804% ?- zdd((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2805% sets(Y, Sy))). 2806zdd_remove(X, Y, Z, S):- setup_call_cleanup( 2807 open_state(M, [hash_size(256)]), 2808 zdd_remove(X, Y, Z, S, M), 2809 close_state(M)). 2810 2811zdd_remove(_, X, X, _, _):- X<2, !. 2812zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2813 ( nonvar(J) -> true 2814 ; cofact(I, t(Ai, Li, Ri), S), 2815 zdd_compare(C, A, Ai, S), 2816 ( C = (<) -> J = I 2817 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2818 zdd_remove(A, Ri, Ria, S, M), 2819 cofact(J, t(Ai, Lia, Ria), S) 2820 ; zdd_join(Li, Ri, J, S) 2821 ) 2822 ). 2823 2824% ?- ltr_zdd X<< dnf(a->b), psa(X), 2825% use_table(pred_remove_atoms(negative_literal, X, Y)), psa(Y). 2826 2827% ?- ltr_zdd X<< dnf(a->b->c), psa(X), 2828 2829negative_literal(-(_)). 2830 2831:- meta_predicate pred_remove_atoms(, , ). 2832 2833pred_remove_atoms(_, X, X):- X<2, !. 2834pred_remove_atoms(Pred, I, J):- 2835 cofact(I, t(A, L, R)), 2836 pred_remove_atoms(Pred, L, L0), 2837 pred_remove_atoms(Pred, R, R0), 2838 ( call(Pred, A) -> 2839 zdd_join(L0, R0, J) 2840 ; cofact(J, t(A, L0, R0)) 2841 ). 2842 2843 /********************* 2844 * Cardinality * 2845 *********************/
2850% ?-N = 10000, numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:=2^N. 2851%@ % 1,222,118 inferences, 0.127 CPU in 0.161 seconds (79% CPU, 9587871 Lips) 2852%@ N = 10000, 2853%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2854%@ X = 10001. 2855 2856%@ % 1,204,213 inferences, 0.179 CPU in 0.220 seconds (82% CPU, 6710726 Lips) 2857%@ N = 10000, 2858%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2859%@ X = 10001. 2860 2861% ?- zdd X<<{[a], [b]}, card(X, C). 2862% ?- N = 10000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), card(X, C))). 2863%@ % 1,222,117 inferences, 0.112 CPU in 0.127 seconds (89% CPU, 10886196 Lips) 2864%@ N = 10000, 2865%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2866%@ X = 10001, 2867 2868% ?- X<<card(pow([a,b]) + pow([c,d])). 2869%@ X = 7. 2870% ?- X<<card((+[a]) + (+[b])). 2871 2872% ?- X<<pow(numlist(1, 100)), card(X, D), 2873% zdd_gc(X, X1), zdd_gc(X1, X2), zdd_gc(X2, Y), 2874% card(Y, C). 2875%@ X = X1, X1 = X2, X2 = Y, Y = 101, 2876%@ D = C, C = 1267650600228229401496703205376. 2877 2878card(I, C):- use_memo(cardinality(I,C)). 2879% 2880cardinality(I, I):- I < 2, !. 2881cardinality(I, C):- memo(card(I)-C), 2882 ( nonvar(C) -> true 2883 ; cofact(I, t(_, L, R)), 2884 cardinality(R, Cr), 2885 cardinality(L, Cl), 2886 C is Cl + Cr 2887 ).
2891max_length(X, Max):- use_memo(max_length_with_memo(X, Max)). 2892 2893% 2894max_length_with_memo(X, 0):- X<2, !. 2895max_length_with_memo(X, Max):- 2896 memo(max(X)-Max), 2897 cofact(X, t(_, L, R)), 2898 ( nonvar(Max) -> true 2899 ; max_length_with_memo(L, ML), 2900 max_length_with_memo(R, MR), 2901 Max is max(1 + MR, ML) 2902 ). 2903 2904 /*********************** 2905 * Handy helpers * 2906 ***********************/ 2907 2908% 2909unify_zip([]). 2910unify_zip([X-X|R]):- unify_zip(R). 2911 2912 2913 /****************************************** 2914 * Oprations on clauses of literals * 2915 ******************************************/ 2916 2917% ?- ltr_compare(C, a, -a). 2918% ?- ltr_compare(C, -(a), a). 2919% ?- ltr_compare(C, -(b), a). 2920% ?- ltr_compare(C, -(a), b). 2921% ?- ltr_compare(C, -(a), -(b)). 2922% ?- ltr_compare(C, -(a), -(a)).
2929ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 2930ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 2931 ( C0 == (=) -> C =(<) 2932 ; C0 = C 2933 ). 2934ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 2935 ( C0 == (=) -> C = (>) 2936 ; C0 = C 2937 ). 2938ltr_compare(C, X, Y):- compare(C, X, Y). 2939 2940% ?- zdd {ltr_compare(C, a, b)}. 2941% ?- zdd {ltr_compare(C, -a, a)}. 2942% ?- zdd {ltr_compare(C, a, -a)}. 2943% ?- zdd {ltr_compare(C, -a, b)}. 2944% ltr_compare(C, X, Y, S):- get_compare(F, S), 2945% call(F, C, X, Y).
2950% ?- ltr_sort([b, b, a], X).
2951% ?- ltr_sort([-b, b,-b, -a], X).
2956ltr_sort(X, Y):- get_compare(F), predsort(F, X, Y). 2957 2958 2959% ?- zdd((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false 2960% ?- zdd((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))). 2961% 2962ltr_memberchk(L, Z):- ltr_sort(L, L0), 2963 ltr_ord_memberchk(L0, Z). 2964% 2965ltr_ord_memberchk([], Z):- !, zdd_has_1(Z). 2966ltr_ord_memberchk([A|As], Z):- Z > 1, 2967 cofact(Z, t(B, L, R)), 2968 ltr_compare(C, A, B), 2969 ( C = (=) -> ltr_ord_memberchk(As, R) 2970 ; ltr_ord_memberchk([A|As], L) 2971 ). 2972 2973% ?- call_with_time_limit(100, time(zdd((big_normal_form(30, X), resolve(X))))). 2974% ?- big_normal_form(1, X), ltr_card(X, C). 2975% ?- big_normal_form(2, X), ltr_card(X, C). 2976% ?- big_normal_form(3, X), ltr_card(X, C). 2977% ?- big_normal_form(10, X), ltr_card(X, C). 2978% ?- big_normal_form(20, X), ltr_card(X, C). 2979% ?- time(((big_normal_form(100, X), ltr_card(X, C)))). 2980% ?- time(((big_normal_form(10, X), ltr_card(X, C)))). 2981% ?- N=100, time((big_normal_form(N, X), ltr_card(X, C))), C=:=2^N. 2982 2983big_normal_form(0, 1). 2984big_normal_form(N, X):- N>0, 2985 N0 is N-1, 2986 big_normal_form(N0, X0), 2987 ltr_insert(N, X0, R), 2988 ltr_insert(-N, X0, L), 2989 zdd_join(L, R, X). 2990 2991% ?- numlist(1, 3, Ns), ( ltr_zdd X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 2992% ?- numlist(1, 20, Ns), (ltr_zdd X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 2993% ?- ltr_zdd X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y). 2994% ?- ltr_zdd X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 2995% ltr_choices(Z, U), psa(X), psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V). 2996% ?- ltr_zdd X<< {[a,b]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 2997% ?- ltr_zdd X<< {[a,b,c]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 2998% ?- ltr_zdd X<< {[a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 2999% ?- ltr_zdd X<< {[], [a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 3000% ?- ltr_zdd X<< {[a], [c, d]}, ltr_choices(X, Y), psa(Y). 3001% ?- ltr_zdd X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y). 3002% ?- ltr_zdd X<< {[a,b]}, ltr_choices(X, Y), psa(Y). 3003% ?- ltr_zdd X<< {[]}, ltr_choices(X, Y), psa(Y). 3004% ?- ltr_zdd cnf(a, X), ltr_choices(X, Y), psa(Y). 3005% ?- ltr_zdd cnf(a*b, X), ltr_choices(X, Y), psa(Y). 3006% ?- ltr_zdd cnf(a* (-a), X), ltr_choices(X, Y), psa(Y). 3007 3008% ?- N=10, numlist(2, 10, Ns), (ltr_zdd sample_cnf(Ns, X), ltr_card(X, C)). 3009% ?- N=100, numlist(2, N, Ns), (ltr_zdd sample_cnf(Ns, X), card(X, C), resolve(X)). 3010 3011sample_cnf([], 1). 3012sample_cnf([J|Js], X):- sample_cnf(Js, Y), 3013 ltr_insert(J, Y, Z), 3014 ltr_insert(-J, Y, U), 3015 ltr_join(Z, U, X).
3021accessible_indices(I, A):- zdd_vector(Vec), 3022 accessible_indices(I, A0, [], Vec), 3023 sort(A0, A). 3024 3025accessible_indices(I, A, A, _):- I<2, !. 3026accessible_indices(I, [I|A], B, Vec):- arg(I, Vec, X), 3027 ( atomic(X) -> B = A 3028 ; child_term_indices(X, A, B, Vec) 3029 ). 3030% 3031% child_term_indices(t(_, _, _), A, A, _):-!. 3032child_term_indices(X, A, B, Vec):- X =.. [_|Xs], 3033 child_term_indices_list(Xs, A, B, Vec). 3034% 3035child_term_indices_list([], A, A, _). 3036child_term_indices_list([I|Is], A, B, Vec):- 3037 accessible_indices(I, A, C, Vec), 3038 child_term_indices_list(Is, C, B, Vec). 3039 3040% test sat. PASSED. [2023/11/09] 3041% ?- sat. 3042% ?- sat(-true). % false 3043% ?- sat(a+b), sat_count(C). 3044% ?- sat(a), sat(b). 3045% ?- sat(-(a + -a)). % false 3046% ?- sat(a), sat(b), sat_count(C). 3047% ?- sat(or(a, b)), sat_count(C). 3048% ?- sat(b), sat_count(C). 3049% ?- sat(xor(a, b)), sat_count(C). 3050% ?- sat(exor(a, b)), sat_count(C). 3051% ?- sat(e_x_o_r(a, b)), sat_count(C). 3052% ?- sat(a), sat(-a). % false. 3053% ?- sat(a), sat(a+b), sat_count(C). 3054% ?- sat(a(1)+a(2)), sat_count(C). 3055% ?- sat(A+a(2)), sat_count(C). 3056% ?- sat(A + B), sat_count(C). 3057% ?- sat(a+b+c+d), sat_count(C). 3058% ?- sat(a+b), sat(c+d), sat_count(C). 3059% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 3060% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 3061% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false. 3062% ?- sat(*[p(1),p(2)]), sat_count(C). 3063% ?- sat(+[p(1),p(2)]), sat_count(C). 3064% ?- N=10, findall(p(I, J), 3065% (between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C). 3066% ?- N=10, findall(p(I, J), 3067% (between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C). 3068% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false 3069% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 3070% ?- sat(A + B), sat_count(C). 3071% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 3072% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 3073% ?- sat(a=<(b=<a)), sat_count(Count). 3074% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3075% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3076% ?- Prop = 3077% ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)), 3078% sat(Prop), sat_count(C). 3079% ?- sat(a+b), sat(b+c), b_getval(sat_state, S), 3080% get_key(root, R, S), ltr_card(R, C, S). 3081% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false 3082% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false 3083% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa. 3084% ?- sat(A=:=B), psa, sat(B=:=C), psa. 3085% ?- sat(a), sat(b), sat(c), sat_count(C). 3086% ?- Prop = 3087% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3088% sat(Prop), 3089% sat_count(Count). 3090% ?- Prop = 3091% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3092% sat(-Prop), 3093% sat_count(Count). 3094% ?- sat(a), psa. 3095% ?- sat(a->(b->a)), sat(a->(b->a)), sat_count(C). 3096% ?- sat(A->(B->A)), sat(A->(B->A)), sat_count(C). 3097% ?- sat(a), sat(b), sat_count(C), psa. 3098% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3099% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3100% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3101% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3102% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3103% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C). 3104% ?- sat. 3105% ?- sat(a+b+c), sat_count(C). 3106% ?- sat(x=a+b), sat(y=a+b+b+a), sat(-(x=y)), sat_count(C). % false 3107% ?- sat(x=a+b), sat(y=a+b+b+a), sat((x=y)), sat_count(C). 3108 3109% Setting ZDD Mode. 3110zdd:- open_state. 3111sat:- open_state, 3112 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3113 nb_linkval(zdd_compare, ltr_compare), 3114 nb_linkval(root, 1). 3115ltr:- open_state, 3116 nb_linkval(zdd_compare, ltr_compare), 3117 nb_set_key(varnum, 0), 3118 nb_set_key(atom_index, 0). 3119% 3120sat(X):- 3121 b_getval(root, Root), 3122 dnf(X, Y), 3123 ltr_merge(Y, Root, Root0), 3124 b_setval(root, Root0), 3125 Root0 \== 0. 3126% 3127sat_close:- close_state. 3128% 3129sat_count(C):- b_getval(root, X), ltr_card(X, C). 3130% 3131sat_clear:- close_state. 3132% 3133zdd_numbervars(X):- get_key(varnum, N), 3134 numbervars(X, N, N0), 3135 set_key(varnum, N0). 3136 3137% ?- heavy_valid_formula(H), prove(H). 3138heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10) 3139<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3140<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10) 3141<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3142<=> p2) <=> p1) <=> p0)). 3143 3144% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y). 3145% ?- mk_left_assoc_term(=, 1, X), prove(X). 3146 3147% ?- ltr_zdd X<< {[a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3148% ?- ltr_zdd X<< {[a,b],[b,c]}, ltr_merge(X, X, Z), psa(Z). 3149% ?- zdd X<< {[a,b],[b,c]}, zdd_merge(X, X, Z), psa(Z). 3150% ?- ltr_zdd X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3151% ?- run(1, 100). 3152% ?- run(2, 100). 3153% ?- run(5, 100). 3154% ?- run(1-9, 100). 3155% ?- run(11, 100). 3156% ?- run(12, 360). 3157%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips) 3158% imac 3159% on M1 mbp pro 32 GB, timeout. 3160 3161% ?- mk_left_assoc_term(==, 1, F), prove(F). 3162 3163run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3164 ( mk_left_assoc_term(==, K, F), 3165 format("~nPropositions: p(0) ... p(~w).~n", [K]), 3166 call_with_time_limit(T_limit, time(prove(F))))). 3167 3168% run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3169% ( mk_left_assoc_term(==, K, F), 3170% format("~nPropositions: p(0) ... p(~w).~n", [K]), 3171% call_with_time_limit(T_limit, time(seq:seq_prove(F))))). 3172% 3173run(N, T) :- run(N-N, T). 3174 3175% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X). 3176% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X). 3177 3178mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L), 3179 append(L, L, L2), 3180 reverse(L2, R), 3181 apply_left_assoc(Bop, R, Ex). 3182% 3183apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex). 3184% 3185apply_left_assoc(_, X, [], X):-!. 3186apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X], 3187 apply_left_assoc(Bop, V, Y, W). 3188 3189demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). 3190 3191% Valid formulae. 3192valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)). 3193valid_formula((-(-a) -> a) * (a -> -(-a))). % Double Negation 3194valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3195valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b). 3196valid_formula(a + -a). 3197valid_formula(((a -> b) -> a) -> a). % Peirce’s Law 3198valid_formula(-(-a)->a). 3199valid_formula(a -> a). 3200valid_formula(a -> (b -> a)). 3201valid_formula((a->b)->((b->c)->(a->c))). 3202valid_formula(a->((a->b)->b)). 3203valid_formula((a*(a->b))->b). 3204valid_formula((a->b)->(-b -> -a)). 3205valid_formula((a->b)->((b->c)->(a->c))). 3206valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)). 3207 3208% ?- forall(invalid_formula(A), prove(A)). 3209invalid_formula(a). 3210invalid_formula((a->b)->a). 3211invalid_formula((a->b)->(b->a)). 3212invalid_formula(a -> (b -> c)). 3213invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)). 3214invalid_formula( -((-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f))).
prove(a).
?- prove(a*b->a).
?- prove(a*a->a).
?- prove((-a) + a).
?- prove((-A) + A).
?- prove(A -> (p(B)->A)).
?- prove(-(a->a)).
?- prove(a->a).
?- prove((a->b)->(b->a)).
?- prove((a->b)->(a->b)).
?- prove((a->b)->(a)).
?- prove(a->(b->a)).
?- prove((-(a) * a)).
?- prove(-(-(a) * a)).
?- prove(a+ (-a)).
?- prove((-true)*true).
?- prove(true*true).
?- prove(true*false).
?- prove(false*true).
?- prove(false*false).
?- prove(true+true).
?- prove(true+false).
?- prove(false+true).
?- prove(false+false).
?- prove((a->b)*(b->c) -> (a->c)).
?- prove((a->b) -> ((b->c) -> (a->c))).3246prove(X):- 3247 ltr_open_state, 3248 ( prove_(X) 3249 -> writeln('VALID') 3250 ; writeln('INVALID') 3251 ), 3252 close_state. 3253% 3254prove_(X):- cnf(-X, CNF), 3255 get_key(atom_index, N), 3256 ( CNF = 0 -> N = 0 3257 ; CNF = 1 -> N > 0 3258 ; resolve(CNF) 3259 ).
3265% ?- ltr_zdd ltr_pow([a,b,c], P), resolve(P), psa(P). 3266% ?- numlist(1, 10, L), (ltr_zdd ltr_pow(L, P), ltr_card(P, C)). 3267% ?- numlist(1, 100, L), (ltr_zdd ltr_pow(L, P), ltr_card(P, C)). 3268% ?- N = 100000, numlist(1, N, L), time( (ltr_zdd ltr_pow(L, P), resolve(P))). 3269resolve(X):- zdd_has_1(X), !. % The empty clause found. 3270resolve(X):- X > 1, 3271 cofact(X, t(A, L, R)), 3272 ( L = 0 -> fail % Pure literal rule. 3273 ; A = -(_) -> resolve(L) % Negative pure literal rule. 3274 ; ( cofact(L, t(B, U, V)), % Pure literal rule. 3275 ( B = -(A) 3276 -> ltr_merge(V, R, M), % Resolution + Tautology rule. 3277 ltr_join(U, M, W), 3278 resolve(W) % Updated set of clauses. 3279 ; resolve(L) % Posituve pure literal rule. 3280 ) 3281 ) 3282 ). 3283 3284% ?- N=100, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3285% ?- N = 100, time((ltr_zdd {numlist(1, N, L)}, ltr_pow(L, P), 3286% A << set(L), zdd_subtr(P, A, Q), card(Q, C), 3287% {writeln(C)}, resolve(Q))). % false 3288%@ 1267650600228229401496703205375 3289%@ % 4,545,003 inferences, 0.354 CPU in 0.372 seconds (95% CPU, 12826238 Lips) 3290%@ false. 3291 3292% ?- N = 100, time((ltr_open_state(S), numlist(1, N, L), ltr_pow(L, P, S), 3293% zdd_eval(set(L), A, S), zdd_subtr(P, A, Q, S), card(Q, C, S), 3294% writeln(C), resolve(Q, S))). % false 3295%@ 1267650600228229401496703205375 3296%@ % 4,544,971 inferences, 0.348 CPU in 0.368 seconds (94% CPU, 13068410 Lips) 3297%@ false. 3298 3299% ?- N = 100000, time((ltr_zdd {numlist(1, N, _L)}, ltr_pow(_L, P), 3300% card(P, _C))), _C=:= 2^N. 3301%@ % 31,011,164 inferences, 8.180 CPU in 12.708 seconds (64% CPU, 3790924 Lips) 3302%@ N = 100000, 3303%@ P = 300001. 3304 3305atom_index(X):- memo(atom_index(X)-Y), 3306 ( nonvar(Y) -> true 3307 ; get_key(atom_index, Y), 3308 memo(index_atom(Y)-X), 3309 Y0 is Y + 1, 3310 set_key(atom_index, Y0) 3311 ). 3312 3313% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_zdd nnf_cnf(Y, Z), psa(Z)). 3314boole_nnf(X, Y):- % numbervars_index(X, S), 3315 basic_boole(X, Z), 3316 once(neg_normal(Z, Y)). 3317 3318% ?- basic_boole(a, A). 3319% ?- basic_boole(@(a), A). 3320% ?- basic_boole(0, A). 3321% ?- basic_boole(1, A). 3322% ?- basic_boole(true, A). 3323% ?- basic_boole(a+b, A). 3324% ?- basic_boole(a+b+c, A). 3325% ?- basic_boole(-a + b + c, A). 3326% ?- basic_boole(a -> b -> c, A). 3327% ?- basic_boole((a -> b) -> c, A). 3328% ?- basic_boole(*[(a -> b), c], A). 3329% ?- basic_boole(*[(0 -> 1)->2], A). 3330 3331basic_boole(A, BoolConst):-atomic(A), 3332 boole_op(0, [], Fs, BoolConst), 3333 memberchk(A, Fs), 3334 !. 3335basic_boole(I, @(I)):- integer(I), !. 3336basic_boole(@(I), @(I)):-!. 3337basic_boole(*(L), F):-!, basic_boole_vector(L, *, F). 3338basic_boole(+(L), F):-!, basic_boole_vector(L, +, F). 3339basic_boole(X, Y):- X=..[F|Xs], 3340 length(Xs, N), 3341 boole_op(N, As, Fs, Y), 3342 memberchk(F, Fs), 3343 !, 3344 basic_boole_list(Xs, As). 3345basic_boole(X, @(X)). 3346 3347% 3348basic_boole_list([], []). 3349basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y), 3350 basic_boole_list(Xs, Ys). 3351% 3352basic_boole_vector([], +, false):-!. 3353basic_boole_vector([], *, true):-!. 3354basic_boole_vector([X|Xs], F, Y):- 3355 basic_boole(X, X0), 3356 Y=..[F, X0, Z], 3357 basic_boole_vector(Xs, F, Z). 3358 3359% Remark [2023/11/13]: 3360% Use of 0/1 as Boolean constants has been dropped. 3361% Any integer is now usable for a boolean variable, which 3362% may be useful or (nested) vectors of integers *[...], +[...]. 3363% 0/1 as boolean is error prone because ZDD must use 0/1 internally 3364% as basic constant similar, but not exactly the same, 3365% to true/flase. They are different. 3366% This decision was hard because 0/1 is traditionally useful 3367% as boolean constrants, but clear separation and simplicity 3368% were preferred. 3369 3370boole_op(0, [], [false, ff], false). % 0 for false dropped. 3371boole_op(0, [], [true, tt], true). % 1 for true dropped. 3372boole_op(1, [X], [-, ~, \+, not], -(X)). 3373boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y). 3374boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y). 3375boole_op(2, [X, Y], [->, imply], -X + Y). 3376boole_op(2, [X, Y], [<-], Y->X). 3377boole_op(2, [X, Y], [iff, ==, =, =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y). 3378boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)). % -(X==Y) = xor(X, Y) 3379boole_op(2, [X, Y], [nand], -(X) + (-Y)). 3380 3381 3382% ?- neg_normal(-(true + b), X). 3383% ?- neg_normal(-(a), X). 3384% ?- neg_normal(-(a), X). 3385% ?- neg_normal(-(a), X). 3386neg_normal(true, true). 3387neg_normal(false, false). 3388neg_normal(-(false), true). 3389neg_normal(-(true), false). 3390neg_normal(-(-X), Z) :- neg_normal(X, Z). 3391neg_normal(-(X+Y), Z) :- neg_normal(-X* -Y, Z). 3392neg_normal(-(X*Y), Z) :- neg_normal(-X+ -Y, Z). 3393neg_normal(-(X), -(Y)) :- neg_normal(X, Y). 3394neg_normal(X+Y, X0+Y0) :- neg_normal(X, X0), 3395 neg_normal(Y, Y0). 3396neg_normal(X*Y, X0*Y0) :- neg_normal(X, X0), 3397 neg_normal(Y, Y0). 3398neg_normal(@(X), @(X)):-!. 3399neg_normal(X, @(X)):-!. 3400 3401% ?- zdd((intern(-(a;b;c), X), boole_to_dnf(X, Z), sets(Z, U), extern(U, Y))). 3402%% extern(+X, -Y) is det. 3403% Convert an internal form X into an external one 3404% in order to unify Y with the result. 3405 3406extern(X, Y):-integer(X), !, 3407 ( X < 2 -> Y = X 3408 ; memo(index_atom(X)-Y) 3409 ). 3410extern(X, X):- atomic(X), !. 3411extern(X, Y):- X =.. [F|Xs], 3412 extern_list(Xs, Ys), 3413 Y =..[F|Ys]. 3414% 3415extern_list([], []). 3416extern_list([X|Xs], [Y|Ys]):- extern(X, Y), 3417 extern_list(Xs, Ys). 3418 3419 /********************************************* 3420 * Cofact/insert/join/merge on literals * 3421 *********************************************/
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 ).3436ltr_cofact(Z, Y):- nonvar(Z), !, cofact(Z, Y). 3437ltr_cofact(Z, t(A, V, U)):- U > 1, !, 3438 cofact(U, t(B, L, _)), 3439 ( ltr_invert(A, B) 3440 -> ltr_cofact(Z, t(A, V, L)) 3441 ; cofact(Z, t(A, V, U)) 3442 ). 3443ltr_cofact(Z, T):- cofact(Z, T).
3452% PASS. 3453% ?- ltr_zdd cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S). 3454% ?- ltr_zdd dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S). 3455% ?- ltr_zdd ltr_insert(a, 1, X), sets(X, S). 3456% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), sets(Y, S). 3457% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), 3458% ltr_insert(-b, Y, Z), sets(Z, S). 3459% ?- ltr_zdd X<<set([a]), ltr_insert(b, X, Y), psa(Y). 3460% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3461% ?- ltr_zdd X<<set([b]), ltr_insert(a, X, Y), psa(Y). 3462% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3463% ?- ltr_zdd X<<set([-a]), ltr_insert(a, X, Y), psa(Y))). 3464% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y). 3465% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y). 3466% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y). 3467% ?- ltr_zdd X<<{[a]}, ltr_insert(a, X, Y), psa(Y). 3468% ?- ltr_zdd X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y). 3469% ?- ltr_zdd X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y). 3470% ?- ltr_zdd X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y). 3471% ?- ltr_zdd X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y). 3472% ?- ltr_zdd X<< dnf(a), ltr_insert(b, X, Y), psa(Y). 3473% ?- ltr_zdd X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y). 3474% ?- ltr_zdd X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y). 3475% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3476% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3477% ?- sat((x=\=y)*x*y). % false 3478% ?- sat((a * -a)). % false 3479% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y). 3480% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y). 3481% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y). 3482% ?- ltr_zdd dnf((-a)*b, X), psa(X). 3483% ?- ltr_zdd cnf((-a)*b, X). 3484% ?- ltr_zdd cnf((a), X). 3485 3486ltr_insert(_, 0, 0):-!. 3487ltr_insert(A, 1, J):-!, zdd_singleton(A, J). 3488ltr_insert(A, I, J):- memo(ltr_insert(A,I)-J), 3489 ( nonvar(J) -> true 3490 ; cofact(I, t(B, L, R)), 3491 zdd_compare(C, A, B), 3492 ( C = (<) -> 3493 ( complementary(A, B) -> 3494 cofact(J, t(A, 0, L)) 3495 ; cofact(J, t(A, 0, I)) 3496 ) 3497 ; C = (=) -> 3498 ( negative(A) -> 3499 ltr_join(L, R, K), 3500 cofact(J, t(A, 0, K)) 3501 ; ltr_insert_aux(J, A, L, R) 3502 ) 3503 ; ( complementary(A, B) -> ltr_insert(A, L, J) 3504 ; ltr_insert(A, L, L0), 3505 ltr_insert(A, R, R0), 3506 cofact(J, t(B, L0, R0)) 3507 ) 3508 ) 3509 ). 3510 3511% for suppressing use of cofact/3 and ltr_insert/4 3512ltr_insert_aux(J, A, L, R):- % A is positive. R has no -A. 3513 ( L < 2 -> cofact(J, t(A, L, R)) 3514 ; cofact(L, t(B, L0, _)), 3515 ( complementary(A, B)-> 3516 ltr_join(L0, R, K), 3517 cofact(J, t(A, 0, K)) 3518 ; ltr_join(L, R, K), 3519 cofact(J, t(A, 0, K)) 3520 ) 3521 ).
3527% 3528ltr_join(X, X, X):-!. % idemopotent law of logical disjunction (OR) 3529ltr_join(0, X, X):-!. 3530ltr_join(X, 0, X):-!. 3531ltr_join(1, _, 1):-!. 3532ltr_join(_, 1, 1):-!. 3533ltr_join(X, Y, Z):- 3534 ( X=<Y -> memo(ltr_join(X,Y)-Z) 3535 ; memo(ltr_join(Y,X)-Z) 3536 ), 3537 ( nonvar(Z) -> true %, write(.) 3538 ; cofact(X, t(A, L, R)), 3539 cofact(Y, t(A0, L0, R0)), 3540 zdd_compare(C, A, A0), 3541 ( C = (=) -> 3542 ltr_join(R, R0, U), 3543 ltr_join(L, L0, V), 3544 cofact(Z, t(A, V, U)) 3545 ; C = (<) -> 3546 ltr_join(L, Y, U), 3547 cofact(Z, t(A, U, R)) 3548 ; ltr_join(L0, X, U), 3549 cofact(Z, t(A0, U, R0)) 3550 ) 3551 ).
3560ltr_merge(X, X, X):-!. % idempotent law of logical conjunction (AND). 3561ltr_merge(0, _, 0):-!. 3562ltr_merge(_, 0, 0):-!. 3563ltr_merge(1, X, X):-!. 3564ltr_merge(X, 1, X):-!. 3565ltr_merge(X, Y, Z):- 3566 ( X =< Y -> memo(ltr_merge(X,Y)-Z) 3567 ; memo(ltr_merge(Y,X)-Z) 3568 ), 3569 ( nonvar(Z) -> true 3570 ; cofact(Y, t(A, L, R)), 3571 ltr_merge(X, R, U), 3572 ltr_merge(X, L, V), 3573 ltr_insert(A, U, U0), 3574 ltr_join(V, U0, Z) 3575 ).
xor(X, Y) = X*-Y + -X*Y.
?- ltr_zdd X<<dnf(a+b), Y<<dnf(b+c), ltr_xor(X, Y, Z), psa(Z), ltr_card(Z, C).
?- ltr_zdd Z<< dnf((a+b)=\=(b+c)), psa(Z), ltr_card(Z, C).3582ltr_xor(X, Y, Z):- 3583 ltr_negate(Y, Y0), 3584 ltr_merge(X, Y0, U), 3585 ltr_negate(X, X0), 3586 ltr_merge(X0, Y, V), 3587 ltr_join(U, V, Z). 3588 3589 /****************************************** 3590 * Auxiliary operations on literals * 3591 ******************************************/
3595complementary(-(A), A):-!. 3596complementary(A, -(A)). 3597% 3598negative(-(_)).
3607% ?- ltr_zdd ltr_pow([a], X), card(X, C), psa(X). 3608% ?- ltr_zdd ltr_pow([a, b], X), card(X, C), psa(X). 3609% ?- ltr_zdd {numlist(1, 100, L)}, ltr_pow(L, X), card(X, C). 3610ltr_pow([], 1). 3611ltr_pow([A|As], P):- ltr_pow(As, Q), 3612 ltr_insert(A, Q, R), 3613 ltr_insert(-A, Q, L), 3614 ltr_join(L, R, P).
3622% ?- ltr_zdd ltr_append([-b, a, -d, c], 1, X), psa(X). 3623% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3624% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3625% ?- ltr_zdd X<<dnf(a->a), ltr_card(X, C), psa(X). 3626% 3627ltr_append([], X, X). 3628ltr_append([A|As], X, Y):- ltr_append(As, X, X0), 3629 ltr_insert(A, X0, Y).
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))).3637% 3638ltr_set(X, Y):- ltr_append(X, 1, Y).
3645% ?- zdd((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))). 3646% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))). 3647% ?- zdd((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))). 3648% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3649% ?- zdd((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3650 3651% ?- ltr_zdd X<<dnf(a), ltr_negate(X, Y), psa(Y). 3652% ?- ltr_zdd ltr_negate(0, Y), psa(Y). 3653% ?- ltr_zdd ltr_negate(1, Y), psa(Y). 3654 3655% 3656ltr_negate(X, Y):- ltr_complement(X, X0), ltr_choices(X0, Y).
3665% ?- zdd X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y). 3666% ?- zdd X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y). 3667% 3668ltr_complement(X, X):- X<2, !. 3669ltr_complement(I, Y):- memo(ltr_complement(I)-Y), 3670 ( nonvar(Y) -> true 3671 ; cofact(I, t(A, L, R)), 3672 ltr_complement(L, L0), 3673 ltr_complement(R, R0), 3674 complementary(A, NA), 3675 ltr_insert(NA, R0, R1), 3676 ltr_join(L0, R1, Y) 3677 ). 3678 3679 /************************************ 3680 * Convert Boolean Form to DNF/CNF * 3681 ************************************/
3686% ?- boole_nnf(-(a+b), X). 3687% ?- zdd dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V). 3688% ?- zdd((dnf(-(a=:=b), X), psa(X))). 3689% ?- zdd((dnf((a=\=b), X), psa(X))). 3690% ?- zdd((dnf((0), X), psa(X))). 3691% ?- zdd((dnf(*[1,3,2,3], X), psa(X))). 3692% ?- zdd dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I). 3693% ?- zdd((dnf(*[@(1),3,2,3], X), psa(X))). 3694 3695dnf(X, Y):- zdd_numbervars(X), 3696 boole_nnf(X, Z), 3697 nnf_dnf(Z, Y).
3706% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y). 3707% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U). 3708% ?- ltr_zdd big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D). 3709 3710dnf_cnf(X, Y):- nonvar(X), !, ltr_choices(X, Y). 3711dnf_cnf(X, Y):- ltr_choices(Y, X). 3712% 3713cnf_dnf(X, Y):- dnf_cnf(X, Y). 3714 3715% ?- ltr_zdd X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y). 3716%@ * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug 3717% ?- ltr_zdd X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y). 3718% ?- ltr_zdd X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y). 3719% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3720% ?- ltr_zdd X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y). 3721% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3722% ?- ltr_zdd X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y). 3723% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3724% dnf_cnf(Z, Y), psa(X), psa(Y). 3725 3726% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3727% dnf_cnf(Z, Y), psa(X), psa(Y). 3728 3729% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3730% dnf_cnf(Z, Y). 3731 3732% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), 3733% dnf_cnf(Z, U). 3734 3735% ?- N=100, time((ltr_zdd big_normal_form(N, X), 3736% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3737%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips) 3738%@ N = 100, 3739%@ X = 39901, 3740%@ Y = D, D = 0, % <== CORRECT. 3741%@ C = 1267650600228229401496703205376 . 3742 3743% ?- N=1000, time((ltr_zdd big_normal_form(N, X), 3744% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3745%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips) 3746%@ N = 1000, 3747%@ X = 3999001, 3748%@ Y = D, D = 0, % <== CORRECT. 3749%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
3763ltr_choices(0, 1):-!. 3764ltr_choices(1, 0):-!. 3765ltr_choices(X, Y):- memo(ltr_choices(X)-Y), 3766 ( nonvar(Y)->true %, write(.) % many hits. 3767 ; cofact(X, t(A, L, R)), 3768 ltr_choices(L, L0), 3769 ltr_choices(R, R0), 3770 cofact(R1, t(A, R0, 1)), 3771 ltr_merge(L0, R1, Y) 3772 ).
3777nnf_dnf(false * _, 0):-!. 3778nnf_dnf(_ * false, 0):-!. 3779nnf_dnf(true * X, Y):-!, nnf_dnf(X, Y). 3780nnf_dnf(X * true, Y):-!, nnf_dnf(X, Y). 3781nnf_dnf(X * Y, Z):-!, memo(dnf(X*Y)-Z), 3782 ( nonvar(Z) -> true 3783 ; nnf_dnf(X, U), 3784 nnf_dnf(Y, V), 3785 ltr_merge(U, V, Z) 3786 ). 3787nnf_dnf(false + X, Y):-!, nnf_dnf(X, Y). 3788nnf_dnf(X + false, Y):-!, nnf_dnf(X, Y). 3789nnf_dnf(true + X, Y):-!, nnf_dnf(X, Z), 3790 ltr_join(1, Z, Y). 3791nnf_dnf(X + true, Y):-!, nnf_dnf(X, Z), 3792 ltr_join(1, Z, Y). 3793nnf_dnf(X + Y, Z):-!, memo(dnf(X+Y)-Z), 3794 ( nonvar(Z) -> true 3795 ; nnf_dnf(X, U), 3796 nnf_dnf(Y, V), 3797 ltr_join(U, V, Z) 3798 ). 3799nnf_dnf(@(X), I):-!, atom_index(X), 3800 zdd_singleton(X, I). 3801nnf_dnf(-(@(X)), I):- atom_index(X), 3802 zdd_singleton(-(X), I).
3808% ?- zdd((cnf(a, X), S<<sets(X))). 3809% ?- ltr_zdd((cnf(a*b, X), S<<sets(X))). 3810% ?- zdd((X<<cnf(-a), Y<<sets(X))). 3811% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 3812% ?- zdd((X<<cnf(+([a,b,c])), Y<<sets(X))). 3813% ?- zdd((X<<cnf(*([a,b,c])), Y<<sets(X))). 3814% ?- zdd((X<<dnf(+([a,b,c])), Y<<sets(X))). 3815% ?- zdd((X<<dnf(*([a,b,c])), Y<<sets(X))). 3816% ?- zdd((cnf(a, X), psa(X))). 3817% ?- zdd((cnf(-a, X), psa(X))). 3818% ?- zdd((cnf(a+b, X), psa(X))). 3819% ?- zdd((cnf(a+b+(-c), X), psa(X))). 3820% ?- zdd((cnf(-a * a, X), psa(X))). 3821% ?- zdd((cnf(a->a, X), psa(X))). 3822% ?- zdd((cnf(-a * a, X), psa(X))). 3823% ?- zdd((cnf( a + a, X), psa(X))). 3824% ?- zdd((cnf( A + A, X), psa(X))). 3825% ?- zdd((cnf(-(a*b), X), psa(X))). 3826% ?- zdd((cnf(*([a,b,c]), X), psa(X))). 3827% ?- zdd {N = 10, numlist(2, N, Ns)}, cnf(*(Ns), X), ltr_card(X, C, K). 3828% ?- ltr_zdd((dnf(a, X), psa(X))). 3829% ?- ltr_zdd((cnf(-(a->b), X), psa(X))). 3830% ?- ltr_zdd((cnf(a, X), psa(X))). 3831% ?- boole_nnf(-(*[0,1,2]), X). 3832% ?- ltr_zdd {mk_left_assoc_term(==, 1, F)}, cnf(F, X), psa(X). 3833cnf(X, Y):- zdd_numbervars(X), 3834 boole_nnf(X, Z), 3835 nnf_cnf(Z, Y). 3836% 3837nnf_cnf(true, 1):-!. 3838nnf_cnf(false, 0):-!. 3839nnf_cnf(false * _, 0):-!. 3840nnf_cnf(_ * false, 0):-!. 3841nnf_cnf(true * X, Y):-!, nnf_cnf(X, Y). 3842nnf_cnf(X * true, Y):-!, nnf_cnf(X, Y). 3843nnf_cnf(X * X, Y):-!, nnf_cnf(X, Y). 3844nnf_cnf(X * Y, Z):-!, memo(cnf(X*Y)-Z), 3845 ( nonvar(Z)->true %, write(.) % many hits. 3846 ; nnf_cnf(X, U), 3847 nnf_cnf(Y, V), 3848 ltr_join(U, V, Z) 3849 ). 3850nnf_cnf(false + X, Y):-!, nnf_cnf(X, Y). 3851nnf_cnf(X + false, Y):-!, nnf_cnf(X, Y). 3852nnf_cnf(true + _, 1):-!. 3853nnf_cnf(_ + true, 1):-!. 3854nnf_cnf(X + X, Y):-!, nnf_cnf(X, Y). 3855nnf_cnf(X + Y, Z):-!, memo(cnf(X+Y)-Z), 3856 ( nonvar(Z)->true %, write(+) % many hits. 3857 ; nnf_cnf(X, U), 3858 nnf_cnf(Y, V), 3859 ltr_merge(U, V, Z) 3860 ). 3861nnf_cnf(@(X), I):-!, atom_index(X), 3862 zdd_singleton(X, I). 3863nnf_cnf(-(@(X)), I):- atom_index(X), 3864 zdd_singleton(-(X), I). 3865 3866 3867 /***************************************************** 3868 * ltr_card/[3,4] Counting solutions of a DNF. * 3869 *****************************************************/ 3870 3871 3872% ?- sat_count_by_collect_atoms(a, C). 3873% ?- sat_count_by_collect_atoms(a+b, C). 3874% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C). 3875% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 3876 3877sat_count_by_collect_atoms(X, C):- sat_fetch(S), 3878 dnf(X, Y, S), 3879 sat_count_by_collect_atoms(Y, C, S), 3880 sat_close. 3881% 3882sat_count_by_collect_atoms(X, C):- 3883 zdd_boole_atoms(Us), 3884 zdd_sort(Us, Vs), 3885 expand_dnf(Vs, X, Y), 3886 card(Y, C). 3887 3888% ?- ltr_zdd X<<dnf(b+a), zdd_boole_atoms(Us). 3889zdd_boole_atoms(Us):- 3890 ( get_key(atom_index, N) -> 3891 collect_boole_atoms(0, N, Us) 3892 ; Us = [] 3893 ). 3894 3895% 3896collect_boole_atoms(I, N, []):- I>=N, !. 3897collect_boole_atoms(I, N, [A|U]):- memo(index_atom(I)-A), 3898 J is I+1, 3899 collect_boole_atoms(J, N, U). 3900 3901 /****************************** 3902 * find_counter_example * 3903 ******************************/
3907% ?- findall_counter_examples(a, X), psa(X). 3908% ?- findall_counter_examples((a->b)->a, X), psa(X). 3909% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 3910% ?- findall_counter_examples(a->b, X), psa(X). 3911% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 3912% ?- findall_counter_examples(a->b, Out), psa(Out). 3913findall_counter_examples(In, Out):- 3914 ltr_fetch_state, 3915 dnf(In, InZ), 3916 zdd_boole_atoms(Us), 3917 zdd_sort(Us, Vs), 3918 expand_prefix_dnf(Vs, 1, All), 3919 expand_dnf(Vs, InZ, Y), 3920 zdd_subtr(All, Y, Out).
3927% ?- ltr. 3928% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 3929% ?- X<< dnf(a), psa(X), ltr_card(X, C). 3930% ?- X<< dnf(a->a), ltr_card(X, C). 3931% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 3932% ?- X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C). 3933 3934% ?- findall(p(J), between(1, 100, J), Ps), 3935% time((X<< dnf(+Ps), ltr_card(X, C))). 3936% ?- N = 1000, findall(p(J), between(1, N, J), Ps), 3937% time((X<< dnf(+Ps),ltr_card(X, C))), 3938% C =:= 2^1000 - 1. 3939 3940ltr_card(In, Out):- 3941 zdd_boole_atoms(Us), 3942 zdd_sort(Us, Vs), 3943 expand_dnf(Vs, In, Y), 3944 card(Y, Out). 3945 3946% ?- ltr_var(-(5), X). 3947ltr_var(-(V), V):-!. 3948ltr_var(V, V).
3955% ?- ltr_zdd((X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y))). 3956% ?- ltr_zdd((X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), card(Y, C))). 3957% ?- ltr_zdd((X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C))). 3958% ?- ltr_zdd((X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y))). 3959% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 3960% ?- ltr_zdd((X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 3961% ?- ltr_zdd((X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C))). 3962 3963expand_dnf([], X, X):-!. 3964expand_dnf(_, 0, 0):-!. 3965expand_dnf(Vs, 1, Y):-!, expand_prefix_dnf(Vs, 1, Y). 3966expand_dnf(Vs, X, Y):- memo(expand_dnf(X,Vs)-Y), 3967 ( nonvar(Y) -> true %, write(.) % Many hits. 3968 ; cofact(X, t(A, L, R)), 3969 ltr_var(A, K), 3970 divide_ord_list(Vs, K, [], Us, Ws), 3971 expand_dnf(Us, R, R0), 3972 ltr_insert(A, R0, R1), 3973 expand_left_dnf(K, Us, L, L0), 3974 ltr_join(L0, R1, X0), 3975 expand_prefix_dnf(Ws, X0, Y) 3976 ).
divide_ord_list([a,b,c,d,e], c, [u], T, W).
?- divide_ord_list([a,b,c, d], e, [], X, Y). % false3984divide_ord_list([V|Vs], V, Us, Vs, Us):-!. 3985divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U), 3986 divide_ord_list(Vs, U, [V|Us], Ws, Ps).
3993% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))). 3994expand_prefix_dnf(Vs, X, Y):- zdd_sort(Vs, OrdVs), 3995 expand_ord_prefix_dnf(OrdVs, X, Y). 3996 3997% 3998expand_ord_prefix_dnf([], X, X):-!. 3999expand_ord_prefix_dnf([V|Vs], X, Y):- 4000 expand_ord_prefix_dnf(Vs, X, X0), 4001 ltr_insert(V, X0, X1), 4002 ltr_insert(-V, X0, X2), 4003 ltr_join(X1, X2, Y).
4013expand_left_dnf(_, _, 0, 0):-!. 4014expand_left_dnf(K, Us, 1, Y):-!, expand_prefix_dnf([K|Us], 1, Y). 4015expand_left_dnf(K, Us, X, Y):- cofact(X, t(A, L, R)), 4016 ltr_var(A, J), 4017 ( K = J -> 4018 expand_dnf(Us, R, R0), 4019 ltr_insert(A, R0, R1) 4020 ; divide_ord_list([K|Us], J, [], Vs, Ws), 4021 expand_dnf(Vs, R, R0), 4022 ltr_insert(A, R0, Q), 4023 expand_prefix_dnf(Ws, Q, R1) 4024 ), 4025 expand_dnf([K|Us], L, L0), 4026 ltr_join(L0, R1, Y). 4027 4028 /******************************* 4029 * Filter on cardinality * 4030 *******************************/
4036% ?- zdd((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))). 4037card_filter_gte(0, X, X):- !. % gte: greater than or equal 4038card_filter_gte(1, X, Y):- !, zdd_subtr(X, 1, Y). 4039card_filter_gte(_, X, 0):- X<2, !. 4040card_filter_gte(N, X, Y):- memo(filter_gte(N,X)-Y), 4041 ( nonvar(Y) -> true % many hits. 4042 ; cofact(X, t(A, L, R)), 4043 N0 is N - 1, 4044 card_filter_gte(N, L, L0), 4045 card_filter_gte(N0, R, R0), 4046 cofact(Y, t(A, L0, R0)) 4047 ).
4053% ?- X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y). 4054card_filter_lte(0, X, Y):- % lte: less than or equal 4055 ( zdd_has_1(X) -> Y = 1 4056 ; Y = 0 4057 ). 4058card_filter_lte(_, X, X):- X<2, !. 4059card_filter_lte(N, X, Y):- memo(filter_lte(N,X)-Y), 4060 ( nonvar(Y) -> true % many hits. 4061 ; cofact(X, t(A, L, R)), 4062 N0 is N - 1, 4063 card_filter_lte(N, L, L0), 4064 card_filter_lte(N0, R, R0), 4065 cofact(Y, t(A, L0, R0)) 4066 ).
time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))).4072card_filter_between(I, J, X, Y):- 4073 card_filter_gte(I, X, Z), 4074 card_filter_lte(J, Z, Y). 4075 4076% ?- time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))). 4077card_filter_between_by_meet(I, J, X, Y):- 4078 card_filter_gte(I, X, Z), 4079 card_filter_lte(J, X, U), 4080 zdd_meet(Z, U, Y). 4081 4082 4083 /********************************************************* 4084 * Solve boolean equations and verify the solution * 4085 *********************************************************/ 4086% Recovered [2023/11/14] 4087%! dnf_subst(+V, +T, +X, -Y) is det. 4088% Y is the ZDD obtained by substituting each 4089% occurrence of atom V in X with T. 4090 4091% ?-ltr_zdd X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4092% ?-ltr_zdd X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4093% ?-ltr_zdd X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4094 4095dnf_subst(_, _, X, X):- X < 2, !. 4096dnf_subst(V, D, X, Y):- 4097 cofact(X, t(A, L, R)), 4098 dnf_subst(V, D, L, L0), 4099 once( A = -(U); U = A ), 4100 ltr_compare(C, V, U), 4101 ( C = (<) -> Y = X 4102 ; ( C = (=) -> 4103 ( A = (-V) -> 4104 ltr_negate(D, D0), 4105 ltr_merge(D0, R, R0) 4106 ; A = V -> 4107 ltr_merge(D, R, R0) 4108 ) 4109 ; dnf_subst(V, D, R, R1), 4110 ltr_insert(A, R1, R0) 4111 ), 4112 ltr_join(L0, R0, Y) 4113 ).
4121% exists x s.t. C0*(L,-x) + C1*x = 1 4122% if and only if 4123% C0 + C1 = 1 satisfiable 4124% x = a*C1 + (-C0). 4125 4126% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S). 4127% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S). 4128% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S). 4129 4130solve_boole_with_check(Exp, Xs, Ps):- 4131 dnf(Exp, E), 4132 solve_boolean_equations(E, Xs, Ps, Sols), 4133 eliminate_variables(E, Sols, Cond), 4134 !, 4135 dnf_valid_check(Cond). 4136 4137% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), 4138% solutions_to_sets(Sols, Sols0). 4139% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0). 4140 4141solve_boolean_equations(_, [], _, []):-!. 4142solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols]):- 4143 solve_boolean_equations_basic(E, X, A, Sol0, E0), 4144 solve_boolean_equations(E0, Xs, As, Sols), 4145 dnf_subst_list(Sols, Sol0, Sol). 4146 4147% ?- ltr_zdd E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond). 4148solve_boolean_equations_basic(E, X, A, Sol, Cond):- 4149 dnf_subst(X, 1, E, C1), 4150 dnf_subst(X, 0, E, C0), 4151 ltr_join(C0, C0, Cond), 4152 ltr_negate(C0, NC0), 4153 ltr_insert(A, C1, AC1), 4154 ltr_join(NC0, AC1, Sol). 4155% 4156dnf_subst_list([], E, E). 4157dnf_subst_list([X=A|Eqs], E, F):- 4158 dnf_subst(X, A, E, E0), 4159 dnf_subst_list(Eqs, E0, F). 4160% 4161solutions_to_sets([], []). 4162solutions_to_sets([X = E|Sols], [X = E0|Sols0]):- 4163 sets(E, E0), 4164 solutions_to_sets(Sols, Sols0). 4165 4166% ?- 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). 4167 4168% ?- 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). 4169 4170% ?- 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). 4171 4172eliminate_variables(Exp, Eqns, Cond):- 4173 apply_subst_list(Eqns, Exp, Cond). 4174% 4175apply_subst_list([], E, E). 4176apply_subst_list([X=U|Eqns], E, E0):- 4177 dnf_subst(X, U, E, E1), 4178 dnf_subst_list(Eqns, E1, E0). 4179% 4180dnf_valid_check(X):- 4181 ltr_atoms_by_scan(X, As), 4182 ltr_sort(As, Bs), 4183 expand_dnf(Bs, X, Y), 4184 card(Y, C), 4185 length(Bs, N), 4186 ( C =:= (1<< N) -> writeln('Solved and Verified.') 4187 ; writeln('Solved but NOT verified.') 4188 ). 4189 4190% ?- ltr_zdd X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), {sort(As, Bs)}. 4191ltr_atoms_by_scan(X, []):- X<2, !. 4192ltr_atoms_by_scan(X, P):- memo(ltr_atoms(X)-P), 4193 ( nonvar(P) -> true 4194 ; cofact(X, t(A, L, R)), 4195 ltr_atoms_by_scan(L, Al), 4196 ltr_atoms_by_scan(R, Ar), 4197 ltr_var(A, A0), 4198 union([A0|Al], Ar, P) 4199 ). 4200 4201 /********************************* 4202 * operations on reducible zdd * 4203 *********************************/
4209% ?- numlist(1, 100, Ns), X<<pow(Ns), card(X, C). 4210% ?- bdd_sort_append([c, a, b,c], 1, Z), psa(Z). 4211bdd_sort_append(X, Y, Z):- zdd_sort(X, X0), 4212 bdd_append(X0, Y, Z). 4213 4214% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y). 4215% ?- zdd bdd_append([x, a, y, b], 0, Y), psa(Y). 4216% ?- zdd bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z). 4217 4218bdd_append([], Z, Z). 4219bdd_append([X|Y], Z, U):- 4220 bdd_append(Y, Z, Z0), 4221 bdd_cons(U, X, Z0). 4222 4223% ?- zdd bdd_list([b, b], Y), bdd_sort_append([b,b], Y, Z), psa(Z). 4224% ?- zdd bdd_list([b, b], Y), bdd_list(X, Y). 4225bdd_list(List, X):- var(X), !, bdd_append(List, 1, X). 4226bdd_list(List, X):- get_bdd_list(X, List). 4227 4228% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L). 4229% ?- zdd bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L). 4230get_bdd_list(1, []):-!. 4231get_bdd_list(X, [A|As]):- X>1, bdd_cons(X, A, X0), 4232 get_bdd_list(X0, As). 4233 4234% ?- zdd bdd_append([a,a,b,b], 1, X), 4235% bdd_append([1,1,2,2], 1, Y), 4236% bdd_zip(X, Y, Z), psa(Z). 4237bdd_zip(0, _, 0):-!. 4238bdd_zip(_, 0, 0):-!. 4239bdd_zip(1, _, 1):-!. 4240bdd_zip(_, 1, 1):-!. 4241bdd_zip(X, Y, Z):- bdd_cons(X, A, X0), 4242 bdd_cons(Y, B, Y0), 4243 bdd_zip(X0, Y0, Z0), 4244 bdd_cons(Z, A-B, Z0). 4245 4246% ?- zdd bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y). 4247bdd_normal(X, X):- X<2, !. 4248bdd_normal(X, Y):- cofact(X, t(A, L, R)), 4249 bdd_normal(L, L0), 4250 bdd_normal(R, R1), 4251 zdd_insert(A, R1, R0), 4252 zdd_join(L0, R0, Y). 4253 4254% ?- zdd bdd_append([a,b,a,b], 1, X), 4255% bdd_append([a,b, c, a,b, c], 1, Y), 4256% bdd_append([b, a, b, a, a,b ], 1, Z), 4257% bdd_list_normal([X, Y, Z], R), psa(R). 4258 4259bdd_list_normal([], 0). 4260bdd_list_normal([A|As], R):- bdd_list_normal(As, R0), 4261 bdd_normal(A, A0), 4262 zdd_join(A0, R0, R). 4263 4264% 4265bdd_insert(_, 0, 0):-!. 4266bdd_insert(A, 1, X):-!, zdd_singleton(A, X). 4267bdd_insert(A, X, Y):- cofact(X, t(B, L, R)), 4268 bdd_insert(A, L, L0), 4269 bdd_append([A,B], R, R0), 4270 zdd_join(L0, R0, Y).
4279% ?- bdd_list_raise([], 0, X). 4280% ?- bdd_list_raise([a], 0, X). 4281% ?- bdd_list_raise([a], 1, X), psa(X). 4282% ?- bdd_list_raise([a,b], 1, X), psa(X). 4283% ?- N = 1, numlist(1, N, Ns), bdd_list_raise(Ns, N, X), card(X, C). 4284 4285% ?- zdd {N = 15, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X),card(X, C). 4286 4287bdd_list_raise(_, 0, 1):-!. 4288bdd_list_raise(L, N, X):- N0 is N-1, 4289 bdd_list_raise(L, N0, X0), 4290 bdd_map_insert(L, X0, X). 4291% 4292bdd_map_insert([], _, 0). 4293bdd_map_insert([A|As], X, Y):- 4294 bdd_insert(A, X, X0), 4295 bdd_map_insert(As, X, Y0), 4296 zdd_join(X0, Y0, Y). 4297 4298% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert, 4299% also work for bddered zdd. 4300 4301% ?- zdd X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U), 4302% psa(X), psa(Y), psa(Z), psa(U). 4303% ?- zdd X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z), 4304% psa(Z, S), card(Z, C). 4305% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4306% card(Z, C). 4307% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z), 4308% card(Z, C), card(X, D). 4309 4310bdd_merge(0, _, 0):-!. 4311bdd_merge(_, 0, 0):-!. 4312bdd_merge(1, X, X):-!. 4313bdd_merge(X, 1, X):-!. 4314bdd_merge(X, Y, Z):- memo(bdd_merge(X, Y)-Z), 4315 ( nonvar(Z) -> true % , write(.) % So so frequently hits. 4316 ; cofact(X, t(A, L, R)), 4317 bdd_merge(L, Y, L0), 4318 bdd_merge(R, Y, R1), 4319 bdd_cons(R0, A, R1), 4320 zdd_join(L0, R0, Z) 4321 ). 4322 4323 /**************n*************************** 4324 * Interleave bddered atoms in BDD * 4325 ******************************************/
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.4334% ?- X<< +[*[a,b], *[x,y]], Y<< +[*[1]], 4335% bdd_interleave(X, Y, Z), psa(Z). 4336% ?- zdd X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z). 4337% ?- zdd X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z). 4338 4339bdd_interleave(0, _, 0):-!. 4340bdd_interleave(_, 0, 0):-!. 4341bdd_interleave(1, X, X):-!. 4342bdd_interleave(X, 1, X):-!. 4343bdd_interleave(X, Y, Z):- % memo is useless here. 4344 cofact(Y, t(B, L, R)), 4345 ( L < 2 -> L0 = 0 4346 ; bdd_interleave(X, L, L0) 4347 ), 4348 bdd_interleave(X, B, R, R0), 4349 zdd_join(L0, R0, Z). 4350% 4351bdd_interleave(0, _, _, 0):-!. 4352bdd_interleave(1, B, Y, Z):-!, cofact(Z, t(B, 0, Y)). 4353bdd_interleave(X, B, Y, Z):- memo(merge(X, Y, B)-Z), 4354 ( nonvar(Z) -> true % , write(+) % many hits. 4355 ; cofact(X, t(A, L, R)), 4356 ( L < 2 -> L0 = 0 4357 ; bdd_interleave(L, B, Y, L0) 4358 ), 4359 bdd_interleave(A, R, B, Y, R0), 4360 zdd_join(L0, R0, Z) 4361 ). 4362% 4363bdd_interleave(A, X, B, Y, Z):- % memo is useless here. 4364 bdd_interleave(X, B, Y, U), 4365 cofact(Z0, t(A, 0, U)), 4366 bdd_interleave(Y, A, X, V), 4367 cofact(Z1, t(B, 0, V)), 4368 zdd_join(Z0, Z1, Z).
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.4377% ?- zdd bdd_funs(mono([1,2]-[a,b])*mono([3,4]-[c,d]), X), psa(X). 4378% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), psa(X). 4379% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), 4380% zdd_normalize(X, Y), psa(Y). 4381 4382bdd_funs(A*B, F):-!, bdd_funs(A, A0), 4383 bdd_funs(B, B0), 4384 bdd_merge(A0, B0, F). 4385bdd_funs(A&B, F):-!, bdd_funs(A, A0), 4386 bdd_funs(B, B0), 4387 bdd_interleave(A0, B0, F). 4388bdd_funs(A, F):- fun_block(A, F). 4389 4390 /************** 4391 * misc * 4392 **************/
4397% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), zdd_flatten(X, Y), psa(Y)). 4398zdd_flatten(X, 0):- X<2, !. 4399zdd_flatten(X, Y):- memo(flatten(X)-Y), 4400 ( nonvar(Y) -> true % Many hits. 4401 ; cofact(X, t(A, L, R)), 4402 zdd_flatten(L, L0), 4403 zdd_flatten(R, R0), 4404 zdd_join(L0, R0, Y0), 4405 cofact(Y, t(A, Y0, 1)) 4406 )