1:- module(zmod, 2 [ (<<)/2, zdd/0, zdd_eval/2, zdd_eval/3, ltr/0 3 , ltr_join/3, ltr_join_list/2, ltr_join_list/3 4 , ltr_merge/3, card/2, ltr_card/2 5 , card_filter_gte/3, card_filter_lte/3 6 , card_filter_between/4 7 , max_length/2 8 , sat/0, sat/1, sat_count/1 9 , set_at/2 10 , obj_id/2 11 , dnf/2, cnf/2, nnf_dnf/2, nnf_cnf/2 12 , all_fun/3 13 , all_mono/3, all_epi/3, merge_funs/2 14 , bdd_list/2, bdd_list_raise/3, bdd_append/3, bdd_interleave/3 15 , zdd_div_by_list/3 16 , opp_compare/3 17 , bdd_sort_append/3, bdd_append/3 18 , zdd_insert/3, zdd_insert/4, zdd_insert_atoms/3 19 , bdd_cons/3 20 , l_cons/3 21 , zdd_insert_atoms/3 22 , zdd_ord_insert/3, zdd_reorder/3 23 , zdd_has_1/1 24 , zdd_memberchk/2 25 , zdd_family/2 26 , zdd_subfamily/2 27 , zdd_join/3, zdd_join_1/2, zdd_join_list/2, zdd_singleton/2 28 , zdd_merge/3, zdd_disjoint_merge/3 29 , zdd_merge_list/3 30 , zdd_meet/3 31 , zdd_subtr/3, zdd_subtr_1/2, zdd_xor/3 32 , zdd_div/3, zdd_mod/3, zdd_divmod/4, zdd_div_div/4 33 , zdd_divisible_by_list/3 34 , zdd_power/2, zdd_ord_power/3 35 , zdd_rand_path/1, zdd_rand_path/2, zdd_rand_path/3 36 , ltr_meet_filter/3, ltr_join_filter/3 37 , get_key/2, atom_index/1 38 , set_key/2, update_key/3 39 , set_pred/2, zdd_compare/3 40 , zdd_sort/2 41 , open_key/2, close_key/1 42 , set_compare/1, get_compare/1 43 , map_zdd/3, zdd_find/3 44 , psa/0, psa/1, psa/2, mp/2 45 , sets/2, ppoly/1, poly_term/2 46 , eqns/2 47 , zdd_list/2 48 , significant_length/3 49 , charlist/2, charlist/3, atomlist/2 50 , op(900, xfx, <<) 51 ]). 52 53% ?- zdd. 54% ?- N = 10000, numlist(1, N, Ns), time(((X<<pow(Ns), card(X, _C)))), _C=:=2^N. 55% :- doc_server(7000). 56% :- use_module(library(pldoc/doc_library)). 57% :- doc_load_library. 58% :- doc_browser. 59 60:- use_module(library(apply)). 61:- use_module(library(apply_macros)). 62:- use_module(library(clpfd)). 63:- use_module(library(statistics)). 64:- use_module(zdd('zdd-array')). 65:- use_module(util(math)). 66:- use_module(util(meta2)). 67:- use_module(pac(basic)). 68:- use_module(pac(meta)). 69:- use_module(util(misc)). 70:- use_module(pac('expand-pac')). % For the kind block. 71:- use_module(pac(op)). 72:- use_module(zdd('frontier-vector')). 73:- use_module(zdd(zsat)). 74 75:- set_prolog_flag(stack_limit, 10_200_147_483_648). 76:- nb_setval(default_zdd_mode, zdd). 77 78% :- initialization(activate_zdd). % choices: zdd/ltr/sat 79activate_zdd:- b_getval(default_zdd_mode, Mode), 80 call(Mode), 81 format( 82 "\n%\s~w mode activated. 83%\sCurrently available modes: zdd/ltr/sat\n", [Mode]). 84 85attr_unify_hook(V, Y):- 86 ( get_attr(Y, zdd, A) 87 -> zdd_unify(V, A) 88 ; zdd_unify(V, Y) 89 ). 90 91 :- op(800, xfy, &). 92 :- op(820, fy, \). % NOT 93 :- op(830, xfy, /\). % AND 94 :- op(840, xfy, \/). % OR 95 :- op(860, xfy, ~). % equivalence 96 :- op(860, xfy, #). % exor 97 :- op(860, xfy, <->). % equivalence 98 :- op(860, xfy, <=> ). % equivalence 99 :- op(870, yfx, <-). 100 101% for pac query. 102term_expansion --> pac:expand_pac. 103 104% ?- zdd. 105% ?- numlist(1, 2, Ns), Y<<pow(Ns), card(Y, C). 106% ?- set_memo(a-1), set_memo(a-2), memo(a-V). 107% ?- X<<{[1,1]}, psa(X). 108% ?- X<< *[ *a, *a, *b,*c], psa(X). 109% ?- set_key(root, hello), get_key(root, R). 110% ?- all_fun([a],[b], F), psa(F). 111% ?- all_fun([],[b], F), psa(F). 112% ?- all_fun([a],[], F), psa(F). 113% ?- all_fun([a,b],[c,d], F), psa(F), card(F, C). 114% ?- N = 20, numlist(1, N, A), raise_list(A, 2, A2), all_fun(A2, A, F), card(F, C). 115% ?- time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 116% all_fun(Ns, Ms, F), card(F, C))). 117 118% Cardinality # of Y^X = { f | f: X-> Y }. 119% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 120 121% ?- I=1, J=1, K=1, L=1, 122% numlist(1, I, X), numlist(1, K, Y), 123% raise_list(X, J, Xj), 124% raise_list(Y, L, Yl), 125% time(call_with_time_limit(200, (all_fun(Xj, Yl, F), card(F, C)))), 126% C =:= (K^L)^(I^J), 127% significant_length(C, Keta, 10). 128 129% ?- I=3, J=5, K=3, L=5, 130% numlist(1, I, X), numlist(1, K, Y), 131% raise_list(X, J, Xj), 132% raise_list(Y, L, Yl), 133% time( ( call_with_time_limit(200, ( 134% (all_fun(Xj, Yl, F), card(F, C)))))), 135% C =:= (K^L)^(I^J), 136% significant_length(C, Keta, 10). 137%@ % 477,828,435 inferences, 56.259 CPU in 58.472 seconds (96% CPU, 8493400 Lips) 138%@ F = 7204222, 139%@ Keta = 580. 140 141% ?- significant_length(020, X, 10). 142significant_length(0, 0, _):-!. 143significant_length(X, 1, Radix):- X < Radix, !. 144significant_length(X, L, Radix):- Y is X // Radix, 145 significant_length(Y, L0, Radix), 146 L is L0+1. 147 148% 149zdd_atom(X):- get_key(is_atom, Pred), !, call(Pred, X). 150zdd_atom(X):- (atomic(X); dvar(X)), !.
obj_id([a,b,c], Id), obj_id(Obj, Id).155obj_id(X, Id):- cofact(Id, t(X, 0, 1)). 156% 157hyphen(X, Y, X-Y). 158comma(X, Y, (X,Y)). 159equality(X, Y, (X=Y)). 160dvar('$VAR'(_)). 161 162 /***************************************** 163 * all_fun/all_mono/all_epi in ZDD * 164 *****************************************/
168% ?- all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F). 169% ?- all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C). 170% ?- N = 100, numlist(1, N, Ns), all_fun(Ns, Ns, F)^, card(F, C). 171% ?- numlist(1, 5, Ns), numlist(6, 10, Ms), 172% all_fun(Ns, Ns, F), 173% all_fun(Ms, Ms, G), 174% zdd_merge(F, G, H), 175% card(H, C), 176% C =:= 5^5 * 5^5. 177 178all_fun(D, R, F):- zdd_sort(D, D0), 179 zdd_sort(R, R0), 180 length(D0, I), 181 length(R0, J), 182 ( I > 0, J = 0 -> F = 0 183 ; bdd_sort_append(D0, 1, D1), 184 findall_fun(D1, R0, F) 185 ). 186% 187findall_fun(X, _, X):- X < 2, !. 188findall_fun(X, Rng, Y):- memo(findall_fun(X)-Y), 189 ( nonvar(Y) -> true % , write(.) % many hits. 190 ; cofact(X, t(A, L, R)), 191 findall_fun(L, Rng, L0), 192 findall_fun(R, Rng, R1), 193 join_for_alt_val(A, Rng, R1, 0, R0), 194 zdd_join(L0, R0, Y) 195 ). 196% 197join_for_alt_val(_, [], _, V, V). 198join_for_alt_val(A, [B|Bs], F, F0, F1):- 199 bdd_cons(F2, A-B, F), 200 zdd_join(F0, F2, F3), 201 join_for_alt_val(A, Bs, F, F3, F1).
206% ?- all_mono([1],[a], Is), psa(Is). 207% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 208% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 209% ?- all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C). 210% ?- all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C). 211% ?- time((numlist(1, 10, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(10, C))). 212% ?- time((numlist(1, 12, Ns), all_mono(Ns, Ns, F), card(F, C))). 213% ?- N =10, numlist(1, N, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(N, C). 214 215all_mono(D, R, F):- zdd_sort(D, D0), 216 zdd_sort(R, R0), 217 length(D0, I), 218 length(R0, J), 219 ( I @=< J -> 220 bdd_sort_append(D0, 1, D1), 221 findall_mono(D1, R0, F) 222 ; F = 0 223 ). 224 225% ?- bdd_sort_append([], 1, X), findall_mono(X, [a], Y). 226% ?- bdd_sort_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y). 227% ?- N=14, numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 228% findall_mono(X, Ns, Y), card(Y, C), 229% factorial(14, D), ( D=:=C -> writeln("*** OK ***")). 230 231findall_mono(X, _, X):- X < 2, !. 232findall_mono(X, Rng, Y):- memo(findall_mono(X,Rng)-Y), 233 ( nonvar(Y) -> true % , write(.) % many hits. 234 ; cofact(X, t(A, L, R)), 235 findall_mono(L, Rng, L0), 236 findall_mono(A, R, Rng, R0), 237 zdd_join(L0, R0, Y) 238 ). 239% 240findall_mono(A, R, Rng, R0):- findall(B-U, select(B, Rng, U), Cases), 241 findall_mono(Cases, A, R, 0, R0). 242% 243findall_mono([], _A, _R, V, V). 244findall_mono([B-Rng|Cases], A, R, U, V):- 245 findall_mono(R, Rng, U0), 246 cofact(U1, t(A-B, 0, U0)), 247 zdd_join(U, U1, U2), 248 findall_mono(Cases, A, R, U2, V).
254% ?- all_epi([],[], F). 255% ?- all_epi([a],[1], F), psa(F). 256% ?- all_epi([a,b],[1], F), psa(F). 257% ?- all_epi([a],[1,2], F), psa(F). 258% ?- all_epi([a,b,c],[1,2], F), psa(F). 259% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (all_epi(Ns, Ms, F)). 260% ?- time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (all_epi(Ns, Ms, F)))). 261 262all_epi(D, R, F):- 263 zdd_sort(D, D0), 264 zdd_sort(R, R0), 265 length(D0, I), length(R0, J), 266 ( I @>= J -> 267 bdd_sort_append(D0, 1, D1), 268 findall_epi(D1, R0-R0, F) 269 ; F = 0 270 ).
numlist(1, N, Ns), (all_perm(Ns, X), card(X, C), psa(X)).
?- N=3, numlist(1, N, Ns), (all_perm(Ns, X), card(X, C), psa(X)).
?- N=10, numlist(1, N, Ns), (all_perm(Ns, X), card(X, C)).
?- N=11, numlist(1, N, Ns), (all_perm(Ns, X), card(X, C)).
?- N=14, time((numlist(1, N, Ns), ( all_perm(Ns, X), card(X, C)))).
?- N=15, time((numlist(1, N, Ns), ( all_perm(Ns, X), card(X, C)))).
?- N=16, time((numlist(1, N, Ns), ( all_perm(Ns, X), card(X, C)))).
@ % 245,856,272 inferences, 173.924 CPU in 179.904 seconds (97% CPU, 1413587 Lips)
@ N = 16,
@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
@ X = 2490369,
@ C = 20922789888000.
@ % 185,729,299 inferences, 205.838 CPU in 207.237 seconds (99% CPU, 902308 Lips)
?- factorial(16, X).290% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R), 291% length(R, L). 292 293all_perm(D, P):- zdd_sort(D, D0), 294 findall_perm(D0, P). 295% 296findall_perm([], 1):-!. 297findall_perm(D, X):- memo(perm(D)-X), 298 ( nonvar(X) -> true % , write(.) % many hits. 299 ; 300 findall(I-D0, select(I, D, D0), U), 301 join_perm_for_selection(U, 0, X)). 302% 303join_perm_for_selection([], X, X). 304join_perm_for_selection([I-D|U], X, Y):- 305 findall_perm(D, X0), 306 bdd_cons(X1, I, X0), 307 zdd_join(X1, X, X2), 308 join_perm_for_selection(U, X2, Y). 309 310 /************************************************* 311 * terms in based on families of lists * 312 *************************************************/
320% ?- coalgebra_for_signature([x], [f/1], [x], E), psa(E). 321% ?- coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E). 322% ?- time((coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2], 323% [x,y,z,u,v,0,1], E), card(E, C))). 324%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips) 325%@ E = 173825, 326%@ C = 68641485507. 327 328coalgebra_for_signature(D, Sgn, As, E):- 329 signature(Sgn, As, T), 330 signature_map(D, T, E). 331% 332signature_map([], _, 1):-!. 333signature_map([X|Xs], T, E):- 334 signature_map(Xs, T, E0), 335 extend_signature_map(X, T, E0, E). 336% 337extend_signature_map(_, 0, _, 0):-!. 338extend_signature_map(_, 1, E, E):-!. 339extend_signature_map(X, T, E, F):- cofact(T, t(A, L, _)), 340 extend_signature_map(X, L, E, E0), 341 l_cons(X->A, E, E1), 342 zdd_join(E0, E1, F).
347% ?- term_path(a, R), psa(R), term_path(A, R). 348term_path(X, Y):- 349 ( nonvar(X) -> term_to_path(X, Y) 350 ; path_to_term(Y, X) 351 ).
356% ?- term_to_path(a, R), psa(R). 357% ?- term_to_path(f(a, b), R), psa(R). 358% ?- term_to_path(f(g(a, b), h(c, d)), R), psa(R). 359% ?- term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R). 360term_to_path(X, Y):- functor(X, F, N), 361 ( N = 0 -> zdd_singleton(X, Y) 362 ; functor(X, F, N), 363 arg_path(F/N, 1, X, Y) 364 ). 365% 366arg_path(_/N, J, _, 0):- J>N, !. 367arg_path(F, I, X, Y):- J is I + 1, 368 arg(I, X, A), 369 term_to_path(A, U), 370 arg_path(F, J, X, V), 371 cofact(Y, t(arg(F, I), V, U)).
377% ?- term_to_path(a, X), path_to_term(X, R). 378% ?- term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R). 379% ?- term_to_path(f(1,2), X), path_to_term(X, R). 380% ?- T=f(h(a), 3, g(b,2), 5), 381% (term_to_path(T, X), path_to_term(X, R)), T = R. 382 383path_to_term(X, Y):- X>1, cofact(X, t(A, L, R)), 384 ( R = 1 -> Y = A 385 ; A = arg(F/_, _), 386 path_to_term(R, R0), 387 path_to_term(L, L0, []), 388 Y =..[F, R0|L0] 389 ). 390% 391path_to_term(X, U, U):- X<2, !. 392path_to_term(X, [R0|U], V):- cofact(X, t(_, L, R)), 393 path_to_term(R, R0), 394 path_to_term(L, U, V).
compare(C, U, V) is performed.401% ?- X=f(a,b), Y=f(a,b, c), (term_path(X, T), term_path(Y, U), 402% term_path_compare(C0, T, U)), compare(C, X, Y). 403% ?- X=g(a,b), Y=f(a,b, c), (term_path(X, T), term_path(Y, U), 404% term_path_compare(C0, T, U)), compare(C, X, Y). 405% ?- X=g(a,b,c), Y=f(a,b), (term_path(X, T), term_path(Y, U), 406% term_path_compare(C0, T, U)), compare(C, X, Y). 407 408term_path_compare(=, X, X):-!. 409term_path_compare(<, 0, _):-!. 410term_path_compare(>, _, 0):-!. 411term_path_compare(<, 1, _):-!. 412term_path_compare(>, _, 1):-!. 413term_path_compare(C, X, Y):- cofact(X, t(A, L, R)), 414 cofact(Y, t(B, L0, R0)), 415 arity_compare(C0, A, B), 416 ( C0 = (=) -> 417 term_path_compare(C1, R, R0), 418 ( C1 = (=) -> 419 left_branch_compare(C, L, L0) 420 ; C = C0 421 ) 422 ; C = C0 423 ). 424 425% Left branches are for argument lists of the name length. 426left_branch_compare(=, 0, 0):-!. 427left_branch_compare(C, X, Y):- 428 cofact(X, t(_, L, R)), 429 cofact(Y, t(_, L0, R0)), 430 term_path_compare(C0, R, R0), 431 ( C0 = (=) -> 432 left_branch_compare(C, L, L0) 433 ; C = C0 434 ). 435 436% 437arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G). 438arity_compare(C, A, B):-!, compare(C, A, B).
444% ?- zdd_lift(1, X). 445% ?- X<< pow([1,2]), zdd_lift(X, Y), card(Y, D), psa(Y). 446% ?- X<< pow(numlist(1,10)), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D). 447% ?- N=16, numlist(1, N, Ns), 448% time((X<< pow(Ns), zdd_lift(X, Y), card(Y, D))), D=:=2^N. 449%@ % 19,643,341 inferences, 31.553 CPU in 31.694 seconds (100% CPU, 622559 Lips) 450 451zdd_lift(X, X):- X<2, !. 452zdd_lift(X, Y):- memo(zdd_lift(X)-Y), 453 ( nonvar(Y) -> true %, write(.) % So so hits. 454 ; cofact(X, t(A, L, R)), 455 zdd_lift(L, L0), 456 zdd_lift(R, R0), 457 zdd_lift(A, R0, R1), 458 zdd_join(L0, R1, Y) 459 ). 460% 461zdd_lift(_, 0, 0):-!. 462zdd_lift(A, 1, Y):-!, zdd_singleton([A], Y). 463zdd_lift(A, X, Y):- cofact(X, t(B, L, _)), 464 zdd_singleton([A|B], R0), 465 zdd_lift(A, L, L0), 466 zdd_join(L0, R0, Y).
472% ?- X<< pow([a,b]), card(X, C), zdd_univ(X, Y), psa(Y). 473% ?- X<< pow([a,b]), zdd_univ(X, Y), psa(Y). 474 475zdd_univ(X, X):- X<2, !. 476zdd_univ(X, Y):- cofact(X, t(A, L, R)), 477 zdd_univ(R, [A], R0), 478 zdd_univ(L, L0), 479 zdd_join(L0, R0, Y). 480 481% ?- X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 482% ?- X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 483 484zdd_univ(0, _, 0):-!. 485zdd_univ(1, Stack, X):-!, reverse(Stack, Stack0), 486 U =.. Stack0, 487 zdd_singleton(U, X). 488zdd_univ(X, Stack, Y):- cofact(X, t(A, L, R)), 489 zdd_univ(L, Stack, L0), 490 zdd_univ(R, [A|Stack], R0), 491 zdd_join(L0, R0, Y).
g(a1, ..., an)
where G=g/n and ai in As.497% ?- arity_term(f/2, [1, x, y], T), psa(T). 498arity_term(F/N, As, T):- memo((F/N)-T), 499 ( nonvar(T) -> true 500 ; all_list(N, As, X), 501 l_cons(F, X, T0), 502 zdd_univ(T0, [], T) 503 ).
511% ?- N=10, numlist(1, N, Ns), 512% time((X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))). 513% ?- X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y). 514% ?- N=100, numlist(1, N, Ns), 515% time((X<<pow(Ns), l_cons(f, X, Y), card(Y, C))). 516% ?- N=10, numlist(1, N, Ns), 517% time((X<<pow(Ns), zdd_mul_list([f, g, h], X, Y), card(Y, C))). 518 519zdd_functor(F, X, Y):- zdd_functor(F, X, [], Y). 520% 521zdd_functor(_, 0, _, 0):-!. 522zdd_functor(F, 1, St, Y):-!, T =..[F|St], 523 zdd_singleton(T, Y). 524zdd_functor(F, X, St, Y):-cofact(X, t(A, L, R)), 525 zdd_functor(F, L, St, Y0), 526 zdd_functor(F, R, [A|St], Y1), 527 zdd_join(Y0, Y1, Y).
f(a1, ..., an)
with f/n in G and ai in As.533% ?- signature([f/1, g/2], [1, x, y], U), psa(U). 534% ?- time((signature([f/2, g/2, h/3, i/4, k/5], 535% [0, 1, 2, x, y, z, u, v, w], U), card(U, C))). 536 537signature([], _, 0):-!. 538signature([G|Gs], As, T):- 539 arity_term(G, As, T0), 540 signature(Gs, As, T1), 541 zdd_join(T0, T1, T).
547% ?- spy(power_list). 548% ?- power_list(0, [a,b], P). 549% ?- power_list(1, [a,b], P). 550% ?- N = 100, numlist(1, N, _Ns), 551% time(((power_list(N, _Ns, X), card(X, _Count)))), 552% _Count > 100^100, writeln(_Count). 553%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips) 554%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101 555%@ N = 100, 556%@ X = 515002. 557 558power_list(N, As, P):- obj_id(As, Id), 559 power_list_with_id(N, Id, P). 560% 561power_list_with_id(0, Id, 1):-!, memo(power_list(0, Id)-1). 562power_list_with_id(N, Id, Y):- 563 N0 is N - 1, 564 power_list_with_id(N0, Id, Y0), 565 all_list_with_id(N, Id, Y1), 566 zdd_join(Y0, Y1, Y).
572% ?- all_list(0, [a], X), psa(X). 573% ?- all_list(1, [a], X), psa(X). 574% ?- N=10, numlist(1, N, Ns), (all_list(4, Ns, X), card(X, C)). 575% ?- N=100, numlist(1, N, Ns), time(((all_list(100, Ns, X), card(X, C)))). 576%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips) 577 578all_list(N, As, Y):- obj_id(As, Id), 579 all_list_with_id(N, Id, Y). 580% 581all_list_with_id(0, Id, 1):-!, memo(all_list(0, Id)-1). 582all_list_with_id(N, Id, Y):- memo(all_list(N, Id)-Y), 583 ( nonvar(Y) -> true 584 ; N0 is N-1, 585 all_list_with_id(N0, Id, Y0), 586 obj_id(As, Id), 587 zdd_mul_list(As, Y0, 0, Y) 588 ).
593singleton_family([], 0):-!. 594singleton_family([A|As], X):- 595 singleton_family(As, X0), 596 zdd_singleton(A, U), 597 zdd_join(U, X0, X).
602distribute_con(F, X, Y):- zdd_mul_list(F, X, 0, Y). 603% 604zdd_mul_list([], _, Y, Y). 605zdd_mul_list([A|As], Y, U, V):- 606 l_cons(A, Y, V0), 607 zdd_join(U, V0, U0), 608 zdd_mul_list(As, Y, U0, V).
613% ?- X<<pow([1,2]), l_cons(a, X, Y), psa(Y). 614 615l_cons(A, Y, U):- cofact(U, t(A, 0, Y)).
append(L, U, M) with U in X.
?- X<<pow([1,2]), l_append([a,b], X, Y), psa(Y).622l_append([], X, X). 623l_append([A|As], X, Y):- 624 l_append(As, X, X0), 625 l_cons(A, X0, Y). 626 627% ?- bdd_sort_append([], 1, X), findall_epi(X, [a]-[a], Y). 628% ?- bdd_sort_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 629% ?- bdd_sort_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 630% ?- bdd_sort_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C). 631% ?- bdd_sort_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y). 632% ?- N = 2, (numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 633% ?- N = 3, (numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 634% ?- N = 10,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 635% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 636% ?- N = 11,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 637% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 638% ?- N = 12,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 639% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 640% ?- N = 13,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 641% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 642 643select_target(Range, U, B, V):- member(B, Range), 644 ( select(B, U, V) -> true 645 ; V = U 646 ). 647 648% 649findall_epi(0, _, 0):-!. 650findall_epi(1, _-U, X):-!, 651 ( U=[] -> X = 1 652 ; X = 0 653 ). 654findall_epi(X, RngU, Y):- memo(findall_epi(X, RngU)-Y), 655 ( nonvar(Y) -> true % , write(.) % many hits. 656 ; cofact(X, t(A, L, R)), 657 findall_epi(L, RngU, L0), 658 findall_epi(A, R, RngU, R0), 659 zdd_join(L0, R0, Y) 660 ). 661% 662findall_epi(A, R, Rng-U, R0):- 663 findall(B-(Rng-V), select_target(Rng, U, B, V), Cases), 664 findall_epi(Cases, A, R, 0, R0). 665% 666findall_epi([], _, _, V, V). 667findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V):- 668 findall_epi(R, Rng-Rng0, U0), 669 cofact(U1, t(A-B, 0, U0)), 670 zdd_join(U, U1, U2), 671 findall_epi(Cases, A, R, U2, V). 672 673% ?- merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X). 674merge_funs(Fs, X):- fold_merge_funs(Fs, 1, X). 675% 676fold_merge_funs([], X, X). 677fold_merge_funs([G|Fs], X, Y):- 678 fun_block(G, X0), 679 zdd_merge(X, X0, X1), 680 fold_merge_funs(Fs, X1, Y). 681% 682fun_block(G, X):- 683 ( G = mono(D-R) -> all_mono(D, R, X) 684 ; G = epi(D-R) -> all_epi(D, R, X) 685 ; G = fun(D-R), 686 all_fun(D, R, X) 687 ). 688 689% ?- N=2, numlist(1, N, Ns), 690% ( set_compare(opp_compare), 691% X<<pow(Ns), psa(X), set_compare(compare), 692% zdd_normalize(X, Y), psa(Y)). 693 694zdd_normalize(X, X):- X<2, !. 695zdd_normalize(X, Y):- memo(normalize(X)-Y), 696 ( nonvar(Y) -> true % , write(.) % Many hits. 697 ; cofact(X, t(A, L, R)), 698 zdd_normalize(L, L0), 699 zdd_normalize(R, R1), 700 zdd_insert(A, R1, R0), 701 zdd_join(L0, R0, Y) 702 ). 703 704% ?- N = 1000, numlist(1, N, Ns), 705% time((X<<pow(Ns), rank_family_by_card(X, P), card(P, C))). 706 707% ?- N = 1000, numlist(1, N, Ns), 708% time((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C))). 709 710% ?- N = 1000, numlist(1, N, Ns), 711% time((( X<<pow(Ns), 712% get_family_of_rank(500, X, Y), 713% card(Y, C)))).
718get_family_of_rank(Order, X, F):- rank_family_by_card(X, _), 719 memo(family_with_card(Order)-F). 720 721% ?- X<<pow([1]). 722% ?- X<<set([a]), rank_family_by_card(X, P), 723% memo(family_with_card(0)-L), sets(L, Sl), 724% memo(family_with_card(1)-M), sets(M, Sm).
730rank_family_by_card(0, 0):-!. 731rank_family_by_card(1, 0):-!, memo(family_with_card(0)-1). 732rank_family_by_card(I, P):- memo(rank_family_by_card_done(I)-B), 733 ( nonvar(B) -> true 734 ; cofact(I, t(A, L, R)), 735 rank_family_by_card(L, Pl), 736 rank_family_by_card(R, Pr), 737 max(Pl, Pr, P0), 738 insert_one_to_family(A, P0, New), 739 P is P0 + 1, 740 memo(family_with_card(P)-New), 741 B = true 742 ). 743% 744insert_one_to_family(A, 0, G):-!, memo(family_with_card(0)-F), 745 zdd_insert(A, F, G). 746insert_one_to_family(A, P, G):- P0 is P-1, 747 insert_one_to_family(A, P0, G0), 748 memo(family_with_card(P)-Fp), 749 zdd_insert(A, Fp, G), 750 zdd_join(Fp, G0, Gp), 751 set_memo(family_with_card(P)-Gp). 752 753 /********************** 754 * State access * 755 **********************/ 756 757get_extra(Extra):- b_getval(zdd_extra, Extra). 758% 759set_extra(Extra):- b_setval(zdd_extra, Extra). 760 761% ?- bump_up(a, N), bump_up(a, K). 762bump_up(Key):- b_getval(zdd_extra, Extra), 763 ( select(Key-N0, Extra, Extra0) -> true 764 ; N0 = 0, 765 Extra0 = Extra 766 ), 767 N is N0 + 1, 768 b_setval(zdd_extra, [Key-N|Extra0]). 769 770 771:- meta_predicate set_compare(). 772set_compare(Compare):- nb_setval(zdd_compare, Compare). 773 774% ?- zdd_compare(C, a, b). 775get_compare(Compare):- b_getval(zdd_compare, Compare). 776% 777zdd_compare(C, X, Y):- get_compare(F), call(F, C, X, Y). 778 779% ?- zdd_sort([1->1, 1->2, 1-1, 2-2], X). 780zdd_sort(X, Y):- get_compare(Comp), predsort(Comp, X, Y). 781 782% ?- get_key(a, V), set_key(a, 1), get_key(a, W). % fail. 783% ?- set_key(a, 1), get_key(a, W). 784get_key(K, V):- b_getval(zdd_extra, Assoc), 785 memberchk(K-V, Assoc). 786% 787set_key(K, V) :- b_getval(zdd_extra, Assoc), 788 ( select(K-_, Assoc, Assoc0) 789 -> b_setval(zdd_extra, [K-V|Assoc0]) % nb_linkval not work. 790 ; b_setval(zdd_extra, [K-V|Assoc]) % nb_linkval not work. 791 ). 792% 793nb_set_key(K, V) :- b_getval(zdd_extra, Assoc), 794 ( select(K-_, Assoc, Assoc0) 795 -> nb_setval(zdd_extra, [K-V|Assoc0]) 796 ; nb_setval(zdd_extra, [K-V|Assoc]) 797 ). 798 799:- meta_predicate set_pred(, ). 800set_pred(K, V) :- set_key(K, V). 801 802% ?- open_key(a, []), update_key(a, X, Y), X=[1|Y], 803% get_key(a, Z), close_key(a). 804 805% ?- zdd. 806% ?- ((open_key(a, []), update_key(a, X, Y), X=[1|Y], 807% get_key(a, Z), close_key(a), get_key(a, U))). % false 808 809% 810open_key(K, Val):- set_key(K, Val). 811% 812update_key(X, Old, New):- b_getval(zdd_extra, Assoc), 813 select(X-Old, Assoc, Assoc0), 814 b_setval(zdd_extra, [X-New|Assoc0]). 815% 816close_key(Key):- b_getval(zdd_extra, Assoc), 817 ( select(Key-_, Assoc, Assoc0) -> 818 b_setval(zdd_extra, Assoc0) 819 ; true 820 ). 821 822% ?- varnum(D), varnum(E).
827varnum(D):- get_key(varnum, D). 828 829% ?- sort([1->1, 1->2, 1-1, 2-2], X). 830% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X). 831% ?- zdd_sort_rev([1,2,3], X). 832 833compare_rev(Comp, C, A, B):- call(Comp, C, B, A). 834% 835zdd_sort_rev(X, Y):- get_compare(Comp), 836 predsort(compare_rev(Comp), X, Y). 837 838% ?- pred_zdd(opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)). 839:- meta_predicate pred_zdd(, ). 840pred_zdd(Comp, X):- set_compare(Comp), call(X). 841 842% ?- X<<pow([a,b,c]), zdd_memberchk([a,c], X). 843% ?- X<<pow([a,b,c]). 844 845% ?- zdd, ((X<<pow([a,b,c]), zdd_memberchk([], X))). 846% ?- zdd, ((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
851zdd_memberchk(L, Z):- zdd_sort(L, L0), zdd_ord_memberchk(L0, Z). 852% 853zdd_ord_memberchk([], Z):- !, zdd_has_1(Z). 854zdd_ord_memberchk([A|As], Z):- Z>1, 855 cofact(Z, t(B, L, R)), 856 ( A == B 857 -> zdd_ord_memberchk(As, R) 858 ; A @> B, 859 zdd_ord_memberchk([A|As], L) 860 ). 861 862% PASS 863% ?- X<<pow([a,b]), card(X, C). 864% ?- ((X<<(pow([a,b])-pow([a])), card(X, C))). 865% ?- X=1, Y =2, Z is X + Y. 866% ?- X<<set([a]), sets(X, U). 867% ?- ((X<<pow([a,b]), S<<sets(X))). 868% ?- ((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 869% ?- (((X<< *(:append([a,b], [c,d]))), sets(X, Y))). 870% ?- ((X<<(*[a,b]& *[c,d]), S<<sets(X))). 871% ?- ((X<<{[a],[b],[c]}, sets(X,S))). 872% ?- ((X<<{[a],[b, c]}, sets(X,S))). 873% ?- ((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 874% ?- ((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 875% ?- I =1000, J =2000, 876% time( (zdd, 877% numlist(1, I, L), 878% numlist(1, J, M), 879% X << pow(L), 880% Y << pow(M), 881% Z << (Y - X), 882% card(Z, C), 883% C =:= 2^J-2^I )). 884 885 886% PASS 887% ?- ((X<<cnf(0), Y<<sets(X))). 888% ?- ((X<<cnf(1), Y<<sets(X))). 889% ?- ((X<<cnf(2), Y<<sets(X))). 890% ?- ((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 891% ?- ltr_((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 892% ?- (X<<cnf(a), Y<<sets(X))). 893% ?- ((X<<cnf(-a), Y<<sets(X))). 894% ?- ((X<<cnf(a+b), Y<<sets(X))). 895% ?- ((X<<cnf(-(a+b)), Y<<sets(X))). 896% ?- ((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 897% ?- ((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 898% ?- ((X<<cnf(-(-a + -b)), Y<<sets(X))). 899% ?- ((X<<dnf(a), Y<<sets(X), extern(Y, Y0))). 900% ?- ((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))). 901% ?- ((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))). 902% ?- ((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))). 903% ?- ((X<<dnf(a+b), Y<<sets(X))). 904% ?- ((X<<dnf(-(a+b)), Y<<sets(X))). 905% ?- ((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 906% ?- ((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 907% ?- ((X<<dnf(-(-a + -b)), Y<<sets(X))). 908% ?- ((X<<dnf((-a + a)), Y<<sets(X))). 909% ?- ((X<<dnf(-(-a + a)), Y<<sets(X))). 910% ?- (X << *(:append([a,b], [c,d]))). 911% ?- ((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))). 912% ?- ((X << *[a,b], sets(X, S))). 913% ?- ((X << +[a,b], sets(X, S))). 914% ?- ((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 915% ?- ((zdd_list_to_singletons([], X), prz(X))). 916% ?- ((zdd_list_to_singletons([a], X), prz(X))). 917% ?- ((zdd_list_to_singletons([a,b], X), prz(X))). 918% ?- ((zdd_list_to_singletons([c, a, b], X), prz(X))). 919% ?- X << *[a,b], psa(X). 920% ?- X << +[a,b], psa(X). 921 922% ?- I =1000, J is I + 1, numlist(1, I, L), 923% prepare_ltr_list(L, L0), 924% time((( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
932zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 933% 934zdd_list_to_singletons([], 1, _). 935zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 936 zdd_singleton(A, Y0, S), 937 zdd_join(Y0, Y, X, S). 938 939% PASS. 940% ?- ((zdd_partial_choices([], X), prz(X))). 941% ?- ((zdd_partial_choices([[a], [b]], X), prz(X))). 942% ?- ((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 943% ?- ((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 944% ?- ((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 945% ?- ((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 946% ?- ((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))). 947% ?- ((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 948% ?- ((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 949% ?- findall([I], between(1, 10000, I), Ls), 950% ((zdd_partial_choices(Ls, X), 951% card(X, C))), !, C =:= 2^10000.
956zdd_partial_choices([], 1):-!. 957zdd_partial_choices([L|Ls], X):- zdd_partial_choices(Ls, X0), 958 sw_fold_insert(zdd, L, X0, 0, X1), 959 zdd_join(X0, X1, X). 960 961:- meta_predicate zdd_find(, , ).
966% ?- X<< pow([a,b,c]), zdd_find(=(c), X, Y). 967% ?- X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y). 968% ?- X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y). 969 970zdd_find(F, X, Y):- X>1, 971 cofact(X, t(A, L, R)), 972 ( call(F, A), Y = A 973 ; zdd_find(F, L, Y) 974 ; zdd_find(F, R, Y) 975 ). 976 977use_table(G):- functor(G, F, N), 978 setup_call_cleanup( 979 table(F/N), % 980 G, 981 untable(F/N) % 982 ). 983 984 985 986% PASS. 987% 988% ?- P<<pow([1,2,3]), {X=1;X=2}, card(P,C). 989% ?- P<<pow([1,2,3]), card(P,C). 990% ?- P<<pow([1,2,3]), card(P,C). 991 992% ?- P << set([1,2,3,2,3]), psa(P). 993 994% ?- P << ({[1,2,3,2,3]} + {[4, 2,4]}), psa(P). 995 996% ?- X << :append([a,b], [c,d]). 997% ?- (X << :append([a,b], [c,d])). 998% ?- ((X << :append([a,b], [c,d]))). 999% ?- ((( X<<pow([1,2]), true, true))). 1000% ?- (X<<pow([1,2]), true, true, card(X, C)). 1001% ?- numlist(1, 100, Ns), (X<<pow(Ns), card(X, C)). 1002 1003 1004% ?- show_state. 1005% ?- fetch_state, X<<pow([a,b]), fetch_state, card(X, C). 1006% ?- X<<{[a],[b]}, Y<<{[b], [c]}, zdd_merge(X, Y, Z), psa(Z). 1007% ?- 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)).1016opp_compare(<, -(_,_), ->(_,_)):-!. 1017opp_compare(>, ->(_,_), -(_,_)):-!. 1018opp_compare(C, X, Y):- compare(C, Y, X). % reverse order 1019 1020% ?- X<< @(abc), psa(X). 1021% ?- 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.1038% ?- X<< +[ *[a,b], *[c, d]], psa(X). 1039% ?- <<(X, +[*[a,b], *[c,d]]), psa(X). 1040% ?- X<< card(pow([1,2]) + pow([a,b])). 1041% ?- X<< card(pow([1,2])). 1042 1043 1044:- meta_predicate <<(, ). 1045<<(X, E) :- zdd_eval(E, X).
--- 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.
--- 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,
1083% Pass. 1084% ?- X<<dnf(a*b), psa(X). 1085% ?- X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C). 1086% ?- X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))). 1087% ?- X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C). 1088 1089% Pass. 1090% ?- X<< @a. 1091% ?- X<< a, psa(X). 1092% ?- X<<pow([a,b]), card(X, C). 1093% ?- X<<pow([a,b])-pow([a]), card(X, C). 1094% ?- X<< set(:(append([1,2],[3,4]))), psa(X). 1095% ?- ((X<< +(:append([1,2],[3,4])), psa(X))). 1096% ?- ((X<< (@a + @b), psa(X))). 1097% ?- ((X<< ((@a + @b)* @c), psa(X))). 1098% ?- ((X<< [a,b])). 1099% ?- ((X<< set(:(append([a,b],[c,d]))), psa(X))). 1100% ?- ((X<< set(!append([a,b],[c,d])), psa(X))). % error 1101% ?- (X<< card(pow([a,b]))). 1102% ?- (X<< card(pow(:numlist(1, 100)))). 1103% ?- ((X<< set([1]), Y<< (X+X), psa(X))). 1104% ?- ((X<< set([1]), psa(X))). 1105% ?- ((X<< set([]))). 1106% ?- ((X << {[a], [b], [c]}, psa(X))). 1107% ?- ((X << {[a], [b], [c]}, card(X, C))). 1108 1109% PASS. 1110% ?- X << card(pow(append(numlist(1,3), numlist(4,5)))). 1111% ?- ((X << set(append(numlist(1,2), numlist(4,5))))). 1112% ?- ((X << set(append(numlist(1,10), numlist(11,20))))). 1113% ?- numlist(1,10,A), numlist(11,20, B), X<< pow(append(A, B)), 1114% card(X, C). 1115% ?- X << pow(numlist(1,2)), card(X, C). 1116% ?- X << pow(numlist(1,2)). 1117 1118% ?- ((X << pow(:(! charlist(a,z))), card(X, C))). 1119% ?- ((X << pow(:(! charlist(a-z))), card(X, C))). 1120% ?- ((X << pow([a,b]))). 1121% ?- ((X << *[a, b, c])). 1122% ?- ((X << (*[a, b, c] + *[a,b,c]), psa(X))). 1123% ?- ((X << (*[a, b, c] + *[2, 3]), psa(X))). 1124% ?- ((C << card(pow([a,b,c,1,2,3])))). 1125% ?- ((C << card(pow(:append([a,b,c], [1,2,3]))))). 1126% ?- ((C << pow(:numlist(1, 3)))). 1127% ?- ((C << @(a), psa(C))). 1128 1129% Pass. 1130% ?- ((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))). 1131% ?- ((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))). 1132% ?- ((U << +((append([a,b,c], [d,e,f]))), psa(U))). 1133% ?- ((U << *((append([a,b,c], [d,e,f]))), psa(U))). 1134% ?- ((U << +((append(append([a,b,c], [x,y,z]), [1, 2]))), psa(U))). 1135% ?- ((U << +[ *[a,b], *[c,d]], psa(U))). 1136% ?- ((U << *[ +[a,b], +[c,d]], psa(U))). 1137% ?- ((U << *[ *[a,b], *[c,d]], psa(U))). 1138% ?- ((U << *[ *[a,b], +[c,d]], psa(U))). 1139% ?- ((U << card(pow((append(append([a,b,c], [x,y,z]), [1,2,3])))))). 1140% ?- ((U << card(pow((append(append([a,b,c], [x,y,z]), [1,2,3])))))). 1141% ?- ((U << #(card(pow([a]))))). 1142% ?- ((U << succ((card(pow([a])))))). 1143% ?- ((U << card(pow([a])))). 1144% ?- U << card(pow([a])+pow([b])). 1145% ?- ((U << (=(3)))). 1146% ?- ((U << *([1,2,3]), psa(U))). 1147% ?- ((U << plus(card(pow([a,b])), card(pow([1,2]))))). 1148% ?- ((U << @a)). % singleton. 1149% ?- ((U << @2)). 1150% ?- ((U << [a,b])). 1151% ?- ((U << *[a,b], psa(U))). 1152% ?- ((U << +[a,b], psa(U))). 1153% ?- ((U << +[*[a,b], *[c,d]], psa(U))). 1154% ?- ((U << +[+[a,b], +[c,d]], psa(U))). 1155% ?- ((U << *[+[a,b], +[c,d]], psa(U))). 1156% ?- ((U << *[*[a,b], *[c,d]], psa(U))). 1157% ?- ((U << call(=, hello))). 1158% ?- ((U << call(=, append([a,b],[c,d])))). 1159% ?- X<< *[a,b], Y<< *[c,d], Z<< zdd_join(X, Y), psa(Z). 1160% ?- X<< *[a,b], Y<< *[c,d], Z<< (X+Y), psa(Z). 1161% 1162basic_type(X):- number(X); 1163 string(X); 1164 is_list(X); 1165 var(X). 1166 1167% ?- X<< p(2,3), psa(X). 1168% ?- X<< pq(2,3), psa(X). % Error. 1169% ?- findall(p(I), between(1,3,I), As), X<< +As, psa(X). 1170 1171default_atom(X):- functor(X, F, _), 1172 atom_chars(F, [A|As]), 1173 char_type(A, alpha), 1174 digit_chars(As). 1175% 1176digit_chars([]). 1177digit_chars([D|Ds]):- char_type(D, digit), 1178 digit_chars(Ds).
1183% Unusual first, but legal samples. 1184% ?- U << @(=(3)), psa(U). 1185% ?- U << +(!append([a], [b])), psa(U). 1186% ?- U << (@a+ @b+ @c), psa(U). 1187% ?- U << append([a], [b]). 1188% ?- U << +(append([[a]], [[b]])), psa(U). 1189% ?- U << get_compare. 1190% ?- get_compare(X). 1191% ?- U << arith(1+2). 1192% ?- U << plus(arith(1+2), arith(3+4)). 1193% ?- U << (@A+ @B+ @C), psa(U). 1194 1195zdd_eval(X, Y):- context_module(M), 1196 zdd_numbervars(X), 1197 zdd_eval(X, Y, M).
1203% Note that intgeger is used as a unique name of a ZDD. 1204% use indicator `@` as `@(3)` for 3 as an atom. 1205 1206zdd_eval(X, X, _) :- basic_type(X), !. 1207zdd_eval({}, 0, _) :-!. % The empty family of sets. 1208zdd_eval({X}, Y, _) :-!, associative_comma(X, U, []), zdd_family(U, Y). 1209zdd_eval($(X), X, _) :-!. 1210zdd_eval(!(X), Y, M) :-!, call(M:X, Y). 1211zdd_eval(M:X, Y, _) :-!, zdd_eval(X, Y, M). 1212zdd_eval(X, Y, _) :- zdd_basic(X, Y), !. 1213zdd_eval(X, Y, M) :- zdd_eval_args(X, X0, M), 1214 ( zdd_apply(X0, Y) -> true 1215 ; call(M:X0, Y) 1216 ). 1217% 1218zdd_eval_args(A, A, _):- atomic(A), !. 1219zdd_eval_args(A, B, M):- 1220 functor(A, Fa, Na), 1221 functor(B, Fa, Na), 1222 zdd_eval_args(1, A, B, M). 1223% 1224zdd_eval_args(I, A, B, M):- arg(I, A, U), !, 1225 zdd_eval(U, V, M), 1226 arg(I, B, V), 1227 J is I+1, 1228 zdd_eval_args(J, A, B, M). 1229zdd_eval_args(_, _, _, _). 1230 1231 /*********************************************** 1232 * Currently reserved names of operations. * 1233 ***********************************************/ 1234zdd_basic(@(A), Y) :-!, zdd_singleton(A, Y). 1235zdd_basic(X, Y) :- default_atom(X), !, zdd_singleton(X, Y). 1236zdd_basic(dnf(A), X) :-!, dnf(A, X). 1237zdd_basic(cnf(A), X) :-!, cnf(A, X). 1238zdd_basic(arith(E), X) :-!, X is E. 1239zdd_basic(X, Y) :- (atom(X); dvar(X)), !, zdd_singleton(X, Y).
1246zdd_apply(ltr_set(L), Y):-!, ltr_append(L, 1, Y). 1247zdd_apply(gf2(A), X) :-!, gf2(A, X). 1248zdd_apply(qp(A), X) :-!, mqp(A, X). 1249zdd_apply(cofact(A, L, R), X) :-!, cofact(X, t(A, L, R)). 1250zdd_apply(cofact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1251zdd_apply(fact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1252zdd_apply(+(X), Y) :-!, zdd_vector_exp(+(X), Y). 1253zdd_apply(*(X), Y) :-!, zdd_vector_exp(*(X), Y). 1254zdd_apply(X + Y, Z) :-!, zdd_join(X, Y, Z). 1255zdd_apply(X * Y, Z) :-!, zdd_merge(X, Y, Z). 1256zdd_apply(merge(X, Y), Z) :-!, zdd_merge(X, Y, Z). 1257zdd_apply(-(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1258zdd_apply(\(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1259zdd_apply((X // Y), Z) :-!, zdd_div(X, Y, Z). 1260zdd_apply((X / Y), Z) :-!, zdd_mod(X, Y, Z). 1261zdd_apply((X mod Y), Z) :-!, zdd_mod(X, Y, Z). 1262zdd_apply(&(X, Y), Z) :-!, zdd_meet(X, Y, Z). 1263zdd_apply(prod(X, Y), Z):-!, zdd_product(X, Y, Z). 1264zdd_apply(**(X, Y), Z) :-!, zdd_product(X, Y, Z). 1265zdd_apply(pow(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1266zdd_apply(power(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1267zdd_apply(set(X), Z) :- bdd_sort_append(X, 1, Z). 1268 1269 1270 /********************************* 1271 * vector expressions * 1272 *********************************/
1277% ?- ((X<< +[[1,2],[a,b]], psa(X), card(X, C))). 1278% ?- ((X<< *[[1,2],[a,b]], psa(X), card(X, C))). 1279% ?- ((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))). 1280% ?- X<< +[*[1,2], *[a,b]], psa(X). 1281% ?- X<< +[*[1,2], *[1]], psa(X). 1282% ?- X<< +[*[1,2], *[a,b]]. 1283% ?- ((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))). 1284% ?- ((X<< *[1,2], psa(X), card(X, C))). 1285% ?- ((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))). 1286% ?- zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1287% ?- zdd_vector_exp(+[[a],*[b,c]], X), psa(X). 1288% ?- zdd_vector_exp(+[a,b,c], X), psa(X). 1289% ?- zdd_vector_exp(*[a,b,c], X), psa(X). 1290% ?- zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X). 1291% ?- zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X). 1292% ?- zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X). 1293% ?- X<< *[a, b], psa(X). 1294% ?- X<< +[a, b], psa(X). 1295% ?- X<< *[A, B], psa(X). 1296% ?- X<< *[*[0, 1], *[2,3]], psa(X). 1297% ?- X<< *[*[], *[2,3]], psa(X). 1298% ?- X<< *[0, 1, *[2,3]], psa(X). 1299% ?- zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1300% ?- zdd_vector_exp(+[a,b], X), psa(X). 1301 1302zdd_vector_exp(*(X), Y):-!, zdd_vector_exp(*, X, Y). 1303zdd_vector_exp(+(X), Y):-!, zdd_vector_exp(+, X, Y). 1304zdd_vector_exp(X, Y):- zdd_singleton(X, Y). 1305% 1306zdd_vector_exp(*, [], 1):-!. 1307zdd_vector_exp(+, [], 0):-!. 1308zdd_vector_exp(F, [A|As], R):-!, % F in [*,+]. 1309 zdd_vector_exp(A, U), 1310 zdd_vector_exp(F, As, V), 1311 apply_binary_basic(F, U, V, R). 1312zdd_vector_exp(_, A, R):- zdd_singleton(A, R). 1313% 1314apply_binary_basic(*, X, Y, Z):-!, zdd_merge(X, Y, Z). 1315apply_binary_basic(+, X, Y, Z):- zdd_join(X, Y, Z). 1316% 1317zdd_fold_join([], Z, Z). 1318zdd_fold_join([X|Xs], Z, Z0):- 1319 zdd_join(X, Z, Z1), 1320 zdd_fold_join(Xs, Z1, Z0). 1321% 1322zdd_fold_merge([], Z, Z). 1323zdd_fold_merge([X|Xs], Z, Z0):- 1324 zdd_merge(X, Z, Z1), 1325 zdd_fold_merge(Xs, Z1, Z0). 1326% 1327fold_singleton_join([], X, X). 1328fold_singleton_join([A|As], X, Y):- 1329 zdd_singleton(A, U), 1330 zdd_join(U, X, X0), 1331 fold_singleton_join(As, X0, Y). 1332 1333% ?- X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X). 1334% ?- X<< (+[a,b]), psa(X). 1335% ?- X<< +[*[a,b]] + +[*[c,d]], psa(X). 1336% ?- X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X\Y). 1337% ?- X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X-Y). 1338 1339zdd_super_power([], P, P). 1340zdd_super_power([A|As], P, Q):- 1341 zdd_super_power(As, P, Q0), 1342 zdd_insert(A, Q0, Q). 1343% 1344single_set(L, Y) :-!, bdd_sort_append(L, 1, Y). 1345 1346% ?- ((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 1347family(X, Y):- zdd_numbervars(X), zdd_family(X, Y).
1353zdd_family(X, Y):- zdd_numbervars(X), zdd_family(X, 0, Y). 1354 1355% ?- zdd_family([[a],[a,b]], X), card(X, C), psa(X). 1356% ?- zdd_family([[], [a,a],[a,b]], X), psa(X). 1357zdd_family([], U, U). 1358zdd_family([X|Xs], U, V):- 1359 zdd_insert_atoms(X, 1, X1), 1360 zdd_join(X1, U, U0), 1361 zdd_family(Xs, U0, V). 1362 1363% ?- ((ltr_family([[a, b], [c, d]], X), sets(X,S))). 1364% ?- ((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 1365% ?- ((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 1366% ?- ((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 1367% ?- ((X << dnf((a+(-b)+a)), psa(X))). 1368% ?- ((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 1369% ?- ((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))). 1370% ?- ltr_ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X). 1371% ?- ltr_ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X). 1372% ?- ltr_ltr_family([[a],[-b, -a,-c]], X), psa(X). 1373% 1374ltr_family(X, Y):- ltr_family(X, 0, Y). 1375 1376% 1377ltr_family([], U, U). 1378ltr_family([X|Xs], U, V):- 1379 ltr_append(X, 1, X0), 1380 ltr_join(X0, U, U0), 1381 ltr_family(Xs, U0, V). 1382 1383 /************************ 1384 * choices * 1385 ************************/
1390% ?- zdd, X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y). 1391% ?- N=10, numlist(1, N, Ns), (X<< pow(Ns), zdd_subtr(X, 1, Y), 1392% zdd_choices(X, Y), card(Y, C)). 1393% ?- N=1000, numlist(1, N, Ns),time( (X<< pow(Ns), zdd_subtr(X, 1, Y), 1394% zdd_choices(X, Y), card(Y, C))). 1395 1396zdd_choices(0, 1):-!. 1397zdd_choices(1, 0):-!. 1398zdd_choices(X, Y):- memo(choices(X)-Y), 1399 ( nonvar(Y)->true %, write(+) % many hits when X has the empty set. 1400 ; cofact(X, t(A, L, R)), 1401 zdd_choices(L, L0), 1402 zdd_choices(R, R0), 1403 cofact(R1, t(A, R0, 1)), 1404 zdd_merge(L0, R1, Y) 1405 ). 1406 1407 1408 /************************************************* 1409 * Operation on join/merge/meet/subtr/cons * 1410 *************************************************/
1415zdd_join(0, X, X):-!. 1416zdd_join(X, 0, X):-!. 1417zdd_join(X, X, X):-!. 1418zdd_join(1, X, Y):-!, zdd_join_1(X, Y). 1419zdd_join(X, 1, Y):-!, zdd_join_1(X, Y). 1420zdd_join(X, Y, Z):- 1421 ( Y < X -> memo(zdd_join(Y, X)-Z) 1422 ; memo(zdd_join(X, Y)-Z) 1423 ), 1424 ( nonvar(Z) -> true 1425 ; cofact(X, t(A, L, R)), 1426 cofact(Y, t(A0, L0, R0)), 1427 zdd_compare(C, A, A0), 1428 ( C = (<) -> 1429 zdd_join(L, Y, U), 1430 cofact(Z, t(A, U, R)) 1431 ; C = (=) -> 1432 zdd_join(L, L0, U), 1433 zdd_join(R, R0, V), 1434 cofact(Z, t(A, U, V)) 1435 ; zdd_join(L0, X, U), 1436 cofact(Z, t(A0, U, R0)) 1437 ) 1438 ).
cofact(Z, t(X, 0, Y), S).
Having analogy Z = [X|Y] in mind.1444% ?- bdd_cons(X, a, 1), bdd_cons(X, A, B). 1445% ?- bdd_cons(X, a, 0), bdd_cons(X, A, B). % false 1446 1447bdd_cons(X, Y, Z):- ( var(X); X>1 ), !, cofact(X, t(Y, 0, Z)). 1448 1449% ?- ((X<<(*[a]+ *[b]+ []), psa(X))). % false for []. 1450% ?- ((X<<(*[a]+ *[b]+ 1), psa(X))). 1451% ?- ((X<<(*[a]+ *[b]+ 0), psa(X))). 1452% ?- ((X<<(*[a]+ *[b]), psa(X))). 1453% ?- ((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))). 1454 1455% zdd_join_1(+X, -Y, +G) is det. 1456% Y is the union of X and 1 (the singleton {{}}). 1457 1458zdd_join_1(X, X):- zdd_has_1(X), !. 1459zdd_join_1(X, Y):- zdd_add_1(X, Y). 1460% 1461zdd_add_1(0, 1):-!. 1462zdd_add_1(X, Y):- cofact(X, t(A, L, R)), 1463 zdd_add_1(L, L0), 1464 cofact(Y, t(A, L0, R)). 1465 1466% ?- ((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1467% ?- ((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1468% ?- ((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))). 1469% ?- ((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))). 1470% ?- trace, (X=[b, a]). 1471% ?- ((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 1472% ?- ((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
1477zdd_meet(0, _, 0):-!. 1478zdd_meet(_, 0, 0):-!. 1479zdd_meet(1, X, Y):-!, zdd_meet_1(X, Y). 1480zdd_meet(X, 1, Y):-!, zdd_meet_1(X, Y). 1481zdd_meet(X, X, X):-!. 1482zdd_meet(X, Y, Z):- 1483 ( X @< Y -> memo(zdd_meet(X,Y)-Z) 1484 ; memo(zdd_meet(Y,X)-Z) 1485 ), 1486 ( nonvar(Z) -> true 1487 ; cofact(X, t(A, L, R)), 1488 cofact(Y, t(A0, L0, R0)), 1489 zdd_compare(C, A, A0), 1490 ( C = (<) -> zdd_meet(L, Y, Z) 1491 ; C = (=) -> 1492 zdd_meet(L, L0, U), 1493 zdd_meet(R, R0, V), 1494 cofact(Z, t(A, U, V)) 1495 ; zdd_meet(L0, X, Z) 1496 ) 1497 ).
1502zdd_meet_1(X, 1):- zdd_has_1(X), !. 1503zdd_meet_1(_, 0).
1508% ?- X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), Z<<(X-Y), psa(Z). 1509% ?- ((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 1510% 1511zdd_subtr(X, X, 0):-!. 1512zdd_subtr(0, _, 0):-!. 1513zdd_subtr(X, 0, X):-!. 1514zdd_subtr(X, 1, Y):-!, zdd_subtr_1(X, Y). 1515zdd_subtr(1, X, Y):-!, 1516 ( zdd_has_1(X) -> Y = 0 1517 ; Y = 1 1518 ). 1519zdd_subtr(X, Y, Z):- memo(zdd_subtr(X,Y)-Z), 1520 ( nonvar(Z) -> true 1521 ; cofact(X, t(A, L, R)), 1522 cofact(Y, t(A0, L0, R0)), 1523 zdd_compare(C, A, A0), 1524 ( C = (<) -> 1525 zdd_subtr(L, Y, U), 1526 cofact(Z, t(A, U, R)) 1527 ; C = (=) -> 1528 zdd_subtr(L, L0, U), 1529 zdd_subtr(R, R0, V), 1530 cofact(Z, t(A, U, V)) 1531 ; zdd_subtr(X, L0, Z) 1532 ) 1533 ).
1538% ?- X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y). 1539% ?- X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y). 1540% ?- X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y). 1541% 1542zdd_subtr_1(X, 0):- X < 2, !. % empty family or singleton of the empty. 1543zdd_subtr_1(X, Y):- cofact(X, t(A, L, R)), 1544 zdd_subtr_1(L, L0), 1545 cofact(Y, t(A, L0, R)).
1550% ?- X<<{[a]}, Z << zdd_xor(X, X). 1551% ?- X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z). 1552% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms), 1553% time((X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))). 1554% ?- time((Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))). 1555zdd_xor(X, Y, Z):-zdd_subtr(X, Y, A), 1556 zdd_subtr(Y, X, B), 1557 zdd_join(A, B, Z). 1558 1559% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S), 1560% zdd_meet(X, Y, B, S), 1561% zdd_subtr(A, B, Z, S).
Remark. The merge is associative and commutative, but not idempotent.
1570% ?- (( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 1571% ?- time((( X<<pow(!charlist(a-z)), Y<<pow(:numlist(1, 26))))). 1572% ?- time((( X<<pow(:charlist($(a-z))), Y<<pow(:numlist(1, 26)), 1573% zdd_merge(X, Y, Z), U << zdd_meet(X, Z), card(X, C)))), C is 2^26. 1574 1575zdd_merge(0, _, 0):-!. 1576zdd_merge(_, 0, 0):-!. 1577zdd_merge(1, X, X):-!. 1578zdd_merge(X, 1, X):-!. 1579zdd_merge(X, Y, Z):- 1580 ( X > Y -> memo(zdd_merge(Y, X)-Z) 1581 ; memo(zdd_merge(X, Y)-Z) 1582 ), 1583 ( nonvar(Z) -> true 1584 ; cofact(X, t(A, L, R)), 1585 zdd_merge(L, Y, L0), 1586 zdd_merge(R, Y, R0), 1587 zdd_insert(A, R0, R1), 1588 zdd_join(L0, R1, Z) 1589 ). 1590% 1591 1592zdd_merge_list([], X, X). 1593zdd_merge_list([A|As], X, Y):- 1594 ( integer(A) -> zdd_merge(A, X, X0) 1595 ; zdd_insert(A, X, X0) % atom case 1596 ), 1597 zdd_merge_list(As, X0, Y).
1605zdd_disjoint_merge(0, _, 0):-!. 1606zdd_disjoint_merge(_, 0, 0):-!. 1607zdd_disjoint_merge(1, X, X):-!. 1608zdd_disjoint_merge(X, 1, X):-!. 1609zdd_disjoint_merge(X, Y, Z):- 1610 ( X @> Y -> memo(disj_merge(Y, X)-Z) 1611 ; memo(disj_merge(X, Y)-Z) 1612 ), 1613 ( nonvar(Z) -> true 1614 ; cofact(X, t(A, L, R)), 1615 cofact(Y, t(A0, L0, R0)), 1616 zdd_compare(C, A, A0), 1617 ( C= (<) -> 1618 zdd_disjoint_merge(L, Y, U), 1619 zdd_disjoint_merge(R, Y, V), 1620 cofact(Z, t(A, U, V)) 1621 ; C = (=) -> 1622 zdd_disjoint_merge(L, L0, U), 1623 zdd_disjoint_merge(L, R0, V), 1624 zdd_disjoint_merge(R, L0, W), 1625 zdd_join(V, W, P), 1626 cofact(Z, t(A, U, P)) 1627 ; zdd_disjoint_merge(X, L0, U), 1628 zdd_disjoint_merge(X, R0, V), 1629 cofact(Z, t(A0, U, V)) 1630 ) 1631 ). 1632 1633 1634% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1635% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1636%@ false. 1637% ?- ((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1638% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1639% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1640% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1645zdd_subfamily(X, X):-!. 1646zdd_subfamily(0, _):-!. 1647zdd_subfamily(_, 0):-!, fail. 1648zdd_subfamily(1, X):-!, zdd_has_1(X). 1649zdd_subfamily(X, X0):- 1650 cofact(X, t(A, L, R)), 1651 cofact(X0, t(A0, L0, R0)), 1652 zdd_compare(C, A, A0), 1653 ( C = (=) -> 1654 zdd_subfamily(L, L0), 1655 zdd_subfamily(R, R0) 1656 ; C = (>), 1657 zdd_subfamily(X, L0) 1658 ). 1659 1660 /********************************* 1661 * division/residue in * 1662 *********************************/
zdd_divmod(X, Y, D, M, S),
psa(X, S), psa(D, S), psa(M, S).
1670zdd_divmod(X, Y, D, M):-
1671 zdd_div_div(X, Y, D1, D),
1672 zdd_subtr(X, D1, M).1678% ?- X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S), 1679% psa(X, S), psa(D, S), psa(M, S). 1680zdd_divmod0(X, Y, D, M):- 1681 zdd_divisible(X, Y, D), 1682 zdd_subtr(X, D, M).
1688% ?- X<< +[b], zdd_div_div(X, 1, D, M), psa(X), psa(D), psa(M). 1689% ?- X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), psa(X), psa(Y), psa(D), psa(M). 1690% ?- X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), 1691% psa(X), psa(Y), psa(D), psa(M). 1692% ?- X<< +[*[a,b]], Y<< +[*[b]], psa(X), psa(Y), zdd_div_div(X, Y, D, M), 1693% psa(D), psa(M). 1694% ?- X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]], 1695% zdd_div_div(X, Y, D, D1), 1696% psa(D), psa(D1). 1697 1698zdd_div_div(0, _, 0, 0):-!. 1699zdd_div_div(1, X, Y, Y):-!, 1700 ( zdd_has_1(X) -> Y = 1 1701 ; Y = 0 1702 ). 1703zdd_div_div(_, 0, 0, 0):-!. 1704zdd_div_div(X, 1, X, X):-!. 1705zdd_div_div(X, Y, Z, U):- memo(div_div(X, Y)- P), 1706 ( nonvar(P) -> P = (Z, U) 1707 ; cofact(X, t(A, L, R)), 1708 zdd_div_div(L, Y, L0, U0), 1709 zdd_div_div(A, R, Y, R0, V0), 1710 zdd_join(L0, R0, Z), 1711 zdd_join(U0, V0, U), 1712 P = (Z, U) 1713 ). 1714% 1715zdd_div_div(_, 0, _, 0, 0):-!. 1716zdd_div_div(_, 1, 0, 0, 0):-!. % ??? 1717zdd_div_div(A, 1, 1, Z, Z):-!, zdd_singleton(A, Z). 1718zdd_div_div(_, _, 0, 0, 0):-!. 1719zdd_div_div(A, X, 1, Z, Z):-!, cofact(Z, t(A, 0, X)). 1720zdd_div_div(A, X, Y, Z, U):- cofact(Y, t(B, L, R)), 1721 zdd_compare(C, A, B), 1722 ( C = (<) -> 1723 zdd_div_div(X, Y, Z0, U0), 1724 zdd_insert(A, Z0, Z), 1725 zdd_insert(A, U0, U) 1726 ; C = (=) -> 1727 zdd_div_div(X, L, Z0, U0), 1728 zdd_insert(A, Z0, Z1), 1729 zdd_insert(A, U0, U1), 1730 zdd_div_div(X, R, Z2, U2), 1731 zdd_insert(A, Z2, Z3), % A is absorbed due to hit (A=B). 1732 zdd_join(Z1, Z3, Z), 1733 zdd_join(U1, U2, U) 1734 ; zdd_div_div(A, X, L, Z, U) 1735 ).
1741% ?- (( X<< {[a]}, zdd_div(X, X, Z), psa(Z))). 1742% ?- (( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1743% ?- (( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))). 1744% ?- (( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1745% ?- (( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1746% ?- (( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1747% ?- (( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1748% ?- (( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1749% ?- (( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1750% ?- (( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1751% ?- (( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))). 1752% ?- (( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1753% ?- (( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1754% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1755% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))). 1756% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1757% ?- (( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))). 1758% ?- (( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1759% ?- (( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1760% ?- (( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))). 1761% ?- (( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))). 1762% ?- (( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1763% ?- (( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1764 1765% 1766zdd_div(0, _, 0):-!. 1767zdd_div(1, X, Y):-!, 1768 ( zdd_has_1(X) -> Y = 1 1769 ; Y = 0 1770 ). 1771zdd_div(X, Y, Z):- memo(zdd_div(X, Y)- Z), 1772 ( nonvar(Z) -> true 1773 ; cofact(X, t(A, L, R)), 1774 zdd_div(L, Y, L0), 1775 zdd_div(A, R, Y, R0), 1776 zdd_join(L0, R0, Z) 1777 ). 1778% 1779zdd_div(_, _, 0, 0):-!. 1780zdd_div(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1781zdd_div(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1782 zdd_compare(C, A, B), 1783 ( C = (<) -> 1784 zdd_div(X, Y, Z0), 1785 cofact(Z, t(A, 0, Z0)) 1786 ; C = (=) -> 1787 zdd_div(X, L, L0), 1788 zdd_div(X, R, R0), 1789 cofact(Z, t(A, R0, L0)) 1790 ; zdd_div(A, X, L, Z) 1791 ).
1797% ?- zdd, N=10, numlist(1, N, Ns), numlist(1, 10, Js), X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z). 1798% ?- X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1799% ?- X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1800% ?- X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1801% ?- X<<pow([a, b, c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z). 1802 1803zdd_divisible(0, _, 0):-!. 1804zdd_divisible(1, X, Y):-!, 1805 ( zdd_has_1(X) -> Y = 1 1806 ; Y = 0 1807 ). 1808zdd_divisible(X, Y, Z):- memo(zdd_divisible(X, Y)- Z), 1809 ( nonvar(Z) -> true 1810 ; cofact(X, t(A, L, R)), 1811 zdd_divisible(L, Y, L0), 1812 zdd_divisible(A, R, Y, R0), 1813 zdd_join(L0, R0, Z) 1814 ). 1815% 1816zdd_divisible(_, _, 0, 0):-!. 1817zdd_divisible(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1818zdd_divisible(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1819 zdd_compare(C, A, B), 1820 ( C = (<) -> 1821 zdd_divisible(X, Y, Z0), 1822 cofact(Z, t(A, 0, Z0)) 1823 ; C = (=) -> 1824 zdd_divisible(X, L, L0), 1825 zdd_divisible(X, R, R0), 1826 zdd_join(L0, R0, Z0), 1827 cofact(Z, t(A, 0, Z0)) 1828 ; zdd_divisible(A, X, L, Z) 1829 ).
1834% ?- X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1835% ?- X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1836% ?- X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S). 1837% ?- X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S). 1838% ?- N = 300, numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns], 1839% time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S). 1840 1841% ?- X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z). 1842 1843zdd_divisible_by_all(X, Y, X):-Y<2, !. % It was hard to find this. 1844zdd_divisible_by_all(X, _, 0):-X<2, !. % It was a little bit hard to find this. 1845zdd_divisible_by_all(X, Y, Z):- memo(div_by_all(X, Y)-Z), 1846 ( nonvar(Z) -> true 1847 ; cofact(X, t(A, L, R)), 1848 zdd_divisible_by_all(L, Y, L0), 1849 zdd_divisible_by_all(A, R, Y, R0), 1850 zdd_join(L0, R0, Z) 1851 ). 1852% 1853zdd_divisible_by_all(A, X, Y, Z):- Y<2, !, 1854 cofact(Z, t(A, 0, X)). 1855zdd_divisible_by_all(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1856 zdd_compare(C, A, B), 1857 ( C = (<) -> 1858 zdd_divisible_by_all(X, Y, Z0), 1859 zdd_insert(A, Z0, Z) 1860 ; C = (=) -> 1861 zdd_divisible_by_all(X, R, R1), 1862 zdd_insert(A, R1, R0), 1863 zdd_divisible_by_all(R0, L, Z) 1864 ; Z = 0 % It was hard to find this. 1865 ).
1869zdd_mod(X, Y, Z) :- zdd_divisible(Y, X, X0),
1870 zdd_subtr(X, X0, Z).1875% ?- zdd_list(X, [[a]]), zdd_list(Y, [[a,c],[a,d]]), 1876% zdd_multiple(X, Y, Z), psa(Z). 1877% ?- zdd_list(X, [[a,b]]), zdd_list(Y, [[a,c],[a,d]]), 1878% zdd_multiple(X, Y, Z), psa(Z). 1879% ?- zdd_list(X, [[a,b]]), Y<<pow([a,b,c]), 1880% zdd_multiple(X, Y, Z), psa(Z). 1881% ?- Y<<pow([a,b,c]), zdd_multiple(0, Y, Z), psa(Z). 1882% ?- Y<<pow([a,b]), zdd_multiple(1, Y, Z), psa(Z). 1883 1884zdd_multiple(0, _, 0):-!. 1885zdd_multiple(1, Y, Y):-!. 1886zdd_multiple(_, Y, 0):-Y<2, !. 1887zdd_multiple(X, Y, Z):-memo(multiple(X, Y)-Z), 1888 ( nonvar(Z) -> true 1889 ; cofact(X, t(A, L, R)), 1890 zdd_multiple(L, Y, L0), 1891 zdd_multiple(A, R, Y, R0), 1892 zdd_join(L0, R0, Z) 1893 ). 1894% 1895zdd_multiple(_, _, Y, 0):- Y<2, !. 1896zdd_multiple(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1897 zdd_multiple(A, X, L, L0), 1898 zdd_compare(C, A, B), 1899 ( C = (<) -> R0 = 0 1900 ; C = (=) -> 1901 zdd_multiple(X, R, R1), 1902 zdd_insert(A, R1, R0) 1903 ; zdd_multiple(A, X, R, R1), 1904 zdd_insert(B, R1, R0) 1905 ), 1906 zdd_join(L0, R0, Z). 1907 1908 /********************************* 1909 * division/resudue in List * 1910 *********************************/
zdd_list(Y, U, Z), zdd_mod_by_list(X, U, Z, S).
?- ((X<<pow([a,b]), zdd_mod_by_list(X, [a], Y), psa(Y))).
?- ((X<<pow([a,b]), zdd_mod_by_list(X, [], Y), psa(Y))).
?- ((X<<pow([a,b]), zdd_mod_by_list(X, [a, b], Y), psa(Y))).
?- ((X<<pow([a,b,c]), zdd_mod_by_list(X, [b,c], Y), psa(Y))).
?- ((X<<pow([a,b,c]), zdd_mod_by_list(X, [a,c], Y), psa(Y))).
?- ((X<<pow([a]), zdd_mod_by_list(X, [c], Y), psa(Y))).
?- N=100, numlist(1, N, Ns), numlist(1, N, Js), ((X<<pow(Ns), zdd_mod_by_list(X, Js, Z), card(Z, C))).
1923zdd_mod_by_list(X, Y, Z):- zdd_divisible_by_list(X, Y, Z0),
1924 zdd_subtr(X, Z0, Z).zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).1930% ?- ((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1931% ?- ((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 1932 1933zdd_div_by_list(X, [], X):-!. 1934zdd_div_by_list(X, F, Y):- F=[A|As], 1935 ( X<2 -> Y = 0 1936 ; cofact(X, t(B, L, R)), 1937 zdd_div_by_list(L, F, L0), 1938 zdd_compare(C, B, A), 1939 ( C = (>) -> R0 = 0 1940 ; C = (=) -> 1941 zdd_div_by_list(R, As, R0) 1942 ; zdd_div_by_list(R, F, R1), 1943 zdd_insert(B, R1, R0) 1944 ), 1945 zdd_join(L0, R0, Y) 1946 ).
zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).1952% ?- ((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1953% ?- ((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 1954 1955zdd_divisible_by_list(X, [], X):-!. 1956zdd_divisible_by_list(X, F, Y):- F=[A|As], 1957 ( X<2 -> Y = 0 1958 ; cofact(X, t(B, L, R)), 1959 zdd_divisible_by_list(L, F, L0), 1960 zdd_compare(C, B, A), 1961 ( C = (>) -> R0 = 0 1962 ; C = (=) -> zdd_divisible_by_list(R, As, R0) 1963 ; zdd_divisible_by_list(R, F, R0) 1964 ), 1965 cofact(Y, t(B, L0, R0)) 1966 1967 ). 1968 1969 1970 /********************* 1971 * meta on * 1972 *********************/
map_zdd(F, X, Y) works roughly like
maplist(maplist(F), X, Y)) with a list X of lists.
1981% ?- zdd. 1982% ?- X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 1983% ?- X << pow([1,2,4,5,6]), 1984% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 1985% ?- N=2, numlist(1, N, L), X<<pow(L), 1986% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 1987% ?- N=10, numlist(1, N, L), 1988% X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 1989% ?- N=10, numlist(1, N, L), 1990% X<<pow(L), map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C), C=:= 2^N. 1991% ?- N=1000, numlist(1, N, L), X<<pow(L), 1992% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C), C=:= 2^N. 1993% ?- X<<pow([a,b,c]), map_zdd(pred([b,a] & [A, A]), X, Y), psa(Y), card(Y, C). 1994 1995:- meta_predicate map_zdd(,,). 1996map_zdd(F, X, Y):- open_memo(map_zdd), map_zdd_memo(F, X, Y). 1997 1998map_zdd_memo(_, X, X):- X<2, !. 1999map_zdd_memo(F, X, Y):- memo(map(X,F)-Y, map_zdd), 2000 ( nonvar(Y)-> true 2001 ; cofact(X, t(A, L, R)), 2002 map_zdd_memo(F, L, L0), 2003 map_zdd_memo(F, R, R0), 2004 call(F, A, B), 2005 zdd_insert(B, R0, R1), 2006 zdd_join(L0, R1, Y) 2007 ).
2012% ?- X<<pow([a,b,c]), identify_atoms(a, b, X, Y), psa(Y), card(Y, C). 2013identify_atoms(A, B, X, Y):-map_zdd(identify_map(A, B), X, Y). 2014% 2015identify_map(A, B, A, B):-!. 2016identify_map(_, _, X, X). 2017 2018% ?- X<< (*[a,b,c]), psa(X). 2019% ?- X<< (+[a,b]), psa(X). 2020% ?- X<<pow([a,b,c]), psa(X). 2021% ?- prz(1). 2022% ?- prz(0). 2023% ?- mp(hello, 1). 2024% ?- mp(hello, 0).
2028prz(X):- print_set_at(X).2032mp(M, X) :- mpsa(M, X). 2033 2034mpsa(M, X):- writeln(M), 2035 print_set_at(X), 2036 writeln('-------------------'). 2037 2038% ?- sat. 2039% ?- sat(a+b), sat(b+c), psa. 2040% ?- sat(A+B), sat(B+C), psa. 2041 2042psa :- b_getval(root, R), psa(R).
pow([a]), psa(X).
?- X<<{[a]}, psa(X).2049psa(X):- print_set_at(X), 2050 writeln('-------------------'). 2051% 2052psa(X, G):- print_set_at(X, G), 2053 writeln('-------------------').
Users/cantor/devel/zdd/prolog/zdd/zdd.pl2058print_set_at(0):-!, format("\szid = 0\n\t0\n"). 2059print_set_at(1):-!, format("\szid = 1\n\t[]\n"). 2060print_set_at(X):- format("\szid = ~w\n", [X]), 2061 forall(set_at(P, X), format("\t~w\n", [P])). 2062% 2063print_set_at(0, _):-!, format("\szid = 0\n\t0\n"). 2064print_set_at(1, _):-!, format("\szid = 1\n\t[]\n"). 2065print_set_at(X, G):- format("\szid = ~w\n", [X]), 2066 forall(set_at(P, X, G), format("\t~w\n", [P])). 2067 2068% ?- X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X). 2069% ?- X<<pow([1,2]), set_at(U, X), psa(X). 2070 2071% ?- zdd, ((X<<pow([1,2]), mp(powerset, X))). 2072set_at([], 1):-!. 2073set_at(P, X):- X>1, 2074 cofact(X, t(A, L, R)), 2075 ( set_at(P, L) 2076 ; set_at(As, R), 2077 P=[A|As] 2078 ). 2079% 2080set_at([], 1, _):-!. 2081set_at(P, X, G):- X>1, 2082 cofact(X, t(A, L, R), G), 2083 ( set_at(P, L, G) 2084 ; set_at(As, R, G), 2085 P=[A|As] 2086 ). 2087 2088% ?- zdd_singleton(a, X), show_fos(X). 2089% ?- X<< {[a,b], [b,c]}, show_fos(X). 2090% ?- X<< pow([a,b]), show_fos(X).
2094show_fos(X):- X > 1, 2095 accessible_nodes(X, Ns), 2096 forall( member(M, Ns), 2097 ( cofact(M, T), 2098 writeln(M->T))). 2099% 2100accessible_nodes(X, Ns):- 2101 accessible_nodes(X, Ns0, []), 2102 sort(Ns0, Ns1), 2103 reverse(Ns1, Ns). 2104% 2105accessible_nodes(X, A, A):- X<2, !. 2106accessible_nodes(X, [X|A], B):- 2107 cofact(X, t(_, L, R)), 2108 accessible_nodes(L, A, A0), 2109 accessible_nodes(R, A0, B).
2115% ?- zdd, ((X<<pow([a,b,c]), zdd_list(X, Y), zdd_list(X0, Y))). 2116% ?- powerset([a,b,c], Y), zdd, ((zdd_list(X, Y), zdd_list(X, Y0), zdd_list(X0, Y0))), 2117% maplist(sort, Y, Y1), sort(Y1, Y2). 2118% 2119zdd_list(X, Y):- nonvar(X), !, zdd_sets(X, Y). 2120zdd_list(X, Y):- zdd_family(Y, X). 2121 2122% ?- ((X<<pow([a,b,c]), sets(X, P))). 2123% ?- ((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))). 2124% ?- ((X<<pow([]), sets(X, P))). 2125% ?- ((X<<pow([a]), sets(X, P))). 2126% ?- ((X<<pow(:numlist(1,3)), sets(X, Y))). 2127% ?- ((X<<pow([a,b,c]), sets(X, Y))). 2128% ?- ((X<<pow(:charlist($a, $c)), sets(X, Y))). 2129% ?- ((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))), sets(X, Y))).
2134sets(X, Y):- zdd_sets(X, Y0), zdd_sort(Y0, Y). 2135% 2136zdd_sets(1, [[]]):-!. 2137zdd_sets(0, []):-!. 2138zdd_sets(X, P):- 2139 cofact(X, t(A,L,R)), 2140 zdd_sets(L, Y), 2141 zdd_sets(R, Z), 2142 maplist(cons(A), Z, AZ), 2143 append(AZ, Y, P). 2144 2145% ?- zdd_eval(pow([a, b, c, d, e, f]), I), eqns(I, X), 2146% maplist(writeln, X). 2147% 2148eqns(X, Y):- zdd_eqns(X, Y). 2149 2150basic_zdd(0). 2151basic_zdd(1). 2152 2153% % ?- X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es). 2154% % ?- X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es). 2155 2156% zdd_eqns(I, Es):- nonvar(I), var(Es), !, zdd_to_eqns(I, Es, []). 2157% zdd_eqns(I, Es):- var(I), nonvar(Es), !, 2158% ( check_eqns_for_zdd(Es) -> 2159% Es = [X=_|_], 2160% eqns_to_zdd(Es, X, I) 2161% ; throw('Violating-underlying-ordering-on-atoms.'(Es)) 2162% ). 2163% % 2164% zdd_to_eqns(I, X, Y):- zdd_to_eqns(I, X, [], S), 2165% zdd_sort(X, X1, S), 2166% reverse(X1, X). 2167% % 2168% zdd_to_eqns(I, X, X):- I<2, !. 2169% zdd_to_eqns(I, X, Y):- memo(visited(I)-F), 2170% ( nonvar(F) -> Y = X 2171% ; F = true, 2172% cofact(I, t(A, L, R)), 2173% X = [I=t(A, L, R)|X0], 2174% zdd_to_eqns(L, X0, X1), 2175% zdd_to_eqns(R, X1, Y) 2176% ). 2177% % 2178% check_eqns_for_zdd(Es):- are_eqns_closed(Es, Es), 2179% sort(Es, Fs), 2180% has_unique_left(Fs), 2181% sort(2, @=<, Es, Gs), 2182% has_unique_right(Gs). 2183% % 2184% are_eqns_closed([], _). 2185% are_eqns_closed([_ = t(A, L, R)|Rest], Es):- 2186% ( basic_zdd(L) -> true 2187% ; memberchk(L = t(B, _, _), Es), 2188% zdd_compare(<, A, B) 2189% ), 2190% ( basic_zdd(R) -> true 2191% ; memberchk(L = t(C, _, _), Es), 2192% zdd_compare(<, A, C) 2193% ), 2194% are_eqns_closed(Rest, Es). 2195% % 2196% eqns_to_zdd(_, 0, 0):-!. 2197% eqns_to_zdd(_, 1, 1):-!. 2198% eqns_to_zdd(Es, X, I):- memo(solve(X)-I), 2199% ( nonvar(I) -> true 2200% ; memberchk(X = t(A, L, R)), 2201% eqns_to_zdd(Es, L, L0), 2202% eqns_to_zdd(Es, R, R0), 2203% cofact(I, t(A, L0, R0)) 2204% ).
is_function([a-1,b-2,c-3]).
?- is_function([a-1,b-2,a-3]).2210is_function(X):- sort(X, Y), has_unique_left(Y). 2211% 2212has_unique_left([X,Y|Z]):-!, 2213 ( arg(1, X, A), arg(1, Y, A) -> false 2214 ; has_unique_left([Y|Z]) 2215 ). 2216has_unique_left(_).
2221% ?- check_one_to_one([a-1,b-2,c-3]). 2222% ?- check_one_to_one([a-1,b-2,c-1]). % false 2223 2224check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y). 2225% 2226has_unique_right([X,Y|Z]):-!, 2227 ( arg(2, X, A), arg(2, Y, A) -> false 2228 ; has_unique_right([Y|Z]) 2229 ). 2230has_unique_right(_).
ppoly(+X) is det.
Print X in polynomical form.2234ppoly(X):- poly_term(X, Poly), 2235 writeln(Poly). 2236 2237% ?- ((X<<pow([a,b]), poly_term(X, P))). 2238% ?- ((X<<pow([a,b,c]), poly_term(X, P))). 2239% ?- ((X<<(@a + @b), psa(X))). 2240 2241poly_term(X, Poly):- zdd_sets(X, Sets), 2242 get_compare(Pred), 2243 maplist(predsort(Pred), Sets, Sets0), 2244 predsort(Pred, Sets0, Sets1), 2245 poly_term0(Sets1, Poly). 2246 2247% ?- poly_term0([], Y). 2248% ?- poly_term0([[]], Y). 2249% ?- poly_term0([[a], [b]], Y). 2250% ?- poly_term0([[a*b], [c]], Y). 2251 2252poly_term0(X, Y):- maplist(mul_term, X, X0), 2253 sum_term(X0, Y). 2254% 2255mul_term([], 1):-!. 2256mul_term([X], X):-!. 2257mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 2258% 2259sum_term([], 0):-!. 2260sum_term([X], X):-!. 2261sum_term([X, Y|Xs], Z):-sum_term([X+Y|Xs], Z).
?- ((X << pow([a, b, c]), zdd_rand_path(X))).
?- ((X << {[a], [b], [c]}, zdd_rand_path(X))).
?- ((X << pow([a, b, c, d, e, f, g]), zdd_rand_path(X))).
2270zdd_rand_path(I):- zdd_rand_path(I, P, []), writeln(P). 2271% 2272zdd_rand_path(I, P):- zdd_rand_path(I, P, []). 2273% 2274zdd_rand_path(1, X, X):-!. 2275zdd_rand_path(I, X, Y):- I>1, 2276 cofact(I, t(A, L, R)), 2277 ( L == 0 -> 2278 X = [A|X0], 2279 zdd_rand_path(R, X0, Y) 2280 ; random(2) =:= 0 -> 2281 X = [A|X0], 2282 zdd_rand_path(R, X0, Y) 2283 ; zdd_rand_path(L, X, Y) 2284 ).
zdd_atoms(1, S))).
?- ((family([[a,b],[b,c]], X), zdd_atoms(X, S))).
?- N = 10000, time(((numlist(1, N, L), X<<pow(L), zdd_atoms(X, S)))).
?- X<<pow([a,b,c,d]), zdd_atoms(X, U).2293zdd_atoms(X, []):- X<2, !. 2294zdd_atoms(X, P):- memo(atoms(X)-P), 2295 ( nonvar(P) -> true 2296 ; cofact(X, t(A, L, R)), 2297 zdd_atoms(L, Al), 2298 zdd_atoms(R, Ar), 2299 ord_union(Al, Ar, P0), 2300 P=[A|P0] 2301 ). 2302 2303% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 2304:- meta_predicate delete(, , ). 2305delete(X, Y, Z):- delete(X, Y, Z, []). 2306 2307:- meta_predicate delete(, , , ). 2308delete(_, [], L, L). 2309delete(Pred, [X|Xs], L, L0):- 2310 ( call(Pred, X) 2311 -> delete(Pred, Xs, L, L0) 2312 ; L = [X|L1], 2313 delete(Pred, Xs, L1, L0) 2314 ). 2315 2316% ?- ((zdd_power([a,b], R), sets(R, U))). 2317% ?- ((X<< zdd_power(:charlist($(a-c))), sets(X, U))). 2318% ?- ((R<< pow(: !charlist(a-d)), card(R, C))). 2319%% 2320zdd_power(X, Y):- zdd_sort(X, X0), 2321 zdd_ord_power(X0, 1, Y).
zdd_ord_power([a,b], 1, X), psa(X).2326zdd_ord_power([], P, P). 2327zdd_ord_power([X|Xs], P, Q):- zdd_ord_power(Xs, P, R), 2328 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.2336% ?- atomlist(ax(1+1, 3+1), As). 2337% ?- atomlist(ax(1, 3), As). 2338atomlist(X, As):- X=..[A, I, J], 2339 I0 is I, 2340 J0 is J, 2341 findall(Y, ( between(I0, J0, K), 2342 atom_concat(A, K, Y) 2343 ), 2344 As).
2350% ?- charlist(a-c, X). 2351charlist(A-B, I):- 2352 findall(X, ( char_type(X, alnum), 2353 X @>= A, 2354 X @=< B 2355 ), 2356 I).
charlist(A-B, X).
?- charlist(a, c, X).
@ X = [a, b, c].2362charlist(A, B, I):- charlist(A-B, I). 2363 2364% ?- term_atoms(a+b=c, L). 2365% ?- term_atoms(a+b, L). 2366% ?- term_atoms(f(a+a), L).
2372term_atoms(X, L):- term_atoms(X, L0, []), 2373 sort(L0, L). 2374 2375% 2376term_atoms(X, L, L):- var(X), !. 2377term_atoms(X, [X|L], L):- atom(X), !. 2378term_atoms([X|Y], L, L0):-!, 2379 term_atoms(X, L, L1), 2380 term_atoms(Y, L1, L0). 2381term_atoms(X, L, L0):- compound(X), !, 2382 X =..[_|As], 2383 term_atoms(As, L, L0). 2384term_atoms(_, L, L). 2385 2386% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 2387% ?- subst_opp(a, X, [b-a]). 2388% ?- subst_opp([a], X, [b-a]). 2389 2390subst_opp(X, Y, L):- memberchk(Y-X, L). 2391subst_opp([X|Y], [X0|Y0], L):-!, 2392 subst_opp(X, X0, L), 2393 subst_opp(Y, Y0, L). 2394subst_opp(X, Y, L):- compound(X), !, 2395 X =..[F|As], 2396 subst_opp(As, Bs, L), 2397 Y =..[F|Bs]. 2398subst_opp(X, X, _). 2399 2400% ?- subst_term(f(a), R, [a-b]). 2401% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 2402% ?- subst_term(f(a), R, [a-X]). 2403% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2404% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2405% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
2411subst_term(X, Y):- member(X0-Y), X0==X, !. 2412subst_term(A, B):- compound(A), !, 2413 ( A = [X|Y] -> 2414 B = [X0|Y0], 2415 subst_term(X, X0), 2416 subst_term(Y, Y0) 2417 ; functor(A, F, N), 2418 functor(B, F, N), 2419 subst_term(N, A, B) 2420 ). 2421subst_term(X, X). 2422% 2423subst_term(0, _, _):-!. 2424subst_term(I, X, Y):- 2425 arg(I, X, A), 2426 arg(I, Y, B), 2427 subst_term(A, B), 2428 J is I - 1, 2429 subst_term(J, X, Y). 2430 2431% ?- all_instances([a,b], [0,1], a+b=b, R). 2432% ?- all_instances([x,y], [0,1], x+y=x, R). 2433%! all_instances(+As, +Vs, +X, -Y) is det. 2434% Unify Y with the list of possible variations P of X, 2435% where P is a variation of X if for each A in As with some 2436% V in Vs which depends on A, P is obtained from X by replacing 2437% all occurrences of A appearing in X with V for A in As. 2438 2439all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 2440 apply_maps(Fs, X, Y, []). 2441% 2442apply_maps([], _, Y, Y). 2443apply_maps([F|Fs], X, [X0|Y], Z):- 2444 subst_term(X, X0, F), 2445 apply_maps(Fs, X, Y, Z). 2446 2447% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 2448% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 2449% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 2450% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 2451%! mod_table(+M, +X, +E, -T) is det. 2452% Unify T with a set of form E' = V where 2453% E' is a possible ground instance of an integer expression E 2454% and V is the value of E' with modulo M, where X is a set of 2455% parameters appearing in E. 2456 2457mod_table(M, Xs, Exp, Table):- M0 is M-1, 2458 numlist(0, M0, V), 2459 all_instances(Xs, V, Exp, Exps), 2460 !, 2461 maplist(mod_arith(M), Exps, Table). 2462% 2463mod_arith(M, Exp, Exp=V):- V is Exp mod M. 2464 2465% 2466unify_all([]). 2467unify_all([_]). 2468unify_all([X,Y|Z]):- (zdd):(X=Y), unify_all([Y|Z]). 2469 2470% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 2471% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 2472% ?- ((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 2473% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 2474% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 2475% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
2480% ?- ((X <<{[a,b], [a,c]}, zdd_appear(e, X))). % false 2481% ?- ((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X))). % false 2482% ?- ((X <<(*[a,b]+ *[a,c]), psa(X), zdd_appear(c, X))). 2483% ?- numlist(1, 10000, Ns), ((X<<pow(Ns), zdd_appear(10000, X))). 2484% ?- X<<pow(:numlist(1, 10000)), zdd_appear(10000, X). 2485%@ X = 10001. 2486 2487zdd_appear(A, X):- use_memo(zdd_atom_appear(A, X)). 2488 2489zdd_atom_appear(A, X):- X > 1, 2490 memo(visited(X)-B), 2491 var(B), 2492 cofact(X, t(U,L,R)), 2493 zdd_compare(C, A, U), 2494 ( C = (=) -> true 2495 ; C = (>), 2496 ( zdd_atom_appear(A, L) -> true 2497 ; L < 2 -> 2498 zdd_atom_appear(A, R) 2499 ; memo(visited(L)-true), % for earlier fail. 2500 zdd_atom_appear(A, R) 2501 ) 2502 ).
2507zdd_singleton(X, P):- cofact(P, t(X, 0, 1)).2512zdd_has_1(1):-!. 2513zdd_has_1(X):- X>1, 2514 cofact(X, t(_, L, _)), 2515 zdd_has_1(L).
pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q))).2526zdd_subst(_, _, X, X, _):- X<2, !. 2527zdd_subst(X, U, P, Q):- memo(zdd_subst(X, U, P)-Q), 2528 ( nonvar(Q) -> true 2529 ; cofact(P, t(Y, L, R)), 2530 zdd_subst(X, U, L, L0), 2531 zdd_compare(C, X, Y), 2532 ( C = (=) -> zdd_merge(U, R, R0) 2533 ; C = (<) -> bdd_cons(R0, Y, R) 2534 ; zdd_subst(X, U, R, R1), 2535 zdd_insert(Y, R1, R0) 2536 ), 2537 zdd_join(L0, R0, Q) 2538 ). 2539 2540 /*********************** 2541 * product on * 2542 ***********************/ 2543 2544% ?- ((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))). 2545% ?- ((X<<(a*b), Y<<(c*d), Z<<(X**Y))). 2546% ?- ((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))). 2547% ?- ((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))). 2548% ?- time(((X<<pow(:numlist(1,16)), Z<<(X**X), card(Z, C)))). 2549% ?- N is 10000, time( ( X<<pow(:numlist(1,N)), card(X, _C))), _C =:= 2^N. 2550% ?- call_with_time_limit(120, (numlist(1, 16, R), 2551% time(((X<<pow(R), Z<<(X**X), card(Z, C)))))). 2552 2553% 2554zdd_product(X, Y, 0):- (X<2; Y<2), !. 2555zdd_product(X, Y, Z):- memo(prod(X, Y)-Z), 2556 ( nonvar(Z) -> true % , write(.) % hits found. 2557 ; zdd_product(X, Y, [], Bs, 0, Z0), 2558 append_pairs_list(X, Bs, Z1), 2559 zdd_join(Z0, Z1, Z) 2560 ). 2561% 2562zdd_product(_, X, Bs, Bs, Z, Z):- X<2, !. 2563zdd_product(X, Y, Bs, Q, U, V):- cofact(Y, t(B, L, R)), 2564 zdd_product(X, L, L0), 2565 zdd_join(L0, U, U0), 2566 zdd_product(X, R, [B|Bs], Q, U0, V). 2567% 2568append_pairs_list(X, _, X):- X<2, !. 2569append_pairs_list(X, Bs, U):- cofact(X, t(A, L, R)), 2570 append_pairs_list(R, Bs, R0), 2571 append_pairs_list(L, Bs, L0), 2572 insert_pairs(A, Bs, R0, R1), 2573 zdd_join(L0, R1, U). 2574 2575% 2576insert_pairs(_, [], U, U):-!. 2577insert_pairs(A, [B|Bs], U, V):- 2578 zdd_insert((A-B), U, U0), 2579 insert_pairs(A, Bs, U0, V). 2580 2581 /************************* 2582 * Quotient on * 2583 *************************/
?- ((zdd_insert(a, 1, X), zdd_insert(b, X, X1), prz(X1))).
?- ((X<<pow([a,b,c]), zdd_insert(x, X, X1), psa(X1))).
2592zdd_insert(_, 0, 0):-!. 2593zdd_insert(A, 1, J):-!, zdd_singleton(A, J). 2594zdd_insert(A, I, J):- memo(insert(A, I)-J), 2595 ( nonvar(J) -> true 2596 ; cofact(I, t(X, L, R)), 2597 zdd_compare(C, A, X), 2598 ( C = (=) -> 2599 zdd_join(L, R, K), 2600 cofact(J, t(X, 0, K)) 2601 ; C = (<) -> 2602 cofact(J, t(A, 0, I)) 2603 ; zdd_insert(A, L, L0), 2604 zdd_insert(A, R, R0), 2605 cofact(J, t(X, L0, R0)) 2606 ) 2607 ). 2608 2609% ?- X<<pow([a,b]), Y<<pow([c,d]), 2610% psa(X, S), psa(Y, S), 2611% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S). 2612 2613% ?- X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S), 2614% psa(Y, S). 2615% ?- listing(zdd_insert). 2616 2617:- meta_predicate zdd_insert(, , , ). 2618zdd_insert(_, _, 0, 0):-!. 2619zdd_insert(_, A, 1, Y):-!, zdd_singleton(A, Y). 2620zdd_insert(F, A, X, Y):- memo(zdd_insert(X, A, F)-Y), 2621 ( nonvar(Y) -> true % , write(.) % many hits 2622 ; cofact(X, t(B, L, R)), 2623 zdd_insert(F, A, L, L0), 2624 call(F, C, A, B), 2625 ( C = (=) -> bdd_cons(R0, A, R) 2626 ; C = (<) -> bdd_append([A, B], R, R0) 2627 ; zdd_insert(F, A, R, R1), 2628 bdd_cons(R0, B, R1) 2629 ), 2630 zdd_join(L0, R0, Y) 2631 ). 2632 2633% ?- ((family([[a, b],[b]], X), sets(X, Sx), 2634% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
2639% ?- numlist(1, 10000, Ns), ((zdd_insert_atoms(Ns, 1, X), psa(X))). 2640 2641% ?- ((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))). 2642% ?- ((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))). 2643zdd_insert_atoms(X, Y, Z):- zdd_sort(X, X0), 2644 zdd_ord_insert(X0, Y, Z). 2645 2646% 2647zdd_ord_insert(_, 0, 0):-!. 2648zdd_ord_insert([], X, X):-!. 2649zdd_ord_insert(As, 1, Y):-!, bdd_append(As, 1, Y). 2650zdd_ord_insert(As, X, Y):- memo(ord_insert(X, As)-Y), 2651 ( nonvar(Y) -> true % , write(.) % many hits. 2652 ; As = [A|U], 2653 cofact(X, t(B, L, R)), 2654 zdd_compare(C, A, B), 2655 ( C = (<) -> 2656 zdd_ord_insert(U, X, Y0), 2657 cofact(Y, t(A, 0, Y0)) 2658 ; C = (=) -> 2659 zdd_ord_insert(U, L, L1), 2660 zdd_ord_insert(U, R, R1), 2661 zdd_join(R1, L1, Y0), 2662 cofact(Y, t(A, 0, Y0)) 2663 ; zdd_ord_insert(As, L, L1), 2664 zdd_ord_insert(As, R, R1), 2665 cofact(Y, t(B, L1, R1)) 2666 ) 2667 ). 2668 2669 2670% ?- X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y), psa(Y). 2671:- meta_predicate zdd_reorder(, , ). 2672zdd_reorder(_, X, X):- X<2, !. 2673zdd_reorder(F, X, Y):- cofact(X, t(A, L, R)), 2674 zdd_reorder(F, L, L0), 2675 zdd_reorder(F, R, R1), 2676 zdd_insert(F, A, R1, R0), 2677 zdd_join(L0, R0, Y). 2678 2679 2680 /***************** 2681 * filters * 2682 *****************/ 2683 2684% ?- X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y), psa(Y). 2685% ?- X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y), psa(Y). 2686% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y), psa(Y). 2687% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, 3], X, Y), psa(Y). 2688% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y), psa(Y). 2689% ?- ltr, numlist(1, 1000, Ns) , X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y), card(Y, C), 2690% card(X, D), zdd_compare(E, C, D), U is D-C. 2691 2692% 2693ltr_meet_filter([], X, X):-!. 2694ltr_meet_filter([A|F], X, Y):- 2695 ltr_filter(A, X, X0), 2696 ltr_meet_filter(F, X0, Y). 2697 2698% ?- X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y), psa(Y). 2699% ?- X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y), psa(Y). 2700ltr_join_filter(F, X, Y):- 2701 ltr_join_filter(F, X, 0, Y). 2702% 2703ltr_join_filter([], _, Y, Y):-!. 2704ltr_join_filter([P|F], X, Y, Y0):-!, 2705 ltr_filter(P, X, Y1), 2706 zdd_join(Y, Y1, Y2), 2707 ltr_join_filter(F, X, Y2, Y0). 2708 2709% 2710ltr_filter(-A, X, Y):-!, ltr_filter_negative(A, X, Y). 2711ltr_filter(A, X, Y):- ltr_filter_positive(A, X, Y). 2712 2713% 2714ltr_filter_negative(_, X, X):- X<2, !. 2715ltr_filter_negative(A, X, Y):- memo(letral_neg(X, A)-Y), 2716 ( nonvar(Y) -> true 2717 ; cofact(X, t(B, L, R)), 2718 ltr_filter_negative(A, L, L0), 2719 zdd_compare(C, A, B), 2720 ( C = (=) -> R0 = 0 2721 ; C = (<) -> R0 = R 2722 ; ltr_filter_negative(A, R, R0) 2723 ), 2724 cofact(Y, t(B, L0, R0)) 2725 ). 2726% 2727ltr_filter_positive(_, X, 0):- X<2, !. 2728ltr_filter_positive(A, X, Y):- memo(ltr_pos(X, A)-Y), 2729 ( nonvar(Y) -> true 2730 ; cofact(X, t(B, L, R)), 2731 ltr_filter_positive(A, L, L0), 2732 zdd_compare(C, A, B), 2733 ( C = (=) -> R0 = R 2734 ; C = (<) -> R0 = 0 2735 ; ltr_filter_positive(A, R, R0) 2736 ), 2737 cofact(Y, t(B, L0, R0)) 2738 ). 2739 2740% ?- ((X<<pow([a,b,c]), dnf_filter([[-b,-c]], X, Y), psa(Y))). 2741% ?- ((X<<pow([a,b]), dnf_filter([[b]], X, Y), psa(Y))). 2742% ?- ((X<<pow([a,b]), dnf_filter([[a,b]], X, Y), psa(Y))). 2743% ?- ((X<<pow([a,b]), dnf_filter([], X, Y), psa(Y))). 2744% ?- ((X<<pow([a,b,c]), dnf_filter([[c]], X, Y), psa(Y))). 2745% ?- ((X<<pow([a,b,c]), dnf_filter([], X, Y), psa(Y))). 2746% ?- ((X<<pow([a,b,c]), dnf_filter([[a],[-c]], X, Y), psa(Y))). 2747 2748dnf_filter(DNF, X, Y):- dnf_filter(DNF, X, 0, Y). 2749% 2750dnf_filter([], _, Y, Y, _). 2751dnf_filter([F|Fs], X, Y, Z):- 2752 ltr_meet_filter(F, X, X0), 2753 zdd_join(X0, Y, Y0), 2754 dnf_filter(Fs, X, Y0, Z). 2755 2756% ?- ((X<<pow([a,b,c]), cnf_filter([[-b,-c]], X, Y), psa(Y))). 2757% ?- ((X<<pow([a,b,c]), cnf_filter([[-a, -b, -c]], X, Y), psa(Y))). 2758cnf_filter([], X, X). 2759cnf_filter([F|Fs], X, Y):- 2760 ltr_join_filter(F, X, X0), 2761 cnf_filter(Fs, X0, Y). 2762 2763% 2764zdd_meet_list([A], A):-!. 2765zdd_meet_list([A|As], B):- zdd_meet_list(As, A, B). 2766% 2767zdd_meet_list([], X, X). 2768zdd_meet_list([A|As], X, Y):- zdd_meet(A, X, X0), 2769 zdd_meet_list(As, X0, Y). 2770% 2771zdd_join_list([], 0):-!. 2772zdd_join_list([X|Xs], Y):- zdd_join_list(Xs, X, Y). 2773% 2774zdd_join_list([], X, X):-!. 2775zdd_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2776 zdd_join_list(As, X0, Y). 2777 2778% 2779ltr_join_list([], 0):-!. 2780ltr_join_list([X|Xs], Y):-ltr_join_list(Xs, X, Y). 2781% 2782ltr_join_list([], X, X):-!. 2783ltr_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2784 ltr_join_list(As, X0, Y). 2785 2786 2787 /********************* 2788 * remove atom * 2789 *********************/
2795% ?- ((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2796% sets(Y, Sy))). 2797zdd_remove(X, Y, Z, S):- setup_call_cleanup( 2798 open_state(M, [hash_size(256)]), 2799 zdd_remove(X, Y, Z, S, M), 2800 close_state(M)). 2801 2802zdd_remove(_, X, X, _, _):- X<2, !. 2803zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2804 ( nonvar(J) -> true 2805 ; cofact(I, t(Ai, Li, Ri), S), 2806 zdd_compare(C, A, Ai, S), 2807 ( C = (<) -> J = I 2808 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2809 zdd_remove(A, Ri, Ria, S, M), 2810 cofact(J, t(Ai, Lia, Ria), S) 2811 ; zdd_join(Li, Ri, J, S) 2812 ) 2813 ). 2814 2815% ?- ltr_X<< dnf(a->b), psa(X), 2816% use_table(pred_remove_atoms(negative_literal, X, Y)), psa(Y). 2817 2818% ?- ltr_X<< dnf(a->b->c), psa(X), 2819 2820negative_literal(-(_)). 2821 2822:- meta_predicate pred_remove_atoms(, , ). 2823 2824pred_remove_atoms(_, X, X):- X<2, !. 2825pred_remove_atoms(Pred, I, J):- 2826 cofact(I, t(A, L, R)), 2827 pred_remove_atoms(Pred, L, L0), 2828 pred_remove_atoms(Pred, R, R0), 2829 ( call(Pred, A) -> 2830 zdd_join(L0, R0, J) 2831 ; cofact(J, t(A, L0, R0)) 2832 ). 2833 2834 /********************* 2835 * Cardinality * 2836 *********************/
2841% ?-N = 10000, numlist(1, N, Ns), time((X<<pow(Ns), card(X, _C))), _C=:=2^N. 2842%@ % 1,222,118 inferences, 0.127 CPU in 0.161 seconds (79% CPU, 9587871 Lips) 2843%@ N = 10000, 2844%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2845%@ X = 10001. 2846 2847%@ % 1,204,213 inferences, 0.179 CPU in 0.220 seconds (82% CPU, 6710726 Lips) 2848%@ N = 10000, 2849%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2850%@ X = 10001. 2851 2852% ?- X<<{[a], [b]}, card(X, C). 2853% ?- N = 10000, numlist(1, N, Ns),time( (X<< pow(Ns), card(X, C))). 2854%@ % 1,222,117 inferences, 0.112 CPU in 0.127 seconds (89% CPU, 10886196 Lips) 2855%@ N = 10000, 2856%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2857%@ X = 10001, 2858 2859% ?- X<<card(pow([a,b]) + pow([c,d])). 2860%@ X = 7. 2861% ?- X<<card((+[a]) + (+[b])). 2862% ?- zdd. 2863% ?- X<<pow(numlist(1, 100)), card(X, D). 2864% ?- X<<pow(numlist(1, 100)), card(X, D), 2865% slim_gc(X, X1), slim_gc(X1, X2), slim_gc(X2, Y), 2866% card(Y, C). 2867%@ X = X1, X1 = X2, X2 = Y, Y = 101, 2868%@ D = C, C = 1267650600228229401496703205376. 2869 2870card(I, C):- open_memo(M), 2871 cardinality(I,C,M), 2872 close_memo(M). 2873% 2874cardinality(I, I, _):- I < 2, !. 2875cardinality(I, C, M):- memo(card(I)-C, M), 2876 ( nonvar(C) -> true 2877 ; cofact(I, t(_, L, R)), 2878 cardinality(R, Cr, M), 2879 cardinality(L, Cl, M), 2880 C is Cl + Cr 2881 ).
2885max_length(X, Max):- use_memo(max_length_with_memo(X, Max)). 2886 2887% 2888max_length_with_memo(X, 0):- X<2, !. 2889max_length_with_memo(X, Max):- 2890 memo(max(X)-Max), 2891 cofact(X, t(_, L, R)), 2892 ( nonvar(Max) -> true 2893 ; max_length_with_memo(L, ML), 2894 max_length_with_memo(R, MR), 2895 Max is max(1 + MR, ML) 2896 ). 2897 2898 /*********************** 2899 * Handy helpers * 2900 ***********************/ 2901 2902% 2903unify_zip([]). 2904unify_zip([X-X|R]):- unify_zip(R). 2905 2906 2907 /****************************************** 2908 * Oprations on clauses of literals * 2909 ******************************************/ 2910 2911% ?- ltr_compare(C, a, -a). 2912% ?- ltr_compare(C, -(a), a). 2913% ?- ltr_compare(C, -(b), a). 2914% ?- ltr_compare(C, -(a), b). 2915% ?- ltr_compare(C, -(a), -(b)). 2916% ?- ltr_compare(C, -(a), -(a)).
2923ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 2924ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 2925 ( C0 == (=) -> C =(<) 2926 ; C0 = C 2927 ). 2928ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 2929 ( C0 == (=) -> C = (>) 2930 ; C0 = C 2931 ). 2932ltr_compare(C, X, Y):- compare(C, X, Y). 2933 2934% ?- ltr_compare(C, a, b). 2935% ?- ltr_compare(C, -a, a). 2936% ?- ltr_compare(C, a, -a). 2937% ?- ltr_compare(C, -a, b). 2938% ltr_compare(C, X, Y):- get_compare(F, S), 2939% call(F, C, X, Y).
2944% ?- ltr_sort([b, b, a], X).
2945% ?- ltr_sort([-b, b,-b, -a], X).
2950ltr_sort(X, Y):- get_compare(F), predsort(F, X, Y). 2951 2952 2953% ?- ((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false 2954% ?- ((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))). 2955% 2956ltr_memberchk(L, Z):- ltr_sort(L, L0), 2957 ltr_ord_memberchk(L0, Z). 2958% 2959ltr_ord_memberchk([], Z):- !, zdd_has_1(Z). 2960ltr_ord_memberchk([A|As], Z):- Z > 1, 2961 cofact(Z, t(B, L, R)), 2962 ltr_compare(C, A, B), 2963 ( C = (=) -> ltr_ord_memberchk(As, R) 2964 ; ltr_ord_memberchk([A|As], L) 2965 ). 2966 2967% ?- call_with_time_limit(100, time(((big_normal_form(30, X), resolve(X))))). 2968% ?- big_normal_form(1, X), ltr_card(X, C). 2969% ?- big_normal_form(2, X), ltr_card(X, C). 2970% ?- big_normal_form(3, X), ltr_card(X, C). 2971% ?- big_normal_form(10, X), ltr_card(X, C). 2972% ?- big_normal_form(20, X), ltr_card(X, C). 2973% ?- time(((big_normal_form(100, X), ltr_card(X, C)))). 2974% ?- time(((big_normal_form(10, X), ltr_card(X, C)))). 2975% ?- N=100, time((big_normal_form(N, X), ltr_card(X, C))), C=:=2^N. 2976 2977big_normal_form(0, 1). 2978big_normal_form(N, X):- N>0, 2979 N0 is N-1, 2980 big_normal_form(N0, X0), 2981 ltr_insert(N, X0, R), 2982 ltr_insert(-N, X0, L), 2983 zdd_join(L, R, X). 2984 2985% ?- numlist(1, 3, Ns), ( ltr_X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 2986% ?- numlist(1, 20, Ns), (ltr_X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 2987% ?- ltr_X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y). 2988% ?- ltr_X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 2989% ltr_choices(Z, U), psa(X), psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V). 2990% ?- ltr_X<< {[a,b]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 2991% ?- ltr_X<< {[a,b,c]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 2992% ?- ltr_X<< {[a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 2993% ?- ltr_X<< {[], [a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 2994% ?- ltr_X<< {[a], [c, d]}, ltr_choices(X, Y), psa(Y). 2995% ?- ltr_X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y). 2996% ?- ltr_X<< {[a,b]}, ltr_choices(X, Y), psa(Y). 2997% ?- ltr_X<< {[]}, ltr_choices(X, Y), psa(Y). 2998% ?- ltr_cnf(a, X), ltr_choices(X, Y), psa(Y). 2999% ?- ltr_cnf(a*b, X), ltr_choices(X, Y), psa(Y). 3000% ?- ltr_cnf(a* (-a), X), ltr_choices(X, Y), psa(Y). 3001 3002% ?- N=10, numlist(2, 10, Ns), (ltr_sample_cnf(Ns, X), ltr_card(X, C)). 3003% ?- N=100, numlist(2, N, Ns), (ltr_sample_cnf(Ns, X), card(X, C), resolve(X)). 3004 3005sample_cnf([], 1). 3006sample_cnf([J|Js], X):- sample_cnf(Js, Y), 3007 ltr_insert(J, Y, Z), 3008 ltr_insert(-J, Y, U), 3009 ltr_join(Z, U, X).
3015accessible_indices(I, A):- zdd_vector(Vec), 3016 accessible_indices(I, A0, [], Vec), 3017 sort(A0, A). 3018 3019accessible_indices(I, A, A, _):- I<2, !. 3020accessible_indices(I, [I|A], B, Vec):- arg(I, Vec, X), 3021 ( atomic(X) -> B = A 3022 ; child_term_indices(X, A, B, Vec) 3023 ). 3024% 3025% child_term_indices(t(_, _, _), A, A, _):-!. 3026child_term_indices(X, A, B, Vec):- X =.. [_|Xs], 3027 child_term_indices_list(Xs, A, B, Vec). 3028% 3029child_term_indices_list([], A, A, _). 3030child_term_indices_list([I|Is], A, B, Vec):- 3031 accessible_indices(I, A, C, Vec), 3032 child_term_indices_list(Is, C, B, Vec). 3033 3034% test sat. PASSED. [2023/11/09] 3035% ?- sat. 3036% ?- sat(-true). % false 3037% ?- sat(a+b), sat_count(C). 3038% ?- sat(a), sat(b). 3039% ?- sat(-(a + -a)). % false 3040% ?- sat(a), sat(b), sat_count(C). 3041% ?- sat(or(a, b)), sat_count(C). 3042% ?- sat(b), sat_count(C). 3043% ?- sat(xor(a, b)), sat_count(C). 3044% ?- sat(exor(a, b)), sat_count(C). 3045% ?- sat(e_x_o_r(a, b)), sat_count(C). 3046% ?- sat(a), sat(-a). % false. 3047% ?- sat(a), sat(a+b), sat_count(C). 3048% ?- sat(a(1)+a(2)), sat_count(C). 3049% ?- sat(A+a(2)), sat_count(C). 3050% ?- sat(A + B), sat_count(C). 3051% ?- sat(a+b+c+d), sat_count(C). 3052% ?- sat(a+b), sat(c+d), sat_count(C). 3053% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 3054% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 3055% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false. 3056% ?- sat(*[p(1),p(2)]), sat_count(C). 3057% ?- sat(+[p(1),p(2)]), sat_count(C). 3058% ?- N=10, findall(p(I, J), 3059% (between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C). 3060% ?- N=10, findall(p(I, J), 3061% (between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C). 3062% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false 3063% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 3064% ?- sat(A + B), sat_count(C). 3065% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 3066% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 3067% ?- sat(a=<(b=<a)), sat_count(Count). 3068% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3069% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3070% ?- Prop = 3071% ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)), 3072% sat(Prop), sat_count(C). 3073% ?- sat(a+b), sat(b+c), b_getval(sat_state, S), 3074% get_key(root, R, S), ltr_card(R, C, S). 3075% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false 3076% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false 3077% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa. 3078% ?- sat(A=:=B), psa, sat(B=:=C), psa. 3079% ?- sat(a), sat(b), sat(c), sat_count(C). 3080% ?- Prop = 3081% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3082% sat(Prop), 3083% sat_count(Count). 3084% ?- sat, Prop = 3085% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3086% sat(-Prop), 3087% sat_count(Count). 3088 3089% ?- sat. 3090% ?- sat(A + B), sat_count(Count), A = B, sat_count(Count1). 3091% ?- sat(a), psa. 3092% ?- sat(a->(b->a)), sat(a->(b->a)), sat_count(C). 3093% ?- sat(A->(B->A)), sat(A->(B->A)), sat_count(C). 3094% ?- sat(a), sat(b), sat_count(C), psa. 3095% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3096% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3097% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3098% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3099% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3100% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C). 3101% ?- sat(a+b+c), sat_count(C). 3102% ?- sat(x=a+b), sat(y=a+b+b+a), sat(-(x=y)), sat_count(C). % false 3103% ?- sat(x=a+b), sat(y=a+b+b+a), sat((x=y)), sat_count(C). 3104 3105 /************************************ 3106 * Setting Modes: zdd/sat/ltr * 3107 ************************************/ 3108 3109 3110zdd:- open_state. 3111% 3112sat:- open_state, 3113 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3114 nb_linkval(zdd_compare, ltr_compare), 3115 nb_linkval(root, 1), 3116 open_memo(boole_atom, 32). 3117% 3118ltr:- open_state, 3119 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3120 nb_linkval(zdd_compare, ltr_compare), 3121 open_memo(boole_atom, 32). 3122 3123% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), ltr_card(X, C). 3124 3125% ?- sat, sat(X), sat(X\=Y), sat(Y). % fail. 3126% ?- sat, sat(X), sat(X\=Y), X=Y. % fail. 3127sat(X):- 3128 b_getval(root, Root), 3129 dnf(X, Y), 3130 ltr_merge(Y, Root, Root0), 3131 b_setval(root, Root0), 3132 Root0 \== 0. 3133% 3134sat_close:- close_state. 3135% 3136sat_count(C):- b_getval(root, X), ltr_card(X, C). 3137% 3138sat_clear:- close_state. 3139 3140% ?- sat, zdd_numbervars(f(X, Y, X)), get_attr(X, zsat, I), get_attr(Y, zsat, J). 3141zdd_numbervars(X):- get_key(varnum, N), 3142 term_variables(X, Vs), 3143 attr_numbervars(Vs, N, N0), 3144 set_key(varnum, N0). 3145 3146% 3147attr_numbervars([], N, N). 3148attr_numbervars([V|Vs], N, N0):- 3149 ( get_attr(V, zsat, _) -> 3150 attr_numbervars(Vs, N, N0) 3151 ; put_attr(V, zsat, N), 3152 K is N + 1, 3153 attr_numbervars(Vs, K, N0) 3154 ). 3155 3156% ?- heavy_valid_formula(H), prove(H). 3157heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10) 3158<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3159<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10) 3160<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3161<=> p2) <=> p1) <=> p0)). 3162 3163% ?- ltr. 3164% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y). 3165% ?- mk_left_assoc_term(=, 1, X), prove(X). 3166% ?- X<< {[a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3167% ?- X<< {[a,b],[b,c]}, ltr_merge(X, X, Z), psa(Z). 3168% ?- X<< {[a,b],[b,c]}, zdd_merge(X, X, Z), psa(Z). 3169% ?- X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3170% ?- run(1, 100). 3171% ?- run(2, 100). 3172% ?- run(5, 100). 3173% ?- run(1-9, 100). 3174% ?- run(11, 100). 3175% ?- run(12, 360). 3176%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips) 3177% imac 3178% on M1 mbp pro 32 GB, timeout. 3179 3180% ?- ltr, mk_left_assoc_term(==, 1, F), prove(F). 3181%@ VALID 3182%@ F = (((p(1)==p(0))==p(1))==p(0)). 3183run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3184 ( mk_left_assoc_term(==, K, F), 3185 format("~nPropositions: p(0) ... p(~w).~n", [K]), 3186 call_with_time_limit(T_limit, time(prove(F))))). 3187 3188% run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3189% ( mk_left_assoc_term(==, K, F), 3190% format("~nPropositions: p(0) ... p(~w).~n", [K]), 3191% call_with_time_limit(T_limit, time(seq:seq_prove(F))))). 3192% 3193run(N, T) :- run(N-N, T). 3194 3195% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X). 3196% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X). 3197 3198mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L), 3199 append(L, L, L2), 3200 reverse(L2, R), 3201 apply_left_assoc(Bop, R, Ex). 3202% 3203apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex). 3204% 3205apply_left_assoc(_, X, [], X):-!. 3206apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X], 3207 apply_left_assoc(Bop, V, Y, W). 3208 3209demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). 3210 3211% Valid formulae. 3212% ?- ltr. 3213% ?- forall(valid_formula(A), prove(A)). 3214valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)). 3215valid_formula((-(-a) -> a) * (a -> -(-a))). % Double Negation 3216valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3217valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b). 3218valid_formula(a + -a). 3219valid_formula(((a -> b) -> a) -> a). % Peirce’s Law 3220valid_formula(-(-a)->a). 3221valid_formula(a -> a). 3222valid_formula(a -> (b -> a)). 3223valid_formula((a->b)->((b->c)->(a->c))). 3224valid_formula(a->((a->b)->b)). 3225valid_formula((a*(a->b))->b). 3226valid_formula((a->b)->(-b -> -a)). 3227valid_formula((a->b)->((b->c)->(a->c))). 3228valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)). 3229 3230% ?- ltr. 3231% ?- forall(invalid_formula(A), prove(A)). 3232invalid_formula(a). 3233invalid_formula((a->b)->a). 3234invalid_formula((a->b)->(b->a)). 3235invalid_formula(a -> (b -> c)). 3236invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)). 3237invalid_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))).3268prove(X):- 3269 ( prove_(X) 3270 -> writeln('VALID') 3271 ; writeln('INVALID') 3272 ). 3273 3274% 3275prove_(X):- cnf(-X, CNF), 3276 get_key(atom_index, N), 3277 ( CNF = 0 -> N = 0 3278 ; CNF = 1 -> N > 0 3279 ; resolve(CNF) 3280 ).
3286% ?- ltr_ltr_pow([a,b,c], P), resolve(P), psa(P). 3287% ?- numlist(1, 10, L), (ltr_ltr_pow(L, P), ltr_card(P, C)). 3288% ?- numlist(1, 100, L), (ltr_ltr_pow(L, P), ltr_card(P, C)). 3289% ?- N = 100000, numlist(1, N, L), time( (ltr_ltr_pow(L, P), resolve(P))). 3290resolve(X):- zdd_has_1(X), !. % The empty clause found. 3291resolve(X):- X > 1, 3292 cofact(X, t(A, L, R)), 3293 ( L = 0 -> fail % Pure literal rule. 3294 ; A = -(_) -> resolve(L) % Negative pure literal rule. 3295 ; ( cofact(L, t(B, U, V)), % Pure literal rule. 3296 ( B = -(A) 3297 -> ltr_merge(V, R, M), % Resolution + Tautology rule. 3298 ltr_join(U, M, W), 3299 resolve(W) % Updated set of clauses. 3300 ; resolve(L) % Posituve pure literal rule. 3301 ) 3302 ) 3303 ). 3304 3305% ?- sat. 3306% ?- N=100, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3307%@ false. 3308% ?- N=2, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3309%% Debug. 3310% ?- N=11, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3311%@ false. <=== why ??? 3312 3313% ?- ltr. 3314% ?- N = 100, time((numlist(1, N, L), ltr_pow(L, P), 3315% A << set(L), zdd_subtr(P, A, Q), card(Q, C), 3316% writeln(C), resolve(Q))). % false 3317 3318% ?- N = 100000, time((numlist(1, N, _L), ltr_pow(_L, P), 3319% card(P, _C))), _C=:= 2^N. 3320 3321%@ % 31,011,164 inferences, 8.180 CPU in 12.708 seconds (64% CPU, 3790924 Lips) 3322%@ N = 100000, 3323%@ P = 300001. 3324 3325atom_index(X):- memo(atom_index(X)-Y), 3326 ( nonvar(Y) -> true 3327 ; get_key(atom_index, Y), 3328 memo(index_atom(Y)-X), 3329 Y0 is Y + 1, 3330 set_key(atom_index, Y0) 3331 ). 3332 3333% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_nnf_cnf(Y, Z), psa(Z)). 3334boole_nnf(X, Y):- % numbervars_index(X, S), 3335 basic_boole(X, Z), 3336 once(neg_normal(Z, Y)). 3337 3338% ?- ltr, basic_boole(a, A). 3339% ?- ltr, basic_boole(@(a), A). 3340% ?- ltr, basic_boole(0, A). 3341% ?- ltr, basic_boole(1, A). 3342% ?- ltr, basic_boole(true, A). 3343% ?- ltr, basic_boole(a+b, A). 3344% ?- ltr, basic_boole(a+b+c, A). 3345% ?- ltr, basic_boole(-a + b + c, A). 3346% ?- ltr, basic_boole(a -> b -> c, A). 3347% ?- ltr, basic_boole((a -> b) -> c, A). 3348% ?- ltr, basic_boole(*[(a -> b), c], A). 3349% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3350% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3351% ?- ltr, basic_boole(*[0, 1, 2], A). 3352 3353% ?- ltr. 3354% ?- trace. 3355% ?- ltr, set_key(f, 0), N = 100, numlist(0, N, Ns), 3356% test_rev_memo(Ns), test_rev_memo. 3357 3358test_rev_memo :- get_key(f, K), 3359 K0 is K - 1, 3360 forall(between(0, K0, I), 3361 ( memo(g(I)-R), 3362 ( nonvar(R), memo(f(R)-I) -> true 3363 ; writeln(not(memo(f(R)-I))) 3364 ) 3365 )). 3366 3367test_rev_memo([]). 3368test_rev_memo([A|As]):- memo(f(A)-B), 3369 ( var(B) -> 3370 get_key(f, B), 3371 memo(g(B)-A), 3372 B0 is B + 1, 3373 set_key(f, B0) 3374 ; true 3375 ), 3376 test_rev_memo(As). 3377 3378 3379% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3380% forall(member(I, Ns), (memo(atom_index(I)-A), writeln(atom_index(I)-A))). 3381 3382% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), b_getval(zdd_memo, M), 3383% arg(3, M, V), maplist(writeln, V). 3384 3385% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3386% b_getval(zdd_memo, #(_,_, V)), get_key(atom_index, AtomIndex), 3387% numlist(0, AtomIndex, Is), 3388% maplist(memo_index_atom, Is, As). 3389 3390% ?- listing(memo_index_atom). 3391 3392memo_index_atom(I, A):- memo(index_atom(I)-A). 3393 3394% ?- spy(atom_index). 3395% ?- ltr, N = 100, numlist(1, N, Ns), X<< dnf(+Ns), 3396% get_key(atom_index, K), K0 is K - 1, 3397% numlist(0, K0, Is), 3398% maplist(atom_index, As, Is, As). 3399 3400% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), zdd_boole_atoms(As), forall(between(1, N, J), 3401% once((memo(index_atom(J)-X, boole_atom), 3402% writeln(memo(index_atom(J)-X))))). 3403% 3404% ?- ltr, N = 100000, numlist(0, N, Ns), 3405% maplist(memo_atom, Ns, Is), 3406% maplist(memo_atom, Ns, Is). 3407 3408% ?- ltr, N = 83, numlist(0, N, Ns), 3409% maplist(memo_atom, Ns, Is), 3410% maplist(memo_atom, R, Is), 3411% memo_atom(86, K), memo_atom(87, L), 3412% maplist(memo_atom, U, Is), get_key(atom_index, A), 3413% memo_atom(30, B). 3414 3415% ?- ltr, N = 10000, numlist(0, N, As), 3416% maplist(atom_index, As, Is), 3417% maplist(atom_index, As0, Is), 3418% As = As0, 3419% atom_index(hello, I), 3420% atom_index(A, I). 3421 3422% ?- ltr, atom_index(X, 2). % false. 3423%@ atom_index(_346,2) 3424%@ true. 3425% ?- ltr, N=3, K=100, open_hash(N, H), nb_setval(zdd_memo, H), !, 3426% numlist(1, K, Ks), X<< dnf(+Ks). 3427 3428memo_atom(X):- atom_index(X, _). 3429 3430memo_atom(X, I):- atom_index(X, I). 3431 3432% 3433atom_index(X, I):- var(X), !, memo(index_atom(I)-X). 3434atom_index(X, I):- 3435 memo(atom_index(X)-I), 3436 ( var(I) -> 3437 get_key(atom_index, I), 3438 J is I + 1, 3439 set_key(atom_index, J), 3440 memo(index_atom(I)-X) 3441 ; true 3442 ). 3443 3444% ?- sat. 3445% ?- sat(A=B), sat(B=C), sat_count(D). 3446basic_boole(A, @('$VAR'(I))):-var(A), !, get_attr(A, zsat, I), 3447 memo_atom('$VAR'(I)). 3448basic_boole(A, BoolConst):-atomic(A), 3449 boole_op(0, [], Fs, BoolConst), 3450 memberchk(A, Fs), 3451 !. 3452basic_boole(I, @(I)):- integer(I), !, memo_atom(I). 3453basic_boole(@(I), @(I)):-!, memo_atom(I). 3454basic_boole(*(L), F):-!, basic_boole_vector(L, *, F). 3455basic_boole(+(L), F):-!, basic_boole_vector(L, +, F). 3456basic_boole(X, Y):- X=..[F|Xs], 3457 length(Xs, N), 3458 boole_op(N, As, Fs, Y), 3459 memberchk(F, Fs), 3460 !, 3461 basic_boole_list(Xs, As). 3462basic_boole(X, @(X)):- memo_atom(X). 3463 3464% 3465basic_boole_list([], []). 3466basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y), 3467 basic_boole_list(Xs, Ys). 3468% 3469basic_boole_vector([], +, false):-!. 3470basic_boole_vector([], *, true):-!. 3471basic_boole_vector([X|Xs], F, Y):- 3472 basic_boole(X, X0), 3473 Y=..[F, X0, Z], 3474 basic_boole_vector(Xs, F, Z). 3475 3476% Remark [2023/11/13]: 3477% Use of 0/1 as Boolean constants has been dropped. 3478% Any integer is now usable for a boolean variable, which 3479% may be useful or (nested) vectors of integers *[...], +[...]. 3480% 0/1 as boolean is error prone because ZDD must use 0/1 internally 3481% as basic constant similar, but not exactly the same, 3482% to true/flase. They are different. 3483% This decision was hard because 0/1 is traditionally useful 3484% as boolean constrants, but clear separation and simplicity 3485% were preferred. 3486 3487boole_op(0, [], [false, ff], false). % 0 for false dropped. 3488boole_op(0, [], [true, tt], true). % 1 for true dropped. 3489boole_op(1, [X], [-, ~, \+, not], -(X)). 3490boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y). 3491boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y). 3492boole_op(2, [X, Y], [->, imply], -X + Y). 3493boole_op(2, [X, Y], [<-], Y->X). 3494boole_op(2, [X, Y], [iff, ==, =, =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y). 3495boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)). % -(X==Y) = xor(X, Y) 3496boole_op(2, [X, Y], [nand], -(X) + (-Y)). 3497 3498 3499% ?- neg_normal(-(true + b), X). 3500% ?- neg_normal(-(a), X). 3501% ?- neg_normal(-(a), X). 3502% ?- neg_normal(-(a), X). 3503neg_normal(true, true). 3504neg_normal(false, false). 3505neg_normal(-(false), true). 3506neg_normal(-(true), false). 3507neg_normal(-(-X), Z) :- neg_normal(X, Z). 3508neg_normal(-(X+Y), Z) :- neg_normal(-X* -Y, Z). 3509neg_normal(-(X*Y), Z) :- neg_normal(-X+ -Y, Z). 3510neg_normal(-(X), -(Y)) :- neg_normal(X, Y). 3511neg_normal(X+Y, X0+Y0) :- neg_normal(X, X0), 3512 neg_normal(Y, Y0). 3513neg_normal(X*Y, X0*Y0) :- neg_normal(X, X0), 3514 neg_normal(Y, Y0). 3515neg_normal(@(X), @(X)):-!. 3516neg_normal(X, @(X)):-!.
intern(-(a;b;c), X), boole_to_dnf(X, Z), sets(Z, U), extern(U, Y)).3525extern(X, Y):-integer(X), !, 3526 ( X < 2 -> Y = X 3527 ; memo(index_atom(X)-Y) 3528 ). 3529extern(X, X):- atomic(X), !. 3530extern(X, Y):- X =.. [F|Xs], 3531 extern_list(Xs, Ys), 3532 Y =..[F|Ys]. 3533% 3534extern_list([], []). 3535extern_list([X|Xs], [Y|Ys]):- extern(X, Y), 3536 extern_list(Xs, Ys). 3537 3538 /********************************************* 3539 * Cofact/insert/join/merge on literals * 3540 *********************************************/
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 ).3555ltr_cofact(Z, Y):- nonvar(Z), !, cofact(Z, Y). 3556ltr_cofact(Z, t(A, V, U)):- U > 1, !, 3557 cofact(U, t(B, L, _)), 3558 ( ltr_invert(A, B) 3559 -> ltr_cofact(Z, t(A, V, L)) 3560 ; cofact(Z, t(A, V, U)) 3561 ). 3562ltr_cofact(Z, T):- cofact(Z, T).
3571% ?- ltr. 3572% PASS. 3573% ?- cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S). 3574 3575% ?- ltr. 3576% ?- dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S). 3577% ?- ltr_insert(a, 1, X), sets(X, S). 3578% ?- ltr_insert(a, 1, X), ltr_insert(b, X, Y), sets(Y, S). 3579% ?- ltr_insert(a, 1, X), ltr_insert(b, X, Y), 3580% ltr_insert(-b, Y, Z), sets(Z, S). 3581% ?- X<<set([a]), ltr_insert(b, X, Y), psa(Y). 3582% ?- X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3583% ?- X<<set([b]), ltr_insert(a, X, Y), psa(Y). 3584% ?- X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3585% ?- X<<set([-a]), ltr_insert(a, X, Y), psa(Y))). 3586% ?- X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y). 3587% ?- X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y). 3588% ?- X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y). 3589% ?- X<<{[a]}, ltr_insert(a, X, Y), psa(Y). 3590% ?- X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y). 3591% ?- X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y). 3592% ?- X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y). 3593% ?- X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y). 3594% ?- X<< dnf(a), ltr_insert(b, X, Y), psa(Y). 3595% ?- X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y). 3596% ?- X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y). 3597% ?- X<< dnf((x=\=y)*x*y), psa(X). 3598% ?- X<< dnf((x=\=y)*x*y), psa(X). 3599% ?- sat((x=\=y)*x*y). % false 3600% ?- sat((a * -a)). % false 3601% ?- dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y). 3602% ?- dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y). 3603% ?- dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y). 3604% ?- dnf((-a)*b, X), psa(X). 3605% ?- cnf((-a)*b, X). 3606% ?- cnf((a), X). 3607 3608ltr_insert(_, 0, 0):-!. 3609ltr_insert(A, 1, J):-!, zdd_singleton(A, J). 3610ltr_insert(A, I, J):- memo(ltr_insert(A,I)-J), 3611 ( nonvar(J) -> true 3612 ; cofact(I, t(B, L, R)), 3613 zdd_compare(C, A, B), 3614 ( C = (<) -> 3615 ( complementary(A, B) -> 3616 cofact(J, t(A, 0, L)) 3617 ; cofact(J, t(A, 0, I)) 3618 ) 3619 ; C = (=) -> 3620 ( negative(A) -> 3621 ltr_join(L, R, K), 3622 cofact(J, t(A, 0, K)) 3623 ; ltr_insert_aux(J, A, L, R) 3624 ) 3625 ; ( complementary(A, B) -> ltr_insert(A, L, J) 3626 ; ltr_insert(A, L, L0), 3627 ltr_insert(A, R, R0), 3628 cofact(J, t(B, L0, R0)) 3629 ) 3630 ) 3631 ). 3632 3633% for suppressing use of cofact/3 and ltr_insert/4 3634ltr_insert_aux(J, A, L, R):- % A is positive. R has no -A. 3635 ( L < 2 -> cofact(J, t(A, L, R)) 3636 ; cofact(L, t(B, L0, _)), 3637 ( complementary(A, B)-> 3638 ltr_join(L0, R, K), 3639 cofact(J, t(A, 0, K)) 3640 ; ltr_join(L, R, K), 3641 cofact(J, t(A, 0, K)) 3642 ) 3643 ).
3649% 3650ltr_join(X, X, X):-!. % idemopotent law of logical disjunction (OR) 3651ltr_join(0, X, X):-!. 3652ltr_join(X, 0, X):-!. 3653ltr_join(1, _, 1):-!. 3654ltr_join(_, 1, 1):-!. 3655ltr_join(X, Y, Z):- 3656 ( X=<Y -> memo(ltr_join(X,Y)-Z) 3657 ; memo(ltr_join(Y,X)-Z) 3658 ), 3659 ( nonvar(Z) -> true %, write(.) 3660 ; cofact(X, t(A, L, R)), 3661 cofact(Y, t(A0, L0, R0)), 3662 zdd_compare(C, A, A0), 3663 ( C = (=) -> 3664 ltr_join(R, R0, U), 3665 ltr_join(L, L0, V), 3666 cofact(Z, t(A, V, U)) 3667 ; C = (<) -> 3668 ltr_join(L, Y, U), 3669 cofact(Z, t(A, U, R)) 3670 ; ltr_join(L0, X, U), 3671 cofact(Z, t(A0, U, R0)) 3672 ) 3673 ).
3682ltr_merge(X, X, X):-!. % idempotent law of logical conjunction (AND). 3683ltr_merge(0, _, 0):-!. 3684ltr_merge(_, 0, 0):-!. 3685ltr_merge(1, X, X):-!. 3686ltr_merge(X, 1, X):-!. 3687ltr_merge(X, Y, Z):- 3688 ( X =< Y -> memo(ltr_merge(X,Y)-Z) 3689 ; memo(ltr_merge(Y,X)-Z) 3690 ), 3691 ( nonvar(Z) -> true 3692 ; cofact(Y, t(A, L, R)), 3693 ltr_merge(X, R, U), 3694 ltr_merge(X, L, V), 3695 ltr_insert(A, U, U0), 3696 ltr_join(V, U0, Z) 3697 ).
xor(X, Y) = X*-Y + -X*Y.
?- X<<dnf(a+b), Y<<dnf(b+c), ltr_xor(X, Y, Z), psa(Z), ltr_card(Z, C).
?- Z<< dnf((a+b)=\=(b+c)), psa(Z), ltr_card(Z, C).3704ltr_xor(X, Y, Z):- 3705 ltr_negate(Y, Y0), 3706 ltr_merge(X, Y0, U), 3707 ltr_negate(X, X0), 3708 ltr_merge(X0, Y, V), 3709 ltr_join(U, V, Z). 3710 3711 /****************************************** 3712 * Auxiliary operations on literals * 3713 ******************************************/
3717complementary(-(A), A):-!. 3718complementary(A, -(A)). 3719% 3720negative(-(_)).
3728% ?- ltr_pow([a], X), card(X, C), psa(X). 3729% ?- ltr_pow([a, b], X), card(X, C), psa(X). 3730% ?- numlist(1, 100, L), ltr_pow(L, X), card(X, C). 3731ltr_pow([], 1). 3732ltr_pow([A|As], P):- ltr_pow(As, Q), 3733 ltr_insert(A, Q, R), 3734 ltr_insert(-A, Q, L), 3735 ltr_join(L, R, P).
3743% ?- ltr_append([-b, a, -d, c], 1, X), psa(X). 3744% ?- ltr_append([-b, -d, c], 1, X), psa(X). 3745% ?- ltr_append([-b, -d, c], 1, X), psa(X). 3746% ?- X<<dnf(a->a), ltr_card(X, C), psa(X). 3747% 3748ltr_append([], X, X). 3749ltr_append([A|As], X, Y):- ltr_append(As, X, X0), 3750 ltr_insert(A, X0, Y).
ltr_append(X, 1, Y, S).
?- X<<(ltr_set([a])+ltr_set([b])), psa(X))).
?- X<<(ltr_set([-a])+ltr_set([b])), psa(X))).
?- X<<(ltr_set([-a])+ltr_set([a])), psa(X))).3758% 3759ltr_set(X, Y):- ltr_append(X, 1, Y).
3766% ?- ((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))). 3767% ?- ((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))). 3768% ?- ((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))). 3769% ?- ((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3770% ?- ((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3771 3772% ?- X<<dnf(a), ltr_negate(X, Y), psa(Y). 3773% ?- ltr_negate(0, Y), psa(Y). 3774% ?- ltr_negate(1, Y), psa(Y). 3775 3776% 3777ltr_negate(X, Y):- ltr_complement(X, X0), ltr_choices(X0, Y).
3786% ?- zdd, X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y). 3787% ?- zdd, X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y). 3788% 3789ltr_complement(X, X):- X<2, !. 3790ltr_complement(I, Y):- memo(ltr_complement(I)-Y), 3791 ( nonvar(Y) -> true 3792 ; cofact(I, t(A, L, R)), 3793 ltr_complement(L, L0), 3794 ltr_complement(R, R0), 3795 complementary(A, NA), 3796 ltr_insert(NA, R0, R1), 3797 ltr_join(L0, R1, Y) 3798 ). 3799 3800 /************************************ 3801 * Convert Boolean Form to DNF/CNF * 3802 ************************************/
3807% ?- boole_nnf(-(a+b), X). 3808% ?- zdd, dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V). 3809% ?- ((dnf(-(a=:=b), X), psa(X))). 3810% ?- ((dnf((a=\=b), X), psa(X))). 3811% ?- ((dnf((0), X), psa(X))). 3812% ?- ((dnf(*[1,3,2,3], X), psa(X))). 3813% ?- zdd, dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I). 3814% ?- ((dnf(*[@(1),3,2,3], X), psa(X))). 3815 3816dnf(X, Y):- zdd_numbervars(X), 3817 boole_nnf(X, Z), 3818 nnf_dnf(Z, Y).
3827% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y). 3828% ?- X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U). 3829% ?- big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D). 3830 3831dnf_cnf(X, Y):- nonvar(X), !, ltr_choices(X, Y). 3832dnf_cnf(X, Y):- ltr_choices(Y, X). 3833% 3834cnf_dnf(X, Y):- dnf_cnf(X, Y). 3835 3836% ?- X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y). 3837%@ * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug 3838% ?- X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y). 3839% ?- X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y). 3840% ?- X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3841% ?- X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y). 3842% ?- X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 3843% ?- X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y). 3844% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3845% dnf_cnf(Z, Y), psa(X), psa(Y). 3846 3847% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3848% dnf_cnf(Z, Y), psa(X), psa(Y). 3849 3850% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 3851% dnf_cnf(Z, Y). 3852 3853% ?- X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), 3854% dnf_cnf(Z, U). 3855 3856% ?- N=100, time((big_normal_form(N, X), 3857% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3858%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips) 3859%@ N = 100, 3860%@ X = 39901, 3861%@ Y = D, D = 0, % <== CORRECT. 3862%@ C = 1267650600228229401496703205376 . 3863 3864% ?- N=1000, time((big_normal_form(N, X), 3865% dnf_cnf(Y, X), card(X, C), card(Y, D))). 3866%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips) 3867%@ N = 1000, 3868%@ X = 3999001, 3869%@ Y = D, D = 0, % <== CORRECT. 3870%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
3884ltr_choices(0, 1):-!. 3885ltr_choices(1, 0):-!. 3886ltr_choices(X, Y):- memo(ltr_choices(X)-Y), 3887 ( nonvar(Y)->true %, write(.) % many hits. 3888 ; cofact(X, t(A, L, R)), 3889 ltr_choices(L, L0), 3890 ltr_choices(R, R0), 3891 cofact(R1, t(A, R0, 1)), 3892 ltr_merge(L0, R1, Y) 3893 ).
3898nnf_dnf(false * _, 0):-!. 3899nnf_dnf(_ * false, 0):-!. 3900nnf_dnf(true * X, Y):-!, nnf_dnf(X, Y). 3901nnf_dnf(X * true, Y):-!, nnf_dnf(X, Y). 3902nnf_dnf(X * Y, Z):-!, memo(dnf(X*Y)-Z, boole_atom), 3903 ( nonvar(Z) -> true 3904 ; nnf_dnf(X, U), 3905 nnf_dnf(Y, V), 3906 ltr_merge(U, V, Z) 3907 ). 3908nnf_dnf(false + X, Y):-!, nnf_dnf(X, Y). 3909nnf_dnf(X + false, Y):-!, nnf_dnf(X, Y). 3910nnf_dnf(true + X, Y):-!, nnf_dnf(X, Z), 3911 ltr_join(1, Z, Y). 3912nnf_dnf(X + true, Y):-!, nnf_dnf(X, Z), 3913 ltr_join(1, Z, Y). 3914nnf_dnf(X + Y, Z):-!, memo(dnf(X+Y)-Z, boole_atom), 3915 ( nonvar(Z) -> true 3916 ; nnf_dnf(X, U), 3917 nnf_dnf(Y, V), 3918 ltr_join(U, V, Z) 3919 ). 3920nnf_dnf(@(X), I):-!, zdd_singleton(X, I). 3921nnf_dnf(-(@(X)), I):- zdd_singleton(-(X), I).
3928% ?- ltr. 3929% ?- ((cnf(a, X), S<<sets(X))). 3930% ?- ((cnf(a*b, X), S<<sets(X))). 3931% ?- ((X<<cnf(-a), Y<<sets(X))). 3932% ?- ((X<<cnf(a+b), Y<<sets(X))). 3933% ?- ((X<<cnf(+([a,b,c])), Y<<sets(X))). 3934% ?- ((X<<cnf(*([a,b,c])), Y<<sets(X))). 3935% ?- ((X<<dnf(+([a,b,c])), Y<<sets(X))). 3936% ?- ((X<<dnf(*([a,b,c])), Y<<sets(X))). 3937% ?- ((cnf(a, X), psa(X))). 3938% ?- ((cnf(-a, X), psa(X))). 3939% ?- ((cnf(a+b, X), psa(X))). 3940% ?- ((cnf(a+b+(-c), X), psa(X))). 3941% ?- ((cnf(-a * a, X), psa(X))). 3942% ?- ((cnf(a->a, X), psa(X))). 3943% ?- ((cnf(-a * a, X), psa(X))). 3944% ?- ((cnf( a + a, X), psa(X))). 3945% ?- ((cnf( A + A, X), psa(X))). 3946% ?- ((cnf(-(a*b), X), psa(X))). 3947% ?- ((cnf(*([a,b,c]), X), psa(X))). 3948% ?- ltr, N = 10, numlist(2, N, Ns), cnf(*(Ns), X), ltr_card(X, C). 3949% ?- ((dnf(a, X), psa(X))). 3950% ?- ((cnf(-(a->b), X), psa(X))). 3951% ?- ((cnf(a, X), psa(X))). 3952% ?- boole_nnf(-(*[0,1,2]), X). 3953% ?- ltr, mk_left_assoc_term(==, 1, F), cnf(F, X), psa(X). 3954 3955cnf(X, Y):- zdd_numbervars(X), 3956 boole_nnf(X, Z), 3957 nnf_cnf(Z, Y). 3958% 3959nnf_cnf(true, 1):-!. 3960nnf_cnf(false, 0):-!. 3961nnf_cnf(false * _, 0):-!. 3962nnf_cnf(_ * false, 0):-!. 3963nnf_cnf(true * X, Y):-!, nnf_cnf(X, Y). 3964nnf_cnf(X * true, Y):-!, nnf_cnf(X, Y). 3965nnf_cnf(X * X, Y):-!, nnf_cnf(X, Y). 3966nnf_cnf(X * Y, Z):-!, memo(cnf(X*Y)-Z, boole_atom), 3967 ( nonvar(Z)->true %, write(.) % many hits. 3968 ; nnf_cnf(X, U), 3969 nnf_cnf(Y, V), 3970 ltr_join(U, V, Z) 3971 ). 3972nnf_cnf(false + X, Y):-!, nnf_cnf(X, Y). 3973nnf_cnf(X + false, Y):-!, nnf_cnf(X, Y). 3974nnf_cnf(true + _, 1):-!. 3975nnf_cnf(_ + true, 1):-!. 3976nnf_cnf(X + X, Y):-!, nnf_cnf(X, Y). 3977nnf_cnf(X + Y, Z):-!, memo(cnf(X+Y)-Z, boole_atom), 3978 ( nonvar(Z)->true %, write(+) % many hits. 3979 ; nnf_cnf(X, U), 3980 nnf_cnf(Y, V), 3981 ltr_merge(U, V, Z) 3982 ). 3983nnf_cnf(@(X), I):-!, zdd_singleton(X, I). 3984nnf_cnf(-(@(X)), I):- zdd_singleton(-(X), I). 3985 3986 3987 /***************************************************** 3988 * ltr_card/[3,4] Counting solutions of a DNF. * 3989 *****************************************************/ 3990 3991% ?- sat(a), sat_count(C). 3992% ?- sat(A+B), sat_count(C), zsat:(A=B), sat_count(D). 3993% ?- sat(A+B), sat_count(C), A = B, sat_count(D). 3994% ?- X<< dnf(a), sat_count_by_collect_atoms(X, C). 3995% ?- sat_count_by_collect_atoms(a+b, C). 3996% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C). 3997% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 3998 3999% ?- sat. 4000% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 4001% 4002sat_count_by_collect_atoms(F, C):- dnf(F, X), 4003 zdd_boole_atoms(Us), 4004 zdd_sort(Us, Vs), 4005 expand_dnf(Vs, X, Y), 4006 card(Y, C). 4007 4008% ?- ltr, N=100, numlist(0, N, Ns), X<<dnf(+Ns), zdd_boole_atoms(Us). 4009%@ N = 100, 4010%@ Ns = Us, Us = [0, 1, 2, 3, 4, 5, 6, 7, 8|...], 4011%@ X = 202. 4012 4013zdd_boole_atoms(Us):- get_key(atom_index, N), 4014 collect_boole_atoms(0, N, Us). 4015 4016% 4017collect_boole_atoms(I, N, []):- I>=N, !. 4018collect_boole_atoms(I, N, [A|U]):- 4019 atom_index(A, I), 4020 J is I+1, 4021 collect_boole_atoms(J, N, U). 4022 4023 /****************************** 4024 * find_counter_example * 4025 ******************************/
4029% ?- findall_counter_examples(a, X), psa(X). 4030% ?- findall_counter_examples((a->b)->a, X), psa(X). 4031% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4032% ?- findall_counter_examples(a->b, X), psa(X). 4033% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4034% ?- findall_counter_examples(a->b, Out), psa(Out). 4035findall_counter_examples(In, Out):- 4036 ltr_fetch_state, 4037 dnf(In, InZ), 4038 zdd_boole_atoms(Us), 4039 zdd_sort(Us, Vs), 4040 expand_prefix_dnf(Vs, 1, All), 4041 expand_dnf(Vs, InZ, Y), 4042 zdd_subtr(All, Y, Out).
4049% ?- ltr. 4050% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4051% ?- X<< dnf(a), psa(X), ltr_card(X, C). 4052% ?- X<< dnf(a->a), ltr_card(X, C). 4053% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4054% ?- ltr, X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C). 4055 4056% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4057% time((X<< dnf(+Ps), ltr_card(X, C))). 4058 4059 4060%@ % 123,881 inferences, 0.833 CPU in 1.321 seconds (63% CPU, 148761 Lips) 4061%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4062%@ X = 80, 4063%@ C = 1099511627775. 4064 4065%@ % 123,882 inferences, 0.010 CPU in 0.010 seconds (97% CPU, 12260689 Lips) 4066%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4067%@ X = 80, 4068%@ C = 1099511627775. 4069 4070% ?- ltr, findall(p(J), between(1, 30, J), Ps), 4071% time((X<< dnf(+Ps), ltr_card(X, C))). 4072% ?- ltr, numlist(1, 30, Ps), time((X<< dnf(+Ps), ltr_card(X, C))). 4073% ?- sat, numlist(1, 30, Ps), sat(+Ps), sat_count(C). 4074 4075% ?- spy(ltr_card). 4076% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4077% time((X<< dnf(+Ps), ltr_card(X, C))). 4078 4079% ?- findall(p(J), between(1, 100, J), Ps), 4080% time((X<< dnf(*Ps), ltr_card(X, C))). 4081 4082% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps). 4083% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4084% time((X<< dnf(+Ps),ltr_card(X, C))), 4085% C =:= 2^1000 - 1. 4086 4087% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4088% time((X<< dnf(+Ps), card(X, C))). 4089 4090ltr_card(In, Out):- 4091 zdd_boole_atoms(Us), 4092 zdd_sort(Us, Vs), 4093 expand_dnf(Vs, In, Y), 4094 card(Y, Out). 4095 4096% ?- ltr_var(-(5), X). 4097ltr_var(-(V), V):-!. 4098ltr_var(V, V).
4105% ?- ltr, X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y). 4106% ?- ltr, X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), ltr_card(Y, C). 4107% ?- ltr, X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C). 4108% ?- ltr, X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y). 4109% ?- ltr, X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4110% ?- ltr, X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4111% ?- ltr, X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4112 4113expand_dnf([], X, X):-!. 4114expand_dnf(_, 0, 0):-!. 4115expand_dnf(Vs, 1, Y):-!, expand_prefix_dnf(Vs, 1, Y). 4116expand_dnf(Vs, X, Y):- memo(expand_dnf(X,Vs)-Y), 4117 ( nonvar(Y) -> true %, write(.) % Many hits. 4118 ; cofact(X, t(A, L, R)), 4119 ltr_var(A, K), 4120 divide_ord_list(Vs, K, [], Us, Ws), 4121 expand_dnf(Us, R, R0), 4122 ltr_insert(A, R0, R1), 4123 expand_left_dnf(K, Us, L, L0), 4124 ltr_join(L0, R1, X0), 4125 expand_prefix_dnf(Ws, X0, Y) 4126 ).
divide_ord_list([a,b,c,d,e], c, [u], T, W).
?- divide_ord_list([a,b,c, d], e, [], X, Y). % false4134divide_ord_list([V|Vs], V, Us, Vs, Us):-!. 4135divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U), 4136 divide_ord_list(Vs, U, [V|Us], Ws, Ps).
4144% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))). 4145expand_prefix_dnf(Vs, X, Y):- zdd_sort(Vs, OrdVs), 4146 expand_ord_prefix_dnf(OrdVs, X, Y). 4147 4148% 4149expand_ord_prefix_dnf([], X, X):-!. 4150expand_ord_prefix_dnf([V|Vs], X, Y):- 4151 expand_ord_prefix_dnf(Vs, X, X0), 4152 ltr_insert(V, X0, X1), 4153 ltr_insert(-V, X0, X2), 4154 ltr_join(X1, X2, Y).
4164expand_left_dnf(_, _, 0, 0):-!. 4165expand_left_dnf(K, Us, 1, Y):-!, expand_prefix_dnf([K|Us], 1, Y). 4166expand_left_dnf(K, Us, X, Y):- cofact(X, t(A, L, R)), 4167 ltr_var(A, J), 4168 ( K = J -> 4169 expand_dnf(Us, R, R0), 4170 ltr_insert(A, R0, R1) 4171 ; divide_ord_list([K|Us], J, [], Vs, Ws), 4172 expand_dnf(Vs, R, R0), 4173 ltr_insert(A, R0, Q), 4174 expand_prefix_dnf(Ws, Q, R1) 4175 ), 4176 expand_dnf([K|Us], L, L0), 4177 ltr_join(L0, R1, Y). 4178 4179 /******************************* 4180 * Filter on cardinality * 4181 *******************************/
4187% ?- zdd, ((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))). 4188card_filter_gte(0, X, X):- !. % gte: greater than or equal 4189card_filter_gte(1, X, Y):- !, zdd_subtr(X, 1, Y). 4190card_filter_gte(_, X, 0):- X<2, !. 4191card_filter_gte(N, X, Y):- memo(filter_gte(N,X)-Y), 4192 ( nonvar(Y) -> true % many hits. 4193 ; cofact(X, t(A, L, R)), 4194 N0 is N - 1, 4195 card_filter_gte(N, L, L0), 4196 card_filter_gte(N0, R, R0), 4197 cofact(Y, t(A, L0, R0)) 4198 ).
4204% ?- X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y). 4205card_filter_lte(0, X, Y):- % lte: less than or equal 4206 ( zdd_has_1(X) -> Y = 1 4207 ; Y = 0 4208 ). 4209card_filter_lte(_, X, X):- X<2, !. 4210card_filter_lte(N, X, Y):- memo(filter_lte(N,X)-Y), 4211 ( nonvar(Y) -> true % many hits. 4212 ; cofact(X, t(A, L, R)), 4213 N0 is N - 1, 4214 card_filter_lte(N, L, L0), 4215 card_filter_lte(N0, R, R0), 4216 cofact(Y, t(A, L0, R0)) 4217 ).
time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))).4223card_filter_between(I, J, X, Y):- 4224 card_filter_gte(I, X, Z), 4225 card_filter_lte(J, Z, Y). 4226 4227% ?- time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))). 4228card_filter_between_by_meet(I, J, X, Y):- 4229 card_filter_gte(I, X, Z), 4230 card_filter_lte(J, X, U), 4231 zdd_meet(Z, U, Y). 4232 4233 4234 /********************************************************* 4235 * Solve boolean equations and verify the solution * 4236 *********************************************************/ 4237% Recovered [2023/11/14] 4238%! dnf_subst(+V, +T, +X, -Y) is det. 4239% Y is the ZDD obtained by substituting each 4240% occurrence of atom V in X with T. 4241 4242% ?-X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4243% ?-X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4244% ?-X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4245 4246dnf_subst(_, _, X, X):- X < 2, !. 4247dnf_subst(V, D, X, Y):- 4248 cofact(X, t(A, L, R)), 4249 dnf_subst(V, D, L, L0), 4250 once( A = -(U); U = A ), 4251 ltr_compare(C, V, U), 4252 ( C = (<) -> Y = X 4253 ; ( C = (=) -> 4254 ( A = (-V) -> 4255 ltr_negate(D, D0), 4256 ltr_merge(D0, R, R0) 4257 ; A = V -> 4258 ltr_merge(D, R, R0) 4259 ) 4260 ; dnf_subst(V, D, R, R1), 4261 ltr_insert(A, R1, R0) 4262 ), 4263 ltr_join(L0, R0, Y) 4264 ).
4272% exists x s.t. C0*(L,-x) + C1*x = 1 4273% if and only if 4274% C0 + C1 = 1 satisfiable 4275% x = a*C1 + (-C0). 4276 4277% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S). 4278% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S). 4279% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S). 4280 4281solve_boole_with_check(Exp, Xs, Ps):- 4282 dnf(Exp, E), 4283 solve_boolean_equations(E, Xs, Ps, Sols), 4284 eliminate_variables(E, Sols, Cond), 4285 !, 4286 dnf_valid_check(Cond). 4287 4288% ?- E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), 4289% solutions_to_sets(Sols, Sols0). 4290% ?- E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0). 4291 4292solve_boolean_equations(_, [], _, []):-!. 4293solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols]):- 4294 solve_boolean_equations_basic(E, X, A, Sol0, E0), 4295 solve_boolean_equations(E0, Xs, As, Sols), 4296 dnf_subst_list(Sols, Sol0, Sol). 4297% ?- E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond). 4298solve_boolean_equations_basic(E, X, A, Sol, Cond):- 4299 dnf_subst(X, 1, E, C1), 4300 dnf_subst(X, 0, E, C0), 4301 ltr_join(C0, C0, Cond), 4302 ltr_negate(C0, NC0), 4303 ltr_insert(A, C1, AC1), 4304 ltr_join(NC0, AC1, Sol). 4305% 4306dnf_subst_list([], E, E). 4307dnf_subst_list([X=A|Eqs], E, F):- 4308 dnf_subst(X, A, E, E0), 4309 dnf_subst_list(Eqs, E0, F). 4310% 4311solutions_to_sets([], []). 4312solutions_to_sets([X = E|Sols], [X = E0|Sols0]):- 4313 sets(E, E0), 4314 solutions_to_sets(Sols, Sols0). 4315 4316% ?- 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). 4317 4318% ?- 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). 4319 4320% ?- 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). 4321 4322eliminate_variables(Exp, Eqns, Cond):- 4323 apply_subst_list(Eqns, Exp, Cond). 4324% 4325apply_subst_list([], E, E). 4326apply_subst_list([X=U|Eqns], E, E0):- 4327 dnf_subst(X, U, E, E1), 4328 dnf_subst_list(Eqns, E1, E0). 4329% 4330dnf_valid_check(X):- 4331 ltr_atoms_by_scan(X, As), 4332 ltr_sort(As, Bs), 4333 expand_dnf(Bs, X, Y), 4334 card(Y, C), 4335 length(Bs, N), 4336 ( C =:= (1<< N) -> writeln('Solved and Verified.') 4337 ; writeln('Solved but NOT verified.') 4338 ). 4339 4340% ?- ltr. 4341% ?- X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), sort(As, Bs). 4342 4343ltr_atoms_by_scan(X, []):- X<2, !. 4344ltr_atoms_by_scan(X, P):- memo(ltr_atoms(X)-P), 4345 ( nonvar(P) -> true 4346 ; cofact(X, t(A, L, R)), 4347 ltr_atoms_by_scan(L, Al), 4348 ltr_atoms_by_scan(R, Ar), 4349 ltr_var(A, A0), 4350 union([A0|Al], Ar, P) 4351 ). 4352 4353 /********************************* 4354 * operations on reducible zdd * 4355 *********************************/
4361% ?- numlist(1, 100, Ns), X<<pow(Ns), card(X, C). 4362% ?- bdd_sort_append([c, a, b,c], 1, Z), psa(Z). 4363bdd_sort_append(X, Y, Z):- zdd_sort(X, X0), 4364 bdd_append(X0, Y, Z). 4365 4366% ?- zdd, bdd_append([x, a, y, b], 1, Y), psa(Y). 4367% ?- zdd, bdd_append([x, a, y, b], 0, Y), psa(Y). 4368% ?- zdd, bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z). 4369 4370bdd_append([], Z, Z). 4371bdd_append([X|Y], Z, U):- 4372 bdd_append(Y, Z, Z0), 4373 bdd_cons(U, X, Z0). 4374 4375% ?- zdd, bdd_list([b, b], Y), bdd_sort_append([b,b], Y, Z), psa(Z). 4376% ?- zdd, bdd_list([b, b], Y), bdd_list(X, Y). 4377bdd_list(List, X):- var(X), !, bdd_append(List, 1, X). 4378bdd_list(List, X):- get_bdd_list(X, List). 4379 4380% ?- zdd, bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L). 4381% ?- zdd, bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L). 4382get_bdd_list(1, []):-!. 4383get_bdd_list(X, [A|As]):- X>1, bdd_cons(X, A, X0), 4384 get_bdd_list(X0, As). 4385 4386% ?- zdd, bdd_append([a,a,b,b], 1, X), 4387% bdd_append([1,1,2,2], 1, Y), 4388% bdd_zip(X, Y, Z), psa(Z). 4389bdd_zip(0, _, 0):-!. 4390bdd_zip(_, 0, 0):-!. 4391bdd_zip(1, _, 1):-!. 4392bdd_zip(_, 1, 1):-!. 4393bdd_zip(X, Y, Z):- bdd_cons(X, A, X0), 4394 bdd_cons(Y, B, Y0), 4395 bdd_zip(X0, Y0, Z0), 4396 bdd_cons(Z, A-B, Z0). 4397 4398% ?- zdd, bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y). 4399bdd_normal(X, X):- X<2, !. 4400bdd_normal(X, Y):- cofact(X, t(A, L, R)), 4401 bdd_normal(L, L0), 4402 bdd_normal(R, R1), 4403 zdd_insert(A, R1, R0), 4404 zdd_join(L0, R0, Y). 4405 4406% ?- zdd, bdd_append([a,b,a,b], 1, X), 4407% bdd_append([a,b, c, a,b, c], 1, Y), 4408% bdd_append([b, a, b, a, a,b ], 1, Z), 4409% bdd_list_normal([X, Y, Z], R), psa(R). 4410 4411bdd_list_normal([], 0). 4412bdd_list_normal([A|As], R):- bdd_list_normal(As, R0), 4413 bdd_normal(A, A0), 4414 zdd_join(A0, R0, R). 4415 4416% 4417bdd_insert(_, 0, 0):-!. 4418bdd_insert(A, 1, X):-!, zdd_singleton(A, X). 4419bdd_insert(A, X, Y):- cofact(X, t(B, L, R)), 4420 bdd_insert(A, L, L0), 4421 bdd_append([A,B], R, R0), 4422 zdd_join(L0, R0, Y).
4431% ?- bdd_list_raise([], 0, X). 4432% ?- bdd_list_raise([a], 0, X). 4433% ?- bdd_list_raise([a], 1, X), psa(X). 4434% ?- bdd_list_raise([a,b], 1, X), psa(X). 4435% ?- N = 1, numlist(1, N, Ns), bdd_list_raise(Ns, N, X), card(X, C). 4436 4437% ?- zdd, N = 15, numlist(1, N, Ns), bdd_list_raise(Ns, N, X),card(X, C). 4438bdd_list_raise(_, 0, 1):-!. 4439bdd_list_raise(L, N, X):- N0 is N-1, 4440 bdd_list_raise(L, N0, X0), 4441 bdd_map_insert(L, X0, X). 4442% 4443bdd_map_insert([], _, 0). 4444bdd_map_insert([A|As], X, Y):- 4445 bdd_insert(A, X, X0), 4446 bdd_map_insert(As, X, Y0), 4447 zdd_join(X0, Y0, Y). 4448 4449% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert, 4450% also work for bddered zdd. 4451 4452% ?- zdd, X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U), 4453% psa(X), psa(Y), psa(Z), psa(U). 4454% ?- zdd, X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z), 4455% psa(Z, S), card(Z, C). 4456% ?- zdd, numlist(1, 10, Ns), X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4457% card(Z, C). 4458% ?- zdd, numlist(1, 10, Ns), X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z), 4459% card(Z, C), card(X, D). 4460 4461bdd_merge(0, _, 0):-!. 4462bdd_merge(_, 0, 0):-!. 4463bdd_merge(1, X, X):-!. 4464bdd_merge(X, 1, X):-!. 4465bdd_merge(X, Y, Z):- memo(bdd_merge(X, Y)-Z), 4466 ( nonvar(Z) -> true % , write(.) % So so frequently hits. 4467 ; cofact(X, t(A, L, R)), 4468 bdd_merge(L, Y, L0), 4469 bdd_merge(R, Y, R1), 4470 bdd_cons(R0, A, R1), 4471 zdd_join(L0, R0, Z) 4472 ). 4473 4474 /**************n*************************** 4475 * Interleave bddered atoms in BDD * 4476 ******************************************/
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.4485% ?- X<< +[*[a,b], *[x,y]], Y<< +[*[1]], 4486% bdd_interleave(X, Y, Z), psa(Z). 4487% ?- zdd, X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z). 4488% ?- zdd, X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z). 4489 4490bdd_interleave(0, _, 0):-!. 4491bdd_interleave(_, 0, 0):-!. 4492bdd_interleave(1, X, X):-!. 4493bdd_interleave(X, 1, X):-!. 4494bdd_interleave(X, Y, Z):- % memo is useless here. 4495 cofact(Y, t(B, L, R)), 4496 ( L < 2 -> L0 = 0 4497 ; bdd_interleave(X, L, L0) 4498 ), 4499 bdd_interleave(X, B, R, R0), 4500 zdd_join(L0, R0, Z). 4501% 4502bdd_interleave(0, _, _, 0):-!. 4503bdd_interleave(1, B, Y, Z):-!, cofact(Z, t(B, 0, Y)). 4504bdd_interleave(X, B, Y, Z):- memo(merge(X, Y, B)-Z), 4505 ( nonvar(Z) -> true % , write(+) % many hits. 4506 ; cofact(X, t(A, L, R)), 4507 ( L < 2 -> L0 = 0 4508 ; bdd_interleave(L, B, Y, L0) 4509 ), 4510 bdd_interleave(A, R, B, Y, R0), 4511 zdd_join(L0, R0, Z) 4512 ). 4513% 4514bdd_interleave(A, X, B, Y, Z):- % memo is useless here. 4515 bdd_interleave(X, B, Y, U), 4516 cofact(Z0, t(A, 0, U)), 4517 bdd_interleave(Y, A, X, V), 4518 cofact(Z1, t(B, 0, V)), 4519 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.4528% ?- zdd, bdd_funs(mono([1,2]-[a,b])*mono([3,4]-[c,d]), X), psa(X). 4529% ?- zdd, bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), psa(X). 4530% ?- zdd, bdd_funs(mono([1,2]-[a,b])&mono([3,4]-[c,d]), X), 4531% zdd_normalize(X, Y), psa(Y). 4532 4533bdd_funs(A*B, F):-!, bdd_funs(A, A0), 4534 bdd_funs(B, B0), 4535 bdd_merge(A0, B0, F). 4536bdd_funs(A&B, F):-!, bdd_funs(A, A0), 4537 bdd_funs(B, B0), 4538 bdd_interleave(A0, B0, F). 4539bdd_funs(A, F):- fun_block(A, F). 4540 4541 /************** 4542 * misc * 4543 **************/
4548% ?- numlist(1, 100, Ns), (zdd, X<<pow(Ns), zdd_flatten(X, Y), psa(Y)). 4549zdd_flatten(X, 0):- X<2, !. 4550zdd_flatten(X, Y):- memo(flatten(X)-Y), 4551 ( nonvar(Y) -> true % Many hits. 4552 ; cofact(X, t(A, L, R)), 4553 zdd_flatten(L, L0), 4554 zdd_flatten(R, R0), 4555 zdd_join(L0, R0, Y0), 4556 cofact(Y, t(A, Y0, 1)) 4557 )