1:- module(zmod, 2 [ (<<)/2, zdd/0, zdd_eval/2, zdd_eval/3, ltr/0 3 , setup_zdd/1, call_with_zdd/2 4 , ltr_join/3, ltr_join_list/2, ltr_join_list/3 5 , ltr_merge/3, card/2, ltr_card/2 6 , card_filter_gte/3, card_filter_lte/3 7 , card_filter_between/4 8 , max_length/2 9 , sat/0, sat/1, sat_count/1 10 , set_at/2 11 , obj_id/2 12 , dnf/2, cnf/2, nnf_dnf/2, nnf_cnf/2 13 , all_fun/3 14 , all_mono/3, all_epi/3, merge_funs/2 15 , bdd_list/2, bdd_list_raise/3, bdd_append/3, bdd_interleave/3 16 , zdd_div_by_list/3 17 , opp_compare/3 18 , bdd_sort_append/3, bdd_append/3 19 , zdd_insert/3, zdd_insert/4, zdd_insert_atoms/3 20 , bdd_cons/3 21 , l_cons/3 22 , zdd_insert_atoms/3 23 , zdd_ord_insert/3, zdd_reorder/3 24 , zdd_has_1/1 25 , zdd_memberchk/2 26 , zdd_family/2 27 , zdd_subfamily/2 28 , zdd_join/3, zdd_join_1/2, zdd_join_list/2, zdd_singleton/2 29 , zdd_dict_join/3 30 , zdd_merge/3, zdd_disjoint_merge/3, zdd_linear_merge/3 31 , zdd_merge_list/3 32 , zdd_meet/3 33 , zdd_subtr/3, zdd_subtr_1/2, zdd_xor/3 34 , zdd_div/3, zdd_mod/3, zdd_divmod/4, zdd_div_div/4 35 , zdd_divisible_by_list/3 36 , zdd_power/2, zdd_ord_power/3 37 , zdd_rand_path/1, zdd_rand_path/2, zdd_rand_path/3 38 , ltr_meet_filter/3, ltr_join_filter/3 39 , get_key/2, atom_index/1 40 , set_key/2, update_key/3 41 , set_pred/2, zdd_compare/3 42 , zdd_sort/2 43 , open_key/2, close_key/1 44 , set_compare/1, get_compare/1 45 , map_zdd/3, zdd_find/3 46 , psa/0, psa/1, psa/2, mp/2 47 , sets/2, ppoly/1, poly_term/2 48 , eqns/2 49 , zdd_list/2 50 , significant_length/3 51 , charlist/2, charlist/3, atomlist/2 52 , op(900, xfx, <<) 53 ]). 54 55 56% ?- listing(zdd). 57% ?- zdd. 58% ?- N = 10000, numlist(1, N, Ns), time(((X<<pow(Ns), card(X, _C)))), _C=:=2^N. 59% :- doc_server(7000). 60% :- use_module(library(pldoc/doc_library)). 61% :- doc_load_library. 62% :- doc_browser. 63 64:- use_module(library(apply)). 65:- use_module(library(apply_macros)). 66:- use_module(library(clpfd)). 67:- use_module(library(statistics)). 68:- use_module(zdd('zdd-array')). 69:- use_module(util(math)). 70:- use_module(util(meta2)). 71:- use_module(pac(basic)). 72:- use_module(pac(meta)). 73:- use_module(util(misc)). 74:- use_module(pac('expand-pac')). % For the kind block. 75:- use_module(pac(op)). 76:- use_module(zdd('frontier-vector')). 77:- use_module(zdd(zsat)). 78 79:- set_prolog_flag(stack_limit, 10_200_147_483_648). 80:- nb_setval(default_zdd_mode, zdd). 81 82% :- initialization(activate_zdd). % choices: zdd/ltr/sat 83activate_zdd:- b_getval(default_zdd_mode, Mode), 84 call(Mode), 85 format( 86 "\n%\s~w mode activated. 87%\sCurrently available modes: zdd/ltr/sat\n", [Mode]). 88 89attr_unify_hook(V, Y):- 90 ( get_attr(Y, zdd, A) 91 -> zdd_unify(V, A) 92 ; zdd_unify(V, Y) 93 ). 94 95 :- op(800, xfy, &). 96 :- op(820, fy, \). % NOT 97 :- op(830, xfy, /\). % AND 98 :- op(840, xfy, \/). % OR 99 :- op(860, xfy, ~). % equivalence 100 :- op(860, xfy, #). % exor 101 :- op(860, xfy, <->). % equivalence 102 :- op(860, xfy, <=> ). % equivalence 103 :- op(870, yfx, <-). 104 105% for pac query. 106term_expansion --> pac:expand_pac. 107 108% ?- zdd. 109% ?- numlist(1, 2, Ns), Y<<pow(Ns), card(Y, C). 110% ?- set_memo(a-1), set_memo(a-2), memo(a-V). 111% ?- X<<{[1,1]}, psa(X). 112% ?- X<< *[ *a, *a, *b,*c], psa(X). 113% ?- set_key(root, hello), get_key(root, R). 114% ?- all_fun([a],[b], F), psa(F). 115% ?- all_fun([],[b], F), psa(F). 116% ?- all_fun([a],[], F), psa(F). 117% ?- all_fun([a,b],[c,d], F), psa(F), card(F, C). 118% ?- N = 3, numlist(1, N, A), raise_list(A, 2, A2), all_fun(A2, A, F), card(F, C). 119% ?- N = 20, numlist(1, N, A), raise_list(A, 2, A2), all_fun(A2, A, F), card(F, C). % take a time while. 120 121% ?- call_with_time_limit(30, 122% time((N=100, M=100, numlist(1, N, Ns), numlist(1, M, Ms), 123% all_fun(Ns, Ms, F), card(F, C)))). 124 125% Cardinality # of Y^X = { f | f: X-> Y }. 126% ({1,...,K}^L)^({1,...,I}^J) = (K^L)^(I^J). 127 128% ?- I=1, J=1, K=1, L=1, 129% numlist(1, I, X), numlist(1, K, Y), 130% raise_list(X, J, Xj), 131% raise_list(Y, L, Yl), 132% call_with_time_limit(200, time((all_fun(Xj, Yl, F), card(F, C)))), 133% C =:= (K^L)^(I^J), 134% significant_length(C, Keta, 10). 135 136% ?- I=3, J=5, K=3, L=5, 137% numlist(1, I, X), numlist(1, K, Y), 138% raise_list(X, J, Xj), 139% raise_list(Y, L, Yl), 140% call_with_time_limit(360, time( 141% (all_fun(Xj, Yl, F), card(F, C)))), 142% C =:= (K^L)^(I^J), 143% significant_length(C, Keta, 10). 144%@ % 684,820,387 inferences, 220.323 CPU in 274.688 seconds (80% CPU, 3108250 Lips) 145%@ I = K, K = 3, 146%@ J = L, L = 5, 147%@ X = Y, Y = [1, 2, 3], 148%@ Xj = Yl, Yl = [[1, 1, 1, 1, 1], [1, 1, 1, 1, 2], [1, 1, 1, 1, 3], [1, 1, 1, 2, 1], [1, 1, 1, 2|...], [1, 1, 1|...], [1, 1|...], [1|...], [...|...]|...], 149%@ F = 7204222, 150%@ C = ... 151%@ Keta = 580. 152 153% ?- significant_length(020, X, 10). 154significant_length(0, 0, _):-!. 155significant_length(X, 1, Radix):- X < Radix, !. 156significant_length(X, L, Radix):- Y is X // Radix, 157 significant_length(Y, L0, Radix), 158 L is L0+1. 159 160% 161zdd_atom(X):- get_key(is_atom, Pred), !, call(Pred, X). 162zdd_atom(X):- (atomic(X); dvar(X)), !.
obj_id([a,b,c], Id), obj_id(Obj, Id).167obj_id(X, Id):- cofact(Id, t(X, 0, 1)). 168% 169hyphen(X, Y, X-Y). 170comma(X, Y, (X,Y)). 171equality(X, Y, (X=Y)). 172dvar('$VAR'(_)). 173 174 /***************************************** 175 * all_fun/all_mono/all_epi in ZDD * 176 *****************************************/
180% ?- all_fun([a, b, c],[1,2,3], F), card(F, C), psa(F). 181% ?- all_fun([a, b, c, d, e], [1,2,3, 4], F), card(F, C). 182% ?- N = 100, numlist(1, N, Ns), all_fun(Ns, Ns, F), card(F, C). 183% ?- numlist(1, 5, Ns), numlist(6, 10, Ms), 184% all_fun(Ns, Ns, F), 185% all_fun(Ms, Ms, G), 186% zdd_merge(F, G, H), 187% card(H, C), 188% C =:= 5^5 * 5^5. 189 190all_fun(D, R, F):- zdd_sort(D, D0), 191 zdd_sort(R, R0), 192 length(D0, I), 193 length(R0, J), 194 ( I > 0, J = 0 -> F = 0 195 ; bdd_sort_append(D0, 1, D1), 196 findall_fun(D1, R0, F) 197 ). 198% 199findall_fun(X, _, X):- X < 2, !. 200findall_fun(X, Rng, Y):- memo(findall_fun(X)-Y), 201 ( nonvar(Y) -> true % , write(.) % many hits. 202 ; cofact(X, t(A, L, R)), 203 findall_fun(L, Rng, L0), 204 findall_fun(R, Rng, R1), 205 join_for_alt_val(A, Rng, R1, 0, R0), 206 zdd_join(L0, R0, Y) 207 ). 208% 209join_for_alt_val(_, [], _, V, V). 210join_for_alt_val(A, [B|Bs], F, F0, F1):- 211 bdd_cons(F2, A-B, F), 212 zdd_join(F0, F2, F3), 213 join_for_alt_val(A, Bs, F, F3, F1).
218% ?- all_mono([1],[a], Is), psa(Is). 219% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 220% ?- all_mono([1,2],[a,b,c], Is), psa(Is). 221% ?- all_mono([1,2,3],[a,b,c], Is), psa(Is), card(Is, C). 222% ?- all_mono([1,2,3,4],[a,b,c,d], Is), card(Is, C). 223% ?- time((numlist(1, 10, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(10, C))). 224% ?- time((numlist(1, 12, Ns), all_mono(Ns, Ns, F), card(F, C))). 225% ?- N =10, numlist(1, N, Ns), all_mono(Ns, Ns, F), card(F, C), factorial(N, C). 226 227all_mono(D, R, F):- zdd_sort(D, D0), 228 zdd_sort(R, R0), 229 length(D0, I), 230 length(R0, J), 231 ( I @=< J -> 232 bdd_sort_append(D0, 1, D1), 233 findall_mono(D1, R0, F) 234 ; F = 0 235 ). 236 237% ?- bdd_sort_append([], 1, X), findall_mono(X, [a], Y). 238% ?- bdd_sort_append([1], 1, X), psa(X), findall_mono(X, [a], Y), psa(Y). 239% ?- N=14, numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 240% findall_mono(X, Ns, Y), card(Y, C), 241% factorial(14, D), ( D=:=C -> writeln("*** OK ***")). 242 243findall_mono(X, _, X):- X < 2, !. 244findall_mono(X, Rng, Y):- memo(findall_mono(X,Rng)-Y), 245 ( nonvar(Y) -> true % , write(.) % many hits. 246 ; cofact(X, t(A, L, R)), 247 findall_mono(L, Rng, L0), 248 findall_mono(A, R, Rng, R0), 249 zdd_join(L0, R0, Y) 250 ). 251% 252findall_mono(A, R, Rng, R0):- findall(B-U, select(B, Rng, U), Cases), 253 findall_mono(Cases, A, R, 0, R0). 254% 255findall_mono([], _A, _R, V, V). 256findall_mono([B-Rng|Cases], A, R, U, V):- 257 findall_mono(R, Rng, U0), 258 cofact(U1, t(A-B, 0, U0)), 259 zdd_join(U, U1, U2), 260 findall_mono(Cases, A, R, U2, V).
266% ?- all_epi([],[], F). 267% ?- all_epi([a],[1], F), psa(F). 268% ?- all_epi([a,b],[1], F), psa(F). 269% ?- all_epi([a],[1,2], F), psa(F). 270% ?- all_epi([a,b,c],[1,2], F), psa(F). 271% ?- numlist(1, 10, Ns), numlist(1, 8, Ms), (all_epi(Ns, Ms, F)). 272% ?- call_with_time_limit(10, time(( numlist(1, 10, Ns), numlist(1, 10, Ms), (all_epi(Ns, Ms, F))))). 273 274all_epi(D, R, F):- 275 zdd_sort(D, D0), 276 zdd_sort(R, R0), 277 length(D0, I), length(R0, J), 278 ( I @>= J -> 279 bdd_sort_append(D0, 1, D1), 280 findall_epi(D1, R0-R0, F) 281 ; F = 0 282 ).
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).302% ?- N=11, numlist(1, N, Ns), findall(X, permutation(Ns, X), R), 303% length(R, L). 304 305all_perm(D, P):- zdd_sort(D, D0), 306 findall_perm(D0, P). 307% 308findall_perm([], 1):-!. 309findall_perm(D, X):- memo(perm(D)-X), 310 ( nonvar(X) -> true % , write(.) % many hits. 311 ; 312 findall(I-D0, select(I, D, D0), U), 313 join_perm_for_selection(U, 0, X)). 314% 315join_perm_for_selection([], X, X). 316join_perm_for_selection([I-D|U], X, Y):- 317 findall_perm(D, X0), 318 bdd_cons(X1, I, X0), 319 zdd_join(X1, X, X2), 320 join_perm_for_selection(U, X2, Y). 321 322 /************************************************* 323 * terms in based on families of lists * 324 *************************************************/
332% ?- coalgebra_for_signature([x], [f/1], [x], E), psa(E). 333% ?- coalgebra_for_signature([x,y], [f/1,g/2], [x,y,1], E), psa(E). 334% ?- time((coalgebra_for_signature([x,y,z,u,v], [f/2,g/2,h/2], 335% [x,y,z,u,v,0,1], E), card(E, C))). 336%@ % 10,326,853 inferences, 1.231 CPU in 1.259 seconds (98% CPU, 8391804 Lips) 337%@ E = 173825, 338%@ C = 68641485507. 339 340coalgebra_for_signature(D, Sgn, As, E):- 341 signature(Sgn, As, T), 342 signature_map(D, T, E). 343% 344signature_map([], _, 1):-!. 345signature_map([X|Xs], T, E):- 346 signature_map(Xs, T, E0), 347 extend_signature_map(X, T, E0, E). 348% 349extend_signature_map(_, 0, _, 0):-!. 350extend_signature_map(_, 1, E, E):-!. 351extend_signature_map(X, T, E, F):- cofact(T, t(A, L, _)), 352 extend_signature_map(X, L, E, E0), 353 l_cons(X->A, E, E1), 354 zdd_join(E0, E1, F).
359% ?- term_path(a, R), psa(R), term_path(A, R). 360term_path(X, Y):- 361 ( nonvar(X) -> term_to_path(X, Y) 362 ; path_to_term(Y, X) 363 ).
368% ?- term_to_path(a, R), psa(R). 369% ?- term_to_path(f(a, b), R), psa(R). 370% ?- term_to_path(f(g(a, b), h(c, d)), R), psa(R). 371% ?- term_to_path(f(g(k(a), j(b)), h(0, 1)), R), psa(R). 372term_to_path(X, Y):- functor(X, F, N), 373 ( N = 0 -> zdd_singleton(X, Y) 374 ; functor(X, F, N), 375 arg_path(F/N, 1, X, Y) 376 ). 377% 378arg_path(_/N, J, _, 0):- J>N, !. 379arg_path(F, I, X, Y):- J is I + 1, 380 arg(I, X, A), 381 term_to_path(A, U), 382 arg_path(F, J, X, V), 383 cofact(Y, t(arg(F, I), V, U)).
389% ?- term_to_path(a, X), path_to_term(X, R). 390% ?- term_to_path(f(h(a), g(b), 3), X), path_to_term(X, R). 391% ?- term_to_path(f(1,2), X), path_to_term(X, R). 392% ?- T=f(h(a), 3, g(b,2), 5), 393% (term_to_path(T, X), path_to_term(X, R)), T = R. 394 395path_to_term(X, Y):- X>1, cofact(X, t(A, L, R)), 396 ( R = 1 -> Y = A 397 ; A = arg(F/_, _), 398 path_to_term(R, R0), 399 path_to_term(L, L0, []), 400 Y =..[F, R0|L0] 401 ). 402% 403path_to_term(X, U, U):- X<2, !. 404path_to_term(X, [R0|U], V):- cofact(X, t(_, L, R)), 405 path_to_term(R, R0), 406 path_to_term(L, U, V).
compare(C, U, V) is performed.413% ?- X=f(a,b), Y=f(a,b, c), (term_path(X, T), term_path(Y, U), 414% term_path_compare(C0, T, U)), compare(C, X, Y). 415% ?- X=g(a,b), Y=f(a,b, c), (term_path(X, T), term_path(Y, U), 416% term_path_compare(C0, T, U)), compare(C, X, Y). 417% ?- X=g(a,b,c), Y=f(a,b), (term_path(X, T), term_path(Y, U), 418% term_path_compare(C0, T, U)), compare(C, X, Y). 419 420term_path_compare(=, X, X):-!. 421term_path_compare(<, 0, _):-!. 422term_path_compare(>, _, 0):-!. 423term_path_compare(<, 1, _):-!. 424term_path_compare(>, _, 1):-!. 425term_path_compare(C, X, Y):- cofact(X, t(A, L, R)), 426 cofact(Y, t(B, L0, R0)), 427 arity_compare(C0, A, B), 428 ( C0 = (=) -> 429 term_path_compare(C1, R, R0), 430 ( C1 = (=) -> 431 left_branch_compare(C, L, L0) 432 ; C = C0 433 ) 434 ; C = C0 435 ). 436 437% Left branches are for argument lists of the name length. 438left_branch_compare(=, 0, 0):-!. 439left_branch_compare(C, X, Y):- 440 cofact(X, t(_, L, R)), 441 cofact(Y, t(_, L0, R0)), 442 term_path_compare(C0, R, R0), 443 ( C0 = (=) -> 444 left_branch_compare(C, L, L0) 445 ; C = C0 446 ). 447 448% 449arity_compare(C, arg(F/N,_), arg(G/K, _)):-!, compare(C, N/F, K/G). 450arity_compare(C, A, B):-!, compare(C, A, B).
456% ?- zdd_lift(1, X). 457% ?- X<< pow([1,2]), zdd_lift(X, Y), card(Y, D), psa(Y). 458% ?- X<< pow(numlist(1,10)), psa(X), card(X, C), zdd_lift(X, Y), card(Y, D). 459% ?- N=16, numlist(1, N, Ns), 460% time((X<< pow(Ns), zdd_lift(X, Y), card(Y, D))), D=:=2^N. 461%@ % 19,643,341 inferences, 31.553 CPU in 31.694 seconds (100% CPU, 622559 Lips) 462 463zdd_lift(X, X):- X<2, !. 464zdd_lift(X, Y):- memo(zdd_lift(X)-Y), 465 ( nonvar(Y) -> true %, write(.) % So so hits. 466 ; cofact(X, t(A, L, R)), 467 zdd_lift(L, L0), 468 zdd_lift(R, R0), 469 zdd_lift(A, R0, R1), 470 zdd_join(L0, R1, Y) 471 ). 472% 473zdd_lift(_, 0, 0):-!. 474zdd_lift(A, 1, Y):-!, zdd_singleton([A], Y). 475zdd_lift(A, X, Y):- cofact(X, t(B, L, _)), 476 zdd_singleton([A|B], R0), 477 zdd_lift(A, L, L0), 478 zdd_join(L0, R0, Y).
484% ?- X<< pow([a,b]), card(X, C), zdd_univ(X, Y), psa(Y). 485% ?- X<< pow([a,b]), zdd_univ(X, Y), psa(Y). 486 487zdd_univ(X, X):- X<2, !. 488zdd_univ(X, Y):- cofact(X, t(A, L, R)), 489 zdd_univ(R, [A], R0), 490 zdd_univ(L, L0), 491 zdd_join(L0, R0, Y). 492 493% ?- X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 494% ?- X<< {[a,b], [a,c,d]}, zdd_univ(X, [], R), psa(R). 495 496zdd_univ(0, _, 0):-!. 497zdd_univ(1, Stack, X):-!, reverse(Stack, Stack0), 498 U =.. Stack0, 499 zdd_singleton(U, X). 500zdd_univ(X, Stack, Y):- cofact(X, t(A, L, R)), 501 zdd_univ(L, Stack, L0), 502 zdd_univ(R, [A|Stack], R0), 503 zdd_join(L0, R0, Y).
g(a1, ..., an)
where G=g/n and ai in As.509% ?- arity_term(f/2, [1, x, y], T), psa(T). 510arity_term(F/N, As, T):- memo((F/N)-T), 511 ( nonvar(T) -> true 512 ; all_list(N, As, X), 513 l_cons(F, X, T0), 514 zdd_univ(T0, [], T) 515 ).
523% ?- N=10, numlist(1, N, Ns), 524% time((X<<pow(Ns), zdd_functor(f, X, Y), card(Y, C))). 525% ?- X<<pow([a,b]), zdd_functor(f, X, Y), psa(Y). 526% ?- N=100, numlist(1, N, Ns), 527% time((X<<pow(Ns), l_cons(f, X, Y), card(Y, C))). 528% ?- N=10, numlist(1, N, Ns), 529% time((X<<pow(Ns), zdd_mul_list([f, g, h], X, Y), card(Y, C))). 530 531zdd_functor(F, X, Y):- zdd_functor(F, X, [], Y). 532% 533zdd_functor(_, 0, _, 0):-!. 534zdd_functor(F, 1, St, Y):-!, T =..[F|St], 535 zdd_singleton(T, Y). 536zdd_functor(F, X, St, Y):-cofact(X, t(A, L, R)), 537 zdd_functor(F, L, St, Y0), 538 zdd_functor(F, R, [A|St], Y1), 539 zdd_join(Y0, Y1, Y).
f(a1, ..., an)
with f/n in G and ai in As.545% ?- signature([f/1, g/2], [1, x, y], U), psa(U). 546% ?- time((signature([f/2, g/2, h/3, i/4, k/5], 547% [0, 1, 2, x, y, z, u, v, w], U), card(U, C))). 548 549signature([], _, 0):-!. 550signature([G|Gs], As, T):- 551 arity_term(G, As, T0), 552 signature(Gs, As, T1), 553 zdd_join(T0, T1, T).
559% ?- spy(power_list). 560% ?- power_list(0, [a,b], P). 561% ?- power_list(1, [a,b], P). 562% ?- N = 100, numlist(1, N, _Ns), 563% time(((power_list(N, _Ns, X), card(X, _Count)))), 564% _Count > 100^100, writeln(_Count). 565%@ % 29,681,962 inferences, 2.735 CPU in 2.917 seconds (94% CPU, 10853693 Lips) 566%@ 101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101 567%@ N = 100, 568%@ X = 515002. 569 570power_list(N, As, P):- obj_id(As, Id), 571 power_list_with_id(N, Id, P). 572% 573power_list_with_id(0, Id, 1):-!, memo(power_list(0, Id)-1). 574power_list_with_id(N, Id, Y):- 575 N0 is N - 1, 576 power_list_with_id(N0, Id, Y0), 577 all_list_with_id(N, Id, Y1), 578 zdd_join(Y0, Y1, Y).
584% ?- all_list(0, [a], X), psa(X). 585% ?- all_list(1, [a], X), psa(X). 586% ?- N=10, numlist(1, N, Ns), (all_list(4, Ns, X), card(X, C)). 587% ?- N=100, numlist(1, N, Ns), time(((all_list(100, Ns, X), card(X, C)))). 588%@ % 29,015,728 inferences, 2.464 CPU in 2.553 seconds (97% CPU, 11774994 Lips) 589 590all_list(N, As, Y):- obj_id(As, Id), 591 all_list_with_id(N, Id, Y). 592% 593all_list_with_id(0, Id, 1):-!, memo(all_list(0, Id)-1). 594all_list_with_id(N, Id, Y):- memo(all_list(N, Id)-Y), 595 ( nonvar(Y) -> true 596 ; N0 is N-1, 597 all_list_with_id(N0, Id, Y0), 598 obj_id(As, Id), 599 zdd_mul_list(As, Y0, 0, Y) 600 ).
605singleton_family([], 0):-!. 606singleton_family([A|As], X):- 607 singleton_family(As, X0), 608 zdd_singleton(A, U), 609 zdd_join(U, X0, X).
614distribute_con(F, X, Y):- zdd_mul_list(F, X, 0, Y). 615% 616zdd_mul_list([], _, Y, Y). 617zdd_mul_list([A|As], Y, U, V):- 618 l_cons(A, Y, V0), 619 zdd_join(U, V0, U0), 620 zdd_mul_list(As, Y, U0, V).
625% ?- X<<pow([1,2]), l_cons(a, X, Y), psa(Y). 626 627l_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).634l_append([], X, X). 635l_append([A|As], X, Y):- 636 l_append(As, X, X0), 637 l_cons(A, X0, Y). 638 639% ?- bdd_sort_append([], 1, X), findall_epi(X, [a]-[a], Y). 640% ?- bdd_sort_append([a], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 641% ?- bdd_sort_append([a,b], 1, X), findall_epi(X, [1]-[1], Y), card(Y, C). 642% ?- bdd_sort_append([a,b], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C). 643% ?- bdd_sort_append([a,b, c], 1, X), findall_epi(X, [1,2]-[1,2], Y), card(Y, C), psa(Y). 644% ?- N = 2, (numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 645% ?- N = 3, (numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), findall_epi(X, Ns-Ns, Y), card(Y, C)). 646% ?- N = 10,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 647% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 648% ?- N = 11,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 649% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 650% ?- N = 12,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 651% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 652% ?- N = 13,(numlist(1, N, Ns), bdd_sort_append(Ns, 1, X), 653% time((findall_epi(X, Ns-Ns, Y), card(Y, C)))). 654 655select_target(Range, U, B, V):- member(B, Range), 656 ( select(B, U, V) -> true 657 ; V = U 658 ). 659 660% 661findall_epi(0, _, 0):-!. 662findall_epi(1, _-U, X):-!, 663 ( U=[] -> X = 1 664 ; X = 0 665 ). 666findall_epi(X, RngU, Y):- memo(findall_epi(X, RngU)-Y), 667 ( nonvar(Y) -> true % , write(.) % many hits. 668 ; cofact(X, t(A, L, R)), 669 findall_epi(L, RngU, L0), 670 findall_epi(A, R, RngU, R0), 671 zdd_join(L0, R0, Y) 672 ). 673% 674findall_epi(A, R, Rng-U, R0):- 675 findall(B-(Rng-V), select_target(Rng, U, B, V), Cases), 676 findall_epi(Cases, A, R, 0, R0). 677% 678findall_epi([], _, _, V, V). 679findall_epi([B-(Rng-Rng0)|Cases], A, R, U, V):- 680 findall_epi(R, Rng-Rng0, U0), 681 cofact(U1, t(A-B, 0, U0)), 682 zdd_join(U, U1, U2), 683 findall_epi(Cases, A, R, U2, V). 684 685% ?- merge_funs([mono([1,2]-[a,b]), mono([3,4]-[c,d])], X), psa(X). 686merge_funs(Fs, X):- fold_merge_funs(Fs, 1, X). 687% 688fold_merge_funs([], X, X). 689fold_merge_funs([G|Fs], X, Y):- 690 fun_block(G, X0), 691 zdd_merge(X, X0, X1), 692 fold_merge_funs(Fs, X1, Y). 693% 694fun_block(G, X):- 695 ( G = mono(D-R) -> all_mono(D, R, X) 696 ; G = epi(D-R) -> all_epi(D, R, X) 697 ; G = fun(D-R), 698 all_fun(D, R, X) 699 ). 700 701% ?- N=2, numlist(1, N, Ns), 702% ( set_compare(opp_compare), 703% X<<pow(Ns), psa(X), set_compare(compare), 704% zdd_normalize(X, Y), psa(Y)). 705 706zdd_normalize(X, X):- X<2, !. 707zdd_normalize(X, Y):- memo(normalize(X)-Y), 708 ( nonvar(Y) -> true % , write(.) % Many hits. 709 ; cofact(X, t(A, L, R)), 710 zdd_normalize(L, L0), 711 zdd_normalize(R, R1), 712 zdd_insert(A, R1, R0), 713 zdd_join(L0, R0, Y) 714 ). 715 716% ?- N = 1000, numlist(1, N, Ns), 717% time((X<<pow(Ns), rank_family_by_card(X, P), card(P, C))). 718 719% ?- N = 1000, numlist(1, N, Ns), 720% time((X<<pow(Ns), rank_family_by_card(X, P), memo(family_with_card(500)-L), card(L, C))). 721 722% ?- N = 1000, numlist(1, N, Ns), 723% time((( X<<pow(Ns), 724% get_family_of_rank(500, X, Y), 725% card(Y, C)))).
730get_family_of_rank(Order, X, F):- rank_family_by_card(X, _), 731 memo(family_with_card(Order)-F). 732 733% ?- X<<pow([1]). 734% ?- X<<set([a]), rank_family_by_card(X, P), 735% memo(family_with_card(0)-L), sets(L, Sl), 736% memo(family_with_card(1)-M), sets(M, Sm).
742rank_family_by_card(0, 0):-!. 743rank_family_by_card(1, 0):-!, memo(family_with_card(0)-1). 744rank_family_by_card(I, P):- memo(rank_family_by_card_done(I)-B), 745 ( nonvar(B) -> true 746 ; cofact(I, t(A, L, R)), 747 rank_family_by_card(L, Pl), 748 rank_family_by_card(R, Pr), 749 max(Pl, Pr, P0), 750 insert_one_to_family(A, P0, New), 751 P is P0 + 1, 752 memo(family_with_card(P)-New), 753 B = true 754 ). 755% 756insert_one_to_family(A, 0, G):-!, memo(family_with_card(0)-F), 757 zdd_insert(A, F, G). 758insert_one_to_family(A, P, G):- P0 is P-1, 759 insert_one_to_family(A, P0, G0), 760 memo(family_with_card(P)-Fp), 761 zdd_insert(A, Fp, G), 762 zdd_join(Fp, G0, Gp), 763 set_memo(family_with_card(P)-Gp). 764 765 /********************** 766 * State access * 767 **********************/ 768 769get_extra(Extra):- b_getval(zdd_extra, Extra). 770% 771set_extra(Extra):- b_setval(zdd_extra, Extra). 772 773% ?- bump_up(a, N), bump_up(a, K). 774bump_up(Key):- b_getval(zdd_extra, Extra), 775 ( select(Key-N0, Extra, Extra0) -> true 776 ; N0 = 0, 777 Extra0 = Extra 778 ), 779 N is N0 + 1, 780 b_setval(zdd_extra, [Key-N|Extra0]). 781 782 783:- meta_predicate set_compare(). 784set_compare(Compare):- nb_setval(zdd_compare, Compare). 785 786% ?- zdd_compare(C, a, b). 787get_compare(Compare):- b_getval(zdd_compare, Compare). 788% 789zdd_compare(C, X, Y):- b_getval(zdd_compare, Compare), 790 call(Compare, C, X, Y). 791 792% ?- zdd_sort([1->1, 1->2, 1-1, 2-2], X). 793zdd_sort(X, Y):- b_getval(zdd_compare, Comp), predsort(Comp, X, Y). 794 795% ?- get_key(a, V), set_key(a, 1), get_key(a, W). % fail. 796% ?- set_key(a, 1), get_key(a, W). 797get_key(K, V):- b_getval(zdd_extra, Assoc), 798 memberchk(K-V, Assoc). 799% 800set_key(K, V) :- b_getval(zdd_extra, Assoc), 801 ( select(K-_, Assoc, Assoc0) 802 -> b_setval(zdd_extra, [K-V|Assoc0]) % nb_linkval not work. 803 ; b_setval(zdd_extra, [K-V|Assoc]) % nb_linkval not work. 804 ). 805% 806nb_set_key(K, V) :- b_getval(zdd_extra, Assoc), 807 ( select(K-_, Assoc, Assoc0) 808 -> nb_setval(zdd_extra, [K-V|Assoc0]) 809 ; nb_setval(zdd_extra, [K-V|Assoc]) 810 ). 811 812:- meta_predicate set_pred(, ). 813set_pred(K, V) :- set_key(K, V). 814 815% ?- open_key(a, []), update_key(a, X, Y), X=[1|Y], 816% get_key(a, Z), close_key(a). 817 818% ?- zdd. 819% ?- ((open_key(a, []), update_key(a, X, Y), X=[1|Y], 820% get_key(a, Z), close_key(a), get_key(a, U))). % false 821 822% 823open_key(K, Val):- set_key(K, Val). 824% 825update_key(X, Old, New):- b_getval(zdd_extra, Assoc), 826 select(X-Old, Assoc, Assoc0), 827 b_setval(zdd_extra, [X-New|Assoc0]). 828% 829close_key(Key):- b_getval(zdd_extra, Assoc), 830 ( select(Key-_, Assoc, Assoc0) -> 831 b_setval(zdd_extra, Assoc0) 832 ; true 833 ). 834 835% ?- varnum(D), varnum(E).
840varnum(D):- get_key(varnum, D). 841 842% ?- sort([1->1, 1->2, 1-1, 2-2], X). 843% ?- predsort(compare_rev(compare), [1->1, 1->2, 1-1, 2-2], X). 844% ?- predsort(compare_rev, [1->1, 1->2, 1-1, 2-2], X). 845% ?- zdd_sort_rev([1,2,3], X). 846 847:- meta_predicate pred_compare_rev(, , , ). 848 849pred_compare_rev(Comp, C, A, B):- call(Comp, C, B, A). 850% ?- compare_opp(C, 1, 2). 851compare_rev(C, A, B):- compare(C, B, A). 852 853% 854zdd_sort_rev(X, Y):- get_compare(Comp), 855 predsort(compare_rev(Comp), X, Y). 856 857% ?- pred_zdd(opp_compare, zdd_sort([1-1, 2-2, 3-3], Y)). 858:- meta_predicate pred_zdd(, ). 859pred_zdd(Comp, X):- set_compare(Comp), call(X). 860 861% ?- X<<pow([a,b,c]), zdd_memberchk([a,c], X). 862% ?- X<<pow([a,b,c]). 863 864% ?- zdd, ((X<<pow([a,b,c]), zdd_memberchk([], X))). 865% ?- zdd, ((X<<pow([a,b,c]), zdd_memberchk([a,c,d], X))). % false
870zdd_memberchk(L, Z):- zdd_sort(L, L0), zdd_ord_memberchk(L0, Z). 871% 872zdd_ord_memberchk([], Z):- !, zdd_has_1(Z). 873zdd_ord_memberchk([A|As], Z):- Z>1, 874 cofact(Z, t(B, L, R)), 875 ( A == B 876 -> zdd_ord_memberchk(As, R) 877 ; A @> B, 878 zdd_ord_memberchk([A|As], L) 879 ). 880 881% PASS 882% ?- X<<pow([a,b]), card(X, C). 883% ?- ((X<<(pow([a,b])-pow([a])), card(X, C))). 884% ?- X=1, Y =2, Z is X + Y. 885% ?- X<<set([a]), sets(X, U). 886% ?- ((X<<pow([a,b]), S<<sets(X))). 887% ?- ((X<<pow([a,b,c,d,e,f]), Y<<pow([a,b,c,d,e,f]), U<<(X-Y), S<<sets(U))). 888% ?- (((X<< *(:append([a,b], [c,d]))), sets(X, Y))). 889% ?- ((X<<(*[a,b]& *[c,d]), S<<sets(X))). 890% ?- ((X<<{[a],[b],[c]}, sets(X,S))). 891% ?- ((X<<{[a],[b, c]}, sets(X,S))). 892% ?- ((X<<{[a],[b, c]}, Y<<{[c, b, c]}, Z<<(X-Y), sets(Z,S))). 893% ?- ((X<<{[a],[b, c]}, Y<<{[b, c], [a], [a]}, Z<< (X-Y), U<<sets(Z))). 894% ?- I =1000, J =2000, 895% time( (zdd, 896% numlist(1, I, L), 897% numlist(1, J, M), 898% X << pow(L), 899% Y << pow(M), 900% Z << (Y - X), 901% card(Z, C), 902% C =:= 2^J-2^I )). 903 904 905% PASS 906% ?- ((X<<cnf(0), Y<<sets(X))). 907% ?- ((X<<cnf(1), Y<<sets(X))). 908% ?- ((X<<cnf(2), Y<<sets(X))). 909% ?- ((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 910% ?- ltr_((X<<cnf(-2), Y<<sets(X), psa(X), extern(Y, Y0))). 911% ?- (X<<cnf(a), Y<<sets(X))). 912% ?- ((X<<cnf(-a), Y<<sets(X))). 913% ?- ((X<<cnf(a+b), Y<<sets(X))). 914% ?- ((X<<cnf(-(a+b)), Y<<sets(X))). 915% ?- ((X<<cnf(-(a+b+b+a)), Y<<sets(X))). 916% ?- ((X<<cnf(-(-(a+b+b+a))), Y<<sets(X))). 917% ?- ((X<<cnf(-(-a + -b)), Y<<sets(X))). 918% ?- ((X<<dnf(a), Y<<sets(X), extern(Y, Y0))). 919% ?- ((X<<dnf(a->b), Y<<sets(X), extern(Y, Y0))). 920% ?- ((X<<dnf(a+b -> c*d), Y<<sets(X), extern(Y, Y0))). 921% ?- ((X<<dnf(-(-a)), extern(X, X0), Y<<sets(X0))). 922% ?- ((X<<dnf(a+b), Y<<sets(X))). 923% ?- ((X<<dnf(-(a+b)), Y<<sets(X))). 924% ?- ((X<<dnf(-(a+b+b+a)), Y<<sets(X))). 925% ?- ((X<<dnf(-(-(a+b+b+a))), Y<<sets(X))). 926% ?- ((X<<dnf(-(-a + -b)), Y<<sets(X))). 927% ?- ((X<<dnf((-a + a)), Y<<sets(X))). 928% ?- ((X<<dnf(-(-a + a)), Y<<sets(X))). 929% ?- (X << *(:append([a,b], [c,d]))). 930% ?- ((X << ((*[a,b]+ *[c,d])* *[c,d]), sets(X, S))). 931% ?- ((X << *[a,b], sets(X, S))). 932% ?- ((X << +[a,b], sets(X, S))). 933% ?- ((X << dnf(a*b+c*d+c*d*d), sets(X, S))). 934% ?- ((zdd_list_to_singletons([], X), prz(X))). 935% ?- ((zdd_list_to_singletons([a], X), prz(X))). 936% ?- ((zdd_list_to_singletons([a,b], X), prz(X))). 937% ?- ((zdd_list_to_singletons([c, a, b], X), prz(X))). 938% ?- X << *[a,b], psa(X). 939% ?- X << +[a,b], psa(X). 940 941% ?- I =1000, J is I + 1, numlist(1, I, L), 942% prepare_ltr_list(L, L0), 943% time((( X<<ltr_ord_power(L0), ltr_has_set([-(1), 3, 3,4, 6, I], X)))).
951zdd_list_to_singletons(As, X):- shift(zdd_list_to_singletons(As, X)). 952% 953zdd_list_to_singletons([], 1, _). 954zdd_list_to_singletons([A|As], X, S):-zdd_list_to_singletons(As, Y, S), 955 zdd_singleton(A, Y0, S), 956 zdd_join(Y0, Y, X, S). 957 958% PASS. 959% ?- ((zdd_partial_choices([], X), prz(X))). 960% ?- ((zdd_partial_choices([[a], [b]], X), prz(X))). 961% ?- ((zdd_partial_choices([[a, a1], [b, b1], [c, c1]], X), prz(X))). 962% ?- ((zdd_partial_choices([[a, a], [a, b], [a, c]], X), prz(X))). 963% ?- ((zdd_partial_choices([[b, a], [a, b], [a, a, b, b]], X), prz(X))). 964% ?- ((zdd_partial_choices([[c, c], [b, b, b], [a, a]], X), prz(X))). 965% ?- ((zdd_partial_choices([[a, a], [], [a, c]], X), prz(X))). 966% ?- ((zdd_partial_choices([[a], [b], [c], [a], [d]], X), prz(X), card(X, C))). 967% ?- ((zdd_partial_choices([[a,a1], [b,b1]], X), prz(X), card(X, C))). 968% ?- findall([I], between(1, 10000, I), Ls), 969% ((zdd_partial_choices(Ls, X), 970% card(X, C))), !, C =:= 2^10000.
975zdd_partial_choices([], 1):-!. 976zdd_partial_choices([L|Ls], X):- zdd_partial_choices(Ls, X0), 977 sw_fold_insert(zdd, L, X0, 0, X1), 978 zdd_join(X0, X1, X). 979 980:- meta_predicate zdd_find(, , ).
985% ?- X<< pow([a,b,c]), zdd_find(=(c), X, Y). 986% ?- X<< pow([a(1),b(2),c(4), c(3)]), zdd_find(=(c(_)), X, Y). 987% ?- X<< ltr_pow([a(1),a(2)]), zdd_find( =(a(_)), X, Y). 988 989zdd_find(F, X, Y):- X>1, 990 cofact(X, t(A, L, R)), 991 ( call(F, A), Y = A 992 ; zdd_find(F, L, Y) 993 ; zdd_find(F, R, Y) 994 ). 995 996use_table(G):- functor(G, F, N), 997 setup_call_cleanup( 998 table(F/N), % 999 G, 1000 untable(F/N) % 1001 ). 1002 1003 1004 1005% PASS. 1006% 1007% ?- P<<pow([1,2,3]), {X=1;X=2}, card(P,C). 1008% ?- P<<pow([1,2,3]), card(P,C). 1009% ?- P<<pow([1,2,3]), card(P,C). 1010 1011% ?- P << set([1,2,3,2,3]), psa(P). 1012 1013% ?- P << ({[1,2,3,2,3]} + {[4, 2,4]}), psa(P). 1014 1015% ?- X << :append([a,b], [c,d]). 1016% ?- (X << :append([a,b], [c,d])). 1017% ?- ((X << :append([a,b], [c,d]))). 1018% ?- ((( X<<pow([1,2]), true, true))). 1019% ?- (X<<pow([1,2]), true, true, card(X, C)). 1020% ?- numlist(1, 100, Ns), (X<<pow(Ns), card(X, C)). 1021 1022 1023% ?- show_state. 1024% ?- fetch_state, X<<pow([a,b]), fetch_state, card(X, C). 1025% ?- X<<{[a],[b]}, Y<<{[b], [c]}, zdd_merge(X, Y, Z), psa(Z). 1026% ?- 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)).1035opp_compare(<, -(_,_), ->(_,_)):-!. 1036opp_compare(>, ->(_,_), -(_,_)):-!. 1037opp_compare(C, X, Y):- compare(C, Y, X). % reverse order 1038 1039% ?- X<< @(abc), psa(X). 1040% ?- 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.1057% ?- X<< +[ *[a,b], *[c, d]], psa(X). 1058% ?- <<(X, +[*[a,b], *[c,d]]), psa(X). 1059% ?- X<< card(pow([1,2]) + pow([a,b])). 1060% ?- X<< card(pow([1,2])). 1061 1062 1063:- meta_predicate <<(, ). 1064<<(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,
1102% Pass. 1103% ?- X<<dnf(a*b), psa(X). 1104% ?- X<<dnf((a->b)*(b->c)*a -> c), ltr_card(X, C). 1105% ?- X<<dnf((a->b)*(b->c)->(b->c)), ltr_card(X, C))). 1106% ?- X<<dnf((a->b)*(b->c)->(b->c)), psa(X), ltr_card(X, C). 1107 1108% Pass. 1109% ?- X<< @a. 1110% ?- X<< a, psa(X). 1111% ?- X<<pow([a,b]), card(X, C). 1112% ?- X<<pow([a,b])-pow([a]), card(X, C). 1113% ?- X<< set(:(append([1,2],[3,4]))), psa(X). 1114% ?- ((X<< +(:append([1,2],[3,4])), psa(X))). 1115% ?- ((X<< (@a + @b), psa(X))). 1116% ?- ((X<< ((@a + @b)* @c), psa(X))). 1117% ?- ((X<< [a,b])). 1118% ?- ((X<< set(:(append([a,b],[c,d]))), psa(X))). 1119% ?- ((X<< set(!append([a,b],[c,d])), psa(X))). % error 1120% ?- (X<< card(pow([a,b]))). 1121% ?- (X<< card(pow(:numlist(1, 100)))). 1122% ?- ((X<< set([1]), Y<< (X+X), psa(X))). 1123% ?- ((X<< set([1]), psa(X))). 1124% ?- ((X<< set([]))). 1125% ?- ((X << {[a], [b], [c]}, psa(X))). 1126% ?- ((X << {[a], [b], [c]}, card(X, C))). 1127 1128% PASS. 1129% ?- X << card(pow(append(numlist(1,3), numlist(4,5)))). 1130% ?- ((X << set(append(numlist(1,2), numlist(4,5))))). 1131% ?- ((X << set(append(numlist(1,10), numlist(11,20))))). 1132% ?- numlist(1,10,A), numlist(11,20, B), X<< pow(append(A, B)), 1133% card(X, C). 1134% ?- X << pow(numlist(1,2)), card(X, C). 1135% ?- X << pow(numlist(1,2)). 1136 1137% ?- ((X << pow(:(! charlist(a,z))), card(X, C))). 1138% ?- ((X << pow(:(! charlist(a-z))), card(X, C))). 1139% ?- ((X << pow([a,b]))). 1140% ?- ((X << *[a, b, c])). 1141% ?- ((X << (*[a, b, c] + *[a,b,c]), psa(X))). 1142% ?- ((X << (*[a, b, c] + *[2, 3]), psa(X))). 1143% ?- ((C << card(pow([a,b,c,1,2,3])))). 1144% ?- ((C << card(pow(:append([a,b,c], [1,2,3]))))). 1145% ?- ((C << pow(:numlist(1, 3)))). 1146% ?- ((C << @(a), psa(C))). 1147 1148% Pass. 1149% ?- ((U << (pow([a])+pow([b,c]) + pow(:charlist($(a-z)))), card(U, C))). 1150% ?- ((U << (pow([a])+pow([b,c]) + pow(:charlist($a,$z))), card(U, C))). 1151% ?- ((U << +((append([a,b,c], [d,e,f]))), psa(U))). 1152% ?- ((U << *((append([a,b,c], [d,e,f]))), psa(U))). 1153% ?- ((U << +((append(append([a,b,c], [x,y,z]), [1, 2]))), 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 << *[ *[a,b], +[c,d]], psa(U))). 1158% ?- ((U << card(pow((append(append([a,b,c], [x,y,z]), [1,2,3])))))). 1159% ?- ((U << card(pow((append(append([a,b,c], [x,y,z]), [1,2,3])))))). 1160% ?- ((U << #(card(pow([a]))))). 1161% ?- ((U << succ((card(pow([a])))))). 1162% ?- ((U << card(pow([a])))). 1163% ?- U << card(pow([a])+pow([b])). 1164% ?- ((U << (=(3)))). 1165% ?- ((U << *([1,2,3]), psa(U))). 1166% ?- ((U << plus(card(pow([a,b])), card(pow([1,2]))))). 1167% ?- ((U << @a)). % singleton. 1168% ?- ((U << @2)). 1169% ?- ((U << [a,b])). 1170% ?- ((U << *[a,b], psa(U))). 1171% ?- ((U << +[a,b], psa(U))). 1172% ?- ((U << +[*[a,b], *[c,d]], psa(U))). 1173% ?- ((U << +[+[a,b], +[c,d]], psa(U))). 1174% ?- ((U << *[+[a,b], +[c,d]], psa(U))). 1175% ?- ((U << *[*[a,b], *[c,d]], psa(U))). 1176% ?- ((U << call(=, hello))). 1177% ?- ((U << call(=, append([a,b],[c,d])))). 1178% ?- X<< *[a,b], Y<< *[c,d], Z<< zdd_join(X, Y), psa(Z). 1179% ?- X<< *[a,b], Y<< *[c,d], Z<< (X+Y), psa(Z). 1180% 1181basic_type(X):- number(X); 1182 string(X); 1183 is_list(X); 1184 var(X). 1185 1186% ?- X<< p(2,3), psa(X). 1187% ?- X<< pq(2,3), psa(X). % Error. 1188% ?- findall(p(I), between(1,3,I), As), X<< +As, psa(X). 1189 1190default_atom(X):- functor(X, F, _), 1191 atom_chars(F, [A|As]), 1192 char_type(A, alpha), 1193 digit_chars(As). 1194% 1195digit_chars([]). 1196digit_chars([D|Ds]):- char_type(D, digit), 1197 digit_chars(Ds).
1202% Unusual first, but legal samples. 1203% ?- U << @(=(3)), psa(U). 1204% ?- U << +(!append([a], [b])), psa(U). 1205% ?- U << (@a+ @b+ @c), psa(U). 1206% ?- U << append([a], [b]). 1207% ?- U << +(append([[a]], [[b]])), psa(U). 1208% ?- U << get_compare. 1209% ?- get_compare(X). 1210% ?- U << arith(1+2). 1211% ?- U << plus(arith(1+2), arith(3+4)). 1212% ?- U << (@A+ @B+ @C), psa(U). 1213 1214zdd_eval(X, Y):- context_module(M), 1215 zdd_numbervars(X), 1216 zdd_eval(X, Y, M).
1222% Note that intgeger is used as a unique name of a ZDD. 1223% use indicator `@` as `@(3)` for 3 as an atom. 1224 1225zdd_eval(X, X, _) :- basic_type(X), !. 1226zdd_eval({}, 0, _) :-!. % The empty family of sets. 1227zdd_eval({X}, Y, _) :-!, associative_comma(X, U, []), zdd_family(U, Y). 1228zdd_eval($(X), X, _) :-!. 1229zdd_eval(!(X), Y, M) :-!, call(M:X, Y). 1230zdd_eval(M:X, Y, _) :-!, zdd_eval(X, Y, M). 1231zdd_eval(X, Y, _) :- zdd_basic(X, Y), !. 1232zdd_eval(X, Y, M) :- zdd_eval_args(X, X0, M), 1233 ( zdd_apply(X0, Y) -> true 1234 ; call(M:X0, Y) 1235 ). 1236% 1237zdd_eval_args(A, A, _):- atomic(A), !. 1238zdd_eval_args(A, B, M):- 1239 functor(A, Fa, Na), 1240 functor(B, Fa, Na), 1241 zdd_eval_args(1, A, B, M). 1242% 1243zdd_eval_args(I, A, B, M):- arg(I, A, U), !, 1244 zdd_eval(U, V, M), 1245 arg(I, B, V), 1246 J is I+1, 1247 zdd_eval_args(J, A, B, M). 1248zdd_eval_args(_, _, _, _). 1249 1250 /*********************************************** 1251 * Currently reserved names of operations. * 1252 ***********************************************/ 1253zdd_basic(@(A), Y) :-!, zdd_singleton(A, Y). 1254zdd_basic(X, Y) :- default_atom(X), !, zdd_singleton(X, Y). 1255zdd_basic(dnf(A), X) :-!, dnf(A, X). 1256zdd_basic(cnf(A), X) :-!, cnf(A, X). 1257zdd_basic(arith(E), X) :-!, X is E. 1258zdd_basic(X, Y) :- (atom(X); dvar(X)), !, zdd_singleton(X, Y).
1265zdd_apply(ltr_set(L), Y):-!, ltr_append(L, 1, Y). 1266zdd_apply(gf2(A), X) :-!, gf2(A, X). 1267zdd_apply(qp(A), X) :-!, mqp(A, X). 1268zdd_apply(cofact(A, L, R), X) :-!, cofact(X, t(A, L, R)). 1269zdd_apply(cofact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1270zdd_apply(fact(X), Y) :-!, integer(X), X>1, cofact(X, Y). 1271zdd_apply(+(X), Y) :-!, zdd_vector_exp(+(X), Y). 1272zdd_apply(*(X), Y) :-!, zdd_vector_exp(*(X), Y). 1273zdd_apply(X + Y, Z) :-!, zdd_join(X, Y, Z). 1274zdd_apply(X * Y, Z) :-!, zdd_merge(X, Y, Z). 1275zdd_apply(merge(X, Y), Z) :-!, zdd_merge(X, Y, Z). 1276zdd_apply(-(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1277zdd_apply(\(X,Y), Z) :-!, zdd_subtr(X, Y, Z). 1278zdd_apply((X // Y), Z) :-!, zdd_div(X, Y, Z). 1279zdd_apply((X / Y), Z) :-!, zdd_mod(X, Y, Z). 1280zdd_apply((X mod Y), Z) :-!, zdd_mod(X, Y, Z). 1281zdd_apply(&(X, Y), Z) :-!, zdd_meet(X, Y, Z). 1282zdd_apply(prod(X, Y), Z):-!, zdd_product(X, Y, Z). 1283zdd_apply(**(X, Y), Z) :-!, zdd_product(X, Y, Z). 1284zdd_apply(pow(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1285zdd_apply(power(X), Z) :-!, zdd_sort(X, Y), zdd_power(Y, Z). 1286zdd_apply(set(X), Z) :- bdd_sort_append(X, 1, Z). 1287 1288 1289 /********************************* 1290 * vector expressions * 1291 *********************************/
1296% ?- ((X<< +[[1,2],[a,b]], psa(X), card(X, C))). 1297% ?- ((X<< *[[1,2],[a,b]], psa(X), card(X, C))). 1298% ?- ((X<< *[*[1,2], *[a,b]], psa(X), card(X, C))). 1299% ?- X<< +[*[1,2], *[a,b]], psa(X). 1300% ?- X<< +[*[1,2], *[1]], psa(X). 1301% ?- X<< +[*[1,2], *[a,b]]. 1302% ?- ((X<< +[*[x(1),x(2)],*[a(1),b(1)]], psa(X), card(X, C))). 1303% ?- ((X<< *[1,2], psa(X), card(X, C))). 1304% ?- ((X<< *[+[1,2],+[a,b]], psa(X), card(X, C))). 1305% ?- zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1306% ?- zdd_vector_exp(+[[a],*[b,c]], X), psa(X). 1307% ?- zdd_vector_exp(+[a,b,c], X), psa(X). 1308% ?- zdd_vector_exp(*[a,b,c], X), psa(X). 1309% ?- zdd_vector_exp(+[*[a,b], *[c,d]], X), psa(X). 1310% ?- zdd_vector_exp(*[*[a,b], *[c,d]], X), psa(X). 1311% ?- zdd_vector_exp(*[+[a,b], +[c,d]], X), psa(X). 1312% ?- X<< *[a, b], psa(X). 1313% ?- X<< +[a, b], psa(X). 1314% ?- X<< *[A, B], psa(X). 1315% ?- X<< *[*[0, 1], *[2,3]], psa(X). 1316% ?- X<< *[*[], *[2,3]], psa(X). 1317% ?- X<< *[0, 1, *[2,3]], psa(X). 1318% ?- zdd_vector_exp(+[[a],[b,c]], X), psa(X). 1319% ?- zdd_vector_exp(+[a,b], X), psa(X). 1320 1321zdd_vector_exp(*(X), Y):-!, zdd_vector_exp(*, X, Y). 1322zdd_vector_exp(+(X), Y):-!, zdd_vector_exp(+, X, Y). 1323zdd_vector_exp(X, Y):- zdd_singleton(X, Y). 1324% 1325zdd_vector_exp(*, [], 1):-!. 1326zdd_vector_exp(+, [], 0):-!. 1327zdd_vector_exp(F, [A|As], R):-!, % F in [*,+]. 1328 zdd_vector_exp(A, U), 1329 zdd_vector_exp(F, As, V), 1330 apply_binary_basic(F, U, V, R). 1331zdd_vector_exp(_, A, R):- zdd_singleton(A, R). 1332% 1333apply_binary_basic(*, X, Y, Z):-!, zdd_merge(X, Y, Z). 1334apply_binary_basic(+, X, Y, Z):- zdd_join(X, Y, Z). 1335% 1336zdd_fold_join([], Z, Z). 1337zdd_fold_join([X|Xs], Z, Z0):- 1338 zdd_join(X, Z, Z1), 1339 zdd_fold_join(Xs, Z1, Z0). 1340% 1341zdd_fold_merge([], Z, Z). 1342zdd_fold_merge([X|Xs], Z, Z0):- 1343 zdd_merge(X, Z, Z1), 1344 zdd_fold_merge(Xs, Z1, Z0). 1345% 1346fold_singleton_join([], X, X). 1347fold_singleton_join([A|As], X, Y):- 1348 zdd_singleton(A, U), 1349 zdd_join(U, X, X0), 1350 fold_singleton_join(As, X0, Y). 1351 1352% ?- X<< zdd_join(+[*[a,b]], +[*[c,d]]), psa(X). 1353% ?- X<< (+[a,b]), psa(X). 1354% ?- X<< +[*[a,b]] + +[*[c,d]], psa(X). 1355% ?- X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X\Y). 1356% ?- X<<pow([1,2,3,4]), Y<<pow([1,2,3]), Z<<(X-Y). 1357 1358zdd_super_power([], P, P). 1359zdd_super_power([A|As], P, Q):- 1360 zdd_super_power(As, P, Q0), 1361 zdd_insert(A, Q0, Q). 1362% 1363single_set(L, Y) :-!, bdd_sort_append(L, 1, Y). 1364 1365% ?- ((zdd_family([[a],[a,b]], X), card(X, C), psa(X))). 1366family(X, Y):- zdd_numbervars(X), zdd_family(X, Y).
1372zdd_family(X, Y):- zdd_numbervars(X), zdd_family(X, 0, Y). 1373 1374% ?- zdd_family([[a],[a,b]], X), card(X, C), psa(X). 1375% ?- zdd_family([[], [a,a],[a,b]], X), psa(X). 1376zdd_family([], U, U). 1377zdd_family([X|Xs], U, V):- 1378 zdd_insert_atoms(X, 1, X1), 1379 zdd_join(X1, U, U0), 1380 zdd_family(Xs, U0, V). 1381 1382% ?- ((ltr_family([[a, b], [c, d]], X), sets(X,S))). 1383% ?- ((ltr_family([[a, b], [c, -c]], X), sets(X,S))). 1384% ?- ((ltr_family([[a,-b, a],[b, a, -b]], X), sets(X,S))). 1385% ?- ((X << cnf((a+(-b)+a)*(b+a+(-b))), S<<sets(X))). 1386% ?- ((X << dnf((a+(-b)+a)), psa(X))). 1387% ?- ((X << dnf((a+(-b)+a)* (b + a+(-b))), psa(X))). 1388% ?- ((X << dnf((A+(-B)+A)* (B + A+(-B))), psa(X))). 1389% ?- ltr_ltr_family([[a],[a,b]], X), ltr_card(X, C), psa(X). 1390% ?- ltr_ltr_family([[], [a],[a,b]], X), ltr_card(X, C), psa(X). 1391% ?- ltr_ltr_family([[a],[-b, -a,-c]], X), psa(X). 1392% 1393ltr_family(X, Y):- ltr_family(X, 0, Y). 1394 1395% 1396ltr_family([], U, U). 1397ltr_family([X|Xs], U, V):- 1398 ltr_append(X, 1, X0), 1399 ltr_join(X0, U, U0), 1400 ltr_family(Xs, U0, V). 1401 1402 /************************ 1403 * choices * 1404 ************************/
1409% ?- zdd, X<< {[a,b],[c,d]}, zdd_choices(X, Y), psa(X), psa(Y). 1410% ?- N=10, numlist(1, N, Ns), (X<< pow(Ns), zdd_subtr(X, 1, Y), 1411% zdd_choices(X, Y), card(Y, C)). 1412% ?- N=1000, numlist(1, N, Ns),time( (X<< pow(Ns), zdd_subtr(X, 1, Y), 1413% zdd_choices(X, Y), card(Y, C))). 1414 1415zdd_choices(0, 1):-!. 1416zdd_choices(1, 0):-!. 1417zdd_choices(X, Y):- memo(choices(X)-Y), 1418 ( nonvar(Y)->true %, write(+) % many hits when X has the empty set. 1419 ; cofact(X, t(A, L, R)), 1420 zdd_choices(L, L0), 1421 zdd_choices(R, R0), 1422 cofact(R1, t(A, R0, 1)), 1423 zdd_merge(L0, R1, Y) 1424 ). 1425 1426 1427 /************************************************* 1428 * Operation on join/merge/meet/subtr/cons * 1429 *************************************************/
1434zdd_join(0, X, X):-!. 1435zdd_join(X, 0, X):-!. 1436zdd_join(X, X, X):-!. 1437zdd_join(1, X, Y):-!, zdd_join_1(X, Y). 1438zdd_join(X, 1, Y):-!, zdd_join_1(X, Y). 1439zdd_join(X, Y, Z):- 1440 ( Y < X -> memo(zdd_join(Y, X)-Z) 1441 ; memo(zdd_join(X, Y)-Z) 1442 ), 1443 ( nonvar(Z) -> true 1444 ; cofact(X, t(A, L, R)), 1445 cofact(Y, t(A0, L0, R0)), 1446 zdd_compare(C, A, A0), 1447 ( C = (<) -> 1448 zdd_join(L, Y, U), 1449 cofact(Z, t(A, U, R)) 1450 ; C = (=) -> 1451 zdd_join(L, L0, U), 1452 zdd_join(R, R0, V), 1453 cofact(Z, t(A, U, V)) 1454 ; zdd_join(L0, X, U), 1455 cofact(Z, t(A0, U, R0)) 1456 ) 1457 ).
1463% ?- open_zdd_dict, zdd_dict_join(1, 0, X). 1464% ?- open_zdd_dict, zdd_dict_join(1, 1, X). 1465zdd_dict_join(0, X, X):-!. 1466zdd_dict_join(X, 0, X):-!. 1467zdd_dict_join(X, X, X):-!. 1468zdd_dict_join(1, X, Y):-!, zdd_dict_join_1(X, Y). 1469zdd_dict_join(X, 1, Y):-!, zdd_dict_join_1(X, Y). 1470zdd_dict_join(X, Y, Z):- 1471 ( Y < X -> zdd_dict_memo(join(Y, X)-Z) 1472 ; zdd_dict_memo(join(X, Y)-Z) 1473 ), 1474 ( nonvar(Z) -> true 1475 ; zdd_dict(X, t(A, L, R), _), 1476 zdd_dict(Y, t(A0, L0, R0), _), 1477 zdd_compare(C, A, A0), 1478 ( C = (<) -> 1479 zdd_dict_join(L, Y, U), 1480 zdd_dict(Z, t(A, U, R), _) 1481 ; C = (=) -> 1482 zdd_dict_join(L, L0, U), 1483 zdd_dict_join(R, R0, V), 1484 zdd_dict(Z, t(A, U, V), _) 1485 ; zdd_dict_join(L0, X, U), 1486 zdd_dict(Z, t(A0, U, R0), _) 1487 ) 1488 ).
cofact(Z, t(X, 0, Y), S).
Having analogy Z = [X|Y] in mind.1494% ?- bdd_cons(X, a, 1), bdd_cons(X, A, B). 1495% ?- bdd_cons(X, a, 0), bdd_cons(X, A, B). 1496 1497% bdd_cons(X, Y, Z):- ( var(X); X>1 ), !, cofact(X, t(Y, 0, Z)). 1498bdd_cons(X, Y, Z):- var(X), !, 1499 iterm_hash(t(Y, Z), X). 1500bdd_cons(X, Y, Z):- X>1, cofact(X, t(Y, _, Z)). 1501 1502 % b_getval(zdd_vec, A), 1503 % arg(2, A, Vec), 1504 % arg(X, Vec, t(Y,_,Z)). 1505 1506% ?- ((X<<(*[a]+ *[b]+ []), psa(X))). % false for []. 1507% ?- ((X<<(*[a]+ *[b]+ 1), psa(X))). 1508% ?- ((X<<(*[a]+ *[b]+ 0), psa(X))). 1509% ?- ((X<<(*[a]+ *[b]), psa(X))). 1510% ?- ((A<<{[a]}, psa(A), zdd_join_1(A, X), psa(X))). 1511 1512% zdd_join_1(+X, -Y, +G) is det. 1513% Y is the union of X and 1 (the singleton {{}}). 1514 1515zdd_join_1(X, X):- zdd_has_1(X), !. 1516zdd_join_1(X, Y):- zdd_add_1(X, Y). 1517% 1518zdd_add_1(0, 1):-!. 1519zdd_add_1(X, Y):- cofact(X, t(A, L, R)), 1520 zdd_add_1(L, L0), 1521 cofact(Y, t(A, L0, R)). 1522 1523 1524% zdd_dict_join_1(+X, -Y, +G) is det. 1525% Y is the union of X and 1 (the singleton {{}}). 1526 1527zdd_dict_join_1(X, X):- zdd_has_1(X), !. 1528zdd_dict_join_1(X, Y):- zdd_dict_add_1(X, Y). 1529% 1530zdd_dict_add_1(0, 1):-!. 1531zdd_dict_add_1(X, Y):- cofact(X, t(A, L, R)), 1532 zdd_dict_add_1(L, L0), 1533 zdd_dict(Y, t(A, L0, R), _). 1534 1535 1536% ?- ((X<< *[a, b], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1537% ?- ((X<< *[a, a], Y<< *[a, b], Z << (X*Y), sets(Z, S))). 1538% ?- ((X<< *[a, b], Y<< *[a, b], Z << (X&Y), sets(Z, S))). 1539% ?- ((X<<(*[a, b]+ *[c,d]), Y<<( *[x,y]+ *[u,v]), Z << (X&Y), sets(Z, S))). 1540% ?- trace, (X=[b, a]). 1541% ?- ((X<<(*[a, b]+ *[c,d]), Y<<(*[x,y]+ *[u,v]), Z << (X**Y), sets(Z, S), card(Z, C))). 1542% ?- ((X<< *[b, a], Y<< *[a, b], Z <<(X+Y), sets(Z, S))).
1547zdd_meet(0, _, 0):-!. 1548zdd_meet(_, 0, 0):-!. 1549zdd_meet(1, X, Y):-!, zdd_meet_1(X, Y). 1550zdd_meet(X, 1, Y):-!, zdd_meet_1(X, Y). 1551zdd_meet(X, X, X):-!. 1552zdd_meet(X, Y, Z):- 1553 ( X @< Y -> memo(zdd_meet(X,Y)-Z) 1554 ; memo(zdd_meet(Y,X)-Z) 1555 ), 1556 ( nonvar(Z) -> true 1557 ; cofact(X, t(A, L, R)), 1558 cofact(Y, t(A0, L0, R0)), 1559 zdd_compare(C, A, A0), 1560 ( C = (<) -> zdd_meet(L, Y, Z) 1561 ; C = (=) -> 1562 zdd_meet(L, L0, U), 1563 zdd_meet(R, R0, V), 1564 cofact(Z, t(A, U, V)) 1565 ; zdd_meet(L0, X, Z) 1566 ) 1567 ).
1572zdd_meet_1(X, 1):- zdd_has_1(X), !. 1573zdd_meet_1(_, 0).
1578% ?- X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), Z<<(X-Y), psa(Z). 1579% ?- ((X<<{[a,b],[b,c]}, Y<<{[b,c]}, psa(Y), zdd_subtr(X, Y, Z), psa(Z))). 1580% 1581zdd_subtr(X, X, 0):-!. 1582zdd_subtr(0, _, 0):-!. 1583zdd_subtr(X, 0, X):-!. 1584zdd_subtr(X, 1, Y):-!, zdd_subtr_1(X, Y). 1585zdd_subtr(1, X, Y):-!, 1586 ( zdd_has_1(X) -> Y = 0 1587 ; Y = 1 1588 ). 1589zdd_subtr(X, Y, Z):- memo(zdd_subtr(X,Y)-Z), 1590 ( nonvar(Z) -> true 1591 ; cofact(X, t(A, L, R)), 1592 cofact(Y, t(A0, L0, R0)), 1593 zdd_compare(C, A, A0), 1594 ( C = (<) -> 1595 zdd_subtr(L, Y, U), 1596 cofact(Z, t(A, U, R)) 1597 ; C = (=) -> 1598 zdd_subtr(L, L0, U), 1599 zdd_subtr(R, R0, V), 1600 cofact(Z, t(A, U, V)) 1601 ; zdd_subtr(X, L0, Z) 1602 ) 1603 ).
1608% ?- X<<(+[] + +[a]), zdd_subtr_1(X, Y), psa(Y). 1609% ?- X<<{[a], [a,b,c]}, zdd_subtr_1(X, Y), psa(Y). 1610% ?- X<<{[a], [a,b,c], []}, zdd_subtr_1(X, Y), psa(Y). 1611% 1612zdd_subtr_1(X, 0):- X < 2, !. % empty family or singleton of the empty. 1613zdd_subtr_1(X, Y):- cofact(X, t(A, L, R)), 1614 zdd_subtr_1(L, L0), 1615 cofact(Y, t(A, L0, R)).
1620% ?- X<<{[a]}, Z << zdd_xor(X, X). 1621% ?- X<<{[a,b],[b,c]}, Y<<{[b,c]}, Z<< zdd_xor(X, Y), psa(Z). 1622% ?- numlist(0, 1000, Ns), numlist(500, 1500, Ms), 1623% time((X<<pow(Ns), Y<<pow(Ms), Z<<zdd_xor(X, Y))). 1624% ?- time((Z<<zdd_xor(pow(:numlist(0, 1000)), pow(:numlist(500, 1500))))). 1625zdd_xor(X, Y, Z):-zdd_subtr(X, Y, A), 1626 zdd_subtr(Y, X, B), 1627 zdd_join(A, B, Z). 1628 1629% ya_zdd_xor(X, Y, Z, S):-zdd_join(X, Y, A, S), 1630% zdd_meet(X, Y, B, S), 1631% zdd_subtr(A, B, Z, S).
Remark. The merge is associative and commutative, but not idempotent.
1640% ?- (( X<<{[a], [b]}, Y<<{[c]}, zdd_merge(X, Y, Z), psa(Z))). 1641% ?- time((( X<<pow(!charlist(a-z)), Y<<pow(numlist(1, 26))))). 1642% ?- time((( X<<pow(charlist($(a-z))), Y<<pow(numlist(1, 26)), 1643% zdd_merge(X, Y, Z), U << zdd_meet(X, Z), card(X, C)))), C is 2^26. 1644 1645zdd_merge(0, _, 0):-!. 1646zdd_merge(_, 0, 0):-!. 1647zdd_merge(1, X, X):-!. 1648zdd_merge(X, 1, X):-!. 1649zdd_merge(X, Y, Z):- 1650 ( X > Y -> memo(zdd_merge(Y, X)-Z) 1651 ; memo(zdd_merge(X, Y)-Z) 1652 ), 1653 ( nonvar(Z) -> true 1654 ; cofact(X, t(A, L, R)), 1655 zdd_merge(L, Y, L0), 1656 zdd_merge(R, Y, R0), 1657 zdd_insert(A, R0, R1), 1658 zdd_join(L0, R1, Z) 1659 ).
1667% ?- X<<{[a]}, Y<<{[b]}, zdd_linear_merge(X, Y, Z), psa(Z). 1668% ?- X<<{[a]}, Y<<{[a, b]}, zdd_linear_merge(X, Y, Z), psa(Z). 1669% ?- X<<{[b, a]}, Y<<{[a, b]}, zdd_linear_merge(X, Y, Z), psa(Z). 1670% ?- X<<{[]}, Y<<{[a, b]}, zdd_linear_merge(X, Y, Z), psa(Z). 1671% ?- X<< 0, Y<<{[a, b]}, zdd_linear_merge(X, Y, Z), psa(Z). 1672 1673zdd_linear_merge(0, _, 0):-!. 1674zdd_linear_merge(_, 0, 0):-!. 1675zdd_linear_merge(1, X, X):-!. 1676zdd_linear_merge(X, 1, X):-!. 1677zdd_linear_merge(X, Y, Z):- 1678 cofact(X, t(A, _, R)), 1679 cofact(Y, t(B, _, R0)), 1680 zdd_compare(C, A, B), 1681 ( C = (=) -> 1682 zdd_linear_merge(R, R0, R1), 1683 bdd_cons(Z, A, R1) 1684 ; C = (<) -> 1685 zdd_linear_merge(R, Y, R1), 1686 bdd_cons(Z, A, R1) 1687 ; zdd_linear_merge(R0, X, R1), 1688 bdd_cons(Z, B, R1) 1689 ). 1690 1691% 1692zdd_merge_list([], X, X). 1693zdd_merge_list([A|As], X, Y):- 1694 ( integer(A) -> zdd_merge(A, X, X0) 1695 ; zdd_insert(A, X, X0) % atom case 1696 ), 1697 zdd_merge_list(As, X0, Y).
zdd_disjoint_merge(X, Y, Z),
psa(Z).
?- X<< +[*[a,b], b], Y<< +[*[a,c], c], zdd_disjoint_merge(X, Y, Z),
psa(Z).
?- X<< +[*[a,b], [b]], Y<< +[*[a,c], [c]], zdd_disjoint_merge(X, Y, Z),
psa(Z).1712zdd_disjoint_merge(0, _, 0):-!. 1713zdd_disjoint_merge(_, 0, 0):-!. 1714zdd_disjoint_merge(1, X, X):-!. 1715zdd_disjoint_merge(X, 1, X):-!. 1716zdd_disjoint_merge(X, Y, Z):- 1717 ( X @> Y -> memo(disj_merge(Y, X)-Z) 1718 ; memo(disj_merge(X, Y)-Z) 1719 ), 1720 ( nonvar(Z) -> true 1721 ; cofact(X, t(A, L, R)), 1722 cofact(Y, t(A0, L0, R0)), 1723 zdd_compare(C, A, A0), 1724 ( C= (<) -> 1725 zdd_disjoint_merge(L, Y, U), 1726 zdd_disjoint_merge(R, Y, V), 1727 cofact(Z, t(A, U, V)) 1728 ; C = (=) -> 1729 zdd_disjoint_merge(L, L0, U), 1730 zdd_disjoint_merge(L, R0, V), 1731 zdd_disjoint_merge(R, L0, W), 1732 zdd_join(V, W, P), 1733 cofact(Z, t(A, U, P)) 1734 ; zdd_disjoint_merge(X, L0, U), 1735 zdd_disjoint_merge(X, R0, V), 1736 cofact(Z, t(A0, U, V)) 1737 ) 1738 ). 1739 1740 1741% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 1742% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 1743%@ false. 1744% ?- ((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 1745% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 1746% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 1747% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
1752zdd_subfamily(X, X):-!. 1753zdd_subfamily(0, _):-!. 1754zdd_subfamily(_, 0):-!, fail. 1755zdd_subfamily(1, X):-!, zdd_has_1(X). 1756zdd_subfamily(X, X0):- 1757 cofact(X, t(A, L, R)), 1758 cofact(X0, t(A0, L0, R0)), 1759 zdd_compare(C, A, A0), 1760 ( C = (=) -> 1761 zdd_subfamily(L, L0), 1762 zdd_subfamily(R, R0) 1763 ; C = (>), 1764 zdd_subfamily(X, L0) 1765 ). 1766 1767 /********************************* 1768 * division/residue in * 1769 *********************************/
zdd_divmod(X, Y, D, M, S),
psa(X, S), psa(D, S), psa(M, S).
1777zdd_divmod(X, Y, D, M):-
1778 zdd_div_div(X, Y, D1, D),
1779 zdd_subtr(X, D1, M).1785% ?- X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod0(X, Y, D, M, S), 1786% psa(X, S), psa(D, S), psa(M, S). 1787zdd_divmod0(X, Y, D, M):- 1788 zdd_divisible(X, Y, D), 1789 zdd_subtr(X, D, M).
1795% ?- X<< +[b], zdd_div_div(X, 1, D, M), psa(X), psa(D), psa(M). 1796% ?- X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), psa(X), psa(Y), psa(D), psa(M). 1797% ?- X<< +[b], Y<< +[b], zdd_div_div(X, Y, D, M), 1798% psa(X), psa(Y), psa(D), psa(M). 1799% ?- X<< +[*[a,b]], Y<< +[*[b]], psa(X), psa(Y), zdd_div_div(X, Y, D, M), 1800% psa(D), psa(M). 1801% ?- X<< +[*[a,b], *[c,d]], Y<< +[*[b], *[d]], 1802% zdd_div_div(X, Y, D, D1), 1803% psa(D), psa(D1). 1804 1805zdd_div_div(0, _, 0, 0):-!. 1806zdd_div_div(1, X, Y, Y):-!, 1807 ( zdd_has_1(X) -> Y = 1 1808 ; Y = 0 1809 ). 1810zdd_div_div(_, 0, 0, 0):-!. 1811zdd_div_div(X, 1, X, X):-!. 1812zdd_div_div(X, Y, Z, U):- memo(div_div(X, Y)- P), 1813 ( nonvar(P) -> P = (Z, U) 1814 ; cofact(X, t(A, L, R)), 1815 zdd_div_div(L, Y, L0, U0), 1816 zdd_div_div(A, R, Y, R0, V0), 1817 zdd_join(L0, R0, Z), 1818 zdd_join(U0, V0, U), 1819 P = (Z, U) 1820 ). 1821% 1822zdd_div_div(_, 0, _, 0, 0):-!. 1823zdd_div_div(_, 1, 0, 0, 0):-!. % ??? 1824zdd_div_div(A, 1, 1, Z, Z):-!, zdd_singleton(A, Z). 1825zdd_div_div(_, _, 0, 0, 0):-!. 1826zdd_div_div(A, X, 1, Z, Z):-!, cofact(Z, t(A, 0, X)). 1827zdd_div_div(A, X, Y, Z, U):- cofact(Y, t(B, L, R)), 1828 zdd_compare(C, A, B), 1829 ( C = (<) -> 1830 zdd_div_div(X, Y, Z0, U0), 1831 zdd_insert(A, Z0, Z), 1832 zdd_insert(A, U0, U) 1833 ; C = (=) -> 1834 zdd_div_div(X, L, Z0, U0), 1835 zdd_insert(A, Z0, Z1), 1836 zdd_insert(A, U0, U1), 1837 zdd_div_div(X, R, Z2, U2), 1838 zdd_insert(A, Z2, Z3), % A is absorbed due to hit (A=B). 1839 zdd_join(Z1, Z3, Z), 1840 zdd_join(U1, U2, U) 1841 ; zdd_div_div(A, X, L, Z, U) 1842 ).
1848% ?- (( X<< {[a]}, zdd_div(X, X, Z), psa(Z))). 1849% ?- (( X<< 0, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1850% ?- (( X<< 0, Y<< 0, zdd_div(X, Y, Z), psa(Z))). 1851% ?- (( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1852% ?- (( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1853% ?- (( X<<{[a,b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1854% ?- (( X<<{[a, b]}, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1855% ?- (( X<<{[a]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1856% ?- (( X<<1, Y<<1, zdd_div(X, Y, Z), psa(Z))). 1857% ?- (( X<<{[a, b]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1858% ?- (( X<<{[a, b, c], [b, c]}, Y<<{[a],[b]}, zdd_div(X, Y, Z), psa(Z))). 1859% ?- (( X<<{[a, b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1860% ?- (( X<<{[a, b], [a, c]}, Y<<{[a]}, zdd_div(X, Y, Z), psa(Z))). 1861% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1862% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b], [a, c]}, zdd_div(X, Y, Z), psa(Z))). 1863% ?- (( X<<{[a, b, c], [a, c]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1864% ?- (( X<<{[c]}, Y<<{[a, c]}, zdd_div(X, Y, Z), psa(Z))). 1865% ?- (( X<<{[a]}, Y<<{[a, b]}, zdd_div(X, Y, Z), psa(Z))). 1866% ?- (( X<<{[a,b]}, Y<<{[a, b, c]}, zdd_div(X, Y, Z), psa(Z))). 1867% ?- (( X<<{[a,b,c]}, Y<<{[a,b], [c]}, zdd_div(X, Y, Z), psa(Z))). 1868% ?- (( X<<{[a, b], [a, c]}, Y<<{[a], [b]}, zdd_div(X, Y, Z), psa(Z))). 1869% ?- (( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1870% ?- (( X<<{[a, b], [a, c]}, Y<<{[b]}, zdd_div(X, Y, Z), psa(Z))). 1871 1872% 1873zdd_div(0, _, 0):-!. 1874zdd_div(1, X, Y):-!, 1875 ( zdd_has_1(X) -> Y = 1 1876 ; Y = 0 1877 ). 1878zdd_div(X, Y, Z):- memo(zdd_div(X, Y)- Z), 1879 ( nonvar(Z) -> true 1880 ; cofact(X, t(A, L, R)), 1881 zdd_div(L, Y, L0), 1882 zdd_div(A, R, Y, R0), 1883 zdd_join(L0, R0, Z) 1884 ). 1885% 1886zdd_div(_, _, 0, 0):-!. 1887zdd_div(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1888zdd_div(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1889 zdd_compare(C, A, B), 1890 ( C = (<) -> 1891 zdd_div(X, Y, Z0), 1892 cofact(Z, t(A, 0, Z0)) 1893 ; C = (=) -> 1894 zdd_div(X, L, L0), 1895 zdd_div(X, R, R0), 1896 cofact(Z, t(A, R0, L0)) 1897 ; zdd_div(A, X, L, Z) 1898 ).
1904% ?- zdd, N=10, numlist(1, N, Ns), numlist(1, 10, Js), X<<pow(Ns), Y<<{Js}, zdd_divisible(X, Y, Z). 1905% ?- X<<{[a, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1906% ?- X<<{[a, b, c], [b]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1907% ?- X<<{[a, c], [a]}, Y<<{[b]}, zdd_divisible(X, Y, Z), psa(Z). 1908% ?- X<<pow([a, b, c]), Y<<{[a], [b]}, zdd_divisible(X, Y, Z), psa(Z). 1909 1910zdd_divisible(0, _, 0):-!. 1911zdd_divisible(1, X, Y):-!, 1912 ( zdd_has_1(X) -> Y = 1 1913 ; Y = 0 1914 ). 1915zdd_divisible(X, Y, Z):- memo(zdd_divisible(X, Y)- Z), 1916 ( nonvar(Z) -> true 1917 ; cofact(X, t(A, L, R)), 1918 zdd_divisible(L, Y, L0), 1919 zdd_divisible(A, R, Y, R0), 1920 zdd_join(L0, R0, Z) 1921 ). 1922% 1923zdd_divisible(_, _, 0, 0):-!. 1924zdd_divisible(A, X, 1, Z):-!, cofact(Z, t(A, 0, X)). 1925zdd_divisible(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1926 zdd_compare(C, A, B), 1927 ( C = (<) -> 1928 zdd_divisible(X, Y, Z0), 1929 cofact(Z, t(A, 0, Z0)) 1930 ; C = (=) -> 1931 zdd_divisible(X, L, L0), 1932 zdd_divisible(X, R, R0), 1933 zdd_join(L0, R0, Z0), 1934 cofact(Z, t(A, 0, Z0)) 1935 ; zdd_divisible(A, X, L, Z) 1936 ).
1941% ?- X<< +[*[a]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1942% ?- X<< +[*[b]], Y<< +[*[a]], zdd_divisible_by_all(X, Y, Z, S). 1943% ?- X<< +[*[a,b], *[c,d]], Y<< +[*[d]], zdd_divisible_by_all(X, Y, Z, S). 1944% ?- X<< +[*[a,b]], Y<< +[*[c]], zdd_divisible_by_all(X, Y, Z, S).S). 1945% ?- N = 300, numlist(1, N, Ns), X<<pow(Ns), Y << +[*Ns], 1946% time(zdd_divisible_by_all(X, Y, Z, S)), psa(Z, S). 1947 1948% ?- X<< +[*[a,b], *[c,d], *[a, d]], Y<< +[*[a], *[d]], zdd_divisible_by_all(X, Y, Z), psa(Z). 1949 1950zdd_divisible_by_all(X, Y, X):-Y<2, !. % It was hard to find this. 1951zdd_divisible_by_all(X, _, 0):-X<2, !. % It was a little bit hard to find this. 1952zdd_divisible_by_all(X, Y, Z):- memo(div_by_all(X, Y)-Z), 1953 ( nonvar(Z) -> true 1954 ; cofact(X, t(A, L, R)), 1955 zdd_divisible_by_all(L, Y, L0), 1956 zdd_divisible_by_all(A, R, Y, R0), 1957 zdd_join(L0, R0, Z) 1958 ). 1959% 1960zdd_divisible_by_all(A, X, Y, Z):- Y<2, !, 1961 cofact(Z, t(A, 0, X)). 1962zdd_divisible_by_all(A, X, Y, Z):- cofact(Y, t(B, L, R)), 1963 zdd_compare(C, A, B), 1964 ( C = (<) -> 1965 zdd_divisible_by_all(X, Y, Z0), 1966 zdd_insert(A, Z0, Z) 1967 ; C = (=) -> 1968 zdd_divisible_by_all(X, R, R1), 1969 zdd_insert(A, R1, R0), 1970 zdd_divisible_by_all(R0, L, Z) 1971 ; Z = 0 % It was hard to find this. 1972 ).
1976zdd_mod(X, Y, Z) :- zdd_divisible(Y, X, X0),
1977 zdd_subtr(X, X0, Z).1982% ?- zdd_list(X, [[a]]), zdd_list(Y, [[a,c],[a,d]]), 1983% zdd_multiple(X, Y, Z), psa(Z). 1984% ?- zdd_list(X, [[a,b]]), zdd_list(Y, [[a,c],[a,d]]), 1985% zdd_multiple(X, Y, Z), psa(Z). 1986% ?- zdd_list(X, [[a,b]]), Y<<pow([a,b,c]), 1987% zdd_multiple(X, Y, Z), psa(Z). 1988% ?- Y<<pow([a,b,c]), zdd_multiple(0, Y, Z), psa(Z). 1989% ?- Y<<pow([a,b]), zdd_multiple(1, Y, Z), psa(Z). 1990 1991zdd_multiple(0, _, 0):-!. 1992zdd_multiple(1, Y, Y):-!. 1993zdd_multiple(_, Y, 0):-Y<2, !. 1994zdd_multiple(X, Y, Z):-memo(multiple(X, Y)-Z), 1995 ( nonvar(Z) -> true 1996 ; cofact(X, t(A, L, R)), 1997 zdd_multiple(L, Y, L0), 1998 zdd_multiple(A, R, Y, R0), 1999 zdd_join(L0, R0, Z) 2000 ). 2001% 2002zdd_multiple(_, _, Y, 0):- Y<2, !. 2003zdd_multiple(A, X, Y, Z):- cofact(Y, t(B, L, R)), 2004 zdd_multiple(A, X, L, L0), 2005 zdd_compare(C, A, B), 2006 ( C = (<) -> R0 = 0 2007 ; C = (=) -> 2008 zdd_multiple(X, R, R1), 2009 zdd_insert(A, R1, R0) 2010 ; zdd_multiple(A, X, R, R1), 2011 zdd_insert(B, R1, R0) 2012 ), 2013 zdd_join(L0, R0, Z). 2014 2015 /********************************* 2016 * division/resudue in List * 2017 *********************************/
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))).
2030zdd_mod_by_list(X, Y, Z):- zdd_divisible_by_list(X, Y, Z0),
2031 zdd_subtr(X, Z0, Z).zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).2037% ?- ((X<<pow([a,b,c]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 2038% ?- ((X<<pow([a,b,c,d]), zdd_div_by_list(X, [b,c], Y), psa(Y))). 2039 2040zdd_div_by_list(X, [], X):-!. 2041zdd_div_by_list(X, F, Y):- F=[A|As], 2042 ( X<2 -> Y = 0 2043 ; cofact(X, t(B, L, R)), 2044 zdd_div_by_list(L, F, L0), 2045 zdd_compare(C, B, A), 2046 ( C = (>) -> R0 = 0 2047 ; C = (=) -> 2048 zdd_div_by_list(R, As, R0) 2049 ; zdd_div_by_list(R, F, R1), 2050 zdd_insert(B, R1, R0) 2051 ), 2052 zdd_join(L0, R0, Y) 2053 ).
zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).2059% ?- ((X<<pow([a,b,c]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 2060% ?- ((X<<pow([a,b,c,d]), zdd_divisible_by_list(X, [b,c], Y), psa(Y))). 2061 2062zdd_divisible_by_list(X, [], X):-!. 2063zdd_divisible_by_list(X, F, Y):- F=[A|As], 2064 ( X<2 -> Y = 0 2065 ; cofact(X, t(B, L, R)), 2066 zdd_divisible_by_list(L, F, L0), 2067 zdd_compare(C, B, A), 2068 ( C = (>) -> R0 = 0 2069 ; C = (=) -> zdd_divisible_by_list(R, As, R0) 2070 ; zdd_divisible_by_list(R, F, R0) 2071 ), 2072 cofact(Y, t(B, L0, R0)) 2073 2074 ). 2075 2076 2077 /********************* 2078 * meta on * 2079 *********************/
map_zdd(F, X, Y) works roughly like
maplist(maplist(F), X, Y)) with a list X of lists.
2088% ?- zdd. 2089% ?- X<< {[1],[2]}, map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 2090% ?- X << pow([1,2,4,5,6]), 2091% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 2092% ?- N=2, numlist(1, N, L), X<<pow(L), 2093% map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 2094% ?- N=10, numlist(1, N, L), 2095% X<<pow(L), map_zdd(pred([A, B]:-plus(A,B,0)), X, Y), sets(Y, S). 2096% ?- N=10, numlist(1, N, L), 2097% X<<pow(L), map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C), C=:= 2^N. 2098% ?- N=1000, numlist(1, N, L), X<<pow(L), 2099% map_zdd(pred([A, B]:- B is A + 1), X, Y), card(Y, C), C=:= 2^N. 2100% ?- X<<pow([a,b,c]), map_zdd(pred([b,a] & [A, A]), X, Y), psa(Y), card(Y, C). 2101 2102:- meta_predicate map_zdd(,,). 2103map_zdd(F, X, Y):- open_memo(map_zdd), map_zdd_hash(F, X, Y). 2104 2105map_zdd_hash(_, X, X):- X<2, !. 2106map_zdd_hash(F, X, Y):- memo(map(X,F)-Y, map_zdd), 2107 ( nonvar(Y)-> true 2108 ; cofact(X, t(A, L, R)), 2109 map_zdd_hash(F, L, L0), 2110 map_zdd_hash(F, R, R0), 2111 call(F, A, B), 2112 zdd_insert(B, R0, R1), 2113 zdd_join(L0, R1, Y) 2114 ).
2119% ?- X<<pow([a,b,c]), identify_atoms(a, b, X, Y), psa(Y), card(Y, C). 2120identify_atoms(A, B, X, Y):-map_zdd(identify_map(A, B), X, Y). 2121% 2122identify_map(A, B, A, B):-!. 2123identify_map(_, _, X, X). 2124 2125% ?- X<< (*[a,b,c]), psa(X). 2126% ?- X<< (+[a,b]), psa(X). 2127% ?- X<<pow([a,b,c]), psa(X). 2128% ?- prz(1). 2129% ?- prz(0). 2130% ?- mp(hello, 1). 2131% ?- mp(hello, 0).
2135prz(X):- print_set_at(X).2139mp(M, X) :- mpsa(M, X). 2140 2141mpsa(M, X):- writeln(M), 2142 print_set_at(X), 2143 writeln('-------------------'). 2144 2145% ?- sat. 2146% ?- sat(a+b), sat(b+c), psa. 2147% ?- sat(A+B), sat(B+C), psa. 2148 2149psa :- b_getval(root, R), psa(R).
pow([a]), psa(X).
?- X<<{[a]}, psa(X).2156psa(X):- print_set_at(X), 2157 writeln('-------------------'). 2158% 2159psa(X, G):- print_set_at(X, G), 2160 writeln('-------------------').
Users/cantor/devel/zdd/prolog/zdd/zdd.pl2165print_set_at(0):-!, format("\szid = 0\n\t0\n"). 2166print_set_at(1):-!, format("\szid = 1\n\t[]\n"). 2167print_set_at(X):- format("\szid = ~w\n", [X]), 2168 forall(set_at(P, X), format("\t~w\n", [P])). 2169% 2170print_set_at(0, _):-!, format("\szid = 0\n\t0\n"). 2171print_set_at(1, _):-!, format("\szid = 1\n\t[]\n"). 2172print_set_at(X, G):- format("\szid = ~w\n", [X]), 2173 forall(set_at(P, X, G), format("\t~w\n", [P])). 2174 2175% ?- X<<(set([1-2, 2-3, 3-4]) + set([1-2,2-3])), set_at(U, X). 2176% ?- X<<pow([1,2]), set_at(U, X), psa(X). 2177 2178% ?- zdd, ((X<<pow([1,2]), mp(powerset, X))). 2179set_at([], 1):-!. 2180set_at(P, X):- X>1, 2181 cofact(X, t(A, L, R)), 2182 ( set_at(P, L) 2183 ; set_at(As, R), 2184 P=[A|As] 2185 ). 2186% 2187set_at([], 1, _):-!. 2188set_at(P, X, G):- X>1, 2189 cofact(X, t(A, L, R), G), 2190 ( set_at(P, L, G) 2191 ; set_at(As, R, G), 2192 P=[A|As] 2193 ). 2194 2195% ?- zdd_singleton(a, X), show_fos(X). 2196% ?- X<< {[a,b], [b,c]}, show_fos(X). 2197% ?- X<< pow([a,b]), show_fos(X).
2201show_fos(X):- X > 1, 2202 accessible_nodes(X, Ns), 2203 forall( member(M, Ns), 2204 ( cofact(M, T), 2205 writeln(M->T))). 2206% 2207accessible_nodes(X, Ns):- 2208 accessible_nodes(X, Ns0, []), 2209 sort(Ns0, Ns1), 2210 reverse(Ns1, Ns). 2211% 2212accessible_nodes(X, A, A):- X<2, !. 2213accessible_nodes(X, [X|A], B):- 2214 cofact(X, t(_, L, R)), 2215 accessible_nodes(L, A, A0), 2216 accessible_nodes(R, A0, B).
2222% ?- zdd, ((X<<pow([a,b,c]), zdd_list(X, Y), zdd_list(X0, Y))). 2223% ?- powerset([a,b,c], Y), zdd, ((zdd_list(X, Y), zdd_list(X, Y0), zdd_list(X0, Y0))), 2224% maplist(sort, Y, Y1), sort(Y1, Y2). 2225% 2226zdd_list(X, Y):- nonvar(X), !, zdd_sets(X, Y). 2227zdd_list(X, Y):- zdd_family(Y, X). 2228 2229% ?- ((X<<pow([a,b,c]), sets(X, P))). 2230% ?- ((set_compare(opp_compare), X<<pow([a,b,c]), sets(X, Y))). 2231% ?- ((X<<pow([]), sets(X, P))). 2232% ?- ((X<<pow([a]), sets(X, P))). 2233% ?- ((X<<pow(:numlist(1,3)), sets(X, Y))). 2234% ?- ((X<<pow([a,b,c]), sets(X, Y))). 2235% ?- ((X<<pow(:charlist($a, $c)), sets(X, Y))). 2236% ?- ((X<<(pow(:charlist($a, $c)) + pow(:numlist(1, 3))), sets(X, Y))).
2241sets(X, Y):- zdd_sets(X, Y0), zdd_sort(Y0, Y). 2242% 2243zdd_sets(1, [[]]):-!. 2244zdd_sets(0, []):-!. 2245zdd_sets(X, P):- 2246 cofact(X, t(A,L,R)), 2247 zdd_sets(L, Y), 2248 zdd_sets(R, Z), 2249 maplist(cons(A), Z, AZ), 2250 append(AZ, Y, P). 2251 2252% ?- zdd_eval(pow([a, b, c, d, e, f]), I), eqns(I, X), 2253% maplist(writeln, X). 2254% 2255eqns(X, Y):- zdd_eqns(X, Y). 2256 2257basic_zdd(0). 2258basic_zdd(1). 2259 2260% % ?- X<< pow(:numlist(2, 100)), zdd_eqns(X, Es), zdd_eqns(J, Es). 2261% % ?- X<< pow(:(!charlist(a,z))), zdd_eqns(X, Es), zdd_eqns(J, Es). 2262 2263% zdd_eqns(I, Es):- nonvar(I), var(Es), !, zdd_to_eqns(I, Es, []). 2264% zdd_eqns(I, Es):- var(I), nonvar(Es), !, 2265% ( check_eqns_for_zdd(Es) -> 2266% Es = [X=_|_], 2267% eqns_to_zdd(Es, X, I) 2268% ; throw('Violating-underlying-ordering-on-atoms.'(Es)) 2269% ). 2270% % 2271% zdd_to_eqns(I, X, Y):- zdd_to_eqns(I, X, [], S), 2272% zdd_sort(X, X1, S), 2273% reverse(X1, X). 2274% % 2275% zdd_to_eqns(I, X, X):- I<2, !. 2276% zdd_to_eqns(I, X, Y):- memo(visited(I)-F), 2277% ( nonvar(F) -> Y = X 2278% ; F = true, 2279% cofact(I, t(A, L, R)), 2280% X = [I=t(A, L, R)|X0], 2281% zdd_to_eqns(L, X0, X1), 2282% zdd_to_eqns(R, X1, Y) 2283% ). 2284% % 2285% check_eqns_for_zdd(Es):- are_eqns_closed(Es, Es), 2286% sort(Es, Fs), 2287% has_unique_left(Fs), 2288% sort(2, @=<, Es, Gs), 2289% has_unique_right(Gs). 2290% % 2291% are_eqns_closed([], _). 2292% are_eqns_closed([_ = t(A, L, R)|Rest], Es):- 2293% ( basic_zdd(L) -> true 2294% ; memberchk(L = t(B, _, _), Es), 2295% zdd_compare(<, A, B) 2296% ), 2297% ( basic_zdd(R) -> true 2298% ; memberchk(L = t(C, _, _), Es), 2299% zdd_compare(<, A, C) 2300% ), 2301% are_eqns_closed(Rest, Es). 2302% % 2303% eqns_to_zdd(_, 0, 0):-!. 2304% eqns_to_zdd(_, 1, 1):-!. 2305% eqns_to_zdd(Es, X, I):- memo(solve(X)-I), 2306% ( nonvar(I) -> true 2307% ; memberchk(X = t(A, L, R)), 2308% eqns_to_zdd(Es, L, L0), 2309% eqns_to_zdd(Es, R, R0), 2310% cofact(I, t(A, L0, R0)) 2311% ).
is_function([a-1,b-2,c-3]).
?- is_function([a-1,b-2,a-3]).2317is_function(X):- sort(X, Y), has_unique_left(Y). 2318% 2319has_unique_left([X,Y|Z]):-!, 2320 ( arg(1, X, A), arg(1, Y, A) -> false 2321 ; has_unique_left([Y|Z]) 2322 ). 2323has_unique_left(_).
2328% ?- check_one_to_one([a-1,b-2,c-3]). 2329% ?- check_one_to_one([a-1,b-2,c-1]). % false 2330 2331check_one_to_one(X):- sort(2, @=<, X, Y), has_unique_right(Y). 2332% 2333has_unique_right([X,Y|Z]):-!, 2334 ( arg(2, X, A), arg(2, Y, A) -> false 2335 ; has_unique_right([Y|Z]) 2336 ). 2337has_unique_right(_).
ppoly(+X) is det.
Print X in polynomical form.2341ppoly(X):- poly_term(X, Poly), 2342 writeln(Poly). 2343 2344% ?- ((X<<pow([a,b]), poly_term(X, P))). 2345% ?- ((X<<pow([a,b,c]), poly_term(X, P))). 2346% ?- ((X<<(@a + @b), psa(X))). 2347 2348poly_term(X, Poly):- zdd_sets(X, Sets), 2349 get_compare(Pred), 2350 maplist(predsort(Pred), Sets, Sets0), 2351 predsort(Pred, Sets0, Sets1), 2352 poly_term0(Sets1, Poly). 2353 2354% ?- poly_term0([], Y). 2355% ?- poly_term0([[]], Y). 2356% ?- poly_term0([[a], [b]], Y). 2357% ?- poly_term0([[a*b], [c]], Y). 2358 2359poly_term0(X, Y):- maplist(mul_term, X, X0), 2360 sum_term(X0, Y). 2361% 2362mul_term([], 1):-!. 2363mul_term([X], X):-!. 2364mul_term([X, Y|Xs], Z):-mul_term([X*Y|Xs], Z). 2365% 2366sum_term([], 0):-!. 2367sum_term([X], X):-!. 2368sum_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))).
2377zdd_rand_path(I):- zdd_rand_path(I, P, []), writeln(P). 2378% 2379zdd_rand_path(I, P):- zdd_rand_path(I, P, []). 2380% 2381zdd_rand_path(1, X, X):-!. 2382zdd_rand_path(I, X, Y):- I>1, 2383 cofact(I, t(A, L, R)), 2384 ( L == 0 -> 2385 X = [A|X0], 2386 zdd_rand_path(R, X0, Y) 2387 ; random(2) =:= 0 -> 2388 X = [A|X0], 2389 zdd_rand_path(R, X0, Y) 2390 ; zdd_rand_path(L, X, Y) 2391 ).
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).2400zdd_atoms(X, []):- X<2, !. 2401zdd_atoms(X, P):- memo(atoms(X)-P), 2402 ( nonvar(P) -> true 2403 ; cofact(X, t(A, L, R)), 2404 zdd_atoms(L, Al), 2405 zdd_atoms(R, Ar), 2406 ord_union(Al, Ar, P0), 2407 P=[A|P0] 2408 ). 2409 2410% ?- delete(pred([a-_]), [a-b, c-d, a-e], L). 2411:- meta_predicate delete(, , ). 2412delete(X, Y, Z):- delete(X, Y, Z, []). 2413 2414:- meta_predicate delete(, , , ). 2415delete(_, [], L, L). 2416delete(Pred, [X|Xs], L, L0):- 2417 ( call(Pred, X) 2418 -> delete(Pred, Xs, L, L0) 2419 ; L = [X|L1], 2420 delete(Pred, Xs, L1, L0) 2421 ). 2422 2423% ?- ((zdd_power([a,b], R), sets(R, U))). 2424% ?- ((X<< zdd_power(:charlist($(a-c))), sets(X, U))). 2425% ?- ((R<< pow(: !charlist(a-d)), card(R, C))). 2426%% 2427zdd_power(X, Y):- zdd_sort(X, X0), 2428 zdd_ord_power(X0, 1, Y).
zdd_ord_power([a,b], 1, X), psa(X).2433zdd_ord_power([], P, P). 2434zdd_ord_power([X|Xs], P, Q):- zdd_ord_power(Xs, P, R), 2435 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.2443% ?- atomlist(ax(1+1, 3+1), As). 2444% ?- atomlist(ax(1, 3), As). 2445atomlist(X, As):- X=..[A, I, J], 2446 I0 is I, 2447 J0 is J, 2448 findall(Y, ( between(I0, J0, K), 2449 atom_concat(A, K, Y) 2450 ), 2451 As).
2457% ?- charlist(a-c, X). 2458charlist(A-B, I):- 2459 findall(X, ( char_type(X, alnum), 2460 X @>= A, 2461 X @=< B 2462 ), 2463 I).
charlist(A-B, X).
?- charlist(a, c, X).
@ X = [a, b, c].2469charlist(A, B, I):- charlist(A-B, I). 2470 2471% ?- term_atoms(a+b=c, L). 2472% ?- term_atoms(a+b, L). 2473% ?- term_atoms(f(a+a), L).
2479term_atoms(X, L):- term_atoms(X, L0, []), 2480 sort(L0, L). 2481 2482% 2483term_atoms(X, L, L):- var(X), !. 2484term_atoms(X, [X|L], L):- atom(X), !. 2485term_atoms([X|Y], L, L0):-!, 2486 term_atoms(X, L, L1), 2487 term_atoms(Y, L1, L0). 2488term_atoms(X, L, L0):- compound(X), !, 2489 X =..[_|As], 2490 term_atoms(As, L, L0). 2491term_atoms(_, L, L). 2492 2493% ?- subst_opp(f(a,b,c,f(a)), Y, [b-a]). 2494% ?- subst_opp(a, X, [b-a]). 2495% ?- subst_opp([a], X, [b-a]). 2496 2497subst_opp(X, Y, L):- memberchk(Y-X, L). 2498subst_opp([X|Y], [X0|Y0], L):-!, 2499 subst_opp(X, X0, L), 2500 subst_opp(Y, Y0, L). 2501subst_opp(X, Y, L):- compound(X), !, 2502 X =..[F|As], 2503 subst_opp(As, Bs, L), 2504 Y =..[F|Bs]. 2505subst_opp(X, X, _). 2506 2507% ?- subst_term(f(a), R, [a-b]). 2508% ?- subst_term(g(f(a),g(a)), R, [f(a)-b]). 2509% ?- subst_term(f(a), R, [a-X]). 2510% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2511% ?- subst_term(g(f(a),g(f(a))), R, [f(a)-X]). 2512% ?- subst_term(g(f(X),g(f(Y))), R, [f(X)-a, f(Y)-b]).
2518subst_term(X, Y):- member(X0-Y), X0==X, !. 2519subst_term(A, B):- compound(A), !, 2520 ( A = [X|Y] -> 2521 B = [X0|Y0], 2522 subst_term(X, X0), 2523 subst_term(Y, Y0) 2524 ; functor(A, F, N), 2525 functor(B, F, N), 2526 subst_term(N, A, B) 2527 ). 2528subst_term(X, X). 2529% 2530subst_term(0, _, _):-!. 2531subst_term(I, X, Y):- 2532 arg(I, X, A), 2533 arg(I, Y, B), 2534 subst_term(A, B), 2535 J is I - 1, 2536 subst_term(J, X, Y). 2537 2538% ?- all_instances([a,b], [0,1], a+b=b, R). 2539% ?- all_instances([x,y], [0,1], x+y=x, R). 2540%! all_instances(+As, +Vs, +X, -Y) is det. 2541% Unify Y with the list of possible variations P of X, 2542% where P is a variation of X if for each A in As with some 2543% V in Vs which depends on A, P is obtained from X by replacing 2544% all occurrences of A appearing in X with V for A in As. 2545 2546all_instances(Ks, Ts, X, Y):- all_maps(Ks, Ts, Fs), 2547 apply_maps(Fs, X, Y, []). 2548% 2549apply_maps([], _, Y, Y). 2550apply_maps([F|Fs], X, [X0|Y], Z):- 2551 subst_term(X, X0, F), 2552 apply_maps(Fs, X, Y, Z). 2553 2554% ?- mod_table(3, [a,b], a+b, Table), maplist(writeln, Table). 2555% ?- mod_table(3, [a,b,c], a+b+c, Table), maplist(writeln, Table). 2556% ?- mod_table(3, [a,b], a*b, Table), maplist(writeln, Table). 2557% ?- mod_table(2, [a], a*a, Table), maplist(writeln, Table). 2558%! mod_table(+M, +X, +E, -T) is det. 2559% Unify T with a set of form E' = V where 2560% E' is a possible ground instance of an integer expression E 2561% and V is the value of E' with modulo M, where X is a set of 2562% parameters appearing in E. 2563 2564mod_table(M, Xs, Exp, Table):- M0 is M-1, 2565 numlist(0, M0, V), 2566 all_instances(Xs, V, Exp, Exps), 2567 !, 2568 maplist(mod_arith(M), Exps, Table). 2569% 2570mod_arith(M, Exp, Exp=V):- V is Exp mod M. 2571 2572% 2573unify_all([]). 2574unify_all([_]). 2575unify_all([X,Y|Z]):- (zdd):(X=Y), unify_all([Y|Z]). 2576 2577% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(Y, X))). 2578% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b]}, zdd_subfamily(X, Y))). % false 2579% ?- ((X<< {[a,b], [a,c], [a]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). 2580% ?- ((X<< {[a,b], [a,c]}, Y<<{[a,b], [a]}, zdd_subfamily(Y, X))). % false 2581% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(X, Y))). 2582% ?- ((X<< pow([a,b]), Y<<pow([a,b,c]), zdd_subfamily(Y, X))). % false
2587% ?- ((X <<{[a,b], [a,c]}, zdd_appear(e, X))). % false 2588% ?- ((X <<(*[a,b]+ *[a,c]), zdd_appear(e, X))). % false 2589% ?- ((X <<(*[a,b]+ *[a,c]), psa(X), zdd_appear(c, X))). 2590% ?- numlist(1, 10000, Ns), ((X<<pow(Ns), zdd_appear(10000, X))). 2591% ?- X<<pow(:numlist(1, 10000)), zdd_appear(10000, X). 2592%@ X = 10001. 2593 2594zdd_appear(A, X):- use_memo(zdd_atom_appear(A, X)). 2595 2596zdd_atom_appear(A, X):- X > 1, 2597 memo(visited(X)-B), 2598 var(B), 2599 cofact(X, t(U,L,R)), 2600 zdd_compare(C, A, U), 2601 ( C = (=) -> true 2602 ; C = (>), 2603 ( zdd_atom_appear(A, L) -> true 2604 ; L < 2 -> 2605 zdd_atom_appear(A, R) 2606 ; memo(visited(L)-true), % for earlier fail. 2607 zdd_atom_appear(A, R) 2608 ) 2609 ).
2614zdd_singleton(X, P):- cofact(P, t(X, 0, 1)).2619% ?- open_zdd_dict, zdd_dict_singleton(X, a, _), zdd_dict_singleton(Y, b, _), 2620% zdd_dict_join(X, Y, Z). 2621zdd_dict_singleton(I, X, V):- zdd_dict(I, t(X, 0, 1), V).
2626zdd_has_1(1):-!. 2627zdd_has_1(X):- X>1, 2628 cofact(X, t(_, L, _)), 2629 zdd_has_1(L). 2630 2631zdd_has_1(1, _):-!. 2632zdd_has_1(X, _):- X>1, 2633 cofact(X, t(_, L, _), AH), 2634 zdd_has_1(L, AH).
pow([x,y]), psa(P), zdd_subst(x, U, P, Q), psa(Q))).2645zdd_subst(_, _, X, X, _):- X<2, !. 2646zdd_subst(X, U, P, Q):- memo(zdd_subst(X, U, P)-Q), 2647 ( nonvar(Q) -> true 2648 ; cofact(P, t(Y, L, R)), 2649 zdd_subst(X, U, L, L0), 2650 zdd_compare(C, X, Y), 2651 ( C = (=) -> zdd_merge(U, R, R0) 2652 ; C = (<) -> bdd_cons(R0, Y, R) 2653 ; zdd_subst(X, U, R, R1), 2654 zdd_insert(Y, R1, R0) 2655 ), 2656 zdd_join(L0, R0, Q) 2657 ). 2658 2659 /*********************** 2660 * product on * 2661 ***********************/ 2662 2663% ?- ((X<<(a*b), Y<<(c*d), Z<<(X**Y), card(Z, C))). 2664% ?- ((X<<(a*b), Y<<(c*d), Z<<(X**Y))). 2665% ?- ((X<< a, Y<< 0, Z<<(X**Y), card(Z, C))). 2666% ?- ((X<<(a*b), Y<<(c+e), Z<<(X**Y), card(Z, C))). 2667% ?- time(((X<<pow(:numlist(1,16)), Z<<(X**X), card(Z, C)))). 2668% ?- N is 10000, time( ( X<<pow(:numlist(1,N)), card(X, _C))), _C =:= 2^N. 2669% ?- call_with_time_limit(120, (numlist(1, 16, R), 2670% time(((X<<pow(R), Z<<(X**X), card(Z, C)))))). 2671 2672% 2673zdd_product(X, Y, 0):- (X<2; Y<2), !. 2674zdd_product(X, Y, Z):- memo(prod(X, Y)-Z), 2675 ( nonvar(Z) -> true % , write(.) % hits found. 2676 ; zdd_product(X, Y, [], Bs, 0, Z0), 2677 append_pairs_list(X, Bs, Z1), 2678 zdd_join(Z0, Z1, Z) 2679 ). 2680% 2681zdd_product(_, X, Bs, Bs, Z, Z):- X<2, !. 2682zdd_product(X, Y, Bs, Q, U, V):- cofact(Y, t(B, L, R)), 2683 zdd_product(X, L, L0), 2684 zdd_join(L0, U, U0), 2685 zdd_product(X, R, [B|Bs], Q, U0, V). 2686% 2687append_pairs_list(X, _, X):- X<2, !. 2688append_pairs_list(X, Bs, U):- cofact(X, t(A, L, R)), 2689 append_pairs_list(R, Bs, R0), 2690 append_pairs_list(L, Bs, L0), 2691 insert_pairs(A, Bs, R0, R1), 2692 zdd_join(L0, R1, U). 2693 2694% 2695insert_pairs(_, [], U, U):-!. 2696insert_pairs(A, [B|Bs], U, V):- 2697 zdd_insert((A-B), U, U0), 2698 insert_pairs(A, Bs, U0, V). 2699 2700 /************************* 2701 * Quotient on * 2702 *************************/
?- ((zdd_insert(a, 1, X), zdd_insert(b, X, X1), prz(X1))).
?- ((X<<pow([a,b,c]), zdd_insert(x, X, X1), psa(X1))).
2711zdd_insert(_, 0, 0):-!. 2712zdd_insert(A, 1, J):-!, zdd_singleton(A, J). 2713zdd_insert(A, I, J):- memo(insert(A, I)-J), 2714 ( nonvar(J) -> true 2715 ; cofact(I, t(X, L, R)), 2716 zdd_compare(C, A, X), 2717 ( C = (=) -> 2718 zdd_join(L, R, K), 2719 cofact(J, t(X, 0, K)) 2720 ; C = (<) -> 2721 cofact(J, t(A, 0, I)) 2722 ; zdd_insert(A, L, L0), 2723 zdd_insert(A, R, R0), 2724 cofact(J, t(X, L0, R0)) 2725 ) 2726 ). 2727 2728% ?- X<<pow([a,b]), Y<<pow([c,d]), 2729% psa(X, S), psa(Y, S), 2730% zdd_join(ahead_compare([d,c,b,a]), X, Y, Z, S), psa(Z, S). 2731 2732% ?- X<<pow([a,b]), zdd_insert(ahead_compare([a,c,b]), c, X, Y, S), 2733% psa(Y, S). 2734% ?- listing(zdd_insert). 2735 2736:- meta_predicate zdd_insert(, , , ). 2737zdd_insert(_, _, 0, 0):-!. 2738zdd_insert(_, A, 1, Y):-!, zdd_singleton(A, Y). 2739zdd_insert(F, A, X, Y):- memo(zdd_insert(X, A, F)-Y), 2740 ( nonvar(Y) -> true % , write(.) % many hits 2741 ; cofact(X, t(B, L, R)), 2742 zdd_insert(F, A, L, L0), 2743 call(F, C, A, B), 2744 ( C = (=) -> bdd_cons(R0, A, R) 2745 ; C = (<) -> bdd_append([A, B], R, R0) 2746 ; zdd_insert(F, A, R, R1), 2747 bdd_cons(R0, B, R1) 2748 ), 2749 zdd_join(L0, R0, Y) 2750 ). 2751 2752% ?- ((family([[a, b],[b]], X), sets(X, Sx), 2753% zdd_insert_atoms([c, d], X, Y), sets(Y, Sy))).
2758% ?- numlist(1, 10000, Ns), ((zdd_insert_atoms(Ns, 1, X), psa(X))). 2759 2760% ?- ((X<<pow([1,2,3]), zdd_insert_atoms([4,5,6], X, Y), card(Y, C))). 2761% ?- ((X<<pow([1,2,3]), zdd_insert_atoms([1,2,3], X, Y), card(Y, C))). 2762zdd_insert_atoms(X, Y, Z):- zdd_sort(X, X0), 2763 zdd_ord_insert(X0, Y, Z). 2764 2765% 2766zdd_ord_insert(_, 0, 0):-!. 2767zdd_ord_insert([], X, X):-!. 2768zdd_ord_insert(As, 1, Y):-!, bdd_append(As, 1, Y). 2769zdd_ord_insert(As, X, Y):- memo(ord_insert(X, As)-Y), 2770 ( nonvar(Y) -> true % , write(.) % many hits. 2771 ; As = [A|U], 2772 cofact(X, t(B, L, R)), 2773 zdd_compare(C, A, B), 2774 ( C = (<) -> 2775 zdd_ord_insert(U, X, Y0), 2776 cofact(Y, t(A, 0, Y0)) 2777 ; C = (=) -> 2778 zdd_ord_insert(U, L, L1), 2779 zdd_ord_insert(U, R, R1), 2780 zdd_join(R1, L1, Y0), 2781 cofact(Y, t(A, 0, Y0)) 2782 ; zdd_ord_insert(As, L, L1), 2783 zdd_ord_insert(As, R, R1), 2784 cofact(Y, t(B, L1, R1)) 2785 ) 2786 ). 2787 2788 2789% ?- X<<pow([a,b]), zdd_reorder(ahead_compare([b,a]), X, Y), psa(Y). 2790:- meta_predicate zdd_reorder(, , ). 2791zdd_reorder(_, X, X):- X<2, !. 2792zdd_reorder(F, X, Y):- cofact(X, t(A, L, R)), 2793 zdd_reorder(F, L, L0), 2794 zdd_reorder(F, R, R1), 2795 zdd_insert(F, A, R1, R0), 2796 zdd_join(L0, R0, Y). 2797 2798 2799 /***************** 2800 * filters * 2801 *****************/ 2802 2803% ?- X<< +[*[a, b], *[b,c]], ltr_meet_filter([a, b], X, Y), psa(Y). 2804% ?- X<< +[*[a, b], *[b]], ltr_meet_filter([-a, b], X, Y), psa(Y). 2805% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, -(2), 3], X, Y), psa(Y). 2806% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([1, 3], X, Y), psa(Y). 2807% ?- numlist(1, 3, Ns), X<< pow(Ns), ltr_meet_filter([-(1), -(3)], X, Y), psa(Y). 2808% ?- ltr, numlist(1, 1000, Ns) , X<< pow(Ns), ltr_meet_filter([-(1000), -(1)], X, Y), card(Y, C), 2809% card(X, D), zdd_compare(E, C, D), U is D-C. 2810 2811% 2812ltr_meet_filter([], X, X):-!. 2813ltr_meet_filter([A|F], X, Y):- 2814 ltr_filter(A, X, X0), 2815 ltr_meet_filter(F, X0, Y). 2816 2817% ?- X<< +[*[a, b], *[b,c]], ltr_join_filter([a, b], X, Y), psa(Y). 2818% ?- X<< +[*[a, b], *[b]], ltr_join_filter([-a, b], X, Y), psa(Y). 2819ltr_join_filter(F, X, Y):- 2820 ltr_join_filter(F, X, 0, Y). 2821% 2822ltr_join_filter([], _, Y, Y):-!. 2823ltr_join_filter([P|F], X, Y, Y0):-!, 2824 ltr_filter(P, X, Y1), 2825 zdd_join(Y, Y1, Y2), 2826 ltr_join_filter(F, X, Y2, Y0). 2827 2828% 2829ltr_filter(-A, X, Y):-!, ltr_filter_negative(A, X, Y). 2830ltr_filter(A, X, Y):- ltr_filter_positive(A, X, Y). 2831 2832% 2833ltr_filter_negative(_, X, X):- X<2, !. 2834ltr_filter_negative(A, X, Y):- memo(letral_neg(X, A)-Y), 2835 ( nonvar(Y) -> true 2836 ; cofact(X, t(B, L, R)), 2837 ltr_filter_negative(A, L, L0), 2838 zdd_compare(C, A, B), 2839 ( C = (=) -> R0 = 0 2840 ; C = (<) -> R0 = R 2841 ; ltr_filter_negative(A, R, R0) 2842 ), 2843 cofact(Y, t(B, L0, R0)) 2844 ). 2845% 2846ltr_filter_positive(_, X, 0):- X<2, !. 2847ltr_filter_positive(A, X, Y):- memo(ltr_pos(X, A)-Y), 2848 ( nonvar(Y) -> true 2849 ; cofact(X, t(B, L, R)), 2850 ltr_filter_positive(A, L, L0), 2851 zdd_compare(C, A, B), 2852 ( C = (=) -> R0 = R 2853 ; C = (<) -> R0 = 0 2854 ; ltr_filter_positive(A, R, R0) 2855 ), 2856 cofact(Y, t(B, L0, R0)) 2857 ). 2858 2859% ?- ((X<<pow([a,b,c]), dnf_filter([[-b,-c]], X, Y), psa(Y))). 2860% ?- ((X<<pow([a,b]), dnf_filter([[b]], X, Y), psa(Y))). 2861% ?- ((X<<pow([a,b]), dnf_filter([[a,b]], X, Y), psa(Y))). 2862% ?- ((X<<pow([a,b]), dnf_filter([], X, Y), psa(Y))). 2863% ?- ((X<<pow([a,b,c]), dnf_filter([[c]], X, Y), psa(Y))). 2864% ?- ((X<<pow([a,b,c]), dnf_filter([], X, Y), psa(Y))). 2865% ?- ((X<<pow([a,b,c]), dnf_filter([[a],[-c]], X, Y), psa(Y))). 2866 2867dnf_filter(DNF, X, Y):- dnf_filter(DNF, X, 0, Y). 2868% 2869dnf_filter([], _, Y, Y, _). 2870dnf_filter([F|Fs], X, Y, Z):- 2871 ltr_meet_filter(F, X, X0), 2872 zdd_join(X0, Y, Y0), 2873 dnf_filter(Fs, X, Y0, Z). 2874 2875% ?- ((X<<pow([a,b,c]), cnf_filter([[-b,-c]], X, Y), psa(Y))). 2876% ?- ((X<<pow([a,b,c]), cnf_filter([[-a, -b, -c]], X, Y), psa(Y))). 2877cnf_filter([], X, X). 2878cnf_filter([F|Fs], X, Y):- 2879 ltr_join_filter(F, X, X0), 2880 cnf_filter(Fs, X0, Y). 2881 2882% 2883zdd_meet_list([A], A):-!. 2884zdd_meet_list([A|As], B):- zdd_meet_list(As, A, B). 2885% 2886zdd_meet_list([], X, X). 2887zdd_meet_list([A|As], X, Y):- zdd_meet(A, X, X0), 2888 zdd_meet_list(As, X0, Y). 2889% 2890zdd_join_list([], 0):-!. 2891zdd_join_list([X|Xs], Y):- zdd_join_list(Xs, X, Y). 2892% 2893zdd_join_list([], X, X):-!. 2894zdd_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2895 zdd_join_list(As, X0, Y). 2896 2897% 2898ltr_join_list([], 0):-!. 2899ltr_join_list([X|Xs], Y):-ltr_join_list(Xs, X, Y). 2900% 2901ltr_join_list([], X, X):-!. 2902ltr_join_list([A|As], X, Y):- zdd_join(A, X, X0), 2903 ltr_join_list(As, X0, Y). 2904 2905 2906 /********************* 2907 * remove atom * 2908 *********************/
2914% ?- ((family([[a,b,c],[a1,b,c1]], X), zdd_remove(b, X, Y), 2915% sets(Y, Sy))). 2916zdd_remove(X, Y, Z, S):- setup_call_cleanup( 2917 open_state(M, [hsize(256)]), 2918 zdd_remove(X, Y, Z, S, M), 2919 close_state(M)). 2920 2921zdd_remove(_, X, X, _, _):- X<2, !. 2922zdd_remove(A, I, J, S, M):- memo(zdd_remove(I)-J, S), 2923 ( nonvar(J) -> true 2924 ; cofact(I, t(Ai, Li, Ri), S), 2925 zdd_compare(C, A, Ai, S), 2926 ( C = (<) -> J = I 2927 ; C = (>) -> zdd_remove(A, Li, Lia, S, M), 2928 zdd_remove(A, Ri, Ria, S, M), 2929 cofact(J, t(Ai, Lia, Ria), S) 2930 ; zdd_join(Li, Ri, J, S) 2931 ) 2932 ). 2933 2934% ?- ltr_X<< dnf(a->b), psa(X), 2935% use_table(pred_remove_atoms(negative_literal, X, Y)), psa(Y). 2936 2937% ?- ltr_X<< dnf(a->b->c), psa(X), 2938 2939negative_literal(-(_)). 2940 2941:- meta_predicate pred_remove_atoms(, , ). 2942 2943pred_remove_atoms(_, X, X):- X<2, !. 2944pred_remove_atoms(Pred, I, J):- 2945 cofact(I, t(A, L, R)), 2946 pred_remove_atoms(Pred, L, L0), 2947 pred_remove_atoms(Pred, R, R0), 2948 ( call(Pred, A) -> 2949 zdd_join(L0, R0, J) 2950 ; cofact(J, t(A, L0, R0)) 2951 ). 2952 2953 /********************* 2954 * Cardinality * 2955 *********************/
2960% ?-N = 10000, numlist(1, N, Ns), time((X<<pow(Ns), card(X, _C))), _C=:=2^N. 2961%@ % 1,222,118 inferences, 0.127 CPU in 0.161 seconds (79% CPU, 9587871 Lips) 2962%@ N = 10000, 2963%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2964%@ X = 10001. 2965 2966%@ % 1,204,213 inferences, 0.179 CPU in 0.220 seconds (82% CPU, 6710726 Lips) 2967%@ N = 10000, 2968%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2969%@ X = 10001. 2970 2971% ?- X<<{[a], [b]}, card(X, C). 2972% ?- N = 10000, numlist(1, N, Ns),time( (X<< pow(Ns), card(X, C))). 2973%@ % 1,222,117 inferences, 0.112 CPU in 0.127 seconds (89% CPU, 10886196 Lips) 2974%@ N = 10000, 2975%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 2976%@ X = 10001, 2977 2978% ?- X<<card(pow([a,b]) + pow([c,d])). 2979%@ X = 7. 2980% ?- X<<card((+[a]) + (+[b])). 2981% ?- zdd. 2982% ?- X<<pow(numlist(1, 100)), card(X, D). 2983% ?- X<<pow(numlist(1, 100)), card(X, D), 2984% slim_gc(X, X1), slim_gc(X1, X2), slim_gc(X2, Y), 2985% card(Y, C). 2986%@ X = X1, X1 = X2, X2 = Y, Y = 101, 2987%@ D = C, C = 1267650600228229401496703205376. 2988 2989card(I, C):- open_memo(M), 2990 cardinality(I,C,M), 2991 close_memo(M). 2992% 2993cardinality(I, I, _):- I < 2, !. 2994cardinality(I, C, M):- memo(card(I)-C, M), 2995 ( nonvar(C) -> true 2996 ; cofact(I, t(_, L, R)), 2997 cardinality(R, Cr, M), 2998 cardinality(L, Cl, M), 2999 C is Cl + Cr 3000 ).
3004max_length(X, Max):- use_memo(max_length_with_memo(X, Max)). 3005 3006% 3007max_length_with_memo(X, 0):- X<2, !. 3008max_length_with_memo(X, Max):- 3009 memo(max(X)-Max), 3010 cofact(X, t(_, L, R)), 3011 ( nonvar(Max) -> true 3012 ; max_length_with_memo(L, ML), 3013 max_length_with_memo(R, MR), 3014 Max is max(1 + MR, ML) 3015 ). 3016 3017 /*********************** 3018 * Handy helpers * 3019 ***********************/ 3020 3021% 3022unify_zip([]). 3023unify_zip([X-X|R]):- unify_zip(R). 3024 3025 3026 /****************************************** 3027 * Oprations on clauses of literals * 3028 ******************************************/ 3029 3030% ?- ltr_compare(C, a, -a). 3031% ?- ltr_compare(C, -(a), a). 3032% ?- ltr_compare(C, -(b), a). 3033% ?- ltr_compare(C, -(a), b). 3034% ?- ltr_compare(C, -(a), -(b)). 3035% ?- ltr_compare(C, -(a), -(a)).
3042ltr_compare(C, -(X), -(Y)):-!, compare(C, X, Y). 3043ltr_compare(C, X, -(Y)):-!, compare(C0, X, Y), 3044 ( C0 == (=) -> C =(<) 3045 ; C0 = C 3046 ). 3047ltr_compare(C, -(X), Y):-!, compare(C0, X, Y), 3048 ( C0 == (=) -> C = (>) 3049 ; C0 = C 3050 ). 3051ltr_compare(C, X, Y):- compare(C, X, Y). 3052 3053% ?- ltr_compare(C, a, b). 3054% ?- ltr_compare(C, -a, a). 3055% ?- ltr_compare(C, a, -a). 3056% ?- ltr_compare(C, -a, b). 3057% ltr_compare(C, X, Y):- get_compare(F, S), 3058% call(F, C, X, Y).
3063% ?- ltr_sort([b, b, a], X).
3064% ?- ltr_sort([-b, b,-b, -a], X).
3069ltr_sort(X, Y):- get_compare(F), predsort(F, X, Y). 3070 3071 3072% ?- ((X << ltr_pow([a, -b, c]), ltr_memberchk([a, -b], X))). % false 3073% ?- ((X << ltr_pow([a, b, c]), ltr_memberchk([a, b, -c], X))). 3074% 3075ltr_memberchk(L, Z):- ltr_sort(L, L0), 3076 ltr_ord_memberchk(L0, Z). 3077% 3078ltr_ord_memberchk([], Z):- !, zdd_has_1(Z). 3079ltr_ord_memberchk([A|As], Z):- Z > 1, 3080 cofact(Z, t(B, L, R)), 3081 ltr_compare(C, A, B), 3082 ( C = (=) -> ltr_ord_memberchk(As, R) 3083 ; ltr_ord_memberchk([A|As], L) 3084 ). 3085 3086% ?- call_with_time_limit(100, time(((big_normal_form(30, X), resolve(X))))). 3087% ?- big_normal_form(1, X), ltr_card(X, C). 3088% ?- big_normal_form(2, X), ltr_card(X, C). 3089% ?- big_normal_form(3, X), ltr_card(X, C). 3090% ?- big_normal_form(10, X), ltr_card(X, C). 3091% ?- big_normal_form(20, X), ltr_card(X, C). 3092% ?- time(((big_normal_form(100, X), ltr_card(X, C)))). 3093% ?- time(((big_normal_form(10, X), ltr_card(X, C)))). 3094% ?- N=100, time((big_normal_form(N, X), ltr_card(X, C))), C=:=2^N. 3095 3096big_normal_form(0, 1). 3097big_normal_form(N, X):- N>0, 3098 N0 is N-1, 3099 big_normal_form(N0, X0), 3100 ltr_insert(N, X0, R), 3101 ltr_insert(-N, X0, L), 3102 zdd_join(L, R, X). 3103 3104% ?- numlist(1, 3, Ns), ( ltr_X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 3105% ?- numlist(1, 20, Ns), (ltr_X<<(pow(Ns)-1), ltr_choices(X, Y), ltr_card(Y, C)). 3106% ?- ltr_X<<((@a * @b)+ @c), ltr_choices(X, Y), psa(Y). 3107% ?- ltr_X<<{[a,b],[c,d]}, ltr_choices(X, Y), ltr_choices(Y, Z), 3108% ltr_choices(Z, U), psa(X), psa(Y), psa(Z), psa(U), ltr_choices(U, V), psa(V). 3109% ?- ltr_X<< {[a,b]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 3110% ?- ltr_X<< {[a,b,c]}, ltr_choices(X, Y), psa(X), {nl}, psa(Y). 3111% ?- ltr_X<< {[a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 3112% ?- ltr_X<< {[], [a, b], [c, d]}, ltr_choices(X, Y), psa(Y). 3113% ?- ltr_X<< {[a], [c, d]}, ltr_choices(X, Y), psa(Y). 3114% ?- ltr_X<< {[a,b], [c, d], [e,f]}, ltr_choices(X, Y), psa(Y). 3115% ?- ltr_X<< {[a,b]}, ltr_choices(X, Y), psa(Y). 3116% ?- ltr_X<< {[]}, ltr_choices(X, Y), psa(Y). 3117% ?- ltr_cnf(a, X), ltr_choices(X, Y), psa(Y). 3118% ?- ltr_cnf(a*b, X), ltr_choices(X, Y), psa(Y). 3119% ?- ltr_cnf(a* (-a), X), ltr_choices(X, Y), psa(Y). 3120 3121% ?- N=10, numlist(2, 10, Ns), (ltr_sample_cnf(Ns, X), ltr_card(X, C)). 3122% ?- N=100, numlist(2, N, Ns), (ltr_sample_cnf(Ns, X), card(X, C), resolve(X)). 3123 3124sample_cnf([], 1). 3125sample_cnf([J|Js], X):- sample_cnf(Js, Y), 3126 ltr_insert(J, Y, Z), 3127 ltr_insert(-J, Y, U), 3128 ltr_join(Z, U, X).
3134accessible_indices(I, A):- zdd_vector(Vec), 3135 accessible_indices(I, A0, [], Vec), 3136 sort(A0, A). 3137 3138accessible_indices(I, A, A, _):- I<2, !. 3139accessible_indices(I, [I|A], B, Vec):- arg(I, Vec, X), 3140 ( atomic(X) -> B = A 3141 ; child_term_indices(X, A, B, Vec) 3142 ). 3143% 3144% child_term_indices(t(_, _, _), A, A, _):-!. 3145child_term_indices(X, A, B, Vec):- X =.. [_|Xs], 3146 child_term_indices_list(Xs, A, B, Vec). 3147% 3148child_term_indices_list([], A, A, _). 3149child_term_indices_list([I|Is], A, B, Vec):- 3150 accessible_indices(I, A, C, Vec), 3151 child_term_indices_list(Is, C, B, Vec). 3152 3153% test sat. PASSED. [2023/11/09] 3154% ?- sat. 3155% ?- sat(-true). % false 3156% ?- sat(a+b), sat_count(C). 3157% ?- sat(a), sat(b). 3158% ?- sat(-(a + -a)). % false 3159% ?- sat(a), sat(b), sat_count(C). 3160% ?- sat(or(a, b)), sat_count(C). 3161% ?- sat(b), sat_count(C). 3162% ?- sat(xor(a, b)), sat_count(C). 3163% ?- sat(exor(a, b)), sat_count(C). 3164% ?- sat(e_x_o_r(a, b)), sat_count(C). 3165% ?- sat(a), sat(-a). % false. 3166% ?- sat(a), sat(a+b), sat_count(C). 3167% ?- sat(a(1)+a(2)), sat_count(C). 3168% ?- sat(A+a(2)), sat_count(C). 3169% ?- sat(A + B), sat_count(C). 3170% ?- sat(a+b+c+d), sat_count(C). 3171% ?- sat(a+b), sat(c+d), sat_count(C). 3172% ?- sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat_count(C). 3173% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat_count(C). 3174% ?- sat(X=(a=b)), sat(Y=(b+c)), sat(X=Y), sat(X = (-Y)). % false. 3175% ?- sat(*[p(1),p(2)]), sat_count(C). 3176% ?- sat(+[p(1),p(2)]), sat_count(C). 3177% ?- N=10, findall(p(I, J), 3178% (between(0, N, I), between(0, N, J)), L), sat(+L), sat_count(C). 3179% ?- N=10, findall(p(I, J), 3180% (between(0, N, I), between(0, N, J)), L), sat(*L), sat_count(C). 3181% ?-sat(a->b), sat(b->c), sat(c->d), sat(d->a), sat(-(d = b)). % false 3182% ?- E = (a=b)*(b=c)*(c=a), sat(E), sat_count(C). 3183% ?- sat(A + B), sat_count(C). 3184% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C). 3185% ?- sat(A -> B), Vs = [A,B], sat_count(+([1|Vs]), C). 3186% ?- sat(a=<(b=<a)), sat_count(Count). 3187% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3188% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3189% ?- Prop = 3190% ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)), 3191% sat(Prop), sat_count(C). 3192% ?- sat(a+b), sat(b+c), b_getval(sat_state, S), 3193% get_key(root, R, S), ltr_card(R, C, S). 3194% ?- sat(a+b+c), sat(-a), sat(-b), sat(-c). % false 3195% ?- sat(a=:=b), sat(b=:=c), sat(-(a=:=c)). % false 3196% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa. 3197% ?- sat(A=:=B), psa, sat(B=:=C), psa. 3198% ?- sat(a), sat(b), sat(c), sat_count(C). 3199% ?- Prop = 3200% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3201% sat(Prop), 3202% sat_count(Count). 3203% ?- sat, Prop = 3204% ( (-(B) -> F) * ((B * F) -> -(I)) * ((I + -(B)) -> -(F)) -> (I * F)), 3205% sat(-Prop), 3206% sat_count(Count). 3207 3208% ?- sat. 3209% ?- sat(A + B), sat_count(Count), A = B, sat_count(Count1). 3210% ?- sat(a), psa. 3211% ?- sat(a->(b->a)), sat(a->(b->a)), sat_count(C). 3212% ?- sat(A->(B->A)), sat(A->(B->A)), sat_count(C). 3213% ?- sat(a), sat(b), sat_count(C), psa. 3214% ?- sat(a+b+c), sat(-b), sat(-c), sat_count(C). 3215% ?- sat(X+A+B+C), sat(-B), sat(-C), sat_count(K). 3216% ?- N=3, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3217% ?- N=20, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3218% ?- N=100, numlist(1, N, Ns), sat(+Ns), sat_count(C). 3219% ?- N=100, numlist(1, N, Ns), sat(*Ns), sat_count(C). 3220% ?- sat(a+b+c), sat_count(C). 3221% ?- sat(x=a+b), sat(y=a+b+b+a), sat(-(x=y)), sat_count(C). % false 3222% ?- sat(x=a+b), sat(y=a+b+b+a), sat((x=y)), sat_count(C). 3223 3224 /************************************ 3225 * Setting Modes: zdd/sat/ltr * 3226 * call_with_zdd, setup_zdd * 3227 * for nested use of zdd * 3228 ************************************/ 3229 3230% 3231zdd:- open_state, nb_setval(zdd_stack, []). 3232% 3233sat:- open_state, nb_setval(zdd_stack, []), 3234 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3235 nb_linkval(zdd_compare, ltr_compare), 3236 nb_linkval(root, 1), 3237 open_memo(boole_atom, 32). 3238% 3239ltr:- open_state, nb_setval(zdd_stack, []), 3240 nb_linkval(zdd_extra, [varnum-0, atom_index-0]), 3241 nb_linkval(zdd_compare, ltr_compare), 3242 open_memo(boole_atom, 32). 3243 3244% ?- zdd, setup_zdd(g), 3245% call_with_zdd(memo(abc-X), g), X = 1, memo(abc-Y). 3246 3247% ?- call_with_zdd(memo(abc-X), g), X = 1, 3248% call_with_zdd(memo(abc-Y), g). 3249 3250% ?- call_with_zdd(memo(abc-X), g), X = 1, 3251% call_with_zdd(memo(abc-Y), g). 3252 3253% ?- N = 1000, zdd, 3254% time(( 3255% setup_zdd(z1), setup_zdd(z2), numlist(1, N, Ns), 3256% call_with_zdd( ( X<<pow(Ns), 3257% call_with_zdd((Y<<pow(Ns), card(Y, _D)), z2), 3258% card(X, _C) 3259% ), z1) 3260% )). 3261 3262:- meta_predicate call_with_zdd(, ). 3263call_with_zdd(E, G):- 3264 setup_call_cleanup( push_zdd_stack(G), 3265 call(E), 3266 pop_zdd_stack). 3267 3268% ?- setup_zdd(g). 3269setup_zdd(G) :- open_array_hash([], X), % normal zdd; 1,0 reserved. 3270 arg(1, X, A), 3271 setarg(1, A, 1), 3272 arg(2, A, V), 3273 setarg(1, V, 0), 3274 nb_linkval(G, X). 3275% 3276push_zdd_stack(G):- b_getval(zdd_node, A), 3277 b_getval(zdd_hash, H), 3278 b_getval(zdd_stack, Z), 3279 b_setval(zdd_stack, [#(A, H)|Z]), 3280 b_getval(G, #(A0, H0)), 3281 b_setval(zdd_node, A0), 3282 b_setval(zdd_hash, H0). 3283% 3284pop_zdd_stack:- b_getval(zdd_stack, [#(A1, H1)|Z1]), 3285 b_setval(zdd_node, A1), 3286 b_setval(zdd_hash, H1), 3287 b_setval(zdd_stack, Z1). 3288 3289 3290% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), ltr_card(X, C). 3291 3292% ?- sat, sat(X), sat(X\=Y), sat(Y). % fail. 3293% ?- sat, sat(X), sat(X\=Y), X=Y. % fail. 3294sat(X):- 3295 b_getval(root, Root), 3296 dnf(X, Y), 3297 ltr_merge(Y, Root, Root0), 3298 b_setval(root, Root0), 3299 Root0 \== 0. 3300% 3301sat_close:- close_state. 3302% 3303sat_count(C):- b_getval(root, X), ltr_card(X, C). 3304% 3305sat_clear:- close_state. 3306 3307% ?- sat, zdd_numbervars(f(X, Y, X)), get_attr(X, zsat, I), get_attr(Y, zsat, J). 3308zdd_numbervars(X):- get_key(varnum, N), 3309 term_variables(X, Vs), 3310 attr_numbervars(Vs, N, N0), 3311 set_key(varnum, N0). 3312 3313% 3314attr_numbervars([], N, N). 3315attr_numbervars([V|Vs], N, N0):- 3316 ( get_attr(V, zsat, _) -> 3317 attr_numbervars(Vs, N, N0) 3318 ; put_attr(V, zsat, N), 3319 K is N + 1, 3320 attr_numbervars(Vs, K, N0) 3321 ). 3322 3323% ?- heavy_valid_formula(H), prove(H). 3324heavy_valid_formula((((((((((((((((((((((((((((p13 <=> p12) <=> p11) <=> p10) 3325<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3326<=> p2) <=> p1) <=> p0) <=> p13) <=> p12) <=> p11) <=> p10) 3327<=> p9) <=> p8) <=> p7) <=> p6) <=> p5) <=> p4) <=> p3) 3328<=> p2) <=> p1) <=> p0)). 3329 3330% ?- ltr. 3331% ?- mk_left_assoc_term(=, 0, X), boole_nnf(X, Y). 3332% ?- mk_left_assoc_term(=, 1, X), prove(X). 3333% ?- X<< {[a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3334% ?- X<< {[a,b],[b,c]}, ltr_merge(X, X, Z), psa(Z). 3335% ?- X<< {[a,b],[b,c]}, zdd_merge(X, X, Z), psa(Z). 3336% ?- X<< {[-a]}, Y<<{[a,b],[b]}, ltr_merge(X, Y, Z), psa(Z). 3337% ?- run(1, 100). 3338% ?- run(2, 100). 3339% ?- run(5, 100). 3340% ?- run(1-9, 100). 3341% ?- run(11, 100). 3342% ?- run(12, 360). 3343%@ % 1,170,754,751 inferences, 139.220 CPU in 141.221 seconds (99% CPU, 8409411 Lips) 3344% imac 3345% on M1 mbp pro 32 GB, timeout. 3346 3347% ?- ltr, mk_left_assoc_term(==, 1, F), prove(F). 3348%@ VALID 3349%@ F = (((p(1)==p(0))==p(1))==p(0)). 3350run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3351 ( mk_left_assoc_term(==, K, F), 3352 format("~nPropositions: p(0) ... p(~w).~n", [K]), 3353 call_with_time_limit(T_limit, time(prove(F))))). 3354 3355% run(N0-N, T_limit) :-!, forall( between(N0, N, K), 3356% ( mk_left_assoc_term(==, K, F), 3357% format("~nPropositions: p(0) ... p(~w).~n", [K]), 3358% call_with_time_limit(T_limit, time(seq:seq_prove(F))))). 3359% 3360run(N, T) :- run(N-N, T). 3361 3362% ?- mk_left_assoc_term(==, 1, X), write_canonical(X), print(X). 3363% ?- mk_left_assoc_term(<=>, 13, X), write_canonical(X). 3364 3365mk_left_assoc_term(Bop, N, Ex):- findall(p(I), between(0, N, I), L), 3366 append(L, L, L2), 3367 reverse(L2, R), 3368 apply_left_assoc(Bop, R, Ex). 3369% 3370apply_left_assoc(Bop, [X|Y], Ex):- apply_left_assoc(Bop, X, Y, Ex). 3371% 3372apply_left_assoc(_, X, [], X):-!. 3373apply_left_assoc(Bop, U, [X|Y], W):- V=..[Bop, U, X], 3374 apply_left_assoc(Bop, V, Y, W). 3375 3376demorgan( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). 3377 3378% Valid formulae. 3379% ?- ltr. 3380% ?- forall(valid_formula(A), prove(A)). 3381valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)). 3382valid_formula((-(-a) -> a) * (a -> -(-a))). % Double Negation 3383valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law 3384valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b). 3385valid_formula(a + -a). 3386valid_formula(((a -> b) -> a) -> a). % Peirce’s Law 3387valid_formula(-(-a)->a). 3388valid_formula(a -> a). 3389valid_formula(a -> (b -> a)). 3390valid_formula((a->b)->((b->c)->(a->c))). 3391valid_formula(a->((a->b)->b)). 3392valid_formula((a*(a->b))->b). 3393valid_formula((a->b)->(-b -> -a)). 3394valid_formula((a->b)->((b->c)->(a->c))). 3395valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)). 3396 3397% ?- ltr. 3398% ?- forall(invalid_formula(A), prove(A)). 3399invalid_formula(a). 3400invalid_formula((a->b)->a). 3401invalid_formula((a->b)->(b->a)). 3402invalid_formula(a -> (b -> c)). 3403invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)). 3404invalid_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))).3435prove(X):- 3436 ( prove_(X) 3437 -> writeln('VALID') 3438 ; writeln('INVALID') 3439 ). 3440 3441% 3442prove_(X):- cnf(-X, CNF), 3443 get_key(atom_index, N), 3444 ( CNF = 0 -> N = 0 3445 ; CNF = 1 -> N > 0 3446 ; resolve(CNF) 3447 ).
3453% ?- ltr_ltr_pow([a,b,c], P), resolve(P), psa(P). 3454% ?- numlist(1, 10, L), (ltr_ltr_pow(L, P), ltr_card(P, C)). 3455% ?- numlist(1, 100, L), (ltr_ltr_pow(L, P), ltr_card(P, C)). 3456% ?- N = 100000, numlist(1, N, L), time( (ltr_ltr_pow(L, P), resolve(P))). 3457resolve(X):- zdd_has_1(X), !. % The empty clause found. 3458resolve(X):- X > 1, 3459 cofact(X, t(A, L, R)), 3460 ( L = 0 -> fail % Pure literal rule. 3461 ; A = -(_) -> resolve(L) % Negative pure literal rule. 3462 ; ( cofact(L, t(B, U, V)), % Pure literal rule. 3463 ( B = -(A) 3464 -> ltr_merge(V, R, M), % Resolution + Tautology rule. 3465 ltr_join(U, M, W), 3466 resolve(W) % Updated set of clauses. 3467 ; resolve(L) % Posituve pure literal rule. 3468 ) 3469 ) 3470 ). 3471 3472% ?- sat. 3473% ?- N=100, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3474%@ false. 3475% ?- N=2, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3476%% Debug. 3477% ?- N=11, numlist(0, N, Ns), sat(*Ns), sat_count(C). 3478%@ false. <=== why ??? 3479 3480% ?- ltr. 3481% ?- N = 100, time((numlist(1, N, L), ltr_pow(L, P), 3482% A << set(L), zdd_subtr(P, A, Q), card(Q, C), 3483% writeln(C), resolve(Q))). % false 3484 3485% ?- N = 100000, time((numlist(1, N, _L), ltr_pow(_L, P), 3486% card(P, _C))), _C=:= 2^N. 3487 3488%@ % 31,011,164 inferences, 8.180 CPU in 12.708 seconds (64% CPU, 3790924 Lips) 3489%@ N = 100000, 3490%@ P = 300001. 3491 3492atom_index(X):- memo(atom_index(X)-Y), 3493 ( nonvar(Y) -> true 3494 ; get_key(atom_index, Y), 3495 memo(index_atom(Y)-X), 3496 Y0 is Y + 1, 3497 set_key(atom_index, Y0) 3498 ). 3499 3500% ?- mk_left_assoc_term(==, 1, F), boole_nnf(F, Y), (ltr_nnf_cnf(Y, Z), psa(Z)). 3501boole_nnf(X, Y):- % numbervars_index(X, S), 3502 basic_boole(X, Z), 3503 once(neg_normal(Z, Y)). 3504 3505% ?- ltr, basic_boole(a, A). 3506% ?- ltr, basic_boole(@(a), A). 3507% ?- ltr, basic_boole(0, A). 3508% ?- ltr, basic_boole(1, A). 3509% ?- ltr, basic_boole(true, A). 3510% ?- ltr, basic_boole(a+b, A). 3511% ?- ltr, basic_boole(a+b+c, A). 3512% ?- ltr, basic_boole(-a + b + c, A). 3513% ?- ltr, basic_boole(a -> b -> c, A). 3514% ?- ltr, basic_boole((a -> b) -> c, A). 3515% ?- ltr, basic_boole(*[(a -> b), c], A). 3516% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3517% ?- ltr, basic_boole(*[(0 -> 1)->2], A). 3518% ?- ltr, basic_boole(*[0, 1, 2], A). 3519 3520% ?- ltr. 3521% ?- trace. 3522% ?- ltr, set_key(f, 0), N = 100, numlist(0, N, Ns), 3523% test_rev_memo(Ns), test_rev_memo. 3524 3525test_rev_memo :- get_key(f, K), 3526 K0 is K - 1, 3527 forall(between(0, K0, I), 3528 ( memo(g(I)-R), 3529 ( nonvar(R), memo(f(R)-I) -> true 3530 ; writeln(not(memo(f(R)-I))) 3531 ) 3532 )). 3533 3534test_rev_memo([]). 3535test_rev_memo([A|As]):- memo(f(A)-B), 3536 ( var(B) -> 3537 get_key(f, B), 3538 memo(g(B)-A), 3539 B0 is B + 1, 3540 set_key(f, B0) 3541 ; true 3542 ), 3543 test_rev_memo(As). 3544 3545 3546% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3547% forall(member(I, Ns), (memo(atom_index(I)-A), writeln(atom_index(I)-A))). 3548 3549% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), b_getval(zdd_hash, M), 3550% arg(3, M, V), maplist(writeln, V). 3551 3552% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), 3553% b_getval(zdd_hash, #(_,_, V)), get_key(atom_index, AtomIndex), 3554% numlist(0, AtomIndex, Is), 3555% maplist(memo_index_atom, Is, As). 3556 3557% ?- listing(memo_index_atom). 3558 3559memo_index_atom(I, A):- memo(index_atom(I)-A). 3560 3561% ?- spy(atom_index). 3562% ?- ltr, N = 100, numlist(1, N, Ns), X<< dnf(+Ns), 3563% get_key(atom_index, K), K0 is K - 1, 3564% numlist(0, K0, Is), 3565% maplist(atom_index, As, Is, As). 3566 3567% ?- ltr, N=100, numlist(1, N, Ns), X<< dnf(+Ns), zdd_boole_atoms(As), forall(between(1, N, J), 3568% once((memo(index_atom(J)-X, boole_atom), 3569% writeln(memo(index_atom(J)-X))))). 3570% 3571% ?- ltr, N = 100000, numlist(0, N, Ns), 3572% maplist(memo_atom, Ns, Is), 3573% maplist(memo_atom, Ns, Is). 3574 3575% ?- ltr, N = 83, numlist(0, N, Ns), 3576% maplist(memo_atom, Ns, Is), 3577% maplist(memo_atom, R, Is), 3578% memo_atom(86, K), memo_atom(87, L), 3579% maplist(memo_atom, U, Is), get_key(atom_index, A), 3580% memo_atom(30, B). 3581 3582% ?- ltr, N = 10000, numlist(0, N, As), 3583% maplist(atom_index, As, Is), 3584% maplist(atom_index, As0, Is), 3585% As = As0, 3586% atom_index(hello, I), 3587% atom_index(A, I). 3588 3589% ?- ltr, atom_index(X, 2). % false. 3590%@ atom_index(_346,2) 3591%@ true. 3592% ?- ltr, N=3, K=100, open_hash(N, H), nb_setval(zdd_hash, H), !, 3593% numlist(1, K, Ks), X<< dnf(+Ks). 3594 3595memo_atom(X):- atom_index(X, _). 3596 3597memo_atom(X, I):- atom_index(X, I). 3598 3599% 3600atom_index(X, I):- var(X), !, memo(index_atom(I)-X). 3601atom_index(X, I):- 3602 memo(atom_index(X)-I), 3603 ( var(I) -> 3604 get_key(atom_index, I), 3605 J is I + 1, 3606 set_key(atom_index, J), 3607 memo(index_atom(I)-X) 3608 ; true 3609 ). 3610 3611% ?- sat. 3612% ?- sat(A=B), sat(B=C), sat_count(D). 3613basic_boole(A, @('$VAR'(I))):-var(A), !, get_attr(A, zsat, I), 3614 memo_atom('$VAR'(I)). 3615basic_boole(A, BoolConst):-atomic(A), 3616 boole_op(0, [], Fs, BoolConst), 3617 memberchk(A, Fs), 3618 !. 3619basic_boole(I, @(I)):- integer(I), !, memo_atom(I). 3620basic_boole(@(I), @(I)):-!, memo_atom(I). 3621basic_boole(*(L), F):-!, basic_boole_vector(L, *, F). 3622basic_boole(+(L), F):-!, basic_boole_vector(L, +, F). 3623basic_boole(X, Y):- X=..[F|Xs], 3624 length(Xs, N), 3625 boole_op(N, As, Fs, Y), 3626 memberchk(F, Fs), 3627 !, 3628 basic_boole_list(Xs, As). 3629basic_boole(X, @(X)):- memo_atom(X). 3630 3631% 3632basic_boole_list([], []). 3633basic_boole_list([X|Xs], [Y|Ys]):- basic_boole(X, Y), 3634 basic_boole_list(Xs, Ys). 3635% 3636basic_boole_vector([], +, false):-!. 3637basic_boole_vector([], *, true):-!. 3638basic_boole_vector([X|Xs], F, Y):- 3639 basic_boole(X, X0), 3640 Y=..[F, X0, Z], 3641 basic_boole_vector(Xs, F, Z). 3642 3643% Remark [2023/11/13]: 3644% Use of 0/1 as Boolean constants has been dropped. 3645% Any integer is now usable for a boolean variable, which 3646% may be useful or (nested) vectors of integers *[...], +[...]. 3647% 0/1 as boolean is error prone because ZDD must use 0/1 internally 3648% as basic constant similar, but not exactly the same, 3649% to true/flase. They are different. 3650% This decision was hard because 0/1 is traditionally useful 3651% as boolean constrants, but clear separation and simplicity 3652% were preferred. 3653 3654boole_op(0, [], [false, ff], false). % 0 for false dropped. 3655boole_op(0, [], [true, tt], true). % 1 for true dropped. 3656boole_op(1, [X], [-, ~, \+, not], -(X)). 3657boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y). 3658boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y). 3659boole_op(2, [X, Y], [->, imply], -X + Y). 3660boole_op(2, [X, Y], [<-], Y->X). 3661boole_op(2, [X, Y], [iff, ==, =, =:=, equiv, ~, <->, <=>], (-X)* (-Y) + X*Y). 3662boole_op(2, [X, Y], [=\=, \=, xor, #], (-X)*Y + X*(-Y)). % -(X==Y) = xor(X, Y) 3663boole_op(2, [X, Y], [nand], -(X) + (-Y)). 3664 3665 3666% ?- neg_normal(-(true + b), X). 3667% ?- neg_normal(-(a), X). 3668% ?- neg_normal(-(a), X). 3669% ?- neg_normal(-(a), X). 3670neg_normal(true, true). 3671neg_normal(false, false). 3672neg_normal(-(false), true). 3673neg_normal(-(true), false). 3674neg_normal(-(-X), Z) :- neg_normal(X, Z). 3675neg_normal(-(X+Y), Z) :- neg_normal(-X* -Y, Z). 3676neg_normal(-(X*Y), Z) :- neg_normal(-X+ -Y, Z). 3677neg_normal(-(X), -(Y)) :- neg_normal(X, Y). 3678neg_normal(X+Y, X0+Y0) :- neg_normal(X, X0), 3679 neg_normal(Y, Y0). 3680neg_normal(X*Y, X0*Y0) :- neg_normal(X, X0), 3681 neg_normal(Y, Y0). 3682neg_normal(@(X), @(X)):-!. 3683neg_normal(X, @(X)):-!.
intern(-(a;b;c), X), boole_to_dnf(X, Z), sets(Z, U), extern(U, Y)).3692extern(X, Y):-integer(X), !, 3693 ( X < 2 -> Y = X 3694 ; memo(index_atom(X)-Y) 3695 ). 3696extern(X, X):- atomic(X), !. 3697extern(X, Y):- X =.. [F|Xs], 3698 extern_list(Xs, Ys), 3699 Y =..[F|Ys]. 3700% 3701extern_list([], []). 3702extern_list([X|Xs], [Y|Ys]):- extern(X, Y), 3703 extern_list(Xs, Ys). 3704 3705 /********************************************* 3706 * Cofact/insert/join/merge on literals * 3707 *********************************************/
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 ).3722ltr_cofact(Z, Y):- nonvar(Z), !, cofact(Z, Y). 3723ltr_cofact(Z, t(A, V, U)):- U > 1, !, 3724 cofact(U, t(B, L, _)), 3725 ( ltr_invert(A, B) 3726 -> ltr_cofact(Z, t(A, V, L)) 3727 ; cofact(Z, t(A, V, U)) 3728 ). 3729ltr_cofact(Z, T):- cofact(Z, T).
3738% ?- ltr. 3739% PASS. 3740% ?- cnf(a*b, X), ltr_insert(c, X, Y), sets(Y, S). 3741 3742% ?- ltr. 3743% ?- dnf((-a)*b, X), ltr_insert(a, X, Y), sets(Y, S). 3744% ?- ltr_insert(a, 1, X), sets(X, S). 3745% ?- ltr_insert(a, 1, X), ltr_insert(b, X, Y), sets(Y, S). 3746% ?- ltr_insert(a, 1, X), ltr_insert(b, X, Y), 3747% ltr_insert(-b, Y, Z), sets(Z, S). 3748% ?- X<<set([a]), ltr_insert(b, X, Y), psa(Y). 3749% ?- X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3750% ?- X<<set([b]), ltr_insert(a, X, Y), psa(Y). 3751% ?- X<<set([a]), ltr_insert(-a, X, Y), psa(Y). 3752% ?- X<<set([-a]), ltr_insert(a, X, Y), psa(Y))). 3753% ?- X<<{[a,b,c],[u,v]}, ltr_insert(-b, X, Y), psa(Y). 3754% ?- X<<{[a,b,c],[u,v]}, ltr_insert(b, X, Y), psa(Y). 3755% ?- X<<{[a,b,c],[u,v]}, ltr_insert(u, X, Y), psa(Y). 3756% ?- X<<{[a]}, ltr_insert(a, X, Y), psa(Y). 3757% ?- X<<{[a,b,c]}, ltr_insert(-b, X, Y), psa(Y). 3758% ?- X<<{[a,b],[c]}, ltr_insert(-b, X, Y), psa(Y). 3759% ?- X<<{[a,-b],[c]}, ltr_insert(b, X, Y), psa(Y). 3760% ?- X<<{[a,b]}, ltr_insert(-b, X, Y), psa(Y). 3761% ?- X<< dnf(a), ltr_insert(b, X, Y), psa(Y). 3762% ?- X<< dnf(a*c), ltr_insert(b, X, Y), psa(Y). 3763% ?- X<< dnf(-a + b), ltr_insert(a, X, Y), psa(Y). 3764% ?- X<< dnf((x=\=y)*x*y), psa(X). 3765% ?- X<< dnf((x=\=y)*x*y), psa(X). 3766% ?- sat((x=\=y)*x*y). % false 3767% ?- sat((a * -a)). % false 3768% ?- dnf((-a)*b, X), psa(X), ltr_insert(-a, X, Y), psa(Y). 3769% ?- dnf((-a)*b, X), psa(X), ltr_insert(-b, X, Y), psa(Y). 3770% ?- dnf((-a)*b, X), psa(X), ltr_insert(b, X, Y), psa(Y). 3771% ?- dnf((-a)*b, X), psa(X). 3772% ?- cnf((-a)*b, X). 3773% ?- cnf((a), X). 3774 3775ltr_insert(_, 0, 0):-!. 3776ltr_insert(A, 1, J):-!, zdd_singleton(A, J). 3777ltr_insert(A, I, J):- memo(ltr_insert(A,I)-J), 3778 ( nonvar(J) -> true 3779 ; cofact(I, t(B, L, R)), 3780 zdd_compare(C, A, B), 3781 ( C = (<) -> 3782 ( complementary(A, B) -> 3783 cofact(J, t(A, 0, L)) 3784 ; cofact(J, t(A, 0, I)) 3785 ) 3786 ; C = (=) -> 3787 ( negative(A) -> 3788 ltr_join(L, R, K), 3789 cofact(J, t(A, 0, K)) 3790 ; ltr_insert_aux(J, A, L, R) 3791 ) 3792 ; ( complementary(A, B) -> ltr_insert(A, L, J) 3793 ; ltr_insert(A, L, L0), 3794 ltr_insert(A, R, R0), 3795 cofact(J, t(B, L0, R0)) 3796 ) 3797 ) 3798 ). 3799 3800% for suppressing use of cofact/3 and ltr_insert/4 3801ltr_insert_aux(J, A, L, R):- % A is positive. R has no -A. 3802 ( L < 2 -> cofact(J, t(A, L, R)) 3803 ; cofact(L, t(B, L0, _)), 3804 ( complementary(A, B)-> 3805 ltr_join(L0, R, K), 3806 cofact(J, t(A, 0, K)) 3807 ; ltr_join(L, R, K), 3808 cofact(J, t(A, 0, K)) 3809 ) 3810 ).
3816% 3817ltr_join(X, X, X):-!. % idemopotent law of logical disjunction (OR) 3818ltr_join(0, X, X):-!. 3819ltr_join(X, 0, X):-!. 3820ltr_join(1, _, 1):-!. 3821ltr_join(_, 1, 1):-!. 3822ltr_join(X, Y, Z):- 3823 ( X=<Y -> memo(ltr_join(X,Y)-Z) 3824 ; memo(ltr_join(Y,X)-Z) 3825 ), 3826 ( nonvar(Z) -> true %, write(.) 3827 ; cofact(X, t(A, L, R)), 3828 cofact(Y, t(A0, L0, R0)), 3829 zdd_compare(C, A, A0), 3830 ( C = (=) -> 3831 ltr_join(R, R0, U), 3832 ltr_join(L, L0, V), 3833 cofact(Z, t(A, V, U)) 3834 ; C = (<) -> 3835 ltr_join(L, Y, U), 3836 cofact(Z, t(A, U, R)) 3837 ; ltr_join(L0, X, U), 3838 cofact(Z, t(A0, U, R0)) 3839 ) 3840 ).
3849ltr_merge(X, X, X):-!. % idempotent law of logical conjunction (AND). 3850ltr_merge(0, _, 0):-!. 3851ltr_merge(_, 0, 0):-!. 3852ltr_merge(1, X, X):-!. 3853ltr_merge(X, 1, X):-!. 3854ltr_merge(X, Y, Z):- 3855 ( X =< Y -> memo(ltr_merge(X,Y)-Z) 3856 ; memo(ltr_merge(Y,X)-Z) 3857 ), 3858 ( nonvar(Z) -> true 3859 ; cofact(Y, t(A, L, R)), 3860 ltr_merge(X, R, U), 3861 ltr_merge(X, L, V), 3862 ltr_insert(A, U, U0), 3863 ltr_join(V, U0, Z) 3864 ).
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).3871ltr_xor(X, Y, Z):- 3872 ltr_negate(Y, Y0), 3873 ltr_merge(X, Y0, U), 3874 ltr_negate(X, X0), 3875 ltr_merge(X0, Y, V), 3876 ltr_join(U, V, Z). 3877 3878 /****************************************** 3879 * Auxiliary operations on literals * 3880 ******************************************/
3884complementary(-(A), A):-!. 3885complementary(A, -(A)). 3886% 3887negative(-(_)).
3895% ?- ltr_pow([a], X), card(X, C), psa(X). 3896% ?- ltr_pow([a, b], X), card(X, C), psa(X). 3897% ?- numlist(1, 100, L), ltr_pow(L, X), card(X, C). 3898ltr_pow([], 1). 3899ltr_pow([A|As], P):- ltr_pow(As, Q), 3900 ltr_insert(A, Q, R), 3901 ltr_insert(-A, Q, L), 3902 ltr_join(L, R, P).
3910% ?- ltr_append([-b, a, -d, c], 1, X), psa(X). 3911% ?- ltr_append([-b, -d, c], 1, X), psa(X). 3912% ?- ltr_append([-b, -d, c], 1, X), psa(X). 3913% ?- X<<dnf(a->a), ltr_card(X, C), psa(X). 3914% 3915ltr_append([], X, X). 3916ltr_append([A|As], X, Y):- ltr_append(As, X, X0), 3917 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))).3925% 3926ltr_set(X, Y):- ltr_append(X, 1, Y).
3933% ?- ((set_compare(ltr_compare), zdd_sort([-(3), 2, 3], L))). 3934% ?- ((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), sets(Y, Y0))). 3935% ?- ((set_compare(ltr_compare), X<<dnf(a), ltr_negate(X, Y), sets(Y, Y0))). 3936% ?- ((set_compare(ltr_compare), X<<dnf(a*b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3937% ?- ((set_compare(ltr_compare), X<<dnf(a+b), ltr_negate(X, Y), ltr_negate(Y, Z), sets(Y, Y0), sets(Z, Z0))). 3938 3939% ?- X<<dnf(a), ltr_negate(X, Y), psa(Y). 3940% ?- ltr_negate(0, Y), psa(Y). 3941% ?- ltr_negate(1, Y), psa(Y). 3942 3943% 3944ltr_negate(X, Y):- ltr_complement(X, X0), ltr_choices(X0, Y).
3953% ?- zdd, X<<{[a, -b],[-b],[b, c]}, ltr_complement(X, Y), psa(Y). 3954% ?- zdd, X<<{[-b],[-b],[b, c]}, psa(X), ltr_complement(X, Y), psa(Y). 3955% 3956ltr_complement(X, X):- X<2, !. 3957ltr_complement(I, Y):- memo(ltr_complement(I)-Y), 3958 ( nonvar(Y) -> true 3959 ; cofact(I, t(A, L, R)), 3960 ltr_complement(L, L0), 3961 ltr_complement(R, R0), 3962 complementary(A, NA), 3963 ltr_insert(NA, R0, R1), 3964 ltr_join(L0, R1, Y) 3965 ). 3966 3967 /************************************ 3968 * Convert Boolean Form to DNF/CNF * 3969 ************************************/
3974% ?- boole_nnf(-(a+b), X). 3975% ?- zdd, dnf(-(A+B), X), psa(X), get_key(atom_index, N), get_key(varnum,V). 3976% ?- ((dnf(-(a=:=b), X), psa(X))). 3977% ?- ((dnf((a=\=b), X), psa(X))). 3978% ?- ((dnf((0), X), psa(X))). 3979% ?- ((dnf(*[1,3,2,3], X), psa(X))). 3980% ?- zdd, dnf(+[1,3,2,3], X), psa(X), psa(2), psa(3), psa(4), get_key(atom_index, I). 3981% ?- ((dnf(*[@(1),3,2,3], X), psa(X))). 3982 3983dnf(X, Y):- zdd_numbervars(X), 3984 boole_nnf(X, Z), 3985 nnf_dnf(Z, Y).
3994% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), dnf_cnf(Z, Y), psa(X), psa(Y). 3995% ?- X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), dnf_cnf(Z, U). 3996% ?- big_normal_form(100, X), dnf_cnf(Y, X), card(X, C), card(Y, D). 3997 3998dnf_cnf(X, Y):- nonvar(X), !, ltr_choices(X, Y). 3999dnf_cnf(X, Y):- ltr_choices(Y, X). 4000% 4001cnf_dnf(X, Y):- dnf_cnf(X, Y). 4002 4003% ?- X<< cnf(a), psa(X), cnf_dnf(X, Y), psa(Y). 4004%@ * Call: (47) zmod:cnf(a, _18746, s(..)) ? no debug 4005% ?- X<< cnf(a*b), psa(X), cnf_dnf(X, Y), psa(Y). 4006% ?- X<< dnf(a), psa(X), dnf_cnf(X, Y), psa(Y). 4007% ?- X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 4008% ?- X<< dnf(a+b), psa(X), dnf_cnf(X, Y), psa(Y). 4009% ?- X<< dnf(a*b), psa(X), dnf_cnf(X, Y), psa(Y). 4010% ?- X<< dnf(a+b*c), psa(X), dnf_cnf(X, Y), psa(Y). 4011% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 4012% dnf_cnf(Z, Y), psa(X), psa(Y). 4013 4014% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 4015% dnf_cnf(Z, Y), psa(X), psa(Y). 4016 4017% ?- X<<dnf((a+ -b)*(-a + b)), dnf_cnf(X, Y), 4018% dnf_cnf(Z, Y). 4019 4020% ?- X<<dnf(a+b), dnf_cnf(X, Y), dnf_cnf(Z, Y), 4021% dnf_cnf(Z, U). 4022 4023% ?- N=100, time((big_normal_form(N, X), 4024% dnf_cnf(Y, X), card(X, C), card(Y, D))). 4025%@ % 2,957,705 inferences, 0.205 CPU in 0.208 seconds (99% CPU, 14447986 Lips) 4026%@ N = 100, 4027%@ X = 39901, 4028%@ Y = D, D = 0, % <== CORRECT. 4029%@ C = 1267650600228229401496703205376 . 4030 4031% ?- N=1000, time((big_normal_form(N, X), 4032% dnf_cnf(Y, X), card(X, C), card(Y, D))). 4033%@ % 254,040,893 inferences, 30.822 CPU in 31.624 seconds (97% CPU, 8242275 Lips) 4034%@ N = 1000, 4035%@ X = 3999001, 4036%@ Y = D, D = 0, % <== CORRECT. 4037%@ C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376 .
4051ltr_choices(0, 1):-!. 4052ltr_choices(1, 0):-!. 4053ltr_choices(X, Y):- memo(ltr_choices(X)-Y), 4054 ( nonvar(Y)->true %, write(.) % many hits. 4055 ; cofact(X, t(A, L, R)), 4056 ltr_choices(L, L0), 4057 ltr_choices(R, R0), 4058 cofact(R1, t(A, R0, 1)), 4059 ltr_merge(L0, R1, Y) 4060 ).
4065nnf_dnf(false * _, 0):-!. 4066nnf_dnf(_ * false, 0):-!. 4067nnf_dnf(true * X, Y):-!, nnf_dnf(X, Y). 4068nnf_dnf(X * true, Y):-!, nnf_dnf(X, Y). 4069nnf_dnf(X * Y, Z):-!, memo(dnf(X*Y)-Z, boole_atom), 4070 ( nonvar(Z) -> true 4071 ; nnf_dnf(X, U), 4072 nnf_dnf(Y, V), 4073 ltr_merge(U, V, Z) 4074 ). 4075nnf_dnf(false + X, Y):-!, nnf_dnf(X, Y). 4076nnf_dnf(X + false, Y):-!, nnf_dnf(X, Y). 4077nnf_dnf(true + X, Y):-!, nnf_dnf(X, Z), 4078 ltr_join(1, Z, Y). 4079nnf_dnf(X + true, Y):-!, nnf_dnf(X, Z), 4080 ltr_join(1, Z, Y). 4081nnf_dnf(X + Y, Z):-!, memo(dnf(X+Y)-Z, boole_atom), 4082 ( nonvar(Z) -> true 4083 ; nnf_dnf(X, U), 4084 nnf_dnf(Y, V), 4085 ltr_join(U, V, Z) 4086 ). 4087nnf_dnf(@(X), I):-!, zdd_singleton(X, I). 4088nnf_dnf(-(@(X)), I):- zdd_singleton(-(X), I).
4095% ?- ltr. 4096% ?- ((cnf(a, X), S<<sets(X))). 4097% ?- ((cnf(a*b, X), S<<sets(X))). 4098% ?- ((X<<cnf(-a), Y<<sets(X))). 4099% ?- ((X<<cnf(a+b), Y<<sets(X))). 4100% ?- ((X<<cnf(+([a,b,c])), Y<<sets(X))). 4101% ?- ((X<<cnf(*([a,b,c])), Y<<sets(X))). 4102% ?- ((X<<dnf(+([a,b,c])), Y<<sets(X))). 4103% ?- ((X<<dnf(*([a,b,c])), Y<<sets(X))). 4104% ?- ((cnf(a, X), psa(X))). 4105% ?- ((cnf(-a, X), psa(X))). 4106% ?- ((cnf(a+b, X), psa(X))). 4107% ?- ((cnf(a+b+(-c), X), psa(X))). 4108% ?- ((cnf(-a * a, X), psa(X))). 4109% ?- ((cnf(a->a, X), psa(X))). 4110% ?- ((cnf(-a * a, X), psa(X))). 4111% ?- ((cnf( a + a, X), psa(X))). 4112% ?- ((cnf( A + A, X), psa(X))). 4113% ?- ((cnf(-(a*b), X), psa(X))). 4114% ?- ((cnf(*([a,b,c]), X), psa(X))). 4115% ?- ltr, N = 10, numlist(2, N, Ns), cnf(*(Ns), X), ltr_card(X, C). 4116% ?- ((dnf(a, X), psa(X))). 4117% ?- ((cnf(-(a->b), X), psa(X))). 4118% ?- ((cnf(a, X), psa(X))). 4119% ?- boole_nnf(-(*[0,1,2]), X). 4120% ?- ltr, mk_left_assoc_term(==, 1, F), cnf(F, X), psa(X). 4121 4122cnf(X, Y):- zdd_numbervars(X), 4123 boole_nnf(X, Z), 4124 nnf_cnf(Z, Y). 4125% 4126nnf_cnf(true, 1):-!. 4127nnf_cnf(false, 0):-!. 4128nnf_cnf(false * _, 0):-!. 4129nnf_cnf(_ * false, 0):-!. 4130nnf_cnf(true * X, Y):-!, nnf_cnf(X, Y). 4131nnf_cnf(X * true, Y):-!, nnf_cnf(X, Y). 4132nnf_cnf(X * X, Y):-!, nnf_cnf(X, Y). 4133nnf_cnf(X * Y, Z):-!, memo(cnf(X*Y)-Z, boole_atom), 4134 ( nonvar(Z)->true %, write(.) % many hits. 4135 ; nnf_cnf(X, U), 4136 nnf_cnf(Y, V), 4137 ltr_join(U, V, Z) 4138 ). 4139nnf_cnf(false + X, Y):-!, nnf_cnf(X, Y). 4140nnf_cnf(X + false, Y):-!, nnf_cnf(X, Y). 4141nnf_cnf(true + _, 1):-!. 4142nnf_cnf(_ + true, 1):-!. 4143nnf_cnf(X + X, Y):-!, nnf_cnf(X, Y). 4144nnf_cnf(X + Y, Z):-!, memo(cnf(X+Y)-Z, boole_atom), 4145 ( nonvar(Z)->true %, write(+) % many hits. 4146 ; nnf_cnf(X, U), 4147 nnf_cnf(Y, V), 4148 ltr_merge(U, V, Z) 4149 ). 4150nnf_cnf(@(X), I):-!, zdd_singleton(X, I). 4151nnf_cnf(-(@(X)), I):- zdd_singleton(-(X), I). 4152 4153 4154 /***************************************************** 4155 * ltr_card/[3,4] Counting solutions of a DNF. * 4156 *****************************************************/ 4157 4158% ?- sat(a), sat_count(C). 4159% ?- sat(A+B), sat_count(C), zsat:(A=B), sat_count(D). 4160% ?- sat(A+B), sat_count(C), A = B, sat_count(D). 4161% ?- X<< dnf(a), sat_count_by_collect_atoms(X, C). 4162% ?- sat_count_by_collect_atoms(a+b, C). 4163% ?- sat_count_by_collect_atoms((a->b)*(b->c)->(b->c), C). 4164% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 4165 4166% ?- sat. 4167% ?- length(L, 1000), sat_count_by_collect_atoms(+L, C). 4168% 4169sat_count_by_collect_atoms(F, C):- dnf(F, X), 4170 zdd_boole_atoms(Us), 4171 zdd_sort(Us, Vs), 4172 expand_dnf(Vs, X, Y), 4173 card(Y, C). 4174 4175% ?- ltr, N=100, numlist(0, N, Ns), X<<dnf(+Ns), zdd_boole_atoms(Us). 4176%@ N = 100, 4177%@ Ns = Us, Us = [0, 1, 2, 3, 4, 5, 6, 7, 8|...], 4178%@ X = 202. 4179 4180zdd_boole_atoms(Us):- get_key(atom_index, N), 4181 collect_boole_atoms(0, N, Us). 4182 4183% 4184collect_boole_atoms(I, N, []):- I>=N, !. 4185collect_boole_atoms(I, N, [A|U]):- 4186 atom_index(A, I), 4187 J is I+1, 4188 collect_boole_atoms(J, N, U). 4189 4190 /****************************** 4191 * find_counter_example * 4192 ******************************/
4196% ?- findall_counter_examples(a, X), psa(X). 4197% ?- findall_counter_examples((a->b)->a, X), psa(X). 4198% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4199% ?- findall_counter_examples(a->b, X), psa(X). 4200% ?- findall_counter_examples((a->b)->(b->a), X), psa(X). 4201% ?- findall_counter_examples(a->b, Out), psa(Out). 4202findall_counter_examples(In, Out):- 4203 ltr_fetch_state, 4204 dnf(In, InZ), 4205 zdd_boole_atoms(Us), 4206 zdd_sort(Us, Vs), 4207 expand_prefix_dnf(Vs, 1, All), 4208 expand_dnf(Vs, InZ, Y), 4209 zdd_subtr(All, Y, Out).
4216% ?- ltr. 4217% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4218% ?- X<< dnf(a), psa(X), ltr_card(X, C). 4219% ?- X<< dnf(a->a), ltr_card(X, C). 4220% ?- X<< dnf(((a->b) * (b->c) * a -> c)), ltr_card(X, C). 4221% ?- ltr, X<< dnf((a->b)*(b->c)->(a->c)), ltr_card(X, C). 4222 4223% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4224% time((X<< dnf(+Ps), ltr_card(X, C))). 4225 4226 4227%@ % 123,881 inferences, 0.833 CPU in 1.321 seconds (63% CPU, 148761 Lips) 4228%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4229%@ X = 80, 4230%@ C = 1099511627775. 4231 4232%@ % 123,882 inferences, 0.010 CPU in 0.010 seconds (97% CPU, 12260689 Lips) 4233%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...], 4234%@ X = 80, 4235%@ C = 1099511627775. 4236 4237% ?- ltr, findall(p(J), between(1, 30, J), Ps), 4238% time((X<< dnf(+Ps), ltr_card(X, C))). 4239% ?- ltr, numlist(1, 30, Ps), time((X<< dnf(+Ps), ltr_card(X, C))). 4240% ?- sat, numlist(1, 30, Ps), sat(+Ps), sat_count(C). 4241 4242% ?- spy(ltr_card). 4243% ?- ltr, findall(p(J), between(1, 40, J), Ps), 4244% time((X<< dnf(+Ps), ltr_card(X, C))). 4245 4246% ?- findall(p(J), between(1, 100, J), Ps), 4247% time((X<< dnf(*Ps), ltr_card(X, C))). 4248 4249% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps). 4250% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4251% time((X<< dnf(+Ps),ltr_card(X, C))), 4252% C =:= 2^1000 - 1. 4253 4254% ?- ltr, N = 1000, findall(p(J), between(1, N, J), Ps), 4255% time((X<< dnf(+Ps), card(X, C))). 4256 4257ltr_card(In, Out):- 4258 zdd_boole_atoms(Us), 4259 zdd_sort(Us, Vs), 4260 expand_dnf(Vs, In, Y), 4261 card(Y, Out). 4262 4263% ?- ltr_var(-(5), X). 4264ltr_var(-(V), V):-!. 4265ltr_var(V, V).
4272% ?- ltr, X<<dnf(a->a), psa(X), expand_dnf([a], X, Y), psa(Y). 4273% ?- ltr, X<<dnf(a->(b->a)), expand_dnf([a,b], X, Y), ltr_card(Y, C). 4274% ?- ltr, X<<dnf(a->((b->c)->a)), expand_dnf([a,b,c], X, Y), card(Y, C). 4275% ?- ltr, X<<dnf(a*b->b), psa(X), expand_dnf([a,b], X, Y), psa(Y). 4276% ?- ltr, X<<dnf((a->b)*(b->c)->(b->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4277% ?- ltr, X<<dnf((a->b)*(b->c)->(a->c)), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4278% ?- ltr, X<<dnf(a + -a), psa(X), expand_dnf([a,b,c], X, Y), psa(Y), card(Y, C). 4279 4280expand_dnf([], X, X):-!. 4281expand_dnf(_, 0, 0):-!. 4282expand_dnf(Vs, 1, Y):-!, expand_prefix_dnf(Vs, 1, Y). 4283expand_dnf(Vs, X, Y):- memo(expand_dnf(X,Vs)-Y), 4284 ( nonvar(Y) -> true %, write(.) % Many hits. 4285 ; cofact(X, t(A, L, R)), 4286 ltr_var(A, K), 4287 divide_ord_list(Vs, K, [], Us, Ws), 4288 expand_dnf(Us, R, R0), 4289 ltr_insert(A, R0, R1), 4290 expand_left_dnf(K, Us, L, L0), 4291 ltr_join(L0, R1, X0), 4292 expand_prefix_dnf(Ws, X0, Y) 4293 ).
divide_ord_list([a,b,c,d,e], c, [u], T, W).
?- divide_ord_list([a,b,c, d], e, [], X, Y). % false4301divide_ord_list([V|Vs], V, Us, Vs, Us):-!. 4302divide_ord_list([V|Vs], U, Us, Ws, Ps):- ltr_compare(<, V, U), 4303 divide_ord_list(Vs, U, [V|Us], Ws, Ps).
4311% ?- ltr_zdd((expand_prefix_dnf([c,d], 1, Y), expand_prefix_dnf([a,b], Y, Z), psa(Z), card(Z, C))). 4312expand_prefix_dnf(Vs, X, Y):- zdd_sort(Vs, OrdVs), 4313 expand_ord_prefix_dnf(OrdVs, X, Y). 4314 4315% 4316expand_ord_prefix_dnf([], X, X):-!. 4317expand_ord_prefix_dnf([V|Vs], X, Y):- 4318 expand_ord_prefix_dnf(Vs, X, X0), 4319 ltr_insert(V, X0, X1), 4320 ltr_insert(-V, X0, X2), 4321 ltr_join(X1, X2, Y).
4331expand_left_dnf(_, _, 0, 0):-!. 4332expand_left_dnf(K, Us, 1, Y):-!, expand_prefix_dnf([K|Us], 1, Y). 4333expand_left_dnf(K, Us, X, Y):- cofact(X, t(A, L, R)), 4334 ltr_var(A, J), 4335 ( K = J -> 4336 expand_dnf(Us, R, R0), 4337 ltr_insert(A, R0, R1) 4338 ; divide_ord_list([K|Us], J, [], Vs, Ws), 4339 expand_dnf(Vs, R, R0), 4340 ltr_insert(A, R0, Q), 4341 expand_prefix_dnf(Ws, Q, R1) 4342 ), 4343 expand_dnf([K|Us], L, L0), 4344 ltr_join(L0, R1, Y). 4345 4346 /******************************* 4347 * Filter on cardinality * 4348 *******************************/
4354% ?- zdd, ((X<<pow([a,b,c]), card_filter_gte(2, X, Y), psa(Y))). 4355card_filter_gte(0, X, X):- !. % gte: greater than or equal 4356card_filter_gte(1, X, Y):- !, zdd_subtr(X, 1, Y). 4357card_filter_gte(_, X, 0):- X<2, !. 4358card_filter_gte(N, X, Y):- memo(filter_gte(N,X)-Y), 4359 ( nonvar(Y) -> true % many hits. 4360 ; cofact(X, t(A, L, R)), 4361 N0 is N - 1, 4362 card_filter_gte(N, L, L0), 4363 card_filter_gte(N0, R, R0), 4364 cofact(Y, t(A, L0, R0)) 4365 ).
4371% ?- X<<pow([a,b,c]), card_filter_lte(2, X, Y), psa(Y). 4372card_filter_lte(0, X, Y):- % lte: less than or equal 4373 ( zdd_has_1(X) -> Y = 1 4374 ; Y = 0 4375 ). 4376card_filter_lte(_, X, X):- X<2, !. 4377card_filter_lte(N, X, Y):- memo(filter_lte(N,X)-Y), 4378 ( nonvar(Y) -> true % many hits. 4379 ; cofact(X, t(A, L, R)), 4380 N0 is N - 1, 4381 card_filter_lte(N, L, L0), 4382 card_filter_lte(N0, R, R0), 4383 cofact(Y, t(A, L0, R0)) 4384 ).
time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C))).4390card_filter_between(I, J, X, Y):- 4391 card_filter_gte(I, X, Z), 4392 card_filter_lte(J, Z, Y). 4393 4394% ?- time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between_by_meet(50, 51, X, Y), card(Y, C))). 4395card_filter_between_by_meet(I, J, X, Y):- 4396 card_filter_gte(I, X, Z), 4397 card_filter_lte(J, X, U), 4398 zdd_meet(Z, U, Y). 4399 4400 4401 /********************************************************* 4402 * Solve boolean equations and verify the solution * 4403 *********************************************************/ 4404% Recovered [2023/11/14] 4405%! dnf_subst(+V, +T, +X, -Y) is det. 4406% Y is the ZDD obtained by substituting each 4407% occurrence of atom V in X with T. 4408 4409% ?-X<<dnf(-a), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4410% ?-X<<dnf(-a), Z<<dnf(-b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4411% ?-X<<dnf(a+b), Z<<dnf(b), dnf_subst(a, Z, X, Y), psa(X), psa(Y). 4412 4413dnf_subst(_, _, X, X):- X < 2, !. 4414dnf_subst(V, D, X, Y):- 4415 cofact(X, t(A, L, R)), 4416 dnf_subst(V, D, L, L0), 4417 once( A = -(U); U = A ), 4418 ltr_compare(C, V, U), 4419 ( C = (<) -> Y = X 4420 ; ( C = (=) -> 4421 ( A = (-V) -> 4422 ltr_negate(D, D0), 4423 ltr_merge(D0, R, R0) 4424 ; A = V -> 4425 ltr_merge(D, R, R0) 4426 ) 4427 ; dnf_subst(V, D, R, R1), 4428 ltr_insert(A, R1, R0) 4429 ), 4430 ltr_join(L0, R0, Y) 4431 ).
4439% exists x s.t. C0*(L,-x) + C1*x = 1 4440% if and only if 4441% C0 + C1 = 1 satisfiable 4442% x = a*C1 + (-C0). 4443 4444% ?- solve_boole_with_check(x*y=a, [x,y], [u,v], S). 4445% ?- solve_boole_with_check(x*y*z=a, [x,y,z], [u,v,w], S). 4446% ?- solve_boole_with_check(x*y*z*u=a, [x,y,z,u], [l, m, n, o], S). 4447 4448solve_boole_with_check(Exp, Xs, Ps):- 4449 dnf(Exp, E), 4450 solve_boolean_equations(E, Xs, Ps, Sols), 4451 eliminate_variables(E, Sols, Cond), 4452 !, 4453 dnf_valid_check(Cond). 4454 4455% ?- E<<dnf(x*y=a), solve_boolean_equations(E, [x,y], [u,v], Sols), 4456% solutions_to_sets(Sols, Sols0). 4457% ?- E<<dnf(x*y=a), solve_boolean_equations(E, [x,y,z], [u,v,w], Sols), solutions_to_sets(Sols, Sols0). 4458 4459solve_boolean_equations(_, [], _, []):-!. 4460solve_boolean_equations(E, [X|Xs], [A|As], [X=Sol|Sols]):- 4461 solve_boolean_equations_basic(E, X, A, Sol0, E0), 4462 solve_boolean_equations(E0, Xs, As, Sols), 4463 dnf_subst_list(Sols, Sol0, Sol). 4464% ?- E<<dnf(a*b+c*(-a)+b), solve_boolean_equations_basic(E, a, u, Sol, Cond), psa(E), psa(Sol), psa(Cond). 4465solve_boolean_equations_basic(E, X, A, Sol, Cond):- 4466 dnf_subst(X, 1, E, C1), 4467 dnf_subst(X, 0, E, C0), 4468 ltr_join(C0, C0, Cond), 4469 ltr_negate(C0, NC0), 4470 ltr_insert(A, C1, AC1), 4471 ltr_join(NC0, AC1, Sol). 4472% 4473dnf_subst_list([], E, E). 4474dnf_subst_list([X=A|Eqs], E, F):- 4475 dnf_subst(X, A, E, E0), 4476 dnf_subst_list(Eqs, E0, F). 4477% 4478solutions_to_sets([], []). 4479solutions_to_sets([X = E|Sols], [X = E0|Sols0]):- 4480 sets(E, E0), 4481 solutions_to_sets(Sols, Sols0). 4482 4483% ?- 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). 4484 4485% ?- 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). 4486 4487% ?- 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). 4488 4489eliminate_variables(Exp, Eqns, Cond):- 4490 apply_subst_list(Eqns, Exp, Cond). 4491% 4492apply_subst_list([], E, E). 4493apply_subst_list([X=U|Eqns], E, E0):- 4494 dnf_subst(X, U, E, E1), 4495 dnf_subst_list(Eqns, E1, E0). 4496% 4497dnf_valid_check(X):- 4498 ltr_atoms_by_scan(X, As), 4499 ltr_sort(As, Bs), 4500 expand_dnf(Bs, X, Y), 4501 card(Y, C), 4502 length(Bs, N), 4503 ( C =:= (1<< N) -> writeln('Solved and Verified.') 4504 ; writeln('Solved but NOT verified.') 4505 ). 4506 4507% ?- ltr. 4508% ?- X<<dnf(a+ -a*b), ltr_atoms_by_scan(X, As), sort(As, Bs). 4509 4510ltr_atoms_by_scan(X, []):- X<2, !. 4511ltr_atoms_by_scan(X, P):- memo(ltr_atoms(X)-P), 4512 ( nonvar(P) -> true 4513 ; cofact(X, t(A, L, R)), 4514 ltr_atoms_by_scan(L, Al), 4515 ltr_atoms_by_scan(R, Ar), 4516 ltr_var(A, A0), 4517 union([A0|Al], Ar, P) 4518 ). 4519 4520 /********************************* 4521 * operations on reducible zdd * 4522 *********************************/
4528% ?- numlist(1, 100, Ns), X<<pow(Ns), card(X, C). 4529% ?- bdd_sort_append([c, a, b,c], 1, Z), psa(Z). 4530bdd_sort_append(X, Y, Z):- zdd_sort(X, X0), 4531 bdd_append(X0, Y, Z). 4532 4533% ?- zdd, bdd_append([x, a, y, b], 1, Y), psa(Y). 4534% ?- zdd, bdd_append([x, a, y, b], 0, Y), psa(Y). 4535% ?- zdd, bdd_append([b, b], 1, Y), bdd_append([b,b], Y, Z), psa(Z). 4536 4537bdd_append([], Z, Z). 4538bdd_append([X|Y], Z, U):- 4539 bdd_append(Y, Z, Z0), 4540 bdd_cons(U, X, Z0). 4541 4542% ?- zdd, bdd_list([b, b], Y), bdd_sort_append([b,b], Y, Z), psa(Z). 4543% ?- zdd, bdd_list([b, b], Y), bdd_list(X, Y). 4544bdd_list(List, X):- var(X), !, bdd_append(List, 1, X). 4545bdd_list(List, X):- get_bdd_list(X, List). 4546 4547% ?- zdd, bdd_append([x, a, y, b], 1, Y), psa(Y), get_bdd_list(Y, L). 4548% ?- zdd, bdd_append([a, a, a, a], 1, Y), psa(Y), get_bdd_list(Y, L). 4549get_bdd_list(1, []):-!. 4550get_bdd_list(X, [A|As]):- X>1, bdd_cons(X, A, X0), 4551 get_bdd_list(X0, As). 4552 4553% ?- zdd, bdd_append([a,a,b,b], 1, X), 4554% bdd_append([1,1,2,2], 1, Y), 4555% bdd_zip(X, Y, Z), psa(Z). 4556bdd_zip(0, _, 0):-!. 4557bdd_zip(_, 0, 0):-!. 4558bdd_zip(1, _, 1):-!. 4559bdd_zip(_, 1, 1):-!. 4560bdd_zip(X, Y, Z):- bdd_cons(X, A, X0), 4561 bdd_cons(Y, B, Y0), 4562 bdd_zip(X0, Y0, Z0), 4563 bdd_cons(Z, A-B, Z0). 4564 4565% ?- zdd, bdd_append([a,b,a,b], 1, X), bdd_normal(X, Y), psa(Y). 4566bdd_normal(X, X):- X<2, !. 4567bdd_normal(X, Y):- cofact(X, t(A, L, R)), 4568 bdd_normal(L, L0), 4569 bdd_normal(R, R1), 4570 zdd_insert(A, R1, R0), 4571 zdd_join(L0, R0, Y). 4572 4573% ?- zdd, bdd_append([a,b,a,b], 1, X), 4574% bdd_append([a,b, c, a,b, c], 1, Y), 4575% bdd_append([b, a, b, a, a,b ], 1, Z), 4576% bdd_list_normal([X, Y, Z], R), psa(R). 4577 4578bdd_list_normal([], 0). 4579bdd_list_normal([A|As], R):- bdd_list_normal(As, R0), 4580 bdd_normal(A, A0), 4581 zdd_join(A0, R0, R). 4582 4583% 4584bdd_insert(_, 0, 0):-!. 4585bdd_insert(A, 1, X):-!, zdd_singleton(A, X). 4586bdd_insert(A, X, Y):- cofact(X, t(B, L, R)), 4587 bdd_insert(A, L, L0), 4588 bdd_append([A,B], R, R0), 4589 zdd_join(L0, R0, Y).
4598% ?- bdd_list_raise([], 0, X). 4599% ?- bdd_list_raise([a], 0, X). 4600% ?- bdd_list_raise([a], 1, X), psa(X). 4601% ?- bdd_list_raise([a,b], 1, X), psa(X). 4602% ?- N = 1, numlist(1, N, Ns), bdd_list_raise(Ns, N, X), card(X, C). 4603 4604% ?- zdd, N = 15, numlist(1, N, Ns), bdd_list_raise(Ns, N, X),card(X, C). 4605bdd_list_raise(_, 0, 1):-!. 4606bdd_list_raise(L, N, X):- N0 is N-1, 4607 bdd_list_raise(L, N0, X0), 4608 bdd_map_insert(L, X0, X). 4609% 4610bdd_map_insert([], _, 0). 4611bdd_map_insert([A|As], X, Y):- 4612 bdd_insert(A, X, X0), 4613 bdd_map_insert(As, X, Y0), 4614 zdd_join(X0, Y0, Y). 4615 4616% Remark: zdd_join, zdd_meet, zdd_subtr, which does not use zdd_insert, 4617% also work for bddered zdd. 4618 4619% ?- zdd, X<<pow([a]), Y<<pow([b]), bdd_merge(X, Y, Z), zdd_subtr(Z, Y, U), 4620% psa(X), psa(Y), psa(Z), psa(U). 4621% ?- zdd, X<<pow([a, b]), Y<<pow([b,c]), bdd_merge(X, Y, Z), 4622% psa(Z), card(Z, C). 4623% ?- zdd, numlist(1, 10, Ns), X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4624% card(Z, C). 4625% ?- zdd, numlist(1, 10, Ns), X<<pow(Ns), Y<<pow(Ns), zdd_merge(X, Y, Z), 4626% card(Z, C), card(X, D). 4627% ?- zdd, numlist(1, 10, Ns), X<<pow(Ns), Y<<pow(Ns), bdd_merge(X, Y, Z), 4628% card(Z, C), card(X, D). 4629 4630bdd_merge(0, _, 0):-!. 4631bdd_merge(_, 0, 0):-!. 4632bdd_merge(1, X, X):-!. 4633bdd_merge(X, 1, X):-!. 4634bdd_merge(X, Y, Z):- memo(bdd_merge(X, Y)-Z), 4635 ( nonvar(Z) -> true % , write(.) % So so frequently hits. 4636 ; cofact(X, t(A, L, R)), 4637 bdd_merge(L, Y, L0), 4638 bdd_merge(R, Y, R1), 4639 bdd_cons(R0, A, R1), 4640 zdd_join(L0, R0, Z) 4641 ). 4642 4643 4644 /**************n*************************** 4645 * Interleave bddered atoms in BDD * 4646 ******************************************/
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.4655% ?- X<< +[*[a,b], *[x,y]], Y<< +[*[1]], 4656% bdd_interleave(X, Y, Z), psa(Z). 4657% ?- zdd, X<< *[a], Y<< *[b], bdd_interleave(X, Y, Z), psa(Z). 4658% ?- zdd, X<< *[a,b], Y<< *[1,2], bdd_interleave(X, Y, Z), psa(Z). 4659 4660bdd_interleave(0, _, 0):-!. 4661bdd_interleave(_, 0, 0):-!. 4662bdd_interleave(1, X, X):-!. 4663bdd_interleave(X, 1, X):-!. 4664bdd_interleave(X, Y, Z):- % memo is useless here. 4665 cofact(Y, t(B, L, R)), 4666 ( L < 2 -> L0 = 0 4667 ; bdd_interleave(X, L, L0) 4668 ), 4669 bdd_interleave(X, B, R, R0), 4670 zdd_join(L0, R0, Z)