1:- module(zdd_array, [ 2 open_state/0, open_state/1, close_state/0 3 , open_state_core/1, open_state_core/2 4 , open_vector/2 5 , memo/1, memo/2, memoq/1, init_memo_stack/0 6 , memo_index/2 7 , push_memo/0, pop_memo/0 8 , use_memo/1, reset_memo_call/1 9 , open_memo/1, open_memo/2, close_memo/1 10 , open_hash/2, close_hash/1, hash/3 11 , set_memo/1, update_memo/2, dump_memo/0, dump_memo/1, dump_hash/1 12 , insert_memo/2 13 , unify_args/3 14 , add_child/2, add_child/3 15 , pred_memo_update/2 16 , cofact/2, cofact/3, index/3, term/2, show_array/0 17 , iterm/2, iterm/3 18 , slim_gc/2, slim_iterms/2 19 , index/2, index/3]). 20 21:- use_module(zdd(zdd)). 22 23% suppress details of hash/vector. 24atom_only(A, A0) :- ( compound(A) -> A0 = '.' ; A0 = A). 25% 26user:portray(X) :- compound(X), !, 27 ( functor(X, s, N), N > 7 -> write('s(..)') 28 ; functor(X, ctrl, N), N > 2 -> write('<ctrl>') 29 ; compound_name_arguments(X, F, _), 30 ( F = (#) -> write(#(..)) 31 ; F = call_continuation -> write(cont(..)) 32 ) 33 ). 34user:portray(X) :- var(X), get_attr(X, zsat, _), !. 35 36% ?- reset_memo_call(true). 37 38% ?- initial_hash(X), writeln(X). 39% ?- initial_hash(100, X). 40 41initial_hash(X):- X = #(0, 0, #([])). 42% 43initial_hash(N, X):- X = #(0, 0, V), functor(V, #, N). 44% 45hash_key_count(H, C):- arg(1, H, C). 46% 47hash_key_count_set(H, C):- setarg(1, H, C). 48% 49hash_bucket_count(H, C):- arg(2, H, C). 50% 51hash_bucket_count_set(H, C):- setarg(2, H, C). 52% 53hash_vector(H, V):- arg(3, H, V). 54% 55hash_vector_set(H, V):- setarg(3, H, V). 56 57% 58check_rehash(H):- H = #(C, B, V), 59 functor(V, _, N), 60 ( C > B + 1.7 * N -> rehash(H) 61 ; true 62 ). 63% 64hash(X, H, Val):- 65 check_rehash(H), 66 term_bucket_index(X, H, U, I), 67 ( memberchk(X-V, U) -> Val = V 68 ; hash_vector(H, Vec), 69 setarg(I, Vec, [X-Val | U]), 70 hash_key_count(H, C), 71 C0 is C + 1, 72 hash_key_count_set(H, C0), 73 ( U =[] -> % Count up for new bucket. 74 arg(2, H, B), 75 B0 is B + 1, 76 setarg(2, H, B0) 77 ; true 78 ) 79 ). 80 81% ?- open_state. 82% ?- open_state, push_memo, b_getval(zdd_memo, H), pop_memo. 83% ?- open_state, close_state, show_state. 84 85% Assuming a totally ordered set of atoms, a state is a collection of 86% families of (finite) sets of (finite) these atoms. In a state, 87% each family of sets (FOS) is given a unique nonnegative integer. 88% 0 is reserved for the empty family {}, and 1 for {{}} = {0} = 1. 89% If a FOS F is neither 0 nor 1, there must 90% be the maximum atom A among those are an element of a set of F. 91% A is called the maximum atom of F. The maximum atom is defined neither for 92% 0 nor 1. Throuhout successive updating process of a state, once the unique 93% id of a FOS is created, this id is kept for the FOS henceforth. 94% `cofact/3` is the main bidirectional interface predicate on states to get 95% a FOS id (fact), and to store new FOS (cofact) in a state. 96% A nonnegative integer k is used for the FOS whose id is k, and vice versa.
101% ?- open_state, show_state. 102% ?- open_state, cofact(X, t(a,0,1)), show_state. 103open_state :- open_state([]). 104% 105open_state(Args) :- 106 default_compare(Compare), 107 ( memberchk(hash_size(HsizeExp), Args); HsizeExp = 2 ), !, 108 ( memberchk(vector_size(VsizeExp), Args); VsizeExp = 2 ), !, 109 ( memberchk(extra(Extra), Args); Extra = [varnum-0, varzip-[]] ), !, 110 Hsize is HsizeExp, 111 Vsize is VsizeExp, 112 functor(Array, #, Vsize), 113 arg(1, Array, 0), % not used, but for simplicity. 114 open_hash(Hsize, Hash), 115 nb_setval(zdd_hash, Hash), 116 nb_setval(zdd_vec, #(1, Array)), 117 nb_setval(zdd_compare, Compare), 118 nb_setval(zdd_extra, Extra), 119 init_memo_stack. 120 121% ?- open_state_core(G). 122% ?- open_state_core(G), cofact(I, t(a, 0, 1), G), psa(I, G), psa(I, G). 123% ?- open_state_core(G), cofact(X, t(a,0,1), G), cofact(Y, t(b, X, X),G), psa(Y, G). 124% 125% ?- open_state_core(G), cofact(X, t(a,0,1), G), cofact(Y, t(b, X, X), G), 126% cofact(Y, T, G), psa(Y, G). 127 128% ?- zdd. 129% ?- X<<pow([a,b,c]), Y<<pow([b,c,d]), Z<<(X-Y), psa(Z), zdd_gc(Z, U), psa(U). 130% ?- open_state_core(xxx), b_getval(xxx, Core), write(Core). 131 132open_state_core(G) :- open_state_core(G, []). 133% 134open_state_core(G, Args) :- 135 ( var(G) -> gensym(core, G) 136 ; atom(G) 137 ), 138 initial_state_core(Args, Core), 139 nb_linkval(G, Core). 140 141% ?- initial_state_core([], X). 142initial_state_core(Args, #(1,Vector)-Hash):- 143 ( memberchk(hash_size(HsizeExp), Args); HsizeExp = 2 ), !, 144 ( memberchk(vector_size(VsizeExp), Args); VsizeExp = 2 ), !, 145 Hsize is HsizeExp, 146 Vsize is VsizeExp, 147 functor(Vector, #, Vsize), 148 open_hash(Hsize, Hash), 149 arg(1, Vector, 0). 150% 151show_state:- 152 b_getval(zdd_hash, Hash), writeln(zdd_hash = Hash), 153 b_getval(zdd_vec, Vector), writeln(zdd_vec = Vector), 154 b_getval(zdd_compare, Compare), writeln(zdd_compare = Compare), 155 b_getval(zdd_extra, Extra), writeln(zdd_extra = Extra), 156 b_getval(zdd_memo, Buckets), writeln(zdd_memo = Buckets). 157 158 /*********************** 159 * State globals * 160 * -------------------- * 161 * zdd_hash * 162 * zdd_vec * 163 * zdd_extra * 164 * zdd_compare * 165 ***********************/
memo(a-1), push_memo, memo(a-2), memo(a-A), pop_memo, memo(a-B).
?- push_memo, memo(a-1), memo(a-Y), pop_memo, memo(a-2), memo(a-Z).
?- memo_index(x-I), memo_index(y-J), memo_index(x-K).
?- memo_index(a(1)-V), get_key(a, C).
?- memo_index(a(1)-V), memo_index(a(2)-U), get_key(a, C).
?- memo_index(a(1)-V), memo_index(a(2)-U), memo_index(a(2)-W), get_key(a, C).
?- memo_index(a(1), X), memo_index(b(3), W), memo_index(b(2), Y), memo_index(a(1), Z), memo_index(b(2), U).183memo_index(E-V):- memo(E-V), !, 184 ( nonvar(V) -> true 185 ; functor(E, CounterName, _), 186 memo_index(CounterName, V) 187 ). 188% 189memo_index(Name, V0):- 190 b_getval(zdd_extra, Extra), 191 ( select(Name-V, Extra, Extra0) -> 192 V0 is V+1 193 ; Extra0 = Extra, 194 V0 = 1 195 ), 196 nb_linkval(zdd_extra, [Name-V0|Extra0]), 197 !. 198 199% Structure Sharing. 200setarg_state_extra(X, Y):- arg(2, X, Extra), setarg(2, Y, Extra). 201% 202setarg_state_core(X, Y):- arg(1, X, Core), setarg(1, Y, Core). 203% 204default_compare(compare).
show_array(zdd_vec).
! show_array(+G) is det.
Print all triples in array bound to G.211% ?- zdd_eval(pow([a,b,c]), _), show_array. 212% ?- open_state, zmod:zdd_eval(family([[a],[b],[c]]), X), show_array. 213% ?- open_state, show_array. 214 215show_array:- show_array(zdd_vec). 216% 217show_array(G) :- b_getval(G, Vec), show_vector(Vec). 218 219% ?- open_state, show_state. 220show_vector(#(C, Vec)):- 221 forall(between(2, C, I), 222 ( arg(I, Vec, V), writeln(I=V))).
226close_state:- 227 nb_linkval(zdd_hash, []), 228 nb_linkval(zdd_vec, []), 229 nb_linkval(zdd_extra, []), 230 nb_linkval(zdd_compare, []), 231 nb_linkval(zdd_child, []). 232% 233:- meta_predicate use_memo(). 234use_memo(Goal):- setup_call_cleanup( 235 push_memo, 236 call(Goal), 237 pop_memo 238 ). 239 240% 241:- meta_predicate reset_memo_call(). 242reset_memo_call(X):- setup_call_cleanup( 243 reset_memo, 244 call(X), 245 reset_memo 246 ). 247% 248init_memo_stack:- open_hash(64, H), 249 nb_setval(zdd_memo, H), 250 nb_setval(memo_stack, []). 251% 252reset_memo:- open_hash(64, H), 253 nb_setval(zdd_memo, H). 254 255% push/pop memo 256push_memo:- b_getval(zdd_memo, M), 257 b_getval(memo_stack, Ms), 258 b_setval(memo_stack, [M|Ms]), 259 open_hash(64, H), 260 b_setval(zdd_memo, H). 261% 262pop_memo:- b_getval(memo_stack, [M|Ms]), 263 b_setval(zdd_memo, M), 264 b_setval(memo_stack, Ms), 265 !. 266% 267open_memo(Memo_name):- open_memo(Memo_name, 64). 268% 269open_memo(Memo_name, N):- N > 0, 270 ( atom(Memo_name) -> true 271 ; gensym(memo, Memo_name) 272 ), 273 open_hash(N, Hash), 274 nb_linkval(Memo_name, Hash). 275 276% 277close_memo(Memo_name) :- nb_setval(Memo_name, []). 278 279% ?- zdd. 280% ?- memo(a-1). 281% ?- memo(a-1), memoq(a-1). 282% ?- memo(a-1), memoq(a-X). % false 283% ?- memoq(a-X). % false. 284% ?- memo(a-1), memoq(a-X). % false 285% ?- memo(a-1), memo(a-X). 286% ?- X<<pow(numlist(1, 1000)), card(X, C). 287% ?- memo(a-1), memo(a-V), set_memo(a-2), memo(a-U). 288% ?- set_memo(a-1), memo(a-X). 289% ?- open_hash(2, H), hash(a, H, X), X=3, hash(a, H, Y). 290 291% Take time !! 292% ?- open_hash(2, H), time(repeat(10^8, (hash(a, H, X), X=3, hash(a, H, Y)))). 293%@ % 3,100,000,001 inferences, 204.420 CPU in 237.279 seconds (86% CPU, 15164854 Lips) 294%@ H = #(..). 295% ?- open_hash(2, H), hash(a, H, X), hash(a, H, Y), X==Y. 296%! memo(+P) is det. 297% P = X-V, 298% The input pair X-V is unified with with a member of a bucket of the hash 299% table of the state S. Otherwise, create a new entry for X-V. 300 301% ?- zdd. 302memo(X-V):- b_getval(zdd_memo, H), !, hash(X, H, V).
308memo(X-V, G):- b_getval(G, H), !, hash(X, H, V). 309 310% ?- memo(a-Y), memo(a-R). 311% ?- memo(a-Y), memo(a-R). 312% ?- memo(a-1), memo(a-R). 313% ?- set_memo(a-1), memo(a-Y), set_memo(a-V), memo(a-R), V=2. 314 315% set_memo(X-V) is det. 316% Replace old X entry with X-V when X entry exists, 317% otherwise, simply create X-V entry. 318 319set_memo(X-V) :- b_getval(zdd_memo, H), hash_fresh_entry(X, V, _, H). 320% 321set_memo(X-V, G) :- b_getval(G, H), hash_fresh_entry(X, V, _, H). 322 323% ?- memo(a-1), update_memo(a-X, Y), memo(a-U). 324% ?- memo(a-1), update_memo(a-X, Y). 325% ?- memo(a-1). 326% ?- memo(a-1), update_memo(a-X, Y), Y=2, memo(a-U). % fail
334% ?- memo(a-1), update_memo(a-X, Y), X=f(Y). 335update_memo(X-FreshVar, OldVal):- % must_be(var, FreshVar), 336 b_getval(zdd_memo, H), 337 hash_fresh_entry(X, FreshVar, OldVal, H). 338% 339update_memo(X-FreshVar, OldVal, G):- % must_be(var, FreshVar), 340 b_getval(G, H), 341 hash_fresh_entry(X, FreshVar, OldVal, H).
347% ?- insert_memo(abc(5), p(0,0)-p(1,0)), insert_memo(abc(5), p(1,1)-p(0,1)), memo(abc(5)-X), psa(X). 348 349insert_memo(Key, X):- 350 update_memo(Key-New, Old), 351 ( var(Old) -> Old = 1 % empty set 352 ; true 353 ), 354 zdd_insert(X, Old, New).
361:- meta_predicate pred_memo_update(, ). 362pred_memo_update(Pred, K-V):- update_memo(K-L, L0), 363 call(Pred, V, L0, L). 364% 365:- meta_predicate pred_memo_update(, , ). 366pred_memo_update(Pred, K-V, G):- update_memo(K-L, L0, G), 367 call(Pred, V, L0, L).
memo_add_new(a-1), memo(a-X).
?- memo_add_new(a-1), memo_add_new(a-2), memo(a-X).
?- memo_add_new(a-1), memo_add_new(a-2), memo_add_new(a-1), memo(a-X).
376memo_add_new(X):- pred_memo_update(add_new, X).383memo_add_new(X, G):- pred_memo_update(add_new, X, G). 384 385% ?- pred_memo_update(add_new, a-1), memo(a-X). 386add_new(V, [], [V]):-!. 387add_new(V, L0, L0):- memberchk(V, L0), !. 388add_new(V, L0, [V|L0]). 389 390% ?- add_child(suc(a), 1), memo(suc(a)-X). 391% ?- add_child(a, 1), add_child(a, 2), memo(a-X). 392% ?- add_child(a, 1), add_child(a, 2), memochk_stack(a-X). 393% ?- add_child(a, 1), add_child(a, 2), add_child(a, 1), memo(a-X). 394% ?- numlist(1, 100000, Ns), 395% time(( maplist(pred([Child]:- add_child(a, Child)), Ns), memo(a-X))). 396%@ % 2,300,011 inferences, 74.231 CPU in 74.334 seconds (100% CPU, 30985 Lips) 397%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...], 398%@ X = [100000, 99999, 99998, 99997, 99996, 99995, 99994, 99993, 99992|...]. 399 400add_child(X, Child) :- pred_memo_update(add_new, X-Child). 401% 402add_child(X, Child, G):- pred_memo_update(add_new, X-Child, G).
408memochk(X-V):- b_getval(zdd_memo, H), 409 term_bucket_index(X, H, B, _), 410 memberchk(X-V, B). 411% 412memochk_stack(X-V):- b_getval(zdd_memo, H), 413 b_getval(memo_stack, Hs), 414 member(H0, [H|Hs]), 415 term_bucket_index(X, H0, B, _), 416 memberchk(X-V, B). 417% 418memochk(X-V, G):- b_getval(G, H), 419 term_bucket_index(X, H, B, _), 420 memberchk(X-V, B).
==
stored in the hash table of S.
?- zdd.
?- push_memo, memo(a-b), memoq(a-Y). % fail.429memoq(X-V):- memochk(X-U), !, U == V. 430% 431memoq(X-V, G):- memochk(X-U, G), !, U == V.
440% ?- index(I, V, a), index(J, V, b), 441% index(I, V, X), index(J, V, Y). 442 443index(I, A, X):-nonvar(I), !, 444 nonvar(A), 445 arg(2, A, V), 446 arg(I, V, X). 447index(I, A, X):- 448 ( nonvar(A) -> true 449 ; A = #(0, #) 450 ), 451 arg(1, A, K), 452 arg(2, A, U), 453 functor(U, _, M), 454 ( K < M -> true 455 ; extend_vector_double(A) 456 ), 457 I is K + 1, 458 setarg(1, A, I), 459 arg(2, A, V), 460 setarg(I, V, X). 461 462% ?- index(V, a), index(V, b), arg(1, V, K), 463% forall(between(1, K, J), (arg(2, V, A), arg(J, A, B), writeln(J => B))). 464% 465index(A, X):- index(_, A, X). 466 467% ?- open_vector(0, A), extend_vector_double(A), writeln(A). 468% ?- open_vector(0, A), extend_vector_double(A), writeln(A), 469% extend_vector_double(A), writeln(A), 470% extend_vector_double(A), writeln(A), 471% extend_vector_double(A), writeln(A), 472% close_vector(A), writeln(A). 473 474extend_vector_double(A):- nonvar(A), 475 arg(2, A, V), 476 functor(V, F, N), 477 ( N = 0 -> N0 = 2 478 ; N0 is N + N 479 ), 480 functor(U, F, N0), 481 ( N = 0 -> true 482 ; unify_args(1, V, U) 483 ), 484 setarg(2, A, U). 485 486% ?- iterate_double_number(0, 1, X). 487% ?- iterate_double_number(1, 2, X). 488% ?- iterate_double_number(1, 100, X). 489 490iterate_double_number(N, I, N):- I =< N, !. 491iterate_double_number(0, I, I):- !. 492iterate_double_number(N, I, M):- N0 is 2*N, 493 iterate_double_number(N0, I, M). 494 495 496% NEW style for processing arguments. 497% ?- unify_args(1, f(A, B, C), f(U,V, W)). 498unify_args(X, _):- atom(X), !. 499unify_args(X, Y):- unify_args(1, X, Y). 500% 501unify_args(I, X, A):- arg(I, X, U), !, 502 arg(I, A, U), 503 J is I + 1, 504 unify_args(J, X, A). 505unify_args(_, _, _). 506 507% ?- initial_args(1, a(X, Y), 2). 508initial_args(I, V, C):- setarg(I, V, C), !, 509 J is I+1, 510 initial_args(J, V, C). 511initial_args(_, _, _). 512 513 /*********************************************** 514 * new_array_elem/get_elem/set_elem * 515 ***********************************************/ 516 517% ?- open_hash(2, H), write(H).
open_hash(3, H), hash(a, H, X), write(H).522open_hash(N, H):- initial_hash(N, H), 523 hash_vector(H, V), 524 initial_args(1, V, []). % Buckets are empty at start.
528close_hash(H):- hash_vector_set(H, []). % not by nb_setarg, but by setarg.
open_vector(0, H), write(H).
?- open_vector(3, H), write(H).534open_vector(0, H):-!, H = #(0, #). 535open_vector(N, A):- functor(V, #, N), A = #(0, V).
539close_vector(A):- setarg(1, A, 0), setarg(2, A, []).
545% ?- open_hash(2, H),
546% time(repeat(1000, (hash(a, H, X), X=3, hash(a, H, Y)))).
552term_bucket_index(X, H, B, I):-
553 hash_vector(H, Vec),
554 functor(Vec, _, N),
555 term_hash(X, 3, N, I0),
556 I is I0 + 1,
557 arg(I, Vec, B).hash_scan(+X, +Y, ?Val)
562hash_scan(X, H, Val):-
563 term_bucket_index(X, H, U, _),
564 memberchk(X-V, U),
565 Val == V.574hash_fresh_entry(X, FreshVar, OldVal, H):- 575 check_rehash(H), 576 term_bucket_index(X, H, U, I), 577 hash_vector(H, Vec), 578 ( select(X-OldVal, U, U0) -> 579 setarg(I, Vec, [X-FreshVar | U0]) 580 ; setarg(I, Vec, [X-FreshVar | U]) 581 ). 582 583% ?- initial_hash(H), check_rehash(H), writeln(H). 584% ?- initial_hash(H), check_rehash(H), check_rehash(H), 585% check_rehash(H), writeln(H).
590% ?- zdd. 591% ?- numlist(1,3, Ns), X<<pow(Ns), psa(X). 592% ?- numlist(1,3, Ns), zmod:zdd_eval(pow(Ns), X), card(X, C). 593% ?- nb_setval(zdd_vec, #(1, #(0))), 594% new_array_elem(a, A), new_array_elem(b,B), new_array_elem(c, C), 595% b_getval(zdd_vec, V), write(V). 596 597% ?- X<< pow(numlist(1,2)), new_array_elem(a, I), 598% new_array_elem(b, J), 599% new_array_elem(c, K), 600% show_array, b_getval(zdd_vec, V), write(V). 601 602new_array_elem(X, I):- b_getval(zdd_vec, Array), 603 index(I, Array, X). 604 605% ?- initial_hash(H), rehash(H), writeln(H), rehash(H), rehash(H), rehash(H), writeln(H).
610rehash(H):-
611 hash_vector(H, Vec),
612 functor(Vec, F, N),
613 N0 is N + N,
614 functor(Vec0, F, N0),
615 initial_args(1, Vec0, []),
616 ( functor(H, _, 2) ->
617 migrate_hash(1, Vec, Vec0), % Here was a bug
618 hash_vector_set(H, Vec0)
619 ; migrate_hash(1, Vec, Vec0, 0, C), % Here was a bug
620 hash_vector_set(H, Vec0),
621 hash_bucket_count_set(H, C)
622 ).626migrate_hash(I, V, V0):- arg(I, V, B), !, 627 migrate_bucket(B, V0), 628 I0 is I + 1, 629 migrate_hash(I0, V, V0). 630migrate_hash(_, _, _). 631% 632migrate_bucket([], _). 633migrate_bucket([Q|U], H):- 634 ( Q = (X-_) -> E = Q 635 ; X = Q, 636 E = Q 637 ), 638 functor(H, _, S), 639 term_hash(X, 3, S, K), 640 K0 is K + 1, 641 arg(K0, H, D), 642 setarg(K0, H, [E|D]), 643 migrate_bucket(U, H). 644% 645migrate_hash(I, V, V0, C, C0):- arg(I, V, B), !, 646 migrate_bucket(B, V0, C, C1), 647 I0 is I + 1, 648 migrate_hash(I0, V, V0, C1, C0). 649migrate_hash(_, _, _, C, C). 650 651% 652migrate_bucket([], _, C, C). 653migrate_bucket([Q|U], H, C, C0):- 654 ( Q = (X-_) -> E = Q 655 ; X = Q, 656 E = Q 657 ), 658 functor(H, _, S), 659 term_hash(X, 3, S, K), 660 K0 is K + 1, 661 arg(K0, H, D), 662 setarg(K0, H, [E|D]), 663 ( D = [] -> C1 is C + 1 664 ; C1 = C 665 ), 666 migrate_bucket(U, H, C1, C0). 667 668 /**************** 669 * cofact * 670 ****************/
t(A, L, R)
Bidirectional.
X is unified with the index of a triple C, or
C is unified with the triple t/3 stored at index X of the array.
It is explained in terms of famiy of sets as follows.
If X is given then
Y is a triple t(A, L, R) such that
A is the minimum atom in X w.r.t specified 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 { unionf of U and {A} | U in R }.
Non standard use of cofact/3 is possible keeping the structure sharing, but withoug zero_suppress rule. IMO the rule is only meaningful under family of sets semantics for the empty family {} of sets.
?- X <<{[a,b,d]}, cofact(X, T).
?- X <<{[a]}, show_state, b_getval(zdd_vec, Vec), write(Vec).
?- cofact(X, a), cofact(Y, b), cofact(Z, f(X, Y)),
cofact(Z, C), cofact(X, A), cofact(Y, B).
696% 697cofact(I, X):- nonvar(I), !, % I>1 assumed. 698 iterm_get_elem(I, X). 699cofact(I, t(_, I, 0)):-!. % the Minato's zero-suppress rule. 700cofact(I, X):- iterm_hash(X, I). 701% 702cofact(I, X, G):- nonvar(I), !, % X>1 assumed. 703 iterm_get_elem(I, X, G). 704cofact(I, t(_, I, 0), _):- !. % the Minato's zero-suppress rule. 705cofact(I, X, G):- iterm_hash(X, I, G). 706 707% Helpers for cofact/iterm 708iterm_get_elem(I, X):- b_getval(zdd_vec, Vec), 709 arg(2, Vec, Array), 710 arg(I, Array, X). 711% 712iterm_get_elem(I, X, G):- b_getval(G, -(#(_, Array), _)), 713 arg(I, Array, X). 714% 715iterm_hash(X, I):- b_getval(zdd_hash, H), 716 hash(X, H, I), % check X-I entry in H (hash) 717 ( nonvar(I) -> true % X already exists. 718 ; new_array_elem(X, I) % X is new. 719 ). 720% 721iterm_hash(X, I, G):- b_getval(G, A-H), 722 hash(X, H, I), % check X-I entry in H (hash) 723 ( nonvar(I) -> true % X already exists. 724 ; new_array_elem(X, I, A) % X is new. 725 ). 726 727% ?- iterm(X, @(a)), show_array. 728iterm(I, X):- nonvar(I), !, % X>1 assumed. 729 iterm_get_elem(I, X). 730iterm(I, X):- iterm_hash(X, I). 731% 732iterm(I, X, G):- nonvar(I), !, % X>1 assumed. 733 iterm_get_elem(I, X, G). 734iterm(I, t(_, I, 0), _):-!. % Minato's rule. (t/3 is reserved.) 735iterm(I, X, G):- iterm_hash(X, I, G). 736 737 /***************************************************** 738 * bidirectional term to from index converter. * 739 *****************************************************/ 740 741% ?- term(I, a), term(J, @(a)), show_array. 742% ?- term(I, 0), term(J, 1), show_array. 743% ?- X=..[., a, b], term(I, X), iterm(I, U), write_canonical(U). 744% ?- X=..[., a, b], term(I, X), term(I, T), write_canonical(T), compound(T). 745% ?- N = 100, numlist(1, N, Ns), X=..[f|Ns], 746% term(I, X), term(I, Y), X = Y. 747 748term(I, X):- var(I), !, term_to_index(X, I). 749term(I, X):- iterm(I, Y), iterm_to_term(Y, X). 750% 751term_to_index(@(X), I):-!, iterm(I, @(X)). 752term_to_index(X, I):- atomic(X), !, iterm(I, X). 753term_to_index(t(A, L, R), I):-!, 754 term_to_index(L, J), 755 term_to_index(R, K), 756 iterm(I, t(A, J, K)). 757term_to_index(X, I):- functor(X, F, N), 758 functor(Y, F, N), 759 term_to_index(1, X, Y), 760 iterm(I, Y). 761% 762term_to_index(K, X, Y):- arg(K, X, A), !, 763 arg(K, Y, I), 764 term_to_index(A, I), 765 K0 is K + 1, 766 term_to_index(K0, X, Y). 767term_to_index(_, _, _). 768% 769iterm_to_term(@(X), @(X)):-!. 770iterm_to_term(X, X):- atomic(X), !. 771iterm_to_term(t(A, J, K), t(A, L, R)):-!, 772 iterm_to_term(J, L), 773 iterm_to_term(K, R). 774iterm_to_term(X, Y):- functor(X, F, N), 775 functor(Y, F, N), 776 iterm_to_term(1, X, Y). 777% 778iterm_to_term(K, X, Y):- arg(K, X, I), !, 779 arg(K, Y, T), 780 iterm(I, U), 781 iterm_to_term(U, T), 782 K0 is K + 1, 783 iterm_to_term(K0, X, Y). 784iterm_to_term(_, _, _). 785% 786print_root:- b_getval(root, X), 787 print_iterm(X). 788% 789print_iterm(X):-use_memo(print_array_elem(X)). 790% 791print_array_elem(X):- X < 2, !. 792print_array_elem(X):- memo(printed(X)-T), 793 cofact(X, t(A, L, R)), 794 ( nonvar(T)-> true 795 ; T = true, 796 writeln(X = t(A, L, R)), 797 print_array_elem(L), 798 print_array_elem(R) 799 ). 800 801 802 /***************************************** 803 * copy, slim, ord_copy, pred_copy * 804 *****************************************/
slim_iterms(X, Y), and call garbage_collect.809% ?- zdd. 810% ?- X<<{[a,b]}, slim_gc(X, Y), psa(Y). 811 812slim_gc(X, Y):- slim_iterms(X, Y), !, garbage_collect.
818% ?- _<<pow([a,b]), X<<pow([c,d,e]), psa(X), slim_gc(X, Y), psa(Y). 819slim_iterms(X, Y):- 820 b_getval(zdd_vec, #(_,V)), 821 initial_state_core([], A-H), 822 b_setval(zdd_vec, A), 823 b_setval(zdd_hash, H), 824 !, 825 reset_memo_call(slim_iterms(X, Y, V)). 826 827% ?- V = f(0, t(a, 0, 1)), slim_iterms(2, Y, V), psa(Y). 828slim_iterms(X, Y, V):- integer(X), !, slim_iterm(X, Y, V). 829slim_iterms([], [], _):-!. 830slim_iterms([X|Xs], [Y|Ys], V):- 831 slim_iterms(X, Y, V), 832 slim_iterms(Xs, Ys, V). 833% 834slim_iterm(X, X, _):- X< 2,!. 835slim_iterm(X, Y, V):- memo(slim_iterm(X)-Y), 836 ( nonvar(Y) -> true 837 ; arg(X, V, t(A, L, R)), 838 slim_iterm(L, L0, V), 839 slim_iterm(R, R0, V), 840 cofact(Y, t(A, L0, R0)) 841 ). 842 843% ?- ltr, N=3, K=100, open_hash(N, H), nb_setval(zdd_memo, H), 844% numlist(1, K, Ks), X<< dnf(+Ks), dump_memo. 845% 846dump_memo:- dump_memo(zdd_memo). % default main memo. 847% 848dump_memo(Name):- b_getval(Name, H), dump_hash(H). 849% 850dump_hash(#(C,B,V)):-!, functor(V, _, S), 851 writeln((cont=C, bucket=B, hsize=S)), 852 forall(between(1, S, K), ( arg(K, V, D), writeln(D)))