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 55 56% ?- zdd. 57% ?- N = 10000, numlist(1, N, Ns), time(((X<<pow(Ns), card(X, _C)))), _C=:=2^N. 58% :- doc_server(7000). 59% :- use_module(library(pldoc/doc_library)). 60% :- doc_load_library. 61% :- doc_browser. 62 63:- use_module(library(apply)). 64:- use_module(library(apply_macros)). 65:- use_module(library(clpfd)). 66:- use_module(library(statistics)). 67:- use_module(zdd('zdd-array')). 68:- use_module(util(math)). 69:- use_module(util(meta2)). 70:- use_module(pac(basic)). 71:- use_module(pac(meta)). 72:- use_module(util(misc)). 73:- use_module(pac('expand-pac')). % For the kind block. 74:- use_module(pac(op)). 75:- use_module(zdd('frontier-vector')). 76:- use_module(zdd(zsat)). 77 78:- set_prolog_flag(stack_limit, 10_200_147_483_648). 79:- nb_setval(default_zdd_mode, zdd). 80 81% :- initialization(activate_zdd). % choices: zdd/ltr/sat 82activate_zdd:- b_getval(default_zdd_mode, Mode), 83 call(Mode), 84 format( 85 "\n%\s~w mode activated. 86%\sCurrently available modes: zdd/ltr/sat\n", [Mode]). 87 88attr_unify_hook(V, Y):- 89 ( get_attr(Y, zdd, A) 90 -> zdd_unify(V, A) 91 ; zdd_unify(V, Y) 92 ). 93 94 :- op(800, xfy, &). 95 :- op(820, fy, \). % NOT 96 :- op(830, xfy, /\). % AND 97 :- op(840, xfy, \/). % OR 98 :- op(860, xfy, ~). % equivalence 99 :- op(860, xfy, #). % exor 100 :- op(860, xfy, <->). % equivalence 101 :- op(860, xfy, <=> ). % equivalence 102 :- op(870, yfx, <-). 103 104% for pac query. 105term_expansion --> pac:expand_pac. 106 107% ?- zdd. 108% ?- numlist(1, 2, Ns), Y<<pow(Ns), card(Y, C). 109% ?- set_memo(a-1), set_memo(a-2), memo(a-V). 110% ?- X<<{[1,1]}, psa(X). 111% ?- X<< *[ *a, *a, *b,*c], psa(X). 112% ?- set_key(root, hello), get_key(root, R). 113% ?- all_fun([a],[b], F), psa(F). 114% ?- all_fun([],[b], F), psa(F). 115% ?- all_fun([a],[], F), psa(F). 116% ?- all_fun([a,b],[c,d], F), psa(F), card(F, C). 117% ?- N = 20, numlist(1, N, A), raise_list(A, 2, A2), all_fun(A2, A, F), card(F, C). 118% ?- time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 119% all_fun(Ns, Ms, F), card(F, C))). 120 121% Cardinality # of Y^X = { f | f: X-> Y }. 122% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 123 124% ?- I=1, J=1, K=1, L=1, 125% numlist(1, I, X), numlist(1, K, Y), 126% raise_list(X, J, Xj), 127% raise_list(Y, L, Yl), 128% time(call_with_time_limit(200, (all_fun(Xj, Yl, F), card(F, C)))), 129% C =:= (K^L)^(I^J), 130% significant_length(C, Keta, 10). 131 132% ?- I=3, J=5, K=3, L=5, 133% numlist(1, I, X), numlist(1, K, Y), 134% raise_list(X, J, Xj), 135% raise_list(Y, L, Yl), 136% time( ( call_with_time_limit(200, ( 137% (all_fun(Xj, Yl, F), card(F, C)))))), 138% C =:= (K^L)^(I^J), 139% significant_length(C, Keta, 10). 140%@ % 477,828,435 inferences, 56.259 CPU in 58.472 seconds (96% CPU, 8493400 Lips) 141%@ F = 7204222, 142%@ Keta = 580. 143 144% ?- significant_length(020, X, 10). 145significant_length(0, 0, _):-!. 146significant_length(X, 1, Radix):- X < Radix, !. 147significant_length(X, L, Radix):- Y is X // Radix, 148 significant_length(Y, L0, Radix), 149 L is L0+1. 150 151% 152zdd_atom(X):- get_key(is_atom, Pred), !, call(Pred, X). 153zdd_atom(X):- (atomic(X); dvar(X)), !.
obj_id([a,b,c], Id), obj_id(Obj, Id).158obj_id(X, Id):- cofact(Id, t(X, 0, 1)). 159% 160hyphen(X, Y, X-Y). 161comma(X, Y, (X,Y)). 162equality(X, Y, (X=Y)). 163dvar('$VAR'(_)). 164 165 /***************************************** 166 * all_fun/all_mono/all_epi in ZDD * 167 *****************************************/
171% ?- all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F). 172% ?- all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C). 173% ?- N = 100, numlist(1, N, Ns), all_fun(Ns, Ns, F)^, card(F, C). 174% ?- numlist(1, 5, Ns), numlist(6, 10, Ms), 175% all_fun(Ns, Ns, F), 176% all_fun(Ms, Ms, G), 177% zdd_merge(F, G, H), 178% card(H, C), 179% C =:= 5^5 * 5^5. 180 181all_fun(D, R, F):- zdd_sort(D, D0), 182 zdd_sort(R, R0), 183 length(D0, I), 184 length(R0, J), 185 ( I > 0, J = 0 -> F = 0 186 ; bdd_sort_append(D0, 1, D1), 187 findall_fun(D1, R0, F) 188 ). 189% 190findall_fun(X, _, X):- X < 2, !. 191findall_fun(X, Rng, Y):- memo(findall_fun(X)-Y), 192 ( nonvar(Y) -> true % , write(.) % many hits. 193 ; cofact(X, t(A, L, R)), 194 findall_fun(L, Rng, L0), 195 findall_fun(R, Rng, R1), 196 join_for_alt_val(A, Rng, R1, 0, R0), 197 zdd_join(L0, R0, Y) 198 ). 199% 200join_for_alt_val(_, [], _, V, V). 201join_for_alt_val(A, [B|Bs], F, F0, F1):- 202 bdd_cons(F2, A-B, F), 203 zdd_join(F0, F2, F3), 204 join_for_alt_val(A, Bs, F, F3, F1).
209% ?- all_mono([1],[a], Is), psa(Is). 210% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 211% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 212% ?- all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C). 213% ?- all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C). 214% ?- time((numlist(1, 10, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(10, C))). 215% ?- time((numlist(1, 12, Ns), all_mono(Ns, Ns, F), card(F, C))). 216% ?- N =10, numlist(1, N, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(N, C). 217 218all_mono(D, R, F):- zdd_sort(D, D0), 219 zdd_sort(R, R0), 220 length(D0, I), 221 length(R0, J), 222 ( I @=< J -> 223 bdd_sort_append(D0, 1, D1), 224 findall_mono(D1, R0, F) 225 ; F = 0 226 ). 227 228% ?- bdd_sort_append([], 1, X), findall_mono(X, [a], Y). 229% ?- bdd_sort_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y). 230% ?- N=14, numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 231% findall_mono(X, Ns, Y), card(Y, C), 232% factorial(14, D), ( D=:=C -> writeln("*** OK ***")). 233 234findall_mono(X, _, X):- X < 2, !. 235findall_mono(X, Rng, Y):- memo(findall_mono(X,Rng)-Y), 236 ( nonvar(Y) -> true % , write(.) % many hits. 237 ; cofact(X, t(A, L, R)), 238 findall_mono(L, Rng, L0), 239 findall_mono(A, R, Rng, R0), 240 zdd_join(L0, R0, Y) 241 ). 242% 243findall_mono(A, R, Rng, R0):- findall(B-U, select(B, Rng, U), Cases), 244 findall_mono(Cases, A, R, 0, R0). 245% 246findall_mono([], _A, _R, V, V). 247findall_mono([B-Rng|Cases], A, R, U, V):- 248 findall_mono(R, Rng, U0), 249 cofact(U1, t(A-B, 0, U0)), 250 zdd_join(U, U1, U2), 251 findall_mono(Cases, A, R, U2, V).
257% ?- zdd all_epi([],[], F). 258% ?- zdd all_epi([a],[1], F), psa(F). 259% ?- zdd all_epi([a,b],[1], F), psa(F). 260% ?- zdd all_epi([a],[1,2], F), psa(F). 261% ?- zdd all_epi([a,b,c],[1,2], F), psa(F). 262% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (zdd all_epi(Ns, Ms, F)). 263% ?- time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (zdd all_epi(Ns, Ms, F)))). 264 265all_epi(D, R, F):- 266 zdd_sort(D, D0), 267 zdd_sort(R, R0), 268 length(D0, I), length(R0, J), 269 ( I @>= J -> 270 bdd_sort_append(D0, 1, D1), 271 findall_epi(D1, R0-R0, F) 272 ; F = 0 273 ).
278% ?- N=2, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 279% ?- N=3, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C), psa(X)). 280% ?- N=10, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 281% ?- N=11, numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)). 282% ?- N=14, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 283% ?- N=15, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C))))X. 284% ?- N=16, time((numlist(1, N, Ns), (zdd all_perm(Ns, X), card(X, C)))). 285%@ % 185,729,299 inferences, 205.838 CPU in 207.237 seconds (99% CPU, 902308 Lips) 286% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R), 287% length(R, L). 288 289all_perm(D, P):- zdd_sort(D, D0), 290 findall_perm(D0, P). 291% 292findall_perm([], 1):-!. 293findall_perm(D, X):- memo(perm(D)-X), 294 ( nonvar(X) -> true % , write(.) % many hits. 295 ; 296 findall(I-D0, select(I, D, D0), U), 297 join_perm_for_selection(U, 0, X)). 298% 299join_perm_for_selection([], X, X). 300join_perm_for_selection([I-D|U], X, Y):- 301 findall_perm(D, X0), 302 bdd_cons(X1, I, X0), 303 zdd_join(X1, X, X2), 304 join_perm_for_selection(U, X2, Y). 305 306 /************************************************* 307 * terms in ZDD based on families of lists * 308 *************************************************/
316% ?- zdd coalgebra_for_signature([x], [f/1], [x], E), psa(E). 317% ?- zdd coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E). 318% ?- time((zdd coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2], 319% [x,y,z,u,v,0,1], E), card(E, C))). 320%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips) 321%@ E = 173825, 322%@ C = 68641485507. 323 324coalgebra_for_signature(D, Sgn, As, E):- 325 signature(Sgn, As, T), 326 signature_map(D, T, E). 327% 328signature_map([], _, 1):-!. 329signature_map([X|Xs], T, E):- 330 signature_map(Xs, T, E0), 331 extend_signature_map(X, T, E0, E). 332% 333extend_signature_map(_, 0, _, 0):-!. 334extend_signature_map(_, 1, E, E):-!. 335extend_signature_map(X, T, E, F):- cofact(T, t(A, L, _)), 336 extend_signature_map(X, L, E, E0), 337 l_cons(X->A, E, E1), 338 zdd_join(E0, E1, F).
343% ?- zdd term_path(a, R), psa(R), term_path(A, R). 344term_path(X, Y):- 345 ( nonvar(X) -> term_to_path(X, Y) 346 ; path_to_term(Y, X) 347 ).
352% ?- zdd term_to_path(a, R), psa(R). 353% ?- zdd term_to_path(f(a, b), R), psa(R). 354% ?- zdd term_to_path(f(g(a, b), h(c, d)), R), psa(R). 355% ?- zdd term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R). 356term_to_path(X, Y):- functor(X, F, N), 357 ( N = 0 -> zdd_singleton(X, Y) 358 ; functor(X, F, N), 359 arg_path(F/N, 1, X, Y) 360 ). 361% 362arg_path(_/N, J, _, 0):- J>N, !. 363arg_path(F, I, X, Y):- J is I + 1, 364 arg(I, X, A), 365 term_to_path(A, U), 366 arg_path(F, J, X, V), 367 cofact(Y, t(arg(F, I), V, U)).
373% ?- zdd term_to_path(a, X), path_to_term(X, R). 374% ?- zdd term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R). 375% ?- zdd term_to_path(f(1,2), X), path_to_term(X, R). 376% ?- T=f(h(a), 3, g(b,2), 5), 377% (zdd term_to_path(T, X), path_to_term(X, R)), T = R. 378 379path_to_term(X, Y):- X>1, cofact(X, t(A, L, R)), 380 ( R = 1 -> Y = A 381 ; A = arg(F/_, _), 382 path_to_term(R, R0), 383 path_to_term(L, L0, []), 384 Y =..[F, R0|L0] 385 ). 386% 387path_to_term(X, U, U):- X<2, !. 388path_to_term(X, [R0|U], V):- cofact(X, t(_, L, R)), 389 path_to_term(R, R0), 390 path_to_term(L, U, V).
compare(C, U, V) is performed.397% ?- X=f(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 398% term_path_compare(C0, T, U)), compare(C, X, Y). 399% ?- X=g(a,b), Y=f(a,b, c), (zdd term_path(X, T), term_path(Y, U), 400% term_path_compare(C0, T, U)), compare(C, X, Y). 401% ?- X=g(a,b,c), Y=f(a,b), (zdd term_path(X, T), term_path(Y, U), 402% term_path_compare(C0, T, U)), compare(C, X, Y). 403 404term_path_compare(=, X, X):-!. 405term_path_compare(<, 0, _):-!. 406term_path_compare(>, _, 0):-!. 407term_path_compare(<, 1, _):-!. 408term_path_compare(>, _, 1):-!. 409term_path_compare(C, X, Y):- cofact(X, t(A, L, R)), 410 cofact(Y, t(B, L0, R0)), 411 arity_compare(C0, A, B), 412 ( C0 = (=) -> 413 term_path_compare(C1, R, R0), 414 ( C1 = (=) -> 415 left_branch_compare(C, L, L0) 416 ; C = C0 417 ) 418 ; C = C0 419 ). 420 421% Left branches are for argument lists of the name length. 422left_branch_compare(=, 0, 0):-!. 423left_branch_compare(C, X, Y):- 424 cofact(X, t(_, L, R)), 425 cofact(Y, t(_, L0, R0)), 426 term_path_compare(C0, R, R0), 427 ( C0 = (=) -> 428 left_branch_compare(C, L, L0) 429 ; C = C0 430 ). 431 432% 433arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G). 434arity_compare(C, A, B):-!, compare(C, A, B).
440% ?- zdd zdd_lift(1, X). 441% ?- zdd X<< pow([1,2]), zdd_lift(X, Y), card(Y, D), psa(Y). 442% ?- zdd X<< pow(numlist(1,10)), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D). 443% ?- N=16, numlist(1, N, Ns), 444% time((zdd X<< pow(Ns), zdd_lift(X, Y), card(Y, D))), D=:=2^N. 445%@ % 19,643,341 inferences, 31.553 CPU in 31.694 seconds (100% CPU, 622559 Lips) 446 447zdd_lift(X, X):- X<2, !. 448zdd_lift(X, Y):- memo(zdd_lift(X)-Y), 449 ( nonvar(Y) -> true %, write(.) % So so hits. 450 ; cofact(X, t(A, L, R)), 451 zdd_lift(L, L0), 452 zdd_lift(R, R0), 453 zdd_lift(A, R0, R1), 454 zdd_join(L0, R1, Y) 455 ). 456% 457zdd_lift(_, 0, 0):-!. 458zdd_lift(A, 1, Y):-!, zdd_singleton([A], Y). 459zdd_lift(A, X, Y):- cofact(X, t(B, L, _)), 460 zdd_singleton([A|B], R0), 461 zdd_lift(A, L, L0), 462 zdd_join(L0, R0, Y).
468% ?- zdd X<< pow([a,b]), card(X, C), zdd_univ(X, Y), psa(Y). 469% ?- zdd X<< pow([a,b]), zdd_univ(X, Y), psa(Y). 470 471zdd_univ(X, X):- X<2, !. 472zdd_univ(X, Y):- cofact(X, t(A, L, R)), 473 zdd_univ(R, [A], R0), 474 zdd_univ(L, L0), 475 zdd_join(L0, R0, Y). 476 477% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 478% ?- zdd X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 479 480zdd_univ(0, _, 0):-!. 481zdd_univ(1, Stack, X):-!, reverse(Stack, Stack0), 482 U =.. Stack0, 483 zdd_singleton(U, X). 484zdd_univ(X, Stack, Y):- cofact(X, t(A, L, R)), 485 zdd_univ(L, Stack, L0), 486 zdd_univ(R, [A|Stack], R0), 487 zdd_join(L0, R0, Y).
g(a1, ..., an)
where G=g/n and ai in As.493% ?- zdd arity_term(f/2, [1, x, y], T), psa(T). 494arity_term(F/N, As, T):- memo((F/N)-T), 495 ( nonvar(T) -> true 496 ; all_list(N, As, X), 497 l_cons(F, X, T0), 498 zdd_univ(T0, [], T) 499 ).
507% ?- N=10, numlist(1, N, Ns), 508% time((zdd X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))). 509% ?- zdd X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y). 510% ?- N=100, numlist(1, N, Ns), 511% time((zdd X<<pow(Ns), l_cons(f, X, Y), card(Y, C))). 512% ?- N=10, numlist(1, N, Ns), 513% time((zdd X<<pow(Ns), zdd_mul_list([f, g, h], X, Y), card(Y, C))). 514 515zdd_functor(F, X, Y):- zdd_functor(F, X, [], Y). 516% 517zdd_functor(_, 0, _, 0):-!. 518zdd_functor(F, 1, St, Y):-!, T =..[F|St], 519 zdd_singleton(T, Y). 520zdd_functor(F, X, St, Y):-cofact(X, t(A, L, R)), 521 zdd_functor(F, L, St, Y0), 522 zdd_functor(F, R, [A|St], Y1), 523 zdd_join(Y0, Y1, Y).
f(a1, ..., an)
with f/n in G and ai in As.529% ?- zdd signature([f/1, g/2], [1, x, y], U), psa(U). 530% ?- time((zdd signature([f/2, g/2, h/3, i/4, k/5], 531% [0, 1, 2, x, y, z, u, v, w], U), card(U, C))). 532 533signature([], _, 0):-!. 534signature([G|Gs], As, T):- 535 arity_term(G, As, T0), 536 signature(Gs, As, T1), 537 zdd_join(T0, T1, T).
543% ?- spy(power_list). 544% ?- zdd power_list(0, [a,b], P). 545% ?- zdd power_list(1, [a,b], P). 546% ?- N = 100, numlist(1, N, _Ns), 547% time(((zdd power_list(N, _Ns, X), card(X, _Count)))), 548% _Count > 100^100, writeln(_Count). 549%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips) 550%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101 551%@ N = 100, 552%@ X = 515002. 553 554power_list(N, As, P):- obj_id(As, Id), 555 power_list_with_id(N, Id, P). 556% 557power_list_with_id(0, Id, 1):-!, memo(power_list(0, Id)-1). 558power_list_with_id(N, Id, Y):- 559 N0 is N - 1, 560 power_list_with_id(N0, Id, Y0), 561 all_list_with_id(N, Id, Y1), 562 zdd_join(Y0, Y1, Y).
568% ?- zdd all_list(0, [a], X), psa(X). 569% ?- zdd all_list(1, [a], X), psa(X). 570% ?- N=10, numlist(1, N, Ns), (zdd all_list(4, Ns, X), card(X, C)). 571% ?- N=100, numlist(1, N, Ns), time(((zdd all_list(100, Ns, X), card(X, C)))). 572%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips) 573 574all_list(N, As, Y):- obj_id(As, Id), 575 all_list_with_id(N, Id, Y). 576% 577all_list_with_id(0, Id, 1):-!, memo(all_list(0, Id)-1). 578all_list_with_id(N, Id, Y):- memo(all_list(N, Id)-Y), 579 ( nonvar(Y) -> true 580 ; N0 is N-1, 581 all_list_with_id(N0, Id, Y0), 582 obj_id(As, Id), 583 zdd_mul_list(As, Y0, 0, Y) 584 ).
589singleton_family([], 0):-!. 590singleton_family([A|As], X):- 591 singleton_family(As, X0), 592 zdd_singleton(A, U), 593 zdd_join(U, X0, X).
598distribute_con(F, X, Y):- zdd_mul_list(F, X, 0, Y). 599% 600zdd_mul_list([], _, Y, Y). 601zdd_mul_list([A|As], Y, U, V):- 602 l_cons(A, Y, V0), 603 zdd_join(U, V0, U0), 604 zdd_mul_list(As, Y, U0, V).
609% ?- zdd X<<pow([1,2]), l_cons(a, X, Y), psa(Y). 610 611l_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).618l_append([], X, X). 619l_append([A|As], X, Y):- 620 l_append(As, X, X0), 621 l_cons(A, X0, Y). 622 623% ?- zdd bdd_sort_append([], 1, X), findall_epi(X, [a]-[a], Y). 624% ?- zdd bdd_sort_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 625% ?- zdd bdd_sort_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 626% ?- zdd bdd_sort_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C). 627% ?- zdd bdd_sort_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y). 628% ?- N = 2, (zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 629% ?- N = 3, (zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 630% ?- N = 10,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 631% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 632% ?- N = 11,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 633% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 634% ?- N = 12,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 635% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 636% ?- N = 13,(zdd {numlist(1, N, Ns)}, bdd_sort_append(Ns, 1, X), 637% { time((zdd findall_epi(X, Ns-Ns, Y), card(Y, C)))}). 638 639select_target(Range, U, B, V):- member(B, Range), 640 ( select(B, U, V) -> true 641 ; V = U 642 ). 643 644% 645findall_epi(0, _, 0):-!. 646findall_epi(1, _-U, X):-!, 647 ( U=[] -> X = 1 648 ; X = 0 649 ). 650findall_epi(X, RngU, Y):- memo(findall_epi(X, RngU)-Y), 651 ( nonvar(Y) -> true % , write(.) % many hits. 652 ; cofact(X, t(A, L, R)), 653 findall_epi(L, RngU, L0), 654 findall_epi(A, R, RngU, R0), 655 zdd_join(L0, R0, Y) 656 ). 657% 658findall_epi(A, R, Rng-U, R0):- 659 findall(B-(Rng-V), select_target(Rng, U, B, V), Cases), 660 findall_epi(Cases, A, R, 0, R0). 661% 662findall_epi([], _, _, V, V). 663findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V):- 664 findall_epi(R, Rng-Rng0, U0), 665 cofact(U1, t(A-B, 0, U0)), 666 zdd_join(U, U1, U2), 667 findall_epi(Cases, A, R, U2, V). 668 669% ?- zdd merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X). 670merge_funs(Fs, X):- fold_merge_funs(Fs, 1, X). 671% 672fold_merge_funs([], X, X). 673fold_merge_funs([G|Fs], X, Y):- 674 fun_block(G, X0), 675 zdd_merge(X, X0, X1), 676 fold_merge_funs(Fs, X1, Y). 677% 678fun_block(G, X):- 679 ( G = mono(D-R) -> all_mono(D, R, X) 680 ; G = epi(D-R) -> all_epi(D, R, X) 681 ; G = fun(D-R), 682 all_fun(D, R, X) 683 ). 684 685% ?- N=2, numlist(1, N, Ns), 686% (zdd set_compare(opp_compare), 687% X<<pow(Ns), psa(X), set_compare(compare), 688% zdd_normalize(X, Y), psa(Y)). 689 690zdd_normalize(X, X):- X<2, !. 691zdd_normalize(X, Y):- memo(normalize(X)-Y), 692 ( nonvar(Y) -> true % , write(.) % Many hits. 693 ; cofact(X, t(A, L, R)), 694 zdd_normalize(L, L0), 695 zdd_normalize(R, R1), 696 zdd_insert(A, R1, R0), 697 zdd_join(L0, R0, Y) 698 ). 699 700% ?- N = 1000, numlist(1, N, Ns), 701% time((X<<pow(Ns), rank_family_by_card(X, P), card(P, C))). 702 703% ?- N = 1000, numlist(1, N, Ns), 704% time((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C))). 705 706% ?- N = 1000, numlist(1, N, Ns), 707% time((( X<<pow(Ns), 708% get_family_of_rank(500, X, Y), 709% card(Y, C)))).
714get_family_of_rank(Order, X, F):- rank_family_by_card(X, _), 715 memo(family_with_card(Order)-F). 716 717% ?- X<<pow([1]). 718% ?- X<<set([a]), rank_family_by_card(X, P), 719% memo(family_with_card(0)-L), sets(L, Sl), 720% memo(family_with_card(1)-M), sets(M, Sm).
726rank_family_by_card(0, 0):-!. 727rank_family_by_card(1, 0):-!, memo(family_with_card(0)-1). 728rank_family_by_card(I, P):- memo(rank_family_by_card_done(I)-B), 729 ( nonvar(B) -> true 730 ; cofact(I, t(A, L, R)), 731 rank_family_by_card(L, Pl), 732 rank_family_by_card(R, Pr), 733 max(Pl, Pr, P0), 734 insert_one_to_family(A, P0, New), 735 P is P0 + 1, 736 memo(family_with_card(P)-New), 737 B = true 738 ). 739% 740insert_one_to_family(A, 0, G):-!, memo(family_with_card(0)-F), 741 zdd_insert(A, F, G). 742insert_one_to_family(A, P, G):- P0 is P-1, 743 insert_one_to_family(A, P0, G0), 744 memo(family_with_card(P)-Fp), 745 zdd_insert(A, Fp, G), 746 zdd_join(Fp, G0, Gp), 747 set_memo(family_with_card(P)-Gp). 748 749 /********************** 750 * State access * 751 **********************/ 752 753get_extra(Extra):- b_getval(zdd_extra, Extra). 754% 755set_extra(Extra):- b_setval(zdd_extra, Extra). 756 757% ?- bump_up(a, N), bump_up(a, K). 758bump_up(Key):- b_getval(zdd_extra, Extra), 759 ( select(Key-N0, Extra, Extra0) -> true 760 ; N0 = 0, 761 Extra0 = Extra 762 ), 763 N is N0 + 1, 764 b_setval(zdd_extra, [Key-N|Extra0]). 765 766 767:- meta_predicate set_compare(). 768set_compare(Compare):- nb_setval(zdd_compare, Compare). 769 770% ?- zdd_compare(C, a, b). 771get_compare(Compare):- b_getval(zdd_compare, Compare). 772% 773zdd_compare(C, X, Y):- get_compare(F), call(F, C, X, Y). 774 775% ?- zdd_sort([1->1, 1->2, 1-1, 2-2], X). 776zdd_sort(X, Y):- get_compare(Comp), predsort(Comp, X, Y). 777 778% ?- get_key(a, V), set_key(a, 1), get_key(a, W). % fail. 779% ?- set_key(a, 1), get_key(a, W). 780get_key(K, V):- b_getval(zdd_extra, Assoc), 781 memberchk(K-V, Assoc). 782% 783set_key(K, V) :- b_getval(zdd_extra, Assoc), 784 ( select(K-_, Assoc, Assoc0) 785 -> b_setval(zdd_extra, [K-V|Assoc0]) % nb_linkval not work. 786 ; b_setval(zdd_extra, [K-V|Assoc]) % nb_linkval not work. 787 ). 788% 789nb_set_key(K, V) :- b_getval(zdd_extra, Assoc), 790 ( select(K-_, Assoc, Assoc0) 791 -> nb_setval(zdd_extra, [K-V|Assoc0]) 792 ; nb_setval(zdd_extra, [K-V|Assoc]) 793 ). 794 795:- meta_predicate set_pred(, ). 796set_pred(K, V) :- set_key(K, V). 797 798% ?- open_key(a, []), update_key(a, X, Y), X=[1|Y], 799% get_key(a, Z), close_key(a). 800 801% ?- zdd((open_key(a, []), update_key(a, X, Y), {X=[1|Y]}, 802% get_key(a, Z), close_key(a), get_key(a, U))). % false 803 804% 805open_key(K, Val):- set_key(K, Val). 806% 807update_key(X, Old, New):- b_getval(zdd_extra, Assoc), 808 select(X-Old, Assoc, Assoc0), 809 b_setval(zdd_extra, [X-New|Assoc0]). 810% 811close_key(Key):- b_getval(zdd_extra, Assoc), 812 ( select(Key-_, Assoc, Assoc0) -> 813 b_setval(zdd_extra, Assoc0) 814 ; true 815 ). 816 817% ?- varnum(D), varnum(E).
822varnum(D):- get_key(varnum, D). 823 824% ?- sort([1->1, 1->2, 1-1, 2-2], X). 825% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X). 826% ?- zdd_sort_rev([1,2,3], X). 827 828compare_rev(Comp, C, A, B):- call(Comp, C, B, A). 829% 830zdd_sort_rev(X, Y):- get_compare(Comp), 831 predsort(compare_rev(Comp), X, Y). 832 833% ?- pred_zdd(opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)). 834:- meta_predicate pred_zdd(, ). 835pred_zdd(Comp, X):- set_compare(Comp), call(X). 836 837% ?- X<<pow([a,b,c]), zdd_memberchk([a,c], X). 838% ?- X<<pow([a,b,c]). 839% ?- spy(zdd_ord_power). 840 841 842% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([], X))). 843% ?- zdd((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
848zdd_memberchk(L, Z):- zdd_sort(L, L0), zdd_ord_memberchk(L0, Z). 849% 850zdd_ord_memberchk([], Z):- !, zdd_has_1(Z). 851zdd_ord_memberchk([A|As], Z):- Z>1, 852 cofact(Z, t(B, L, R)), 853 ( A == B 854 -> zdd_ord_memberchk(As, R) 855 ; A @> B, 856 zdd_ord_memberchk([A|As], L) 857 ). 858 859% PASS 860% ?- zdd X<<pow([a,b]), card(X, C). 861% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))). 862% ?- zdd {X=1, Y =2, Z is X + Y}. 863% ?- zdd X<<set([a]), sets(X, U). 864% ?- zdd((X<<pow([a,b]), S<<sets(X))). 865% ?- zdd((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 866% ?- zdd(((X<< *(:append([a,b], [c,d]))), sets(X, Y))). 867% ?- zdd((X<<(*[a,b]& *[c,d]), S<<sets(X))). 868% ?- zdd((X<<{[a],[b],[c]}, sets(X,S))). 869% ?- zdd((X<<{[a],[b, c]}, sets(X,S))). 870% ?- zdd((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 871% ?- zdd((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 872% ?- I =1000, J =2000, 873% time( (zdd 874% { numlist(1, I, L), 875% numlist(1, J, M)}, 876% X << pow(L), 877% Y << pow(M), 878% Z << (Y - X), 879% card(Z, C), 880% {C =:= 2^J-2^I} )). 881 882 883% PASS 884% ?- zdd((X<<cnf(0), Y<<sets(X))). 885% ?- zdd((X<<cnf(1), Y<<sets(X))). 886% ?- zdd((X<<cnf(2), Y<<sets(X))). 887% ?- zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 888% ?- ltr_zdd((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 889% ?- zdd((X<<cnf(a), Y<<sets(X))). 890% ?- zdd((X<<cnf(-a), Y<<sets(X))). 891% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 892% ?- zdd((X<<cnf(-(a+b)), Y<<sets(X))). 893% ?- zdd((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 894% ?- zdd((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 895% ?- zdd((X<<cnf(-(-a + -b)), Y<<sets(X))). 896% ?- zdd((X<<dnf(a), Y<<sets(X), extern(Y, Y0))). 897% ?- zdd((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))). 898% ?- zdd((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))). 899% ?- zdd((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))). 900% ?- zdd((X<<dnf(a+b), Y<<sets(X))). 901% ?- zdd((X<<dnf(-(a+b)), Y<<sets(X))). 902% ?- zdd((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 903% ?- zdd((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 904% ?- zdd((X<<dnf(-(-a + -b)), Y<<sets(X))). 905% ?- zdd((X<<dnf((-a + a)), Y<<sets(X))). 906% ?- zdd((X<<dnf(-(-a + a)), Y<<sets(X))). 907% ?- zdd(X << *(:append([a,b], [c,d]))). 908% ?- zdd((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))). 909% ?- zdd((X << *[a,b], sets(X, S))). 910% ?- zdd((X << +[a,b], sets(X, S))). 911% ?- zdd((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 912% ?- zdd((zdd_list_to_singletons([], X), prz(X))). 913% ?- zdd((zdd_list_to_singletons([a], X), prz(X))). 914% ?- zdd((zdd_list_to_singletons([a,b], X), prz(X))). 915% ?- zdd((zdd_list_to_singletons([c, a, b], X), prz(X))). 916% ?- zdd X << *[a,b], psa(X). 917% ?- zdd X << +[a,b], psa(X). 918 919% ?- I =1000, J is I + 1, numlist(1, I, L), 920% prepare_ltr_list(L, L0), 921% time(zdd(( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
929zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 930% 931zdd_list_to_singletons([], 1, _). 932zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 933 zdd_singleton(A, Y0, S), 934 zdd_join(Y0, Y, X, S). 935 936% PASS. 937% ?- zdd((zdd_partial_choices([], X), prz(X))). 938% ?- zdd((zdd_partial_choices([[a], [b]], X), prz(X))). 939% ?- zdd((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 940% ?- zdd((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 941% ?- zdd((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 942% ?- zdd((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 943% ?- zdd((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))). 944% ?- zdd((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 945% ?- zdd((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 946% ?- findall([I], between(1, 10000, I), Ls), 947% zdd((zdd_partial_choices(Ls, X), 948% card(X, C))), !, C =:= 2^10000.
953zdd_partial_choices([], 1):-!. 954zdd_partial_choices([L|Ls], X):- zdd_partial_choices(Ls, X0), 955 sw_fold_insert(zdd, L, X0, 0, X1), 956 zdd_join(X0, X1, X). 957 958:- meta_predicate zdd_find(, , ).
963% ?- zdd X<< pow([a,b,c]), zdd_find(=(c), X, Y). 964% ?- zdd X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y). 965% ?- zdd X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y). 966 967zdd_find(F, X, Y):- X>1, 968 cofact(X, t(A, L, R)), 969 ( call(F, A), Y = A 970 ; zdd_find(F, L, Y) 971 ; zdd_find(F, R, Y) 972 ). 973 974use_table(G):- functor(G, F, N), 975 setup_call_cleanup( 976 table(F/N), % 977 G, 978 untable(F/N) % 979 ). 980 981 982 983% PASS. 984% 985% ?- zdd P<<pow([1,2,3]), {X=1;X=2}, card(P,C). 986% ?- zdd P<<pow([1,2,3]), card(P,C). 987% ?- zdd P<<pow([1,2,3]), card(P,C). 988 989% ?- zdd P << set([1,2,3,2,3]), psa(P). 990 991% ?- zdd P << ({[1,2,3,2,3]} + {[4, 2,4]}), psa(P). 992 993% ?- zdd {append([a,b], [c,d], X)}. 994% ?- zdd X << :append([a,b], [c,d]). 995% ?- zdd (zdd X << :append([a,b], [c,d])). 996% ?- zdd (zdd (zdd X << :append([a,b], [c,d]))). 997% ?- zdd (zdd (zdd ( X<<pow([1,2]), true, true))). 998% ?- zdd (zdd zdd X<<pow([1,2]), true, true, card(X, C)). 999% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), card(X, C)). 1000 1001 1002% ?- show_state. 1003 1004% ?- fetch_state, X<<pow([a,b]), fetch_state, card(X, C). 1005% ?- zdd X<<{[a],[b]}, Y<<{[b], [c]}, zdd_merge(X, Y, Z), psa(Z). 1006% ?- 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)).1015opp_compare(<, -(_,_), ->(_,_)):-!. 1016opp_compare(>, ->(_,_), -(_,_)):-!. 1017opp_compare(C, X, Y):- compare(C, Y, X). % reverse order 1018 1019% ?- zdd X<< @(abc), psa(X). 1020% ?- 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.1037% ?- X<< +[ *[a,b], *[c, d]], psa(X). 1038% ?- <<(X, +[*[a,b], *[c,d]]), psa(X). 1039% ?- X<< card(pow([1,2]) + pow([a,b])). 1040% ?- X<< card(pow([1,2])). 1041 1042 1043:- meta_predicate <<(, ). 1044<<(X, E) :- zdd_eval(E, X).
zdd_solve(+G, +S, +M) is det.
Solve goal G with state S and module M.1051% ?- zdd X<< (+[0, 1]), psa(X). 1052% ?- zdd X<< (+[0,1]), {fetch_state, b_getval('$zdd', S0), writeln(S0)}. 1053% ?- zdd X<< *[0, 1, 2, 3], psa(X). 1054% ?- zdd X<< *[*[]], psa(X). 1055% ?- zdd X<< *[[]], psa(X). 1056% ?- zdd X<< *[+[]], psa(X). 1057% ?- zdd X<<pow(:numlist(1, 100)), card(X, C). 1058% ?- zdd X<< :numlist(1, 100). 1059 1060% % 1061% zdd_solve(true, _) :-!. 1062% zdd_solve(M:G, _) :-!, zdd_solve(G, M). 1063% zdd_solve({G}, M) :-!, call(M:G). 1064% zdd_solve(X<<E, M) :-!, zdd_numbervars(E), zdd_eval(E, X, M). 1065% zdd_solve((A,B), M) :-!, zdd_solve(A, M), zdd_solve(B, M). 1066% zdd_solve((A;B), M) :-!, (zdd_solve(A, M); zdd_solvde(B, M)). 1067% zdd_solve((A->B), M) :-!, (zdd_solve(A, M) -> zdd_solve(B, M)). 1068% 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,
1105% Pass. 1106% ?- X<<dnf(a*b), psa(X). 1107% ?- X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C). 1108% ?- X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))). 1109% ?- X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C). 1110 1111% Pass. 1112% ?- zdd X<< @a. 1113% ?- zdd X<< a, psa(X). 1114% ?- zdd X<<pow([a,b]), card(X, C). 1115% ?- zdd X<<pow([a,b])-pow([a]), card(X, C). 1116% ?- zdd X<< set(:(append([1,2],[3,4]))), psa(X). 1117% ?- zdd((X<< +(:append([1,2],[3,4])), psa(X))). 1118% ?- zdd((X<< (@a + @b), psa(X))). 1119% ?- zdd((X<< ((@a + @b)* @c), psa(X))). 1120% ?- zdd((X<< [a,b])). 1121% ?- zdd((X<< set(:(append([a,b],[c,d]))), psa(X))). 1122% ?- zdd((X<< set(!append([a,b],[c,d])), psa(X))). % error 1123% ?- zdd(X<< card(pow([a,b]))). 1124% ?- zdd(X<< card(pow(:numlist(1, 100)))). 1125% ?- zdd((X<< set([1]), Y<< (X+X), psa(X))). 1126% ?- zdd((X<< set([1]), psa(X))). 1127% ?- zdd((X<< set([]))). 1128% ?- zdd((X << {[a], [b], [c]}, psa(X))). 1129% ?- zdd((X << {[a], [b], [c]}, card(X, C))). 1130 1131% PASS. 1132% ?- zdd X << card(pow(:append(:numlist(1,3), :numlist(4,5)))). 1133 1134% ?- zdd((X << set(:append(numlist(1,2), numlist(4,5))))). 1135% ?- zdd((X << set(:append(numlist(1,10), numlist(11,20))))). 1136% ?- zdd { numlist(1,10,A), numlist(11,20, B)}, X<< pow( :append(A, B)), 1137% card(X, C). 1138% ?- zdd X << pow(:(numlist(1,2))), card(X, C). 1139% ?- zdd X << pow(:(numlist(1,2))). 1140 1141% ?- zdd((X << pow(:(! charlist(a,z))), card(X, C))). 1142% ?- zdd((X << pow(:(! charlist(a-z))), card(X, C))). 1143% ?- zdd((X << pow([a,b]))). 1144% ?- zdd((X << *[a, b, c])). 1145% ?- zdd((X << (*[a, b, c] + *[a,b,c]), psa(X))). 1146% ?- zdd((X << (*[a, b, c] + *[2, 3]), psa(X))). 1147% ?- zdd((C << card(pow([a,b,c,1,2,3])))). 1148% ?- zdd((C << card(pow(:append([a,b,c], [1,2,3]))))). 1149% ?- zdd((C << pow(:numlist(1, 3)))). 1150% ?- zdd((C << @(a), psa(C))). 1151 1152% Pass. 1153% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))). 1154% ?- zdd((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))). 1155% ?- zdd((U << +(:(append([a,b,c], [d,e,f]))), psa(U))). 1156% ?- zdd((U << *(:(append([a,b,c], [d,e,f]))), psa(U))). 1157% ?- zdd((U << +(:(append(:append([a,b,c], [x,y,z]), [1, 2]))), psa(U))). 1158% ?- zdd((U << +[ *[a,b], *[c,d]], psa(U))). 1159% ?- zdd((U << *[ +[a,b], +[c,d]], psa(U))). 1160% ?- zdd((U << *[ *[a,b], *[c,d]], psa(U))). 1161% ?- zdd((U << *[ *[a,b], +[c,d]], psa(U))). 1162% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1163% ?- zdd((U << card(pow(:(append(:append([a,b,c], [x,y,z]), [1,2,3])))))). 1164% ?- zdd((U << #(card(pow([a]))))). 1165% ?- zdd((U << :succ(#(card(pow([a])))))). 1166% ?- zdd((U << card(pow([a])))). 1167% ?- zdd U << card(pow([a])+pow([b])). 1168 1169% ?- zdd((U << :(=(3)))). 1170% ?- zdd((U << *([1,2,3]), psa(U))). 1171% ?- zdd((U << :plus(#(card(pow([a,b]))), #(card(pow([1,2])))))). 1172% ?- zdd((U << @a)). % singleton. 1173% ?- zdd((U << @2)). 1174% ?- zdd((U << [a,b])). 1175% ?- zdd((U << *[a,b], psa(U))). 1176% ?- zdd((U << +[a,b], psa(U))). 1177% ?- zdd((U << +[*[a,b], *[c,d]], psa(U))). 1178% ?- zdd((U << +[+[a,b], +[c,d]], psa(U))). 1179% ?- zdd((U << *[+[a,b], +[c,d]], psa(U))). 1180% ?- zdd((U << *[*[a,b], *[c,d]], psa(U))). 1181% ?- zdd((U << :(!call(=, hello)))). 1182% ?- zdd((U << :(call($(=), :append([a,b],[c,d]))))). 1183% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< zdd_join(X, Y), psa(Z). 1184% ?- zdd X<< *[a,b], Y<< *[c,d], Z<< (X+Y), psa(Z). 1185% 1186basic_type(X):- number(X); 1187 string(X); 1188 is_list(X); 1189 var(X). 1190 1191% ?- X<< p(2,3), psa(X). 1192% ?- X<< pq(2,3), psa(X). % Error. 1193% ?- findall(p(I), between(1,3,I), As), X<< +As, psa(X). 1194 1195default_atom(X):- functor(X, F, _), 1196 atom_chars(F, [A|As]), 1197 char_type(A, alpha), 1198 digit_chars(As). 1199% 1200digit_chars([]). 1201digit_chars([D|Ds]):- char_type(D, digit), 1202 digit_chars(Ds).
1207% Unusual first, but legal samples. 1208% ?- zdd U << @(=(3)), psa(U). 1209% ?- zdd U << +(!append([a], [b])), psa(U). 1210% ?- zdd U << (@a+ @b+ @c), psa(U). 1211% ?- zdd U << append([a], [b]). 1212% ?- zdd U << +(append([[a]], [[b]])), psa(U). 1213% ?- zdd U << get_compare. 1214% ?- zdd get_compare(X). 1215% ?- zdd U << arith(1+2). 1216% ?- zdd U << plus(arith(1+2), arith(3+4)). 1217% ?- zdd U << (@A+ @B+ @C), psa(U). 1218 1219zdd_eval(X, Y):- context_module(M), 1220 zdd_numbervars(X), 1221 zdd_eval(X, Y, M).
1227% Note that intgeger is used as a unique name of a ZDD. 1228% use indicator `@` as `@(3)` for 3 as an atom. 1229 1230zdd_eval(X, X, _) :- basic_type(X), !. 1231zdd_eval({}, 0, _) :-!. % The empty family of sets. 1232zdd_eval({X}, Y, _) :-!, associative_comma(X, U, []), zdd_family(U, Y). 1233zdd_eval($(X), X, _) :-!. 1234zdd_eval(!(X), Y, M) :-!, call(M:X, Y). 1235zdd_eval(M:X, Y, _) :-!, zdd_eval(X, Y, M). 1236zdd_eval(X, Y, _) :- zdd_basic(X, Y), !. 1237zdd_eval(X, Y, M) :- zdd_eval_args(X, X0, M), 1238 ( zdd_apply(X0, Y) -> true 1239 ; call(M:X0, Y) 1240 ). 1241% 1242zdd_eval_args(A, A, _):- atomic(A), !. 1243zdd_eval_args(A, B, M):- 1244 functor(A, Fa, Na), 1245 functor(B, Fa, Na), 1246 zdd_eval_args(1, A, B, M). 1247% 1248zdd_eval_args(I, A, B, M):- arg(I, A, U), !, 1249 zdd_eval(U, V, M), 1250 arg(I, B, V), 1251 J is I+1, 1252 zdd_eval_args(J, A, B, M). 1253zdd_eval_args(_, _, _, _). 1254 1255 /*********************************************** 1256 * Currently reserved names of operations. * 1257 ***********************************************/ 1258zdd_basic(@(A), Y) :-!, zdd_singleton(A, Y). 1259zdd_basic(X, Y) :- default_atom(X), !, zdd_singleton(X, Y). 1260zdd_basic(dnf(A), X) :-!, dnf(A, X). 1261zdd_basic(cnf(A), X) :-!, cnf(A, X). 1262zdd_basic(arith(E), X) :-!, X is E. 1263zdd_basic(X, Y) :- (atom(X); dvar(X)), !, zdd_singleton(X, Y).
1270zdd_apply(ltr_set(L), Y):-!, ltr_append(L, 1, Y). 1271zdd_apply(gf2(A), X) :-!, gf2(A, X). 1272zdd_apply(qp(A), X) :-!, mqp(A, X). 1273zdd_apply(cofact(A, L, R), X) :-!, cofact(X, t(A, L, R)). 1274zdd_apply(cofact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1275zdd_apply(fact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1276zdd_apply(+(X), Y) :-!, zdd_vector_exp(+(X), Y). 1277zdd_apply(*(X), Y) :-!, zdd_vector_exp(*(X), Y). 1278zdd_apply(X + Y, Z) :-!, zdd_join(X, Y, Z). 1279zdd_apply(X * Y, Z) :-!, zdd_merge(X, Y, Z). 1280zdd_apply(merge(X, Y), Z) :-!, zdd_merge(X, Y, Z). 1281zdd_apply(-(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1282zdd_apply(\(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1283zdd_apply((X // Y), Z) :-!, zdd_div(X, Y, Z). 1284zdd_apply((X / Y), Z) :-!, zdd_mod(X, Y, Z). 1285zdd_apply((X mod Y), Z) :-!, zdd_mod(X, Y, Z). 1286zdd_apply(&(X, Y), Z) :-!, zdd_meet(X, Y, Z). 1287zdd_apply(prod(X, Y), Z):-!, zdd_product(X, Y, Z). 1288zdd_apply(**(X, Y), Z) :-!, zdd_product(X, Y, Z). 1289zdd_apply(pow(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1290zdd_apply(power(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1291zdd_apply(set(X), Z) :- bdd_sort_append(X, 1, Z). 1292 1293 1294 /********************************* 1295 * zdd vector expressions * 1296 *********************************/
1301% ?- zdd((X<< +[[1,2],[a,b]], psa(X), card(X, C))). 1302% ?- zdd((X<< *[[1,2],[a,b]], psa(X), card(X, C))). 1303% ?- zdd((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))). 1304% ?- zdd X<< +[*[1,2], *[a,b]], psa(X). 1305% ?- zdd X<< +[*[1,2], *[1]], psa(X). 1306% ?- zdd X<< +[*[1,2], *[a,b]]. 1307% ?- zdd((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))). 1308% ?- zdd((X<< *[1,2], psa(X), card(X, C))). 1309% ?- zdd((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))). 1310% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1311% ?- zdd zdd_vector_exp(+[[a],*[b,c]], X), psa(X). 1312% ?- zdd zdd_vector_exp(+[a,b,c], X), psa(X). 1313% ?- zdd zdd_vector_exp(*[a,b,c], X), psa(X). 1314% ?- zdd zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X). 1315% ?- zdd zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X). 1316% ?- zdd zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X). 1317% ?- zdd X<< *[a, b], psa(X). 1318% ?- zdd X<< +[a, b], psa(X). 1319% ?- zdd X<< *[A, B], psa(X). 1320% ?- zdd X<< *[*[0, 1], *[2,3]], psa(X). 1321% ?- zdd X<< *[*[], *[2,3]], psa(X). 1322% ?- zdd X<< *[0, 1, *[2,3]], psa(X). 1323% ?- zdd zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1324% ?- zdd zdd_vector_exp(+[a,b], X), psa(X). 1325 1326zdd_vector_exp(*(X), Y):-!, zdd_vector_exp(*, X, Y). 1327zdd_vector_exp(+(X), Y):-!, zdd_vector_exp(+, X, Y). 1328zdd_vector_exp(X, Y):- zdd_singleton(X, Y). 1329% 1330zdd_vector_exp(*, [], 1):-!. 1331zdd_vector_exp(+, [], 0):-!. 1332zdd_vector_exp(F, [A|As], R):-!, % F in [*,+]. 1333 zdd_vector_exp(A, U), 1334 zdd_vector_exp(F, As, V), 1335 apply_binary_basic(F, U, V, R). 1336zdd_vector_exp(_, A, R):- zdd_singleton(A, R). 1337% 1338apply_binary_basic(*, X, Y, Z):-!, zdd_merge(X, Y, Z). 1339apply_binary_basic(+, X, Y, Z):- zdd_join(X, Y, Z). 1340% 1341zdd_fold_join([], Z, Z). 1342zdd_fold_join([X|Xs], Z, Z0):- 1343 zdd_join(X, Z, Z1), 1344 zdd_fold_join(Xs, Z1, Z0). 1345% 1346zdd_fold_merge([], Z, Z). 1347zdd_fold_merge([X|Xs], Z, Z0):- 1348 zdd_merge(X, Z, Z1), 1349 zdd_fold_merge(Xs, Z1, Z0). 1350% 1351fold_singleton_join([], X, X). 1352fold_singleton_join([A|As], X, Y):- 1353 zdd_singleton(A, U), 1354 zdd_join(U, X, X0), 1355 fold_singleton_join(As, X0, Y). 1356 1357% ?- zdd X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X). 1358% ?- zdd X<< (+[a,b]), psa(X). 1359% ?- zdd X<< +[*[a,b]] + +[*[c,d]], psa(X). 1360% ?- zdd X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X\Y). 1361% ?- zdd X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X-Y). 1362 1363zdd_super_power([], P, P). 1364zdd_super_power([A|As], P, Q):- 1365 zdd_super_power(As, P, Q0), 1366 zdd_insert(A, Q0, Q). 1367% 1368single_set(L, Y) :-!, bdd_sort_append(L, 1, Y). 1369 1370% ?- zdd((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 1371family(X, Y):- zdd_numbervars(X), zdd_family(X, Y).
1377zdd_family(X, Y):- zdd_numbervars(X), zdd_family(X, 0, Y). 1378 1379% ?- zdd zdd_family([[a],[a,b]], X), card(X, C), psa(X). 1380% ?- zdd zdd_family([[], [a,a],[a,b]], X), psa(X). 1381zdd_family([], U, U). 1382zdd_family([X|Xs], U, V):- 1383 zdd_insert_atoms(X, 1, X1), 1384 zdd_join(X1, U, U0), 1385 zdd_family(Xs, U0, V). 1386 1387% ?- zdd((ltr_family([[a, b], [c, d]], X), sets(X,S))). 1388% ?- zdd((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 1389% ?- zdd((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 1390% ?- zdd((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 1391% ?- zdd((X << dnf((a+(-b)+a)), psa(X))). 1392% ?- zdd((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 1393% ?- zdd((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))). 1394% ?- ltr_zdd ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X). 1395% ?- ltr_zdd ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X). 1396% ?- ltr_zdd ltr_family([[a],[-b, -a,-c]], X), psa(X). 1397% 1398ltr_family(X, Y):- ltr_family(X, 0, Y). 1399 1400% 1401ltr_family([], U, U). 1402ltr_family([X|Xs], U, V):- 1403 ltr_append(X, 1, X0), 1404 ltr_join(X0, U, U0), 1405 ltr_family(Xs, U0, V). 1406 1407 /************************ 1408 * choices * 1409 ************************/
1414% ?- zdd, X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y). 1415% ?- N=10, numlist(1, N, Ns), (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1416% zdd_choices(X, Y), card(Y, C)). 1417% ?- N=1000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), 1418% zdd_choices(X, Y), card(Y, C))). 1419 1420zdd_choices(0, 1):-!. 1421zdd_choices(1, 0):-!. 1422zdd_choices(X, Y):- memo(choices(X)-Y), 1423 ( nonvar(Y)->true %, write(+) % many hits when X has the empty set. 1424 ; cofact(X, t(A, L, R)), 1425 zdd_choices(L, L0), 1426 zdd_choices(R, R0), 1427 cofact(R1, t(A, R0, 1)), 1428 zdd_merge(L0, R1, Y) 1429 ). 1430 1431 1432 /************************************************* 1433 * Operation on zdd join/merge/meet/subtr/cons * 1434 *************************************************/
1439zdd_join(0, X, X):-!. 1440zdd_join(X, 0, X):-!. 1441zdd_join(X, X, X):-!. 1442zdd_join(1, X, Y):-!, zdd_join_1(X, Y). 1443zdd_join(X, 1, Y):-!, zdd_join_1(X, Y). 1444zdd_join(X, Y, Z):- 1445 ( Y < X -> memo(zdd_join(Y, X)-Z) 1446 ; memo(zdd_join(X, Y)-Z) 1447 ), 1448 ( nonvar(Z) -> true 1449 ; cofact(X, t(A, L, R)), 1450 cofact(Y, t(A0, L0, R0)), 1451 zdd_compare(C, A, A0), 1452 ( C = (<) -> 1453 zdd_join(L, Y, U), 1454 cofact(Z, t(A, U, R)) 1455 ; C = (=) -> 1456 zdd_join(L, L0, U), 1457 zdd_join(R, R0, V), 1458 cofact(Z, t(A, U, V)) 1459 ; zdd_join(L0, X, U), 1460 cofact(Z, t(A0, U, R0)) 1461 ) 1462 ).
cofact(Z, t(X, 0, Y), S).
Having analogy Z = [X|Y] in mind.1468% ?- bdd_cons(X, a, 1), bdd_cons(X, A, B). 1469% ?- bdd_cons(X, a, 0), bdd_cons(X, A, B). % false 1470 1471bdd_cons(X, Y, Z):- ( var(X); X>1 ), !, cofact(X, t(Y, 0, Z)). 1472 1473% ?- zdd((X<<(*[a]+ *[b]+ []), psa(X))). % false for []. 1474% ?- zdd((X<<(*[a]+ *[b]+ 1), psa(X))). 1475% ?- zdd((X<<(*[a]+ *[b]+ 0), psa(X))). 1476% ?- zdd((X<<(*[a]+ *[b]), psa(X))). 1477% ?- zdd((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))). 1478 1479% zdd_join_1(+X, -Y, +G) is det. 1480% Y is the union of X and 1 (the singleton {{}}). 1481 1482% ?- numlist(1,100, Ns), (zdd X<<pow(Ns), {fetch_state(S), time(repeat(100, zdd_join_1(X,_,S)))}). 1483zdd_join_1(X, X):- zdd_has_1(X), !. 1484zdd_join_1(X, Y):- zdd_add_1(X, Y). 1485% 1486zdd_add_1(0, 1):-!. 1487zdd_add_1(X, Y):- cofact(X, t(A, L, R)), 1488 zdd_add_1(L, L0), 1489 cofact(Y, t(A, L0, R)). 1490 1491% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1492%@ * 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 1493%@ X = Y, Y = Z, Z = 4, 1494%@ S = [[a, b]]. 1495% ?- zdd((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1496% ?- zdd((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))). 1497% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))). 1498% ?- trace, zdd(X=[b, a]). 1499% ?- zdd((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 1500% ?- zdd((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
1505zdd_meet(0, _, 0):-!. 1506zdd_meet(_, 0, 0):-!. 1507zdd_meet(1, X, Y):-!, zdd_meet_1(X, Y). 1508zdd_meet(X, 1, Y):-!, zdd_meet_1(X, Y). 1509zdd_meet(X, X, X):-!. 1510zdd_meet(X, Y, Z):- 1511 ( X @< Y -> memo(zdd_meet(X,Y)-Z) 1512 ; memo(zdd_meet(Y,X)-Z) 1513 ), 1514 ( nonvar(Z) -> true 1515 ; cofact(X, t(A, L, R)), 1516 cofact(Y, t(A0, L0, R0)), 1517 zdd_compare(C, A, A0), 1518 ( C = (<) -> zdd_meet(L, Y, Z) 1519 ; C = (=) -> 1520 zdd_meet(L, L0, U), 1521 zdd_meet(R, R0, V), 1522 cofact(Z, t(A, U, V)) 1523 ; zdd_meet(L0, X, Z) 1524 ) 1525 ).
1530zdd_meet_1(X, 1):- zdd_has_1(X), !. 1531zdd_meet_1(_, 0).
1536% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), Z<<(X-Y), psa(Z). 1537% ?- zdd((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 1538% 1539zdd_subtr(X, X, 0):-!. 1540zdd_subtr(0, _, 0):-!. 1541zdd_subtr(X, 0, X):-!. 1542zdd_subtr(X, 1, Y):-!, zdd_subtr_1(X, Y). 1543zdd_subtr(1, X, Y):-!, 1544 ( zdd_has_1(X) -> Y = 0 1545 ; Y = 1 1546 ). 1547zdd_subtr(X, Y, Z):- memo(zdd_subtr(X,Y)-Z), 1548 ( nonvar(Z) -> true 1549 ; cofact(X, t(A, L, R)), 1550 cofact(Y, t(A0, L0, R0)), 1551 zdd_compare(C, A, A0), 1552 ( C = (<) -> 1553 zdd_subtr(L, Y, U), 1554 cofact(Z, t(A, U, R)) 1555 ; C = (=) -> 1556 zdd_subtr(L, L0, U), 1557 zdd_subtr(R, R0, V), 1558 cofact(Z, t(A, U, V)) 1559 ; zdd_subtr(X, L0, Z) 1560 ) 1561 ).
1566% ?- zdd X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y). 1567% ?- zdd X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y). 1568% ?- zdd X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y). 1569% 1570zdd_subtr_1(X, 0):- X < 2, !. % empty family or singleton of the empty. 1571zdd_subtr_1(X, Y):- cofact(X, t(A, L, R)), 1572 zdd_subtr_1(L, L0), 1573 cofact(Y, t(A, L0, R)).
1578% ?- zdd X<<{[a]}, Z << zdd_xor(X, X). 1579% ?- zdd X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z). 1580% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms), 1581% time((zdd X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))). 1582% ?- time((zdd Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))). 1583zdd_xor(X, Y, Z):-zdd_subtr(X, Y, A), 1584 zdd_subtr(Y, X, B), 1585 zdd_join(A, B, Z). 1586 1587% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S), 1588% zdd_meet(X, Y, B, S), 1589% zdd_subtr(A, B, Z, S).
Remark. The merge is associative and commutative, but not idempotent.
1598% ?- zdd(( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 1599% ?- time(zdd(( X<<pow(!charlist(a-z)), Y<<pow(:numlist(1, 26))))). 1600% ?- time(zdd(( X<<pow(:charlist($(a-z))), Y<<pow(:numlist(1, 26)), 1601% zdd_merge(X, Y, Z), U << zdd_meet(X, Z), card(X, C)))), C is 2^26. 1602 1603zdd_merge(0, _, 0):-!. 1604zdd_merge(_, 0, 0):-!. 1605zdd_merge(1, X, X):-!. 1606zdd_merge(X, 1, X):-!. 1607zdd_merge(X, Y, Z):- 1608 ( X > Y -> memo(zdd_merge(Y, X)-Z) 1609 ; memo(zdd_merge(X, Y)-Z) 1610 ), 1611 ( nonvar(Z) -> true 1612 ; cofact(X, t(A, L, R)), 1613 zdd_merge(L, Y, L0), 1614 zdd_merge(R, Y, R0), 1615 zdd_insert(A, R0, R1), 1616 zdd_join(L0, R1, Z) 1617 ). 1618% 1619 1620zdd_merge_list([], X, X). 1621zdd_merge_list([A|As], X, Y):- 1622 ( integer(A) -> zdd_merge(A, X, X0) 1623 ; zdd_insert(A, X, X0) % atom case 1624 ), 1625 zdd_merge_list(As, X0, Y).
1633zdd_disjoint_merge(0, _, 0):-!. 1634zdd_disjoint_merge(_, 0, 0):-!. 1635zdd_disjoint_merge(1, X, X):-!. 1636zdd_disjoint_merge(X, 1, X):-!. 1637zdd_disjoint_merge(X, Y, Z):- 1638 ( X @> Y -> memo(disj_merge(Y, X)-Z) 1639 ; memo(disj_merge(X, Y)-Z) 1640 ), 1641 ( nonvar(Z) -> true 1642 ; cofact(X, t(A, L, R)), 1643 cofact(Y, t(A0, L0, R0)), 1644 zdd_compare(C, A, A0), 1645 ( C= (<) -> 1646 zdd_disjoint_merge(L, Y, U), 1647 zdd_disjoint_merge(R, Y, V), 1648 cofact(Z, t(A, U, V)) 1649 ; C = (=) -> 1650 zdd_disjoint_merge(L, L0, U), 1651 zdd_disjoint_merge(L, R0, V), 1652 zdd_disjoint_merge(R, L0, W), 1653 zdd_join(V, W, P), 1654 cofact(Z, t(A, U, P)) 1655 ; zdd_disjoint_merge(X, L0, U), 1656 zdd_disjoint_merge(X, R0, V), 1657 cofact(Z, t(A0, U, V)) 1658 ) 1659 ). 1660 1661 1662% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1663% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1664%@ false. 1665% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1666% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1667% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1668% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1673zdd_subfamily(X, X):-!. 1674zdd_subfamily(0, _):-!. 1675zdd_subfamily(_, 0):-!, fail. 1676zdd_subfamily(1, X):-!, zdd_has_1(X). 1677zdd_subfamily(X, X0):- 1678 cofact(X, t(A, L, R)), 1679 cofact(X0, t(A0, L0, R0)), 1680 zdd_compare(C, A, A0), 1681 ( C = (=) -> 1682 zdd_subfamily(L, L0), 1683 zdd_subfamily(R, R0) 1684 ; C = (>), 1685 zdd_subfamily(X, L0) 1686 ). 1687 1688 /********************************* 1689 * division/residue in ZDD * 1690 *********************************/
zdd_divmod(X, Y, D, M, S),
psa(X, S), psa(D, S), psa(M, S).
1698zdd_divmod(X, Y, D, M):-
1699 zdd_div_div(X, Y, D1, D),
1700 zdd_subtr(X, D1, M).1706% ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S), 1707% psa(X, S), psa(D, S), psa(M, S). 1708zdd_divmod0(X, Y, D, M):- 1709 zdd_divisible(X, Y, D), 1710 zdd_subtr(X, D, M).
1716% ?- zdd X<< +[b], zdd_div_div(X, 1, D, M), psa(X), psa(D), psa(M). 1717% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), psa(X), psa(Y), psa(D), psa(M). 1718% ?- zdd X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), 1719% psa(X), psa(Y), psa(D), psa(M). 1720% ?- zdd X<< +[*[a,b]], Y<< +[*[b]], psa(X), psa(Y), zdd_div_div(X, Y, D, M), 1721% psa(D), psa(M). 1722% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]], 1723% zdd_div_div(X, Y, D, D1), 1724% psa(D), psa(D1). 1725 1726zdd_div_div(0, _, 0, 0):-!. 1727zdd_div_div(1, X, Y, Y):-!, 1728 ( zdd_has_1(X) -> Y = 1 1729 ; Y = 0 1730 ). 1731zdd_div_div(_, 0, 0, 0):-!. 1732zdd_div_div(X, 1, X, X):-!. 1733zdd_div_div(X, Y, Z, U):- memo(div_div(X, Y)- P), 1734 ( nonvar(P) -> P = (Z, U) 1735 ; cofact(X, t(A, L, R)), 1736 zdd_div_div(L, Y, L0, U0), 1737 zdd_div_div(A, R, Y, R0, V0), 1738 zdd_join(L0, R0, Z), 1739 zdd_join(U0, V0, U), 1740 P = (Z, U) 1741 ). 1742% 1743zdd_div_div(_, 0, _, 0, 0):-!. 1744zdd_div_div(_, 1, 0, 0, 0):-!. % ??? 1745zdd_div_div(A, 1, 1, Z, Z):-!, zdd_singleton(A, Z). 1746zdd_div_div(_, _, 0, 0, 0):-!. 1747zdd_div_div(A, X, 1, Z, Z):-!, cofact(Z, t(A, 0, X)). 1748zdd_div_div(A, X, Y, Z, U):- cofact(Y, t(B, L, R)), 1749 zdd_compare(C, A, B), 1750 ( C = (<) -> 1751 zdd_div_div(X, Y, Z0, U0), 1752 zdd_insert(A, Z0, Z), 1753 zdd_insert(A, U0, U) 1754 ; C = (=) -> 1755 zdd_div_div(X, L, Z0, U0), 1756 zdd_insert(A, Z0, Z1), 1757 zdd_insert(A, U0, U1), 1758 zdd_div_div(X, R, Z2, U2), 1759 zdd_insert(A, Z2, Z3), % A is absorbed due to hit (A=B). 1760 zdd_join(Z1, Z3, Z), 1761 zdd_join(U1, U2, U) 1762 ; zdd_div_div(A, X, L, Z, U) 1763 ).
1769% ?- zdd(( X<< {[a]}, zdd_div(X, X, Z), psa(Z))). 1770% ?- zdd(( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1771% ?- zdd(( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))). 1772% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1773% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1774% ?- zdd(( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1775% ?- zdd(( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1776% ?- zdd(( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1777% ?- zdd(( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1778% ?- zdd(( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1779% ?- zdd(( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))). 1780% ?- zdd(( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1781% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1782% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1783% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))). 1784% ?- zdd(( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1785% ?- zdd(( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))). 1786% ?- zdd(( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1787% ?- zdd(( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1788% ?- zdd(( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))). 1789% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))). 1790% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1791% ?- zdd(( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1792 1793% 1794zdd_div(0, _, 0):-!. 1795zdd_div(1, X, Y):-!, 1796 ( zdd_has_1(X) -> Y = 1 1797 ; Y = 0 1798 ). 1799zdd_div(X, Y, Z):- memo(zdd_div(X, Y)- Z), 1800 ( nonvar(Z) -> true 1801 ; cofact(X, t(A, L, R)), 1802 zdd_div(L, Y, L0), 1803 zdd_div(A, R, Y, R0), 1804 zdd_join(L0, R0, Z) 1805 ). 1806% 1807zdd_div(_, _, 0, 0):-!. 1808zdd_div(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1809zdd_div(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1810 zdd_compare(C, A, B), 1811 ( C = (<) -> 1812 zdd_div(X, Y, Z0), 1813 cofact(Z, t(A, 0, Z0)) 1814 ; C = (=) -> 1815 zdd_div(X, L, L0), 1816 zdd_div(X, R, R0), 1817 cofact(Z, t(A, R0, L0)) 1818 ; zdd_div(A, X, L, Z) 1819 ).
1825% ?- zdd {N=10, numlist(1, N, Ns), numlist(1, 10, Js)}, X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z). 1826% ?- zdd X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1827% ?- zdd X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1828% ?- zdd X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1829% ?- zdd X<<pow([a, b, c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z). 1830 1831zdd_divisible(0, _, 0):-!. 1832zdd_divisible(1, X, Y):-!, 1833 ( zdd_has_1(X) -> Y = 1 1834 ; Y = 0 1835 ). 1836zdd_divisible(X, Y, Z):- memo(zdd_divisible(X, Y)- Z), 1837 ( nonvar(Z) -> true 1838 ; cofact(X, t(A, L, R)), 1839 zdd_divisible(L, Y, L0), 1840 zdd_divisible(A, R, Y, R0), 1841 zdd_join(L0, R0, Z) 1842 ). 1843% 1844zdd_divisible(_, _, 0, 0):-!. 1845zdd_divisible(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1846zdd_divisible(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1847 zdd_compare(C, A, B), 1848 ( C = (<) -> 1849 zdd_divisible(X, Y, Z0), 1850 cofact(Z, t(A, 0, Z0)) 1851 ; C = (=) -> 1852 zdd_divisible(X, L, L0), 1853 zdd_divisible(X, R, R0), 1854 zdd_join(L0, R0, Z0), 1855 cofact(Z, t(A, 0, Z0)) 1856 ; zdd_divisible(A, X, L, Z) 1857 ).
1862% ?- zdd X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1863% ?- zdd X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1864% ?- zdd X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S). 1865% ?- zdd X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S). 1866% ?- N = 300, zdd numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns], 1867% time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S). 1868 1869% ?- zdd X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z). 1870 1871zdd_divisible_by_all(X, Y, X):-Y<2, !. % It was hard to find this. 1872zdd_divisible_by_all(X, _, 0):-X<2, !. % It was a little bit hard to find this. 1873zdd_divisible_by_all(X, Y, Z):- memo(div_by_all(X, Y)-Z), 1874 ( nonvar(Z) -> true 1875 ; cofact(X, t(A, L, R)), 1876 zdd_divisible_by_all(L, Y, L0), 1877 zdd_divisible_by_all(A, R, Y, R0), 1878 zdd_join(L0, R0, Z) 1879 ). 1880% 1881zdd_divisible_by_all(A, X, Y, Z):- Y<2, !, 1882 cofact(Z, t(A, 0, X)). 1883zdd_divisible_by_all(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1884 zdd_compare(C, A, B), 1885 ( C = (<) -> 1886 zdd_divisible_by_all(X, Y, Z0), 1887 zdd_insert(A, Z0, Z) 1888 ; C = (=) -> 1889 zdd_divisible_by_all(X, R, R1), 1890 zdd_insert(A, R1, R0), 1891 zdd_divisible_by_all(R0, L, Z) 1892 ; Z = 0 % It was hard to find this. 1893 ).
1897zdd_mod(X, Y, Z) :- zdd_divisible(Y, X, X0),
1898 zdd_subtr(X, X0, Z).1903% ?- zdd zdd_list(X, [[a]]), zdd_list(Y, [[a,c],[a,d]]), 1904% zdd_multiple(X, Y, Z), psa(Z). 1905% ?- zdd zdd_list(X, [[a,b]]), zdd_list(Y, [[a,c],[a,d]]), 1906% zdd_multiple(X, Y, Z), psa(Z). 1907% ?- zdd zdd_list(X, [[a,b]]), Y<<pow([a,b,c]), 1908% zdd_multiple(X, Y, Z), psa(Z). 1909% ?- zdd Y<<pow([a,b,c]), zdd_multiple(0, Y, Z), psa(Z). 1910% ?- zdd Y<<pow([a,b]), zdd_multiple(1, Y, Z), psa(Z). 1911 1912zdd_multiple(0, _, 0):-!. 1913zdd_multiple(1, Y, Y):-!. 1914zdd_multiple(_, Y, 0):-Y<2, !. 1915zdd_multiple(X, Y, Z):-memo(multiple(X, Y)-Z), 1916 ( nonvar(Z) -> true 1917 ; cofact(X, t(A, L, R)), 1918 zdd_multiple(L, Y, L0), 1919 zdd_multiple(A, R, Y, R0), 1920 zdd_join(L0, R0, Z) 1921 ). 1922% 1923zdd_multiple(_, _, Y, 0):- Y<2, !. 1924zdd_multiple(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1925 zdd_multiple(A, X, L, L0), 1926 zdd_compare(C, A, B), 1927 ( C = (<) -> R0 = 0 1928 ; C = (=) -> 1929 zdd_multiple(X, R, R1), 1930 zdd_insert(A, R1, R0) 1931 ; zdd_multiple(A, X, R, R1), 1932 zdd_insert(B, R1, R0) 1933 ), 1934 zdd_join(L0, R0, Z). 1935 1936 /********************************* 1937 * division/resudue in List * 1938 *********************************/
zdd_list(Y, U, Z), zdd_mod_by_list(X, U, Z, S).1944% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a], Y), psa(Y))). 1945% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [], Y), psa(Y))). 1946% ?- zdd((X<<pow([a,b]), zdd_mod_by_list(X, [a, b], Y), psa(Y))). 1947% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [b,c], Y), psa(Y))). 1948% ?- zdd((X<<pow([a,b,c]), zdd_mod_by_list(X, [a,c], Y), psa(Y))). 1949% ?- zdd((X<<pow([a]), zdd_mod_by_list(X, [c], Y), psa(Y))). 1950% ?- N=100, numlist(1, N, Ns), numlist(1, N, Js), zdd((X<<pow(Ns), zdd_mod_by_list(X, Js, Z), card(Z, C))). 1951 1952zdd_mod_by_list(X, Y, Z):- zdd_divisible_by_list(X, Y, Z0), 1953 zdd_subtr(X, Z0, Z).
zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).1959% ?- zdd((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1960% ?- zdd((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1961 1962zdd_div_by_list(X, [], X):-!. 1963zdd_div_by_list(X, F, Y):- F=[A|As], 1964 ( X<2 -> Y = 0 1965 ; cofact(X, t(B, L, R)), 1966 zdd_div_by_list(L, F, L0), 1967 zdd_compare(C, B, A), 1968 ( C = (>) -> R0 = 0 1969 ; C = (=) -> 1970 zdd_div_by_list(R, As, R0) 1971 ; zdd_div_by_list(R, F, R1), 1972 zdd_insert(B, R1, R0) 1973 ), 1974 zdd_join(L0, R0, Y) 1975 ).
zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).1981% ?- zdd((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1982% ?- zdd((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1983 1984zdd_divisible_by_list(X, [], X):-!. 1985zdd_divisible_by_list(X, F, Y):- F=[A|As], 1986 ( X<2 -> Y = 0 1987 ; cofact(X, t(B, L, R)), 1988 zdd_divisible_by_list(L, F, L0), 1989 zdd_compare(C, B, A), 1990 ( C = (>) -> R0 = 0 1991 ; C = (=) -> zdd_divisible_by_list(R, As, R0) 1992 ; zdd_divisible_by_list(R, F, R0) 1993 ), 1994 cofact(Y, t(B, L0, R0)) 1995 1996 ). 1997 1998 1999 /********************* 2000 * meta on ZDD * 2001 *********************/ 2002% 2003% ?- zdd((X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2004% ?- zdd((X<<pow([1,2,4,5,6]), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2005% ?- N=2, numlist(1, N, L), zdd((X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2006% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2007% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S))). 2008% ?- N=10, numlist(1, N, L), zdd((X<<pow(L), 2009% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C))), C=:= 2^N. 2010% ?- N=1000, numlist(1, N, L), zdd((X<<pow(L), 2011% 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.
2020:- meta_predicate map_zdd(,,). 2021 2022map_zdd(_, X, X):- X<2, !. 2023map_zdd(F, X, Y):- memo(map(X,F)-Y), 2024 ( nonvar(Y)-> true 2025 ; cofact(X, t(A, L, R)), 2026 map_zdd(F, L, L0), 2027 map_zdd(F, R, R0), 2028 call(F, A, B), 2029 zdd_insert(B, R0, R1), 2030 zdd_join(L0, R1, Y) 2031 ). 2032 2033% ?- zdd X<< (*[a,b,c]), psa(X). 2034% ?- zdd X<< (+[a,b]), psa(X). 2035% ?- zdd((X<<pow([a,b,c]), psa(X))). 2036% ?- zdd((prz(1))). 2037% ?- zdd((prz(0))). 2038% ?- zdd((mp(hello, 1))). 2039% ?- zdd((mp(hello, 0))).
2043prz(X):- print_set_at(X).2047mp(M, X) :- mpsa(M, X). 2048 2049mpsa(M, X):- writeln(M), 2050 print_set_at(X), 2051 writeln('-------------------'). 2052 2053% ?- sat. 2054% ?- sat(a+b), sat(b+c), psa. 2055% ?- sat(A+B), sat(B+C), psa. 2056 2057psa :- b_getval(root, R), psa(R).
pow([a]), psa(X).
?- X<<{[a]}, psa(X).2064psa(X):- print_set_at(X), 2065 writeln('-------------------'). 2066% 2067psa(X, G):- print_set_at(X, G), 2068 writeln('-------------------').
Users/cantor/devel/zdd/prolog/zdd/zdd.pl2073print_set_at(0):-!, format("\szid = 0\n\t0\n"). 2074print_set_at(1):-!, format("\szid = 1\n\t[]\n"). 2075print_set_at(X):- format("\szid = ~w\n", [X]), 2076 forall(set_at(P, X), format("\t~w\n", [P])). 2077% 2078print_set_at(0, _):-!, format("\szid = 0\n\t0\n"). 2079print_set_at(1, _):-!, format("\szid = 1\n\t[]\n"). 2080print_set_at(X, G):- format("\szid = ~w\n", [X]), 2081 forall(set_at(P, X, G), format("\t~w\n", [P])). 2082 2083% ?- X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X). 2084% ?- X<<pow([1,2]), set_at(U, X), psa(X). 2085 2086% ?- zdd((X<<pow([1,2]), mp(powerset, X))). 2087set_at([], 1):-!. 2088set_at(P, X):- X>1, 2089 cofact(X, t(A, L, R)), 2090 ( set_at(P, L) 2091 ; set_at(As, R), 2092 P=[A|As] 2093 ). 2094% 2095set_at([], 1, _):-!. 2096set_at(P, X, G):- X>1, 2097 cofact(X, t(A, L, R), G), 2098 ( set_at(P, L, G) 2099 ; set_at(As, R, G), 2100 P=[A|As] 2101 ). 2102 2103% ?- zdd zdd_singleton(a, X), show_fos(X). 2104% ?- zdd X<< {[a,b], [b,c]}, show_fos(X). 2105% ?- zdd X<< pow([a,b]), show_fos(X).
2109show_fos(X):- X > 1, 2110 accessible_nodes(X, Ns), 2111 forall( member(M, Ns), 2112 ( cofact(M, T), 2113 writeln(M->T))). 2114% 2115accessible_nodes(X, Ns):- 2116 accessible_nodes(X, Ns0, []), 2117 sort(Ns0, Ns1), 2118 reverse(Ns1, Ns). 2119% 2120accessible_nodes(X, A, A):- X<2, !. 2121accessible_nodes(X, [X|A], B):- 2122 cofact(X, t(_, L, R)), 2123 accessible_nodes(L, A, A0), 2124 accessible_nodes(R, A0, B).
2130% ?- zdd((X<<pow([a,b,c]), zdd_list(X, Y), zdd_list(X0, Y))). 2131% ?- powerset([a,b,c], Y), zdd((zdd_list(X, Y), zdd_list(X, Y0), zdd_list(X0, Y0))), 2132% maplist(sort, Y, Y1), sort(Y1, Y2). 2133% 2134zdd_list(X, Y):- nonvar(X), !, zdd_sets(X, Y). 2135zdd_list(X, Y):- zdd_family(Y, X). 2136 2137% ?- zdd((X<<pow([a,b,c]), sets(X, P))). 2138% ?- zdd((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))). 2139% ?- zdd((X<<pow([]), sets(X, P))). 2140% ?- zdd((X<<pow([a]), sets(X, P))). 2141% ?- zdd((X<<pow(:numlist(1,3)), sets(X, Y))). 2142% ?- zdd((X<<pow([a,b,c]), sets(X, Y))). 2143% ?- zdd((X<<pow(:charlist($a, $c)), sets(X, Y))). 2144% ?- zdd((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))), sets(X, Y))).
2149sets(X, Y):- zdd_sets(X, Y0), zdd_sort(Y0, Y). 2150% 2151zdd_sets(1, [[]]):-!. 2152zdd_sets(0, []):-!. 2153zdd_sets(X, P):- 2154 cofact(X, t(A,L,R)), 2155 zdd_sets(L, Y), 2156 zdd_sets(R, Z), 2157 maplist(cons(A), Z, AZ), 2158 append(AZ, Y, P). 2159 2160% ?- zdd zdd_eval(pow([a, b, c, d, e, f]), I), eqns(I, X), 2161% maplist(writeln, X). 2162% 2163eqns(X, Y):- zdd_eqns(X, Y). 2164 2165basic_zdd(0). 2166basic_zdd(1). 2167 2168% % ?- zdd X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es). 2169% % ?- zdd X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es). 2170 2171% zdd_eqns(I, Es):- nonvar(I), var(Es), !, zdd_to_eqns(I, Es, []). 2172% zdd_eqns(I, Es):- var(I), nonvar(Es), !, 2173% ( check_eqns_for_zdd(Es) -> 2174% Es = [X=_|_], 2175% eqns_to_zdd(Es, X, I) 2176% ; throw('Violating-underlying-ordering-on-atoms.'(Es)) 2177% ). 2178% % 2179% zdd_to_eqns(I, X, Y):- zdd_to_eqns(I, X, [], S), 2180% zdd_sort(X, X1, S), 2181% reverse(X1, X). 2182% % 2183% zdd_to_eqns(I, X, X):- I<2, !. 2184% zdd_to_eqns(I, X, Y):- memo(visited(I)-F), 2185% ( nonvar(F) -> Y = X 2186% ; F = true, 2187% cofact(I, t(A, L, R)), 2188% X = [I=t(A, L, R)|X0], 2189% zdd_to_eqns(L, X0, X1), 2190% zdd_to_eqns(R, X1, Y) 2191% ). 2192% % 2193% check_eqns_for_zdd(Es):- are_eqns_closed(Es, Es), 2194% sort(Es, Fs), 2195% has_unique_left(Fs), 2196% sort(2, @=<, Es, Gs), 2197% has_unique_right(Gs). 2198% % 2199% are_eqns_closed([], _). 2200% are_eqns_closed([_ = t(A, L, R)|Rest], Es):- 2201% ( basic_zdd(L) -> true 2202% ; memberchk(L = t(B, _, _), Es), 2203% zdd_compare(<, A, B) 2204% ), 2205% ( basic_zdd(R) -> true 2206% ; memberchk(L = t(C, _, _), Es), 2207% zdd_compare(<, A, C) 2208% ), 2209% are_eqns_closed(Rest, Es). 2210% % 2211% eqns_to_zdd(_, 0, 0):-!. 2212% eqns_to_zdd(_, 1, 1):-!. 2213% eqns_to_zdd(Es, X, I):- memo(solve(X)-I), 2214% ( nonvar(I) -> true 2215% ; memberchk(X = t(A, L, R)), 2216% eqns_to_zdd(Es, L, L0), 2217% eqns_to_zdd(Es, R, R0), 2218% cofact(I, t(A, L0, R0)) 2219% ).
is_function([a-1,b-2,c-3]).
?- is_function([a-1,b-2,a-3]).2225is_function(X):- sort(X, Y), has_unique_left(Y). 2226% 2227has_unique_left([X,Y|Z]):-!, 2228 ( arg(1, X, A), arg(1, Y, A) -> false 2229 ; has_unique_left([Y|Z]) 2230 ). 2231has_unique_left(_).
2236% ?- check_one_to_one([a-1,b-2,c-3]). 2237% ?- check_one_to_one([a-1,b-2,c-1]). % false 2238 2239check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y). 2240% 2241has_unique_right([X,Y|Z]):-!, 2242 ( arg(2, X, A), arg(2, Y, A) -> false 2243 ; has_unique_right([Y|Z]) 2244 ). 2245has_unique_right(_).
ppoly(+X) is det.
Print X in polynomical form.2249ppoly(X):- poly_term(X, Poly), 2250 writeln(Poly). 2251 2252% ?- zdd((X<<pow([a,b]), poly_term(X, P))). 2253% ?- zdd((X<<pow([a,b,c]), poly_term(X, P))). 2254% ?- zdd((X<<(@a + @b), psa(X))). 2255 2256poly_term(X, Poly):- zdd_sets(X, Sets), 2257 get_compare(Pred), 2258 maplist(predsort(Pred), Sets, Sets0), 2259 predsort(Pred, Sets0, Sets1), 2260 poly_term0(Sets1, Poly). 2261 2262% ?- poly_term0([], Y). 2263% ?- poly_term0([[]], Y). 2264% ?- poly_term0([[a], [b]], Y). 2265% ?- poly_term0([[a*b], [c]], Y). 2266 2267poly_term0(X, Y):- maplist(mul_term, X, X0), 2268 sum_term(X0, Y). 2269% 2270mul_term([], 1):-!. 2271mul_term([X], X):-!. 2272mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 2273% 2274sum_term([], 0):-!. 2275sum_term([X], X):-!. 2276sum_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))).
2285zdd_rand_path(I):- zdd_rand_path(I, P, []), writeln(P). 2286% 2287zdd_rand_path(I, P):- zdd_rand_path(I, P, []). 2288% 2289zdd_rand_path(1, X, X):-!. 2290zdd_rand_path(I, X, Y):- I>1, 2291 cofact(I, t(A, L, R)), 2292 ( L == 0 -> 2293 X = [A|X0], 2294 zdd_rand_path(R, X0, Y) 2295 ; random(2) =:= 0 -> 2296 X = [A|X0], 2297 zdd_rand_path(R, X0, Y) 2298 ; zdd_rand_path(L, X, Y) 2299 ).
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).2308zdd_atoms(X, []):- X<2, !. 2309zdd_atoms(X, P):- memo(atoms(X)-P), 2310 ( nonvar(P) -> true 2311 ; cofact(X, t(A, L, R)), 2312 zdd_atoms(L, Al), 2313 zdd_atoms(R, Ar), 2314 ord_union(Al, Ar, P0), 2315 P=[A|P0] 2316 ). 2317 2318% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 2319:- meta_predicate delete(, , ). 2320delete(X, Y, Z):- delete(X, Y, Z, []). 2321 2322:- meta_predicate delete(, , , ). 2323delete(_, [], L, L). 2324delete(Pred, [X|Xs], L, L0):- 2325 ( call(Pred, X) 2326 -> delete(Pred, Xs, L, L0) 2327 ; L = [X|L1], 2328 delete(Pred, Xs, L1, L0) 2329 ). 2330 2331% ?- zdd((zdd_power([a,b], R), sets(R, U))). 2332% ?- zdd((X<< zdd_power(:charlist($(a-c))), sets(X, U))). 2333% ?- zdd((R<< pow(: !charlist(a-d)), card(R, C))). 2334%% 2335zdd_power(X, Y):- zdd_sort(X, X0), 2336 zdd_ord_power(X0, 1, Y).
zdd_ord_power([a,b], 1, X), psa(X).2341zdd_ord_power([], P, P). 2342zdd_ord_power([X|Xs], P, Q):- zdd_ord_power(Xs, P, R), 2343 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.2351% ?- atomlist(ax(1+1, 3+1), As). 2352% ?- atomlist(ax(1, 3), As). 2353atomlist(X, As):- X=..[A, I, J], 2354 I0 is I, 2355 J0 is J, 2356 findall(Y, ( between(I0, J0, K), 2357 atom_concat(A, K, Y) 2358 ), 2359 As).
2365% ?- charlist(a-c, X). 2366charlist(A-B, I):- 2367 findall(X, ( char_type(X, alnum), 2368 X @>= A, 2369 X @=< B 2370 ), 2371 I).
charlist(A-B, X).
?- charlist(a, c, X).
@ X = [a, b, c].2377charlist(A, B, I):- charlist(A-B, I). 2378 2379% ?- term_atoms(a+b=c, L). 2380% ?- term_atoms(a+b, L). 2381% ?- term_atoms(f(a+a), L).
2387term_atoms(X, L):- term_atoms(X, L0, []), 2388 sort(L0, L). 2389 2390% 2391term_atoms(X, L, L):- var(X), !. 2392term_atoms(X, [X|L], L):- atom(X), !. 2393term_atoms([X|Y], L, L0):-!, 2394 term_atoms(X, L, L1), 2395 term_atoms(Y, L1, L0). 2396term_atoms(X, L, L0):- compound(X), !, 2397 X =..[_|As], 2398 term_atoms(As, L, L0). 2399term_atoms(_, L, L). 2400 2401% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 2402% ?- subst_opp(a, X, [b-a]). 2403% ?- subst_opp([a], X, [b-a]). 2404 2405subst_opp(X, Y, L):- memberchk(Y-X, L). 2406subst_opp([X|Y], [X0|Y0], L):-!, 2407 subst_opp(X, X0, L), 2408 subst_opp(Y, Y0, L). 2409subst_opp(X, Y, L):- compound(X), !, 2410 X =..[F|As], 2411 subst_opp(As, Bs, L), 2412 Y =..[F|Bs]. 2413subst_opp(X, X, _). 2414 2415% ?- subst_term(f(a), R, [a-b]). 2416% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 2417% ?- subst_term(f(a), R, [a-X]). 2418% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2419% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2420% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
2426subst_term(X, Y):- member(X0-Y), X0==X, !. 2427subst_term(A, B):- compound(A), !, 2428 ( A = [X|Y] -> 2429 B = [X0|Y0], 2430 subst_term(X, X0), 2431 subst_term(Y, Y0) 2432 ; functor(A, F, N), 2433 functor(B, F, N), 2434 subst_term(N, A, B) 2435 ). 2436subst_term(X, X). 2437% 2438subst_term(0, _, _):-!. 2439subst_term(I, X, Y):- 2440 arg(I, X, A), 2441 arg(I, Y, B), 2442 subst_term(A, B), 2443 J is I - 1, 2444 subst_term(J, X, Y). 2445 2446% ?- all_instances([a,b], [0,1], a+b=b, R). 2447% ?- all_instances([x,y], [0,1], x+y=x, R). 2448%! all_instances(+As, +Vs, +X, -Y) is det. 2449% Unify Y with the list of possible variations P of X, 2450% where P is a variation of X if for each A in As with some 2451% V in Vs which depends on A, P is obtained from X by replacing 2452% all occurrences of A appearing in X with V for A in As. 2453 2454all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 2455 apply_maps(Fs, X, Y, []). 2456% 2457apply_maps([], _, Y, Y). 2458apply_maps([F|Fs], X, [X0|Y], Z):- 2459 subst_term(X, X0, F), 2460 apply_maps(Fs, X, Y, Z). 2461 2462% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 2463% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 2464% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 2465% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 2466%! mod_table(+M, +X, +E, -T) is det. 2467% Unify T with a set of form E' = V where 2468% E' is a possible ground instance of an integer expression E 2469% and V is the value of E' with modulo M, where X is a set of 2470% parameters appearing in E. 2471 2472mod_table(M, Xs, Exp, Table):- M0 is M-1, 2473 numlist(0, M0, V), 2474 all_instances(Xs, V, Exp, Exps), 2475 !, 2476 maplist(mod_arith(M), Exps, Table). 2477% 2478mod_arith(M, Exp, Exp=V):- V is Exp mod M. 2479 2480% 2481unify_all([]). 2482unify_all([_]). 2483unify_all([X,Y|Z]):- zdd:(X=Y), unify_all([Y|Z]). 2484 2485% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 2486% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 2487% ?- zdd((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 2488% ?- zdd((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 2489% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 2490% ?- zdd((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
2495% ?- zdd((X <<{[a,b], [a,c]}, zdd_appear(e, X))). % false 2496% ?- zdd((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X))). % false 2497% ?- zdd((X <<(*[a,b]+ *[a,c]), psa(X), zdd_appear(c, X))). 2498% ?- numlist(1, 10000, Ns), zdd((X<<pow(Ns), zdd_appear(10000, X))). 2499% ?- zdd X<<pow(:numlist(1, 10000)), zdd_appear(10000, X). 2500%@ X = 10001. 2501 2502zdd_appear(A, X):- use_memo(zdd_atom_appear(A, X)). 2503 2504zdd_atom_appear(A, X):- X > 1, 2505 memo(visited(X)-B), 2506 var(B), 2507 cofact(X, t(U,L,R)), 2508 zdd_compare(C, A, U), 2509 ( C = (=) -> true 2510 ; C = (>), 2511 ( zdd_atom_appear(A, L) -> true 2512 ; L < 2 -> 2513 zdd_atom_appear(A, R) 2514 ; memo(visited(L)-true), % for earlier fail. 2515 zdd_atom_appear(A, R) 2516 ) 2517 ).
2522zdd_singleton(X, P):- cofact(P, t(X, 0, 1)).2527zdd_has_1(1):-!. 2528zdd_has_1(X):- X>1, 2529 cofact(X, t(_, L, _)), 2530 zdd_has_1(L).
zdd((U<<{[a]}, P<<pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q))).2541zdd_subst(_, _, X, X, _):- X<2, !. 2542zdd_subst(X, U, P, Q):- memo(zdd_subst(X, U, P)-Q), 2543 ( nonvar(Q) -> true 2544 ; cofact(P, t(Y, L, R)), 2545 zdd_subst(X, U, L, L0), 2546 zdd_compare(C, X, Y), 2547 ( C = (=) -> zdd_merge(U, R, R0) 2548 ; C = (<) -> bdd_cons(R0, Y, R) 2549 ; zdd_subst(X, U, R, R1), 2550 zdd_insert(Y, R1, R0) 2551 ), 2552 zdd_join(L0, R0, Q) 2553 ). 2554 2555 /*********************** 2556 * product on zdd * 2557 ***********************/ 2558 2559% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))). 2560% ?- zdd((X<<(a*b), Y<<(c*d), Z<<(X**Y))). 2561% ?- zdd((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))). 2562% ?- zdd((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))). 2563% ?- time(zdd((X<<pow(:numlist(1,16)), Z<<(X**X), card(Z, C)))). 2564% ?- N is 10000, time( ( zdd X<<pow(:numlist(1,N)), card(X, _C))), _C =:= 2^N. 2565% ?- call_with_time_limit(120, (numlist(1, 16, R), 2566% time(zdd((X<<pow(R), Z<<(X**X), card(Z, C)))))). 2567 2568% 2569zdd_product(X, Y, 0):- (X<2; Y<2), !. 2570zdd_product(X, Y, Z):- memo(prod(X, Y)-Z), 2571 ( nonvar(Z) -> true % , write(.) % hits found. 2572 ; zdd_product(X, Y, [], Bs, 0, Z0), 2573 append_pairs_list(X, Bs, Z1), 2574 zdd_join(Z0, Z1, Z) 2575 ). 2576% 2577zdd_product(_, X, Bs, Bs, Z, Z):- X<2, !. 2578zdd_product(X, Y, Bs, Q, U, V):- cofact(Y, t(B, L, R)), 2579 zdd_product(X, L, L0), 2580 zdd_join(L0, U, U0), 2581 zdd_product(X, R, [B|Bs], Q, U0, V). 2582% 2583append_pairs_list(X, _, X):- X<2, !. 2584append_pairs_list(X, Bs, U):- cofact(X, t(A, L, R)), 2585 append_pairs_list(R, Bs, R0), 2586 append_pairs_list(L, Bs, L0), 2587 insert_pairs(A, Bs, R0, R1), 2588 zdd_join(L0, R1, U). 2589 2590% 2591insert_pairs(_, [], U, U):-!. 2592insert_pairs(A, [B|Bs], U, V):- 2593 zdd_insert((A-B), U, U0), 2594 insert_pairs(A, Bs, U0, V). 2595 2596 /************************* 2597 * Quotient on ZDD * 2598 *************************/
?- 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))).
2607zdd_insert(_, 0, 0):-!. 2608zdd_insert(A, 1, J):-!, zdd_singleton(A, J). 2609zdd_insert(A, I, J):- memo(insert(A, I)-J), 2610 ( nonvar(J) -> true 2611 ; cofact(I, t(X, L, R)), 2612 zdd_compare(C, A, X), 2613 ( C = (=) -> 2614 zdd_join(L, R, K), 2615 cofact(J, t(X, 0, K)) 2616 ; C = (<) -> 2617 cofact(J, t(A, 0, I)) 2618 ; zdd_insert(A, L, L0), 2619 zdd_insert(A, R, R0), 2620 cofact(J, t(X, L0, R0)) 2621 ) 2622 ). 2623 2624% ?- zdd X<<pow([a,b]), Y<<pow([c,d]), 2625% psa(X, S), psa(Y, S), 2626% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S). 2627 2628% ?- zdd X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S), 2629% psa(Y, S). 2630% ?- listing(zdd_insert). 2631 2632:- meta_predicate zdd_insert(, , , ). 2633zdd_insert(_, _, 0, 0):-!. 2634zdd_insert(_, A, 1, Y):-!, zdd_singleton(A, Y). 2635zdd_insert(F, A, X, Y):- memo(zdd_insert(X, A, F)-Y), 2636 ( nonvar(Y) -> true % , write(.) % many hits 2637 ; cofact(X, t(B, L, R)), 2638 zdd_insert(F, A, L, L0), 2639 call(F, C, A, B), 2640 ( C = (=) -> bdd_cons(R0, A, R) 2641 ; C = (<) -> bdd_append([A, B], R, R0) 2642 ; zdd_insert(F, A, R, R1), 2643 bdd_cons(R0, B, R1) 2644 ), 2645 zdd_join(L0, R0, Y) 2646 ). 2647 2648% ?- zdd((family([[a, b],[b]], X), sets(X, Sx), 2649% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
2654% ?- numlist(1, 10000, Ns), zdd((zdd_insert_atoms(Ns, 1, X), psa(X))). 2655 2656% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))). 2657% ?- zdd((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))). 2658zdd_insert_atoms(X, Y, Z):- zdd_sort(X, X0), 2659 zdd_ord_insert(X0, Y, Z). 2660 2661% 2662zdd_ord_insert(_, 0, 0):-!. 2663zdd_ord_insert([], X, X):-!. 2664zdd_ord_insert(As, 1, Y):-!, bdd_append(As, 1, Y). 2665zdd_ord_insert(As, X, Y):- memo(ord_insert(X, As)-Y), 2666 ( nonvar(Y) -> true % , write(.) % many hits. 2667 ; As = [A|U], 2668 cofact(X, t(B, L, R)), 2669 zdd_compare(C, A, B), 2670 ( C = (<) -> 2671 zdd_ord_insert(U, X, Y0), 2672 cofact(Y, t(A, 0, Y0)) 2673 ; C = (=) -> 2674 zdd_ord_insert(U, L, L1), 2675 zdd_ord_insert(U, R, R1), 2676 zdd_join(R1, L1, Y0), 2677 cofact(Y, t(A, 0, Y0)) 2678 ; zdd_ord_insert(As, L, L1), 2679 zdd_ord_insert(As, R, R1), 2680 cofact(Y, t(B, L1, R1)) 2681 ) 2682 ). 2683 2684 2685% ?- X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y), psa(Y). 2686:- meta_predicate zdd_reorder(, , ). 2687zdd_reorder(_, X, X):- X<2, !. 2688zdd_reorder(F, X, Y):- cofact(X, t(A, L, R)), 2689 zdd_reorder(F, L, L0), 2690 zdd_reorder(F, R, R1), 2691 zdd_insert(F, A, R1, R0), 2692 zdd_join(L0, R0, Y). 2693 2694 2695 /***************** 2696 * filters * 2697 *****************/ 2698 2699% ?- zdd X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y), psa(Y). 2700% ?- zdd X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y), psa(Y). 2701% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y), psa(Y). 2702% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([1, 3], X, Y), psa(Y). 2703% ?- zdd { numlist(1, 3, Ns) }, X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y), psa(Y). 2704% ?- zdd { numlist(1, 1000, Ns) }, X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y), card(Y, C), 2705% card(X, D), zdd_compare(E, C, D), {U is D-C}. 2706 2707% 2708ltr_meet_filter([], X, X):-!. 2709ltr_meet_filter([A|F], X, Y):- 2710 ltr_filter(A, X, X0), 2711 ltr_meet_filter(F, X0, Y). 2712 2713% ?- X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y), psa(Y). 2714% ?- X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y), psa(Y). 2715ltr_join_filter(F, X, Y):- 2716 ltr_join_filter(F, X, 0, Y). 2717% 2718ltr_join_filter([], _, Y, Y):-!. 2719ltr_join_filter([P|F], X, Y, Y0):-!, 2720 ltr_filter(P, X, Y1), 2721 zdd_join(Y, Y1, Y2), 2722 ltr_join_filter(F, X, Y2, Y0). 2723 2724% 2725ltr_filter(-A, X, Y):-!, ltr_filter_negative(A, X, Y). 2726ltr_filter(A, X, Y):- ltr_filter_positive(A, X, Y). 2727 2728% 2729ltr_filter_negative(_, X, X):- X<2, !. 2730ltr_filter_negative(A, X, Y):- memo(letral_neg(X, A)-Y), 2731 ( nonvar(Y) -> true 2732 ; cofact(X, t(B, L, R)), 2733 ltr_filter_negative(A, L, L0), 2734 zdd_compare(C, A, B), 2735 ( C = (=) -> R0 = 0 2736 ; C = (<) -> R0 = R 2737 ; ltr_filter_negative(A, R, R0) 2738 ), 2739 cofact(Y, t(B, L0, R0)) 2740 ). 2741% 2742ltr_filter_positive(_, X, 0):- X<2, !. 2743ltr_filter_positive(A, X, Y):- memo(ltr_pos(X, A)-Y), 2744 ( nonvar(Y) -> true 2745 ; cofact(X, t(B, L, R)), 2746 ltr_filter_positive(A, L, L0), 2747 zdd_compare(C, A, B), 2748 ( C = (=) -> R0 = R 2749 ; C = (<) -> R0 = 0 2750 ; ltr_filter_positive(A, R, R0) 2751 ), 2752 cofact(Y, t(B, L0, R0)) 2753 ). 2754 2755% ?- zdd((X<<pow([a,b,c]), dnf_filter([[-b,-c]], X, Y), psa(Y))). 2756% ?- zdd((X<<pow([a,b]), dnf_filter([[b]], X, Y), psa(Y))). 2757% ?- zdd((X<<pow([a,b]), dnf_filter([[a,b]], X, Y), psa(Y))). 2758% ?- zdd((X<<pow([a,b]), dnf_filter([], X, Y), psa(Y))). 2759% ?- zdd((X<<pow([a,b,c]), dnf_filter([[c]], X, Y), psa(Y))). 2760% ?- zdd((X<<pow([a,b,c]), dnf_filter([], X, Y), psa(Y))). 2761% ?- zdd((X<<pow([a,b,c]), dnf_filter([[a],[-c]], X, Y), psa(Y))). 2762 2763dnf_filter(DNF, X, Y):- dnf_filter(DNF, X, 0, Y). 2764% 2765dnf_filter([], _, Y, Y, _). 2766dnf_filter([F|Fs], X, Y, Z):- 2767 ltr_meet_filter(F, X, X0), 2768 zdd_join(X0, Y, Y0), 2769 dnf_filter(Fs, X, Y0, Z). 2770 2771% ?- zdd((X<<pow([a,b,c]), cnf_filter([[-b,-c]], X, Y), psa(Y))). 2772% ?- zdd((X<<pow([a,b,c]), cnf_filter([[-a, -b, -c]], X, Y), psa(Y))). 2773cnf_filter([], X, X). 2774cnf_filter([F|Fs], X, Y):- 2775 ltr_join_filter(F, X, X0), 2776 cnf_filter(Fs, X0, Y). 2777 2778% 2779zdd_meet_list([A], A):-!. 2780zdd_meet_list([A|As], B):- zdd_meet_list(As, A, B). 2781% 2782zdd_meet_list([], X, X). 2783zdd_meet_list([A|As], X, Y):- zdd_meet(A, X, X0), 2784 zdd_meet_list(As, X0, Y). 2785% 2786zdd_join_list([], 0):-!. 2787zdd_join_list([X|Xs], Y):- zdd_join_list(Xs, X, Y). 2788% 2789zdd_join_list([], X, X):-!. 2790zdd_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2791 zdd_join_list(As, X0, Y). 2792 2793% 2794ltr_join_list([], 0):-!. 2795ltr_join_list([X|Xs], Y):-ltr_join_list(Xs, X, Y). 2796% 2797ltr_join_list([], X, X):-!. 2798ltr_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2799 ltr_join_list(As, X0, Y). 2800 2801 2802 /********************* 2803 * remove atom * 2804 *********************/
2810% ?- zdd((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2811% sets(Y, Sy))). 2812zdd_remove(X, Y, Z, S):- setup_call_cleanup( 2813 open_state(M, [hash_size(256)]), 2814 zdd_remove(X, Y, Z, S, M), 2815 close_state(M)). 2816 2817zdd_remove(_, X, X, _, _):- X<2, !. 2818zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2819 ( nonvar(J) -> true 2820 ; cofact(I, t(Ai, Li, Ri), S), 2821 zdd_compare(C, A, Ai, S), 2822 ( C = (<) -> J = I 2823 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2824 zdd_remove(A, Ri, Ria, S, M), 2825 cofact(J, t(Ai, Lia, Ria), S) 2826 ; zdd_join(Li, Ri, J, S) 2827 ) 2828 ). 2829 2830% ?- ltr_zdd X<< dnf(a->b), psa(X), 2831% use_table(pred_remove_atoms(negative_literal, X, Y)), psa(Y). 2832 2833% ?- ltr_zdd X<< dnf(a->b->c), psa(X), 2834 2835negative_literal(-(_)). 2836 2837:- meta_predicate pred_remove_atoms(, , ). 2838 2839pred_remove_atoms(_, X, X):- X<2, !. 2840pred_remove_atoms(Pred, I, J):- 2841 cofact(I, t(A, L, R)), 2842 pred_remove_atoms(Pred, L, L0), 2843 pred_remove_atoms(Pred, R, R0), 2844 ( call(Pred, A) -> 2845 zdd_join(L0, R0, J) 2846 ; cofact(J, t(A, L0, R0)) 2847 ). 2848 2849 /********************* 2850 * Cardinality * 2851 *********************/
2856% ?-N = 10000, numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:=2^N. 2857%@ % 1,222,118 inferences, 0.127 CPU in 0.161 seconds (79% CPU, 9587871 Lips) 2858%@ N = 10000, 2859%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2860%@ X = 10001. 2861 2862%@ % 1,204,213 inferences, 0.179 CPU in 0.220 seconds (82% CPU, 6710726 Lips) 2863%@ N = 10000, 2864%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2865%@ X = 10001. 2866 2867% ?- zdd X<<{[a], [b]}, card(X, C). 2868% ?- N = 10000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), card(X, C))). 2869%@ % 1,222,117 inferences, 0.112 CPU in 0.127 seconds (89% CPU, 10886196 Lips) 2870%@ N = 10000, 2871%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2872%@ X = 10001, 2873 2874% ?- X<<card(pow([a,b]) + pow([c,d])). 2875%@ X = 7. 2876% ?- X<<card((+[a]) + (+[b])). 2877% ?- zdd. 2878% ?- X<<pow(numlist(1, 100)), card(X, D). 2879% ?- X<<pow(numlist(1, 100)), card(X, D), 2880% slim_gc(X, X1), slim_gc(X1, X2), slim_gc(X2, Y), 2881% card(Y, C). 2882%@ X = X1, X1 = X2, X2 = Y, Y = 101, 2883%@ D = C, C = 1267650600228229401496703205376. 2884 2885card(I, C):- open_memo(M), 2886 cardinality(I,C,M), 2887 close_memo(M). 2888% 2889cardinality(I, I, _):- I < 2, !. 2890cardinality(I, C, M):- memo(card(I)-C, M), 2891 ( nonvar(C) -> true 2892 ; cofact(I, t(_, L, R)), 2893 cardinality(R, Cr, M), 2894 cardinality(L, Cl, M), 2895 C is Cl + Cr 2896 ).
2900max_length(X, Max):- use_memo(max_length_with_memo(X, Max)). 2901 2902% 2903max_length_with_memo(X, 0):- X<2, !. 2904max_length_with_memo(X, Max):- 2905 memo(max(X)-Max), 2906 cofact(X, t(_, L, R)), 2907 ( nonvar(Max) -> true 2908 ; max_length_with_memo(L, ML), 2909 max_length_with_memo(R, MR), 2910 Max is max(1 + MR, ML) 2911 ). 2912 2913 /*********************** 2914 * Handy helpers * 2915 ***********************/ 2916 2917% 2918unify_zip([]). 2919unify_zip([X-X|R]):- unify_zip(R). 2920 2921 2922 /****************************************** 2923 * Oprations on clauses of literals * 2924 ******************************************/ 2925 2926% ?- ltr_compare(C, a, -a). 2927% ?- ltr_compare(C, -(a), a). 2928% ?- ltr_compare(C, -(b), a). 2929% ?- ltr_compare(C, -(a), b). 2930% ?- ltr_compare(C, -(a), -(b)). 2931% ?- ltr_compare(C, -(a), -(a)).
2938ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 2939ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 2940 ( C0 == (=) -> C =(<) 2941 ; C0 = C 2942 ). 2943ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 2944 ( C0 == (=) -> C = (>) 2945 ; C0 = C 2946 ). 2947ltr_compare(C, X, Y):- compare(C, X, Y). 2948 2949% ?- zdd {ltr_compare(C, a, b)}. 2950% ?- zdd {ltr_compare(C, -a, a)}. 2951% ?- zdd {ltr_compare(C, a, -a)}. 2952% ?- zdd {ltr_compare(C, -a, b)}. 2953% ltr_compare(C, X, Y, S):- get_compare(F, S), 2954% call(F, C, X, Y).
2959% ?- ltr_sort([b, b, a], X).
2960% ?- ltr_sort([-b, b,-b, -a], X).
2965ltr_sort(X, Y):- get_compare(F), predsort(F, X, Y). 2966 2967 2968% ?- zdd((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false 2969% ?- zdd((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))). 2970% 2971ltr_memberchk(L, Z):- ltr_sort(L, L0), 2972 ltr_ord_memberchk(L0, Z). 2973% 2974ltr_ord_memberchk([], Z):- !, zdd_has_1(Z). 2975ltr_ord_memberchk([A|As], Z):- Z > 1, 2976 cofact(Z, t(B, L, R)), 2977 ltr_compare(C, A, B), 2978 ( C = (=) -> ltr_ord_memberchk(As, R) 2979 ; ltr_ord_memberchk([A|As], L) 2980 ). 2981 2982% ?- call_with_time_limit(100, time(zdd((big_normal_form(30, X), resolve(X))))). 2983% ?- big_normal_form(1, X), ltr_card(X, C). 2984% ?- big_normal_form(2, X), ltr_card(X, C). 2985% ?- big_normal_form(3, X), ltr_card(X, C). 2986% ?- big_normal_form(10, X), ltr_card(X, C). 2987% ?- big_normal_form(20, X), ltr_card(X, C). 2988% ?- time(((big_normal_form(100, X), ltr_card(X, C)))). 2989% ?- time(((big_normal_form(10, X), ltr_card(X, C)))). 2990% ?- N=100, time((big_normal_form(N, X), ltr_card(X, C))), C=:=2^N. 2991 2992big_normal_form(0, 1). 2993big_normal_form(N, X):- N>0, 2994 N0 is N-1, 2995 big_normal_form(N0, X0), 2996 ltr_insert(N, X0, R), 2997 ltr_insert(-N, X0, L), 2998 zdd_join(L, R, X). 2999 3000% ?- numlist(1, 3, Ns), ( ltr_zdd X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 3001% ?- numlist(1, 20, Ns), (ltr_zdd X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 3002% ?- ltr_zdd X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y). 3003% ?- ltr_zdd X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 3004% ltr_choices(Z, U), psa(X), psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V). 3005% ?- ltr_zdd X<< {[a,b]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 3006% ?- ltr_zdd X<< {[a,b,c]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 3007% ?- ltr_zdd X<< {[a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 3008% ?- ltr_zdd X<< {[], [a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 3009% ?- ltr_zdd X<< {[a], [c, d]}, ltr_choices(X, Y), psa(Y). 3010% ?- ltr_zdd X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y). 3011% ?- ltr_zdd X<< {[a,b]}, ltr_choices(X, Y), psa(Y). 3012% ?- ltr_zdd X<< {[]}, ltr_choices(X, Y), psa(Y). 3013% ?- ltr_zdd cnf(a, X), ltr_choices(X, Y), psa(Y). 3014% ?- ltr_zdd cnf(a*b, X), ltr_choices(X, Y), psa(Y). 3015% ?- ltr_zdd cnf(a* (-a), X), ltr_choices(X, Y), psa(Y). 3016 3017% ?- N=10, numlist(2, 10, Ns), (ltr_zdd sample_cnf(Ns, X), ltr_card(X, C)). 3018% ?- N=100, numlist(2, N, Ns), (ltr_zdd sample_cnf(Ns, X), card(X, C), resolve(X)). 3019 3020sample_cnf([], 1). 3021sample_cnf([J|Js], X):- sample_cnf(Js, Y), 3022 ltr_insert(J, Y, Z), 3023 ltr_insert(-J, Y, U), 3024 ltr_join(Z, U, X).
3030accessible_indices(I, A):- zdd_vector(Vec), 3031 accessible_indices(I, A0, [], Vec), 3032 sort(A0, A). 3033 3034accessible_indices(I, A, A, _):- I<2, !. 3035accessible_indices(I, [I|A], B, Vec):- arg(I, Vec, X), 3036 ( atomic(X) -> B = A 3037 ; child_term_indices(X, A, B, Vec) 3038 ). 3039% 3040% child_term_indices(t(_, _, _), A, A, _):-!. 3041child_term_indices(X, A, B, Vec):- X =.. [_|Xs], 3042 child_term_indices_list(Xs, A, B, Vec). 3043% 3044child_term_indices_list([], A, A, _). 3045child_term_indices_list([I|Is], A, B, Vec):- 3046 accessible_indices(I, A, C, Vec), 3047 child_term_indices_list(Is, C, B, Vec). 3048 3049% test sat. PASSED. [2023/11/09] 3050% ?- sat. 3051% ?- sat(-true). % false 3052% ?- sat(a+b), sat_count(C). 3053% ?- sat(a), sat(b). 3054% ?- sat(-(a + -a)). % false 3055% ?- sat(a), sat(b), sat_count(C). 3056% ?- sat(or(a, b)), sat_count(C). 3057% ?- sat(b), sat_count(C). 3058% ?- sat(xor(a, b)), sat_count(C). 3059% ?- sat(exor(a, b)), sat_count(C). 3060% ?- sat(e_x_o_r(a, b)), sat_count(C). 3061% ?- sat(a), sat(-a). % false. 3062% ?- sat(a), sat(a+b), sat_count(C). 3063% ?- sat(a(1)+a(2)), sat_count(C). 3064% ?- sat(A+a(2)), sat_count(C). 3065% ?- sat(A + B), sat_count(C). 3066% ?- sat(a+b+c+d), sat_count(C). 3067% ?- sat(a+b), sat(c+d), sat_count(C). 3068% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 3069% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 3070% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false. 3071% ?- sat(*[p(1),p(2)]), sat_count(C). 3072% ?- sat(+[p(1),p(2)]), sat_count(C). 3073% ?- N=10, findall(p(I, J), 3074% (between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C). 3075% ?- N=10, findall(p(I, J), 3076% (between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C). 3077% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false 3078% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 3079% ?- sat(A + B), sat_count(C). 3080% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 3081% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 3082% ?- sat(a=<(b=<a)), sat_count(Count). 3083% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3084% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3085% ?- Prop = 3086% ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)), 3087% sat(Prop), sat_count(C). 3088% ?- sat(a+b), sat(b+c), b_getval(sat_state, S), 3089% get_key(root, R, S), ltr_card(R, C, S). 3090% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false 3091% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false 3092% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa. 3093% ?- sat(A=:=B), psa, sat(B=:=C), psa. 3094% ?- sat(a), sat(b), sat(c), sat_count(C). 3095% ?- Prop = 3096% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3097% sat(Prop), 3098% sat_count(Count). 3099% ?- sat, Prop = 3100% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3101% sat(-Prop), 3102% sat_count(Count). 3103 3104% ?- sat. 3105% ?- sat(A + B), sat_count(Count), A = B, sat_count(Count1). 3106% ?- sat(a), psa. 3107% ?- sat(a->(b->a)), sat(a->(b->a)), sat_count(C). 3108% ?- sat(A->(B->A)), sat(A->(B->A)), sat_count(C). 3109% ?- sat(a), sat(b), sat_count(C), psa. 3110% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3111% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3112% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3113% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3114% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3115% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C). 3116% ?- sat(a+b+c), sat_count(C). 3117% ?- sat(x=a+b), sat(y=a+b+b+a), sat(-(x=y)), sat_count(C). % false 3118% ?- sat(x=a+b), sat(y=a+b+b+a), sat((x=y)), sat_count(C). 3119 3120 /************************************ 3121 * Setting Modes: zdd/sat/ltr * 3122 ************************************/ 3123 3124zdd:- open_state. 3125% 3126sat:- open_state, 3127 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3128 nb_linkval(zdd_compare, ltr_compare), 3129 nb_linkval(root, 1), 3130 open_memo(boole_atom, 32). 3131% 3132ltr:- open_state, 3133 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3134 nb_linkval(zdd_compare, ltr_compare), 3135 open_memo(boole_atom, 32). 3136 3137% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), ltr_card(X, C). 3138 3139% ?- sat, sat(X), sat(X\=Y), sat(Y). % fail. 3140% ?- sat, sat(X), sat(X\=Y), X=Y. % fail. 3141sat(X):- 3142 b_getval(root, Root), 3143 dnf(X, Y), 3144 ltr_merge(Y, Root, Root0), 3145 b_setval(root, Root0), 3146 Root0 \== 0. 3147% 3148sat_close:- close_state. 3149% 3150sat_count(C):- b_getval(root, X), ltr_card(X, C). 3151% 3152sat_clear:- close_state. 3153 3154% ?- sat, zdd_numbervars(f(X, Y, X)), get_attr(X, zsat, I), get_attr(Y, zsat, J). 3155zdd_numbervars(X):- get_key(varnum, N), 3156 term_variables(X, Vs), 3157 attr_numbervars(Vs, N, N0), 3158 set_key(varnum, N0). 3159 3160% 3161attr_numbervars([], N, N). 3162attr_numbervars([V|Vs], N, N0):- 3163 ( get_attr(V, zsat, _) -> 3164 attr_numbervars(Vs, N, N0) 3165 ; put_attr(V, zsat, N), 3166 K is N + 1, 3167 attr_numbervars(Vs, K, N0) 3168 ). 3169 3170% ?- heavy_valid_formula(H), prove(H). 3171heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10) 3172<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3173<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10) 3174<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3175<=> p2) <=> p1) <=> p0)). 3176 3177% ?- ltr. 3178% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y). 3179% ?- mk_left_assoc_term(=, 1, X), prove(X). 3180% ?- X<< {[a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3181% ?- X<< {[a,b],[b,c]}, ltr_merge(X, X, Z), psa(Z). 3182% ?- X<< {[a,b],[b,c]}, zdd_merge(X, X, Z), psa(Z). 3183% ?- X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3184% ?- run(1, 100). 3185% ?- run(2, 100). 3186% ?- run(5, 100). 3187% ?- run(1-9, 100). 3188% ?- run(11, 100). 3189% ?- run(12, 360). 3190%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips) 3191% imac 3192% on M1 mbp pro 32 GB, timeout. 3193 3194% ?- ltr, mk_left_assoc_term(==, 1, F), prove(F). 3195%@ VALID 3196%@ F = (((p(1)==p(0))==p(1))==p(0)). 3197run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3198 ( mk_left_assoc_term(==, K, F), 3199 format("~nPropositions: p(0) ... p(~w).~n", [K]), 3200 call_with_time_limit(T_limit, time(prove(F))))). 3201 3202% run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3203% ( mk_left_assoc_term(==, K, F), 3204% format("~nPropositions: p(0) ... p(~w).~n", [K]), 3205% call_with_time_limit(T_limit, time(seq:seq_prove(F))))). 3206% 3207run(N, T) :- run(N-N, T). 3208 3209% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X). 3210% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X). 3211 3212mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L), 3213 append(L, L, L2), 3214 reverse(L2, R), 3215 apply_left_assoc(Bop, R, Ex). 3216% 3217apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex). 3218% 3219apply_left_assoc(_, X, [], X):-!. 3220apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X], 3221 apply_left_assoc(Bop, V, Y, W). 3222 3223demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). 3224 3225% Valid formulae. 3226% ?- ltr. 3227% ?- forall(valid_formula(A), prove(A)). 3228valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)). 3229valid_formula((-(-a) -> a) * (a -> -(-a))). % Double Negation 3230valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3231valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b). 3232valid_formula(a + -a). 3233valid_formula(((a -> b) -> a) -> a). % Peirce’s Law 3234valid_formula(-(-a)->a). 3235valid_formula(a -> a). 3236valid_formula(a -> (b -> a)). 3237valid_formula((a->b)->((b->c)->(a->c))). 3238valid_formula(a->((a->b)->b)). 3239valid_formula((a*(a->b))->b). 3240valid_formula((a->b)->(-b -> -a)). 3241valid_formula((a->b)->((b->c)->(a->c))). 3242valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)). 3243 3244% ?- ltr. 3245% ?- forall(invalid_formula(A), prove(A)). 3246invalid_formula(a). 3247invalid_formula((a->b)->a). 3248invalid_formula((a->b)->(b->a)). 3249invalid_formula(a -> (b -> c)). 3250invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)). 3251invalid_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))).3282prove(X):- 3283 ( prove_(X) 3284 -> writeln('VALID') 3285 ; writeln('INVALID') 3286 ). 3287 3288% 3289prove_(X):- cnf(-X, CNF), 3290 get_key(atom_index, N), 3291 ( CNF = 0 -> N = 0 3292 ; CNF = 1 -> N > 0 3293 ; resolve(CNF) 3294 ).
3300% ?- ltr_zdd ltr_pow([a,b,c], P), resolve(P), psa(P). 3301% ?- numlist(1, 10, L), (ltr_zdd ltr_pow(L, P), ltr_card(P, C)). 3302% ?- numlist(1, 100, L), (ltr_zdd ltr_pow(L, P), ltr_card(P, C)). 3303% ?- N = 100000, numlist(1, N, L), time( (ltr_zdd ltr_pow(L, P), resolve(P))). 3304resolve(X):- zdd_has_1(X), !. % The empty clause found. 3305resolve(X):- X > 1, 3306 cofact(X, t(A, L, R)), 3307 ( L = 0 -> fail % Pure literal rule. 3308 ; A = -(_) -> resolve(L) % Negative pure literal rule. 3309 ; ( cofact(L, t(B, U, V)), % Pure literal rule. 3310 ( B = -(A) 3311 -> ltr_merge(V, R, M), % Resolution + Tautology rule. 3312 ltr_join(U, M, W), 3313 resolve(W) % Updated set of clauses. 3314 ; resolve(L) % Posituve pure literal rule. 3315 ) 3316 ) 3317 ). 3318 3319% ?- sat. 3320% ?- N=100, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3321%@ false. 3322% ?- N=2, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3323%% Debug. 3324% ?- N=11, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3325%@ false. <=== why ??? 3326 3327% ?- ltr. 3328% ?- N = 100, time((numlist(1, N, L), ltr_pow(L, P), 3329% A << set(L), zdd_subtr(P, A, Q), card(Q, C), 3330% writeln(C), resolve(Q))). % false 3331 3332% ?- N = 100000, time((numlist(1, N, _L), ltr_pow(_L, P), 3333% card(P, _C))), _C=:= 2^N. 3334 3335%@ % 31,011,164 inferences, 8.180 CPU in 12.708 seconds (64% CPU, 3790924 Lips) 3336%@ N = 100000, 3337%@ P = 300001. 3338 3339atom_index(X):- memo(atom_index(X)-Y), 3340 ( nonvar(Y) -> true 3341 ; get_key(atom_index, Y), 3342 memo(index_atom(Y)-X), 3343 Y0 is Y + 1, 3344 set_key(atom_index, Y0) 3345 ). 3346 3347% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_zdd nnf_cnf(Y, Z), psa(Z)). 3348boole_nnf(X, Y):- % numbervars_index(X, S), 3349 basic_boole(X, Z), 3350 once(neg_normal(Z, Y)). 3351 3352% ?- ltr, basic_boole(a, A). 3353% ?- ltr, basic_boole(@(a), A). 3354% ?- ltr, basic_boole(0, A). 3355% ?- ltr, basic_boole(1, A). 3356% ?- ltr, basic_boole(true, A). 3357% ?- ltr, basic_boole(a+b, A). 3358% ?- ltr, basic_boole(a+b+c, A). 3359% ?- ltr, basic_boole(-a + b + c, A). 3360% ?- ltr, basic_boole(a -> b -> c, A). 3361% ?- ltr, basic_boole((a -> b) -> c, A). 3362% ?- ltr, basic_boole(*[(a -> b), c], A). 3363% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3364% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3365% ?- ltr, basic_boole(*[0, 1, 2], A). 3366 3367% ?- ltr. 3368% ?- trace. 3369% ?- ltr, set_key(f, 0), N = 100, numlist(0, N, Ns), 3370% test_rev_memo(Ns), test_rev_memo. 3371 3372test_rev_memo :- get_key(f, K), 3373 K0 is K - 1, 3374 forall(between(0, K0, I), 3375 ( memo(g(I)-R), 3376 ( nonvar(R), memo(f(R)-I) -> true 3377 ; writeln(not(memo(f(R)-I))) 3378 ) 3379 )). 3380 3381test_rev_memo([]). 3382test_rev_memo([A|As]):- memo(f(A)-B), 3383 ( var(B) -> 3384 get_key(f, B), 3385 memo(g(B)-A), 3386 B0 is B + 1, 3387 set_key(f, B0) 3388 ; true 3389 ), 3390 test_rev_memo(As). 3391 3392 3393% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3394% forall(member(I, Ns), (memo(atom_index(I)-A), writeln(atom_index(I)-A))). 3395 3396% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), b_getval(zdd_memo, M), 3397% arg(3, M, V), maplist(writeln, V). 3398 3399% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3400% b_getval(zdd_memo, #(_,_, V)), get_key(atom_index, AtomIndex), 3401% numlist(0, AtomIndex, Is), 3402% maplist(memo_index_atom, Is, As). 3403 3404% ?- listing(memo_index_atom). 3405 3406memo_index_atom(I, A):- memo(index_atom(I)-A). 3407 3408% ?- spy(atom_index). 3409% ?- ltr, N = 100, numlist(1, N, Ns), X<< dnf(+Ns), 3410% get_key(atom_index, K), K0 is K - 1, 3411% numlist(0, K0, Is), 3412% maplist(atom_index, As, Is, As). 3413 3414% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), zdd_boole_atoms(As), forall(between(1, N, J), 3415% once((memo(index_atom(J)-X, boole_atom), 3416% writeln(memo(index_atom(J)-X))))). 3417% 3418% ?- ltr, N = 100000, numlist(0, N, Ns), 3419% maplist(memo_atom, Ns, Is), 3420% maplist(memo_atom, Ns, Is). 3421 3422% ?- ltr, N = 83, numlist(0, N, Ns), 3423% maplist(memo_atom, Ns, Is), 3424% maplist(memo_atom, R, Is), 3425% memo_atom(86, K), memo_atom(87, L), 3426% maplist(memo_atom, U, Is), get_key(atom_index, A), 3427% memo_atom(30, B). 3428 3429% ?- ltr, N = 10000, numlist(0, N, As), 3430% maplist(atom_index, As, Is), 3431% maplist(atom_index, As0, Is), 3432% As = As0, 3433% atom_index(hello, I), 3434% atom_index(A, I). 3435 3436% ?- ltr, atom_index(X, 2). % false. 3437%@ atom_index(_346,2) 3438%@ true. 3439% ?- ltr, N=3, K=100, open_hash(N, H), nb_setval(zdd_memo, H), !, 3440% numlist(1, K, Ks), X<< dnf(+Ks). 3441 3442memo_atom(X):- atom_index(X, _). 3443 3444memo_atom(X, I):- atom_index(X, I). 3445 3446% 3447atom_index(X, I):- var(X), !, memo(index_atom(I)-X). 3448atom_index(X, I):- 3449 memo(atom_index(X)-I), 3450 ( var(I) -> 3451 get_key(atom_index, I), 3452 J is I + 1, 3453 set_key(atom_index, J), 3454 memo(index_atom(I)-X) 3455 ; true 3456 ). 3457 3458% ?- sat. 3459% ?- sat(A=B), sat(B=C), sat_count(D). 3460basic_boole(A, @('$VAR'(I))):-var(A), !, get_attr(A, zsat, I), 3461 memo_atom('$VAR'(I)). 3462basic_boole(A, BoolConst):-atomic(A), 3463 boole_op(0, [], Fs, BoolConst), 3464 memberchk(A, Fs), 3465 !. 3466basic_boole(I, @(I)):- integer(I), !, memo_atom(I). 3467basic_boole(@(I), @(I)):-!, memo_atom(I). 3468basic_boole(*(L), F):-!, basic_boole_vector(L, *, F). 3469basic_boole(+(L), F):-!, basic_boole_vector(L, +, F). 3470basic_boole(X, Y):- X=..[F|Xs], 3471 length(Xs, N), 3472 boole_op(N, As, Fs, Y), 3473 memberchk(F, Fs), 3474 !, 3475 basic_boole_list(Xs, As). 3476basic_boole(X, @(X)):- memo_atom(X). 3477 3478% 3479basic_boole_list([], []). 3480basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y), 3481 basic_boole_list(Xs, Ys). 3482% 3483basic_boole_vector([], +, false):-!. 3484basic_boole_vector([], *, true):-!. 3485basic_boole_vector([X|Xs], F, Y):- 3486 basic_boole(X, X0), 3487 Y=..[F, X0, Z], 3488 basic_boole_vector(Xs, F, Z). 3489 3490% Remark [2023/11/13]: 3491% Use of 0/1 as Boolean constants has been dropped. 3492% Any integer is now usable for a boolean variable, which 3493% may be useful or (nested) vectors of integers *[...], +[...]. 3494% 0/1 as boolean is error prone because ZDD must use 0/1 internally 3495% as basic constant similar, but not exactly the same, 3496% to true/flase. They are different. 3497% This decision was hard because 0/1 is traditionally useful 3498% as boolean constrants, but clear separation and simplicity 3499% were preferred. 3500 3501boole_op(0, [], [false, ff], false). % 0 for false dropped. 3502boole_op(0, [], [true, tt], true). % 1 for true dropped. 3503boole_op(1, [X], [-, ~, \+, not], -(X)). 3504boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y). 3505boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y). 3506boole_op(2, [X, Y], [->, imply], -X + Y). 3507boole_op(2, [X, Y], [<-], Y->X). 3508boole_op(2, [X, Y], [iff, ==, =, =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y). 3509boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)). % -(X==Y) = xor(X, Y) 3510boole_op(2, [X, Y], [nand], -(X) + (-Y)). 3511 3512 3513% ?- neg_normal(-(true + b), X). 3514% ?- neg_normal(-(a), X). 3515% ?- neg_normal(-(a), X). 3516% ?- neg_normal(-(a), X). 3517neg_normal(true, true). 3518neg_normal(false, false). 3519neg_normal(-(false), true). 3520neg_normal(-(true), false). 3521neg_normal(-(-X), Z) :- neg_normal(X, Z). 3522neg_normal(-(X+Y), Z) :- neg_normal(-X* -Y, Z). 3523neg_normal(-(X*Y), Z) :- neg_normal(-X+ -Y, Z). 3524neg_normal(-(X), -(Y)) :- neg_normal(X, Y). 3525neg_normal(X+Y, X0+Y0) :- neg_normal(X, X0), 3526 neg_normal(Y, Y0). 3527neg_normal(X*Y, X0*Y0) :- neg_normal(X, X0), 3528 neg_normal(Y, Y0). 3529neg_normal(@(X), @(X)):-!. 3530neg_normal(X, @(X)):-!. 3531 3532% ?- zdd((intern(-(a;b;c), X), boole_to_dnf(X, Z), sets(Z, U), extern(U, Y))). 3533%% extern(+X, -Y) is det. 3534% Convert an internal form X into an external one 3535% in order to unify Y with the result. 3536 3537extern(X, Y):-integer(X), !, 3538 ( X < 2 -> Y = X 3539 ; memo(index_atom(X)-Y) 3540 ). 3541extern(X, X):- atomic(X), !. 3542extern(X, Y):- X =.. [F|Xs], 3543 extern_list(Xs, Ys), 3544 Y =..[F|Ys]. 3545% 3546extern_list([], []). 3547extern_list([X|Xs], [Y|Ys]):- extern(X, Y), 3548 extern_list(Xs, Ys). 3549 3550 /********************************************* 3551 * Cofact/insert/join/merge on literals * 3552 *********************************************/
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 ).3567ltr_cofact(Z, Y):- nonvar(Z), !, cofact(Z, Y). 3568ltr_cofact(Z, t(A, V, U)):- U > 1, !, 3569 cofact(U, t(B, L, _)), 3570 ( ltr_invert(A, B) 3571 -> ltr_cofact(Z, t(A, V, L)) 3572 ; cofact(Z, t(A, V, U)) 3573 ). 3574ltr_cofact(Z, T):- cofact(Z, T).
3583% PASS. 3584% ?- ltr_zdd cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S). 3585% ?- ltr_zdd dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S). 3586% ?- ltr_zdd ltr_insert(a, 1, X), sets(X, S). 3587% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), sets(Y, S). 3588% ?- ltr_zdd ltr_insert(a, 1, X), ltr_insert(b, X, Y), 3589% ltr_insert(-b, Y, Z), sets(Z, S). 3590% ?- ltr_zdd X<<set([a]), ltr_insert(b, X, Y), psa(Y). 3591% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3592% ?- ltr_zdd X<<set([b]), ltr_insert(a, X, Y), psa(Y). 3593% ?- ltr_zdd X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3594% ?- ltr_zdd X<<set([-a]), ltr_insert(a, X, Y), psa(Y))). 3595% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y). 3596% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y). 3597% ?- ltr_zdd X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y). 3598% ?- ltr_zdd X<<{[a]}, ltr_insert(a, X, Y), psa(Y). 3599% ?- ltr_zdd X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y). 3600% ?- ltr_zdd X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y). 3601% ?- ltr_zdd X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y). 3602% ?- ltr_zdd X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y). 3603% ?- ltr_zdd X<< dnf(a), ltr_insert(b, X, Y), psa(Y). 3604% ?- ltr_zdd X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y). 3605% ?- ltr_zdd X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y). 3606% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3607% ?- ltr_zdd X<< dnf((x=\=y)*x*y), psa(X). 3608% ?- sat((x=\=y)*x*y). % false 3609% ?- sat((a * -a)). % false 3610% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y). 3611% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y). 3612% ?- ltr_zdd dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y). 3613% ?- ltr_zdd dnf((-a)*b, X), psa(X). 3614% ?- ltr_zdd cnf((-a)*b, X). 3615% ?- ltr_zdd cnf((a), X). 3616 3617ltr_insert(_, 0, 0):-!. 3618ltr_insert(A, 1, J):-!, zdd_singleton(A, J). 3619ltr_insert(A, I, J):- memo(ltr_insert(A,I)-J), 3620 ( nonvar(J) -> true 3621 ; cofact(I, t(B, L, R)), 3622 zdd_compare(C, A, B), 3623 ( C = (<) -> 3624 ( complementary(A, B) -> 3625 cofact(J, t(A, 0, L)) 3626 ; cofact(J, t(A, 0, I)) 3627 ) 3628 ; C = (=) -> 3629 ( negative(A) -> 3630 ltr_join(L, R, K), 3631 cofact(J, t(A, 0, K)) 3632 ; ltr_insert_aux(J, A, L, R) 3633 ) 3634 ; ( complementary(A, B) -> ltr_insert(A, L, J) 3635 ; ltr_insert(A, L, L0), 3636 ltr_insert(A, R, R0), 3637 cofact(J, t(B, L0, R0)) 3638 ) 3639 ) 3640 ). 3641 3642% for suppressing use of cofact/3 and ltr_insert/4 3643ltr_insert_aux(J, A, L, R):- % A is positive. R has no -A. 3644 ( L < 2 -> cofact(J, t(A, L, R)) 3645 ; cofact(L, t(B, L0, _)), 3646 ( complementary(A, B)-> 3647 ltr_join(L0, R, K), 3648 cofact(J, t(A, 0, K)) 3649 ; ltr_join(L, R, K), 3650 cofact(J, t(A, 0, K)) 3651 ) 3652 ).
3658% 3659ltr_join(X, X, X):-!. % idemopotent law of logical disjunction (OR) 3660ltr_join(0, X, X):-!. 3661ltr_join(X, 0, X):-!. 3662ltr_join(1, _, 1):-!. 3663ltr_join(_, 1, 1):-!. 3664ltr_join(X, Y, Z):- 3665 ( X=<Y -> memo(ltr_join(X,Y)-Z) 3666 ; memo(ltr_join(Y,X)-Z) 3667 ), 3668 ( nonvar(Z) -> true %, write(.) 3669 ; cofact(X, t(A, L, R)), 3670 cofact(Y, t(A0, L0, R0)), 3671 zdd_compare(C, A, A0), 3672 ( C = (=) -> 3673 ltr_join(R, R0, U), 3674 ltr_join(L, L0, V), 3675 cofact(Z, t(A, V, U)) 3676 ; C = (<) -> 3677 ltr_join(L, Y, U), 3678 cofact(Z, t(A, U, R)) 3679 ; ltr_join(L0, X, U), 3680 cofact(Z, t(A0, U, R0)) 3681 ) 3682 ).
3691ltr_merge(X, X, X):-!. % idempotent law of logical conjunction (AND). 3692ltr_merge(0, _, 0):-!. 3693ltr_merge(_, 0, 0):-!. 3694ltr_merge(1, X, X):-!. 3695ltr_merge(X, 1, X):-!. 3696ltr_merge(X, Y, Z):- 3697 ( X =< Y -> memo(ltr_merge(X,Y)-Z) 3698 ; memo(ltr_merge(Y,X)-Z) 3699 ), 3700 ( nonvar(Z) -> true 3701 ; cofact(Y, t(A, L, R)), 3702 ltr_merge(X, R, U), 3703 ltr_merge(X, L, V), 3704 ltr_insert(A, U, U0), 3705 ltr_join(V, U0, Z) 3706 ).
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).3713ltr_xor(X, Y, Z):- 3714 ltr_negate(Y, Y0), 3715 ltr_merge(X, Y0, U), 3716 ltr_negate(X, X0), 3717 ltr_merge(X0, Y, V), 3718 ltr_join(U, V, Z). 3719 3720 /****************************************** 3721 * Auxiliary operations on literals * 3722 ******************************************/
3726complementary(-(A), A):-!. 3727complementary(A, -(A)). 3728% 3729negative(-(_)).
3737% ?- ltr_zdd ltr_pow([a], X), card(X, C), psa(X). 3738% ?- ltr_zdd ltr_pow([a, b], X), card(X, C), psa(X). 3739% ?- ltr_zdd {numlist(1, 100, L)}, ltr_pow(L, X), card(X, C). 3740ltr_pow([], 1). 3741ltr_pow([A|As], P):- ltr_pow(As, Q), 3742 ltr_insert(A, Q, R), 3743 ltr_insert(-A, Q, L), 3744 ltr_join(L, R, P).
3752% ?- ltr_zdd ltr_append([-b, a, -d, c], 1, X), psa(X). 3753% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3754% ?- ltr_zdd ltr_append([-b, -d, c], 1, X), psa(X). 3755% ?- ltr_zdd X<<dnf(a->a), ltr_card(X, C), psa(X). 3756% 3757ltr_append([], X, X). 3758ltr_append([A|As], X, Y):- ltr_append(As, X, X0), 3759 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))).3767% 3768ltr_set(X, Y):- ltr_append(X, 1, Y).
3775% ?- zdd((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))). 3776% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))). 3777% ?- zdd((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))). 3778% ?- zdd((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3779% ?- zdd((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3780 3781% ?- ltr_zdd X<<dnf(a), ltr_negate(X, Y), psa(Y). 3782% ?- ltr_zdd ltr_negate(0, Y), psa(Y). 3783% ?- ltr_zdd ltr_negate(1, Y), psa(Y). 3784 3785% 3786ltr_negate(X, Y):- ltr_complement(X, X0), ltr_choices(X0, Y).
3795% ?- zdd X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y). 3796% ?- zdd X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y). 3797% 3798ltr_complement(X, X):- X<2, !. 3799ltr_complement(I, Y):- memo(ltr_complement(I)-Y), 3800 ( nonvar(Y) -> true 3801 ; cofact(I, t(A, L, R)), 3802 ltr_complement(L, L0), 3803 ltr_complement(R, R0), 3804 complementary(A, NA), 3805 ltr_insert(NA, R0, R1), 3806 ltr_join(L0, R1, Y) 3807 ). 3808 3809 /************************************ 3810 * Convert Boolean Form to DNF/CNF * 3811 ************************************/
3816% ?- boole_nnf(-(a+b), X). 3817% ?- zdd dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V). 3818% ?- zdd((dnf(-(a=:=b), X), psa(X))). 3819% ?- zdd((dnf((a=\=b), X), psa(X))). 3820% ?- zdd((dnf((0), X), psa(X))). 3821% ?- zdd((dnf(*[1,3,2,3], X), psa(X))). 3822% ?- zdd dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I). 3823% ?- zdd((dnf(*[@(1),3,2,3], X), psa(X))). 3824 3825dnf(X, Y):- zdd_numbervars(X), 3826 boole_nnf(X, Z), 3827 nnf_dnf(Z, Y).
3836% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y). 3837% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U). 3838% ?- ltr_zdd big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D). 3839 3840dnf_cnf(X, Y):- nonvar(X), !, ltr_choices(X, Y). 3841dnf_cnf(X, Y):- ltr_choices(Y, X). 3842% 3843cnf_dnf(X, Y):- dnf_cnf(X, Y). 3844 3845% ?- ltr_zdd X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y). 3846%@ * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug 3847% ?- ltr_zdd X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y). 3848% ?- ltr_zdd X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y). 3849% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3850% ?- ltr_zdd X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y). 3851% ?- ltr_zdd X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3852% ?- ltr_zdd X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y). 3853% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3854% dnf_cnf(Z, Y), psa(X), psa(Y). 3855 3856% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3857% dnf_cnf(Z, Y), psa(X), psa(Y). 3858 3859% ?- ltr_zdd X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3860% dnf_cnf(Z, Y). 3861 3862% ?- ltr_zdd X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), 3863% dnf_cnf(Z, U). 3864 3865% ?- N=100, time((ltr_zdd big_normal_form(N, X), 3866% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3867%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips) 3868%@ N = 100, 3869%@ X = 39901, 3870%@ Y = D, D = 0, % <== CORRECT. 3871%@ C = 1267650600228229401496703205376 . 3872 3873% ?- N=1000, time((ltr_zdd big_normal_form(N, X), 3874% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3875%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips) 3876%@ N = 1000, 3877%@ X = 3999001, 3878%@ Y = D, D = 0, % <== CORRECT. 3879%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
3893ltr_choices(0, 1):-!. 3894ltr_choices(1, 0):-!. 3895ltr_choices(X, Y):- memo(ltr_choices(X)-Y), 3896 ( nonvar(Y)->true %, write(.) % many hits. 3897 ; cofact(X, t(A, L, R)), 3898 ltr_choices(L, L0), 3899 ltr_choices(R, R0), 3900 cofact(R1, t(A, R0, 1)), 3901 ltr_merge(L0, R1, Y) 3902 ).
3907nnf_dnf(false * _, 0):-!. 3908nnf_dnf(_ * false, 0):-!. 3909nnf_dnf(true * X, Y):-!, nnf_dnf(X, Y). 3910nnf_dnf(X * true, Y):-!, nnf_dnf(X, Y). 3911nnf_dnf(X * Y, Z):-!, memo(dnf(X*Y)-Z, boole_atom), 3912 ( nonvar(Z) -> true 3913 ; nnf_dnf(X, U), 3914 nnf_dnf(Y, V), 3915 ltr_merge(U, V, Z) 3916 ). 3917nnf_dnf(false + X, Y):-!, nnf_dnf(X, Y). 3918nnf_dnf(X + false, Y):-!, nnf_dnf(X, Y). 3919nnf_dnf(true + X, Y):-!, nnf_dnf(X, Z), 3920 ltr_join(1, Z, Y). 3921nnf_dnf(X + true, Y):-!, nnf_dnf(X, Z), 3922 ltr_join(1, Z, Y). 3923nnf_dnf(X + Y, Z):-!, memo(dnf(X+Y)-Z, boole_atom), 3924 ( nonvar(Z) -> true 3925 ; nnf_dnf(X, U), 3926 nnf_dnf(Y, V), 3927 ltr_join(U, V, Z) 3928 ). 3929nnf_dnf(@(X), I):-!, zdd_singleton(X, I). 3930nnf_dnf(-(@(X)), I):- zdd_singleton(-(X), I).
3936% ?- zdd((cnf(a, X), S<<sets(X))). 3937% ?- ltr_zdd((cnf(a*b, X), S<<sets(X))). 3938% ?- zdd((X<<cnf(-a), Y<<sets(X))). 3939% ?- zdd((X<<cnf(a+b), Y<<sets(X))). 3940% ?- zdd((X<<cnf(+([a,b,c])), Y<<sets(X))). 3941% ?- zdd((X<<cnf(*([a,b,c])), Y<<sets(X))). 3942% ?- zdd((X<<dnf(+([a,b,c])), Y<<sets(X))). 3943% ?- zdd((X<<dnf(*([a,b,c])), Y<<sets(X))). 3944% ?- zdd((cnf(a, X), psa(X))). 3945% ?- zdd((cnf(-a, X), psa(X))). 3946% ?- zdd((cnf(a+b, X), psa(X))). 3947% ?- zdd((cnf(a+b+(-c), X), psa(X))). 3948% ?- zdd((cnf(-a * a, X), psa(X))). 3949% ?- zdd((cnf(a->a, X), psa(X))). 3950% ?- zdd((cnf(-a * a, X), psa(X))). 3951% ?- zdd((cnf( a + a, X), psa(X))). 3952% ?- zdd((cnf( A + A, X), psa(X))). 3953% ?- zdd((cnf(-(a*b), X), psa(X))). 3954% ?- zdd((cnf(*([a,b,c]), X), psa(X))). 3955% ?- zdd {N = 10, numlist(2, N, Ns)}, cnf(*(Ns), X), ltr_card(X, C, K). 3956% ?- ltr_zdd((dnf(a, X), psa(X))). 3957% ?- ltr_zdd((cnf(-(a->b), X), psa(X))). 3958% ?- ltr_zdd((cnf(a, X), psa(X))). 3959% ?- boole_nnf(-(*[0,1,2]), X). 3960% ?- ltr_zdd {mk_left_assoc_term(==, 1, F)}, cnf(F, X), psa(X). 3961cnf(X, Y):- zdd_numbervars(X), 3962 boole_nnf(X, Z), 3963 nnf_cnf(Z, Y). 3964% 3965nnf_cnf(true, 1):-!. 3966nnf_cnf(false, 0):-!. 3967nnf_cnf(false * _, 0):-!. 3968nnf_cnf(_ * false, 0):-!. 3969nnf_cnf(true * X, Y):-!, nnf_cnf(X, Y). 3970nnf_cnf(X * true, Y):-!, nnf_cnf(X, Y). 3971nnf_cnf(X * X, Y):-!, nnf_cnf(X, Y). 3972nnf_cnf(X * Y, Z):-!, memo(cnf(X*Y)-Z, boole_atom), 3973 ( nonvar(Z)->true %, write(.) % many hits. 3974 ; nnf_cnf(X, U), 3975 nnf_cnf(Y, V), 3976 ltr_join(U, V, Z) 3977 ). 3978nnf_cnf(false + X, Y):-!, nnf_cnf(X, Y). 3979nnf_cnf(X + false, Y):-!, nnf_cnf(X, Y). 3980nnf_cnf(true + _, 1):-!. 3981nnf_cnf(_ + true, 1):-!. 3982nnf_cnf(X + X, Y):-!, nnf_cnf(X, Y). 3983nnf_cnf(X + Y, Z):-!, memo(cnf(X+Y)-Z, boole_atom), 3984 ( nonvar(Z)->true %, write(+) % many hits. 3985 ; nnf_cnf(X, U), 3986 nnf_cnf(Y, V), 3987 ltr_merge(U, V, Z) 3988 ). 3989nnf_cnf(@(X), I):-!, zdd_singleton(X, I). 3990nnf_cnf(-(@(X)), I):- zdd_singleton(-(X), I). 3991 3992 3993 /***************************************************** 3994 * ltr_card/[3,4] Counting solutions of a DNF. * 3995 *****************************************************/ 3996 3997% ?- sat(a), sat_count(C). 3998% ?- sat(A+B), sat_count(C), zsat:(A=B), sat_count(D). 3999% ?- sat(A+B), sat_count(C), A = B, sat_count(D). 4000% ?- X<< dnf(a), sat_count_by_collect_atoms(X, C). 4001% ?- sat_count_by_collect_atoms(a+b, C). 4002% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C). 4003% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 4004 4005% ?- sat. 4006% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 4007% 4008sat_count_by_collect_atoms(F, C):- dnf(F, X), 4009 zdd_boole_atoms(Us), 4010 zdd_sort(Us, Vs), 4011 expand_dnf(Vs, X, Y), 4012 card(Y, C). 4013 4014% ?- ltr, N=100, numlist(0, N, Ns), X<<dnf(+Ns), zdd_boole_atoms(Us). 4015%@ N = 100, 4016%@ Ns = Us, Us = [0, 1, 2, 3, 4, 5, 6, 7, 8|...], 4017%@ X = 202. 4018 4019zdd_boole_atoms(Us):- get_key(atom_index, N), 4020 collect_boole_atoms(0, N, Us). 4021 4022% 4023collect_boole_atoms(I, N, []):- I>=N, !. 4024collect_boole_atoms(I, N, [A|U]):- 4025 atom_index(A, I), 4026 J is I+1, 4027 collect_boole_atoms(J, N, U). 4028 4029 /****************************** 4030 * find_counter_example * 4031 ******************************/
4035% ?- findall_counter_examples(a, X), psa(X). 4036% ?- findall_counter_examples((a->b)->a, X), psa(X). 4037% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4038% ?- findall_counter_examples(a->b, X), psa(X). 4039% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4040% ?- findall_counter_examples(a->b, Out), psa(Out). 4041findall_counter_examples(In, Out):- 4042 ltr_fetch_state, 4043 dnf(In, InZ), 4044 zdd_boole_atoms(Us), 4045 zdd_sort(Us, Vs), 4046 expand_prefix_dnf(Vs, 1, All), 4047 expand_dnf(Vs, InZ, Y), 4048 zdd_subtr(All, Y, Out).
4055% ?- ltr. 4056% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4057% ?- X<< dnf(a), psa(X), ltr_card(X, C). 4058% ?- X<< dnf(a->a), ltr_card(X, C). 4059% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4060% ?- ltr, X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C). 4061 4062% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4063% time((X<< dnf(+Ps), ltr_card(X, C))). 4064 4065 4066%@ % 123,881 inferences, 0.833 CPU in 1.321 seconds (63% CPU, 148761 Lips) 4067%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4068%@ X = 80, 4069%@ C = 1099511627775. 4070 4071%@ % 123,882 inferences, 0.010 CPU in 0.010 seconds (97% CPU, 12260689 Lips) 4072%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4073%@ X = 80, 4074%@ C = 1099511627775. 4075 4076% ?- ltr, findall(p(J), between(1, 30, J), Ps), 4077% time((X<< dnf(+Ps), ltr_card(X, C))). 4078% ?- ltr, numlist(1, 30, Ps), time((X<< dnf(+Ps), ltr_card(X, C))). 4079% ?- sat, numlist(1, 30, Ps), sat(+Ps), sat_count(C). 4080 4081% ?- spy(ltr_card). 4082% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4083% time((X<< dnf(+Ps), ltr_card(X, C))). 4084 4085% ?- findall(p(J), between(1, 100, J), Ps), 4086% time((X<< dnf(*Ps), ltr_card(X, C))). 4087 4088% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps). 4089% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4090% time((X<< dnf(+Ps),ltr_card(X, C))), 4091% C =:= 2^1000 - 1. 4092 4093% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4094% time((X<< dnf(+Ps), card(X, C))). 4095 4096ltr_card(In, Out):- 4097 zdd_boole_atoms(Us), 4098 zdd_sort(Us, Vs), 4099 expand_dnf(Vs, In, Y), 4100 card(Y, Out). 4101 4102% ?- ltr_var(-(5), X). 4103ltr_var(-(V), V):-!. 4104ltr_var(V, V).
4111% ?- ltr, X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y). 4112% ?- ltr, X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), ltr_card(Y, C). 4113% ?- ltr, X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C). 4114% ?- ltr, X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y). 4115% ?- ltr, X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4116% ?- ltr, X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4117% ?- ltr, X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4118 4119expand_dnf([], X, X):-!. 4120expand_dnf(_, 0, 0):-!. 4121expand_dnf(Vs, 1, Y):-!, expand_prefix_dnf(Vs, 1, Y). 4122expand_dnf(Vs, X, Y):- memo(expand_dnf(X,Vs)-Y), 4123 ( nonvar(Y) -> true %, write(.) % Many hits. 4124 ; cofact(X, t(A, L, R)), 4125 ltr_var(A, K), 4126 divide_ord_list(Vs, K, [], Us, Ws), 4127 expand_dnf(Us, R, R0), 4128 ltr_insert(A, R0, R1), 4129 expand_left_dnf(K, Us, L, L0), 4130 ltr_join(L0, R1, X0), 4131 expand_prefix_dnf(Ws, X0, Y) 4132 ).
divide_ord_list([a,b,c,d,e], c, [u], T, W).
?- divide_ord_list([a,b,c, d], e, [], X, Y). % false4140divide_ord_list([V|Vs], V, Us, Vs, Us):-!. 4141divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U), 4142 divide_ord_list(Vs, U, [V|Us], Ws, Ps).
4149% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))). 4150expand_prefix_dnf(Vs, X, Y):- zdd_sort(Vs, OrdVs), 4151 expand_ord_prefix_dnf(OrdVs, X, Y). 4152 4153% 4154expand_ord_prefix_dnf([], X, X):-!. 4155expand_ord_prefix_dnf([V|Vs], X, Y):- 4156 expand_ord_prefix_dnf(Vs, X, X0), 4157 ltr_insert(V, X0, X1), 4158 ltr_insert(-V, X0, X2), 4159 ltr_join(X1, X2, Y).
4169expand_left_dnf(_, _, 0, 0):-!. 4170expand_left_dnf(K, Us, 1, Y):-!, expand_prefix_dnf([K|Us], 1, Y). 4171expand_left_dnf(K, Us, X, Y):- cofact(X, t(A, L, R)), 4172 ltr_var(A, J), 4173 ( K = J -> 4174 expand_dnf(Us, R, R0), 4175 ltr_insert(A, R0, R1) 4176 ; divide_ord_list([K|Us], J, [], Vs, Ws), 4177 expand_dnf(Vs, R, R0), 4178 ltr_insert(A, R0, Q), 4179 expand_prefix_dnf(Ws, Q, R1) 4180 ), 4181 expand_dnf([K|Us], L, L0), 4182 ltr_join(L0, R1, Y). 4183 4184 /******************************* 4185 * Filter on cardinality * 4186 *******************************/
4192% ?- zdd((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))). 4193card_filter_gte(0, X, X):- !. % gte: greater than or equal 4194card_filter_gte(1, X, Y):- !, zdd_subtr(X, 1, Y). 4195card_filter_gte(_, X, 0):- X<2, !. 4196card_filter_gte(N, X, Y):- memo(filter_gte(N,X)-Y), 4197 ( nonvar(Y) -> true % many hits. 4198 ; cofact(X, t(A, L, R)), 4199 N0 is N - 1, 4200 card_filter_gte(N, L, L0), 4201 card_filter_gte(N0, R, R0), 4202 cofact(Y, t(A, L0, R0)) 4203 ).
4209% ?- X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y). 4210card_filter_lte(0, X, Y):- % lte: less than or equal 4211 ( zdd_has_1(X) -> Y = 1 4212 ; Y = 0 4213 ). 4214card_filter_lte(_, X, X):- X<2, !. 4215card_filter_lte(N, X, Y):- memo(filter_lte(N,X)-Y), 4216 ( nonvar(Y) -> true % many hits. 4217 ; cofact(X, t(A, L, R)), 4218 N0 is N - 1, 4219 card_filter_lte(N, L, L0), 4220 card_filter_lte(N0, R, R0), 4221 cofact(Y, t(A, L0, R0)) 4222 ).
time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))).4228card_filter_between(I, J, X, Y):- 4229 card_filter_gte(I, X, Z), 4230 card_filter_lte(J, Z, Y). 4231 4232% ?- time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))). 4233card_filter_between_by_meet(I, J, X, Y):- 4234 card_filter_gte(I, X, Z), 4235 card_filter_lte(J, X, U), 4236 zdd_meet(Z, U, Y). 4237 4238 4239 /********************************************************* 4240 * Solve boolean equations and verify the solution * 4241 *********************************************************/ 4242% Recovered [2023/11/14] 4243%! dnf_subst(+V, +T, +X, -Y) is det. 4244% Y is the ZDD obtained by substituting each 4245% occurrence of atom V in X with T. 4246 4247% ?-ltr_zdd X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4248% ?-ltr_zdd X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4249% ?-ltr_zdd X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4250 4251dnf_subst(_, _, X, X):- X < 2, !. 4252dnf_subst(V, D, X, Y):- 4253 cofact(X, t(A, L, R)), 4254 dnf_subst(V, D, L, L0), 4255 once( A = -(U); U = A ), 4256 ltr_compare(C, V, U), 4257 ( C = (<) -> Y = X 4258 ; ( C = (=) -> 4259 ( A = (-V) -> 4260 ltr_negate(D, D0), 4261 ltr_merge(D0, R, R0) 4262 ; A = V -> 4263 ltr_merge(D, R, R0) 4264 ) 4265 ; dnf_subst(V, D, R, R1), 4266 ltr_insert(A, R1, R0) 4267 ), 4268 ltr_join(L0, R0, Y) 4269 ).
4277% exists x s.t. C0*(L,-x) + C1*x = 1 4278% if and only if 4279% C0 + C1 = 1 satisfiable 4280% x = a*C1 + (-C0). 4281 4282% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S). 4283% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S). 4284% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S). 4285 4286solve_boole_with_check(Exp, Xs, Ps):- 4287 dnf(Exp, E), 4288 solve_boolean_equations(E, Xs, Ps, Sols), 4289 eliminate_variables(E, Sols, Cond), 4290 !, 4291 dnf_valid_check(Cond). 4292 4293% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), 4294% solutions_to_sets(Sols, Sols0). 4295% ?- ltr_zdd E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0). 4296 4297solve_boolean_equations(_, [], _, []):-!. 4298solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols]):- 4299 solve_boolean_equations_basic(E, X, A, Sol0, E0), 4300 solve_boolean_equations(E0, Xs, As, Sols), 4301 dnf_subst_list(Sols, Sol0, Sol). 4302 4303% ?- ltr_zdd E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond). 4304solve_boolean_equations_basic(E, X, A, Sol, Cond):- 4305 dnf_subst(X, 1, E, C1), 4306 dnf_subst(X, 0, E, C0), 4307 ltr_join(C0, C0, Cond), 4308 ltr_negate(C0, NC0), 4309 ltr_insert(A, C1, AC1), 4310 ltr_join(NC0, AC1, Sol). 4311% 4312dnf_subst_list([], E, E). 4313dnf_subst_list([X=A|Eqs], E, F):- 4314 dnf_subst(X, A, E, E0), 4315 dnf_subst_list(Eqs, E0, F). 4316% 4317solutions_to_sets([], []). 4318solutions_to_sets([X = E|Sols], [X = E0|Sols0]):- 4319 sets(E, E0), 4320 solutions_to_sets(Sols, Sols0). 4321 4322% ?- 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). 4323 4324% ?- 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). 4325 4326% ?- 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). 4327 4328eliminate_variables(Exp, Eqns, Cond):- 4329 apply_subst_list(Eqns, Exp, Cond). 4330% 4331apply_subst_list([], E, E). 4332apply_subst_list([X=U|Eqns], E, E0):- 4333 dnf_subst(X, U, E, E1), 4334 dnf_subst_list(Eqns, E1, E0). 4335% 4336dnf_valid_check(X):- 4337 ltr_atoms_by_scan(X, As), 4338 ltr_sort(As, Bs), 4339 expand_dnf(Bs, X, Y), 4340 card(Y, C), 4341 length(Bs, N), 4342 ( C =:= (1<< N) -> writeln('Solved and Verified.') 4343 ; writeln('Solved but NOT verified.') 4344 ). 4345 4346% ?- ltr_zdd X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), {sort(As, Bs)}. 4347ltr_atoms_by_scan(X, []):- X<2, !. 4348ltr_atoms_by_scan(X, P):- memo(ltr_atoms(X)-P), 4349 ( nonvar(P) -> true 4350 ; cofact(X, t(A, L, R)), 4351 ltr_atoms_by_scan(L, Al), 4352 ltr_atoms_by_scan(R, Ar), 4353 ltr_var(A, A0), 4354 union([A0|Al], Ar, P) 4355 ). 4356 4357 /********************************* 4358 * operations on reducible zdd * 4359 *********************************/
4365% ?- numlist(1, 100, Ns), X<<pow(Ns), card(X, C). 4366% ?- bdd_sort_append([c, a, b,c], 1, Z), psa(Z). 4367bdd_sort_append(X, Y, Z):- zdd_sort(X, X0), 4368 bdd_append(X0, Y, Z). 4369 4370% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y). 4371% ?- zdd bdd_append([x, a, y, b], 0, Y), psa(Y). 4372% ?- zdd bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z). 4373 4374bdd_append([], Z, Z). 4375bdd_append([X|Y], Z, U):- 4376 bdd_append(Y, Z, Z0), 4377 bdd_cons(U, X, Z0). 4378 4379% ?- zdd bdd_list([b, b], Y), bdd_sort_append([b,b], Y, Z), psa(Z). 4380% ?- zdd bdd_list([b, b], Y), bdd_list(X, Y). 4381bdd_list(List, X):- var(X), !, bdd_append(List, 1, X). 4382bdd_list(List, X):- get_bdd_list(X, List). 4383 4384% ?- zdd bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L). 4385% ?- zdd bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L). 4386get_bdd_list(1, []):-!. 4387get_bdd_list(X, [A|As]):- X>1, bdd_cons(X, A, X0), 4388 get_bdd_list(X0, As). 4389 4390% ?- zdd bdd_append([a,a,b,b], 1, X), 4391% bdd_append([1,1,2,2], 1, Y), 4392% bdd_zip(X, Y, Z), psa(Z). 4393bdd_zip(0, _, 0):-!. 4394bdd_zip(_, 0, 0):-!. 4395bdd_zip(1, _, 1):-!. 4396bdd_zip(_, 1, 1):-!. 4397bdd_zip(X, Y, Z):- bdd_cons(X, A, X0), 4398 bdd_cons(Y, B, Y0), 4399 bdd_zip(X0, Y0, Z0), 4400 bdd_cons(Z, A-B, Z0). 4401 4402% ?- zdd bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y). 4403bdd_normal(X, X):- X<2, !. 4404bdd_normal(X, Y):- cofact(X, t(A, L, R)), 4405 bdd_normal(L, L0), 4406 bdd_normal(R, R1), 4407 zdd_insert(A, R1, R0), 4408 zdd_join(L0, R0, Y). 4409 4410% ?- zdd bdd_append([a,b,a,b], 1, X), 4411% bdd_append([a,b, c, a,b, c], 1, Y), 4412% bdd_append([b, a, b, a, a,b ], 1, Z), 4413% bdd_list_normal([X, Y, Z], R), psa(R). 4414 4415bdd_list_normal([], 0). 4416bdd_list_normal([A|As], R):- bdd_list_normal(As, R0), 4417 bdd_normal(A, A0), 4418 zdd_join(A0, R0, R). 4419 4420% 4421bdd_insert(_, 0, 0):-!. 4422bdd_insert(A, 1, X):-!, zdd_singleton(A, X). 4423bdd_insert(A, X, Y):- cofact(X, t(B, L, R)), 4424 bdd_insert(A, L, L0), 4425 bdd_append([A,B], R, R0), 4426 zdd_join(L0, R0, Y).
4435% ?- bdd_list_raise([], 0, X). 4436% ?- bdd_list_raise([a], 0, X). 4437% ?- bdd_list_raise([a], 1, X), psa(X). 4438% ?- bdd_list_raise([a,b], 1, X), psa(X). 4439% ?- N = 1, numlist(1, N, Ns), bdd_list_raise(Ns, N, X), card(X, C). 4440 4441% ?- zdd {N = 15, numlist(1, N, Ns)}, bdd_list_raise(Ns, N, X),card(X, C). 4442 4443bdd_list_raise(_, 0, 1):-!. 4444bdd_list_raise(L, N, X):- N0 is N-1, 4445 bdd_list_raise(L, N0, X0), 4446 bdd_map_insert(L, X0, X). 4447% 4448bdd_map_insert([], _, 0). 4449bdd_map_insert([A|As], X, Y):- 4450 bdd_insert(A, X, X0), 4451 bdd_map_insert(As, X, Y0), 4452 zdd_join(X0, Y0, Y). 4453 4454% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert, 4455% also work for bddered zdd. 4456 4457% ?- zdd X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U), 4458% psa(X), psa(Y), psa(Z), psa(U). 4459% ?- zdd X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z), 4460% psa(Z, S), card(Z, C). 4461% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4462% card(Z, C). 4463% ?- zdd {numlist(1, 10, Ns)}, X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z), 4464% card(Z, C), card(X, D). 4465 4466bdd_merge(0, _, 0):-!. 4467bdd_merge(_, 0, 0):-!. 4468bdd_merge(1, X, X):-!. 4469bdd_merge(X, 1, X):-!. 4470bdd_merge(X, Y, Z):- memo(bdd_merge(X, Y)-Z), 4471 ( nonvar(Z) -> true % , write(.) % So so frequently hits. 4472 ; cofact(X, t(A, L, R)), 4473 bdd_merge(L, Y, L0), 4474 bdd_merge(R, Y, R1), 4475 bdd_cons(R0, A, R1), 4476 zdd_join(L0, R0, Z) 4477 ). 4478 4479 /**************n*************************** 4480 * Interleave bddered atoms in BDD * 4481 ******************************************/
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.4490% ?- X<< +[*[a,b], *[x,y]], Y<< +[*[1]], 4491% bdd_interleave(X, Y, Z), psa(Z). 4492% ?- zdd X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z). 4493% ?- zdd X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z). 4494 4495bdd_interleave(0, _, 0):-!. 4496bdd_interleave(_, 0, 0):-!. 4497bdd_interleave(1, X, X):-!. 4498bdd_interleave(X, 1, X):-!. 4499bdd_interleave(X, Y, Z):- % memo is useless here. 4500 cofact(Y, t(B, L, R)), 4501 ( L < 2 -> L0 = 0 4502 ; bdd_interleave(X, L, L0) 4503 ), 4504 bdd_interleave(X, B, R, R0), 4505 zdd_join(L0, R0, Z). 4506% 4507bdd_interleave(0, _, _, 0):-!. 4508bdd_interleave(1, B, Y, Z):-!, cofact(Z, t(B, 0, Y)). 4509bdd_interleave(X, B, Y, Z):- memo(merge(X, Y, B)-Z), 4510 ( nonvar(Z) -> true % , write(+) % many hits. 4511 ; cofact(X, t(A, L, R)), 4512 ( L < 2 -> L0 = 0 4513 ; bdd_interleave(L, B, Y, L0) 4514 ), 4515 bdd_interleave(A, R, B, Y, R0), 4516 zdd_join(L0, R0, Z) 4517 ). 4518% 4519bdd_interleave(A, X, B, Y, Z):- % memo is useless here. 4520 bdd_interleave(X, B, Y, U), 4521 cofact(Z0, t(A, 0, U)), 4522 bdd_interleave(Y, A, X, V), 4523 cofact(Z1, t(B, 0, V)), 4524 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.4533% ?- zdd bdd_funs(mono([1,2]-[a,b])*mono([3,4]-[c,d]), X), psa(X). 4534% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), psa(X). 4535% ?- zdd bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), 4536% zdd_normalize(X, Y), psa(Y). 4537 4538bdd_funs(A*B, F):-!, bdd_funs(A, A0), 4539 bdd_funs(B, B0), 4540 bdd_merge(A0, B0, F). 4541bdd_funs(A&B, F):-!, bdd_funs(A, A0), 4542 bdd_funs(B, B0), 4543 bdd_interleave(A0, B0, F). 4544bdd_funs(A, F):- fun_block(A, F). 4545 4546 /************** 4547 * misc * 4548 **************/
4553% ?- numlist(1, 100, Ns), (zdd X<<pow(Ns), zdd_flatten(X, Y), psa(Y)). 4554zdd_flatten(X, 0):- X<2, !. 4555zdd_flatten(X, Y):- memo(flatten(X)-Y), 4556 ( nonvar(Y) -> true % Many hits. 4557 ; cofact(X, t(A, L, R)), 4558 zdd_flatten(L, L0), 4559 zdd_flatten(R, R0), 4560 zdd_join(L0, R0, Y0), 4561 cofact(Y, t(A, Y0, 1)) 4562 )