zdd-array.pl

    1:- module(zdd_array, [
    2				open_state/1, open_state/2, close_state/1
    3			,	memo/2, memochk/2, memoq/2
    4			,	memo_index/2
    5			,	open_hash/2, hash/3, close_hash/1
    6 			,	open_memo/1
    7			,	close_memo/1
    8			,	set_memo/2, update_memo/3
    9			,	get_child/2
   10			,	insert_memo/3
   11			,	unify_args/3
   12			,	add_child/2, add_child/3
   13			,	pred_memo_update/3
   14			,	cofact/3, index/3
   15			,	zdd_slim/3
   16			,	zdd_copy/4, zdd_ord_copy/4, zdd_pred_copy/5
   17			,	inherit_compare/2
   18			,	inherit_compare_opp/2
   19			  ]).   20
   21
   22:- use_module(zdd(zdd)).   23
   24bucket_aware_rehash.		% #(_, _, #(_,_))
   25% \+ bucket_aware_rehash.	% #(_, #(_,_))
   26
   27% suppress details of hash/vector.
   28atom_only(A, A0):- ( compound(A) -> A0 = '.' ;  A0 = A).
   29
   30user:portray(X):- compound(X),
   31	(	functor(X, s, N), N > 7 -> write('s(..)')
   32	;	functor(X, ctrl, N), N > 2 -> write('<ctrl>')
   33	;	compound_name_arguments(X, F, _),
   34		( F = (#) -> write(#(..))
   35		; F = call_continuation -> write(cont(..))
   36		)
   37	).
   38
   39% ?- initial_hash(X), writeln(X).
   40% ?- initial_hash(100, X).
   41:- if(bucket_aware_rehash).   42initial_hash(N, #(0, 0, V)):-!, functor(V, #, N).
   43initial_hash(#(0, 0, #([]))).
   44:- else.   45initial_hash(N, #(0, V)):-!, functor(V, #, N).
   46initial_hash(#(0, #([]))).
   47:- endif.   48
   49% hash table access.
   50:- if(bucket_aware_rehash).   51goal_expansion(initial_hash(X),  X = #(0, 0, #([]))).
   52goal_expansion(initial_hash(N, X),
   53			   (	X = #(0, 0, V),
   54					functor(V, #, N))).
   55goal_expansion(hash_key_count(H, C), ( arg(1, H, C) )).
   56goal_expansion(hash_key_count_set(H, C), ( setarg(1, H, C) )).
   57goal_expansion(hash_bucket_count(H, C), ( arg(2, H, C) )).
   58goal_expansion(hash_bucket_count_set(H, C), ( setarg(2, H, C) )).
   59goal_expansion(hash_vector(H, V), ( arg(3, H, V) )).
   60goal_expansion(hash_vector_set(H, V), ( setarg(3, H, V) )).
   61
   62:- else.   63
   64goal_expansion(initial_hash(X),  X = #(0, #([]))).
   65goal_expansion(initial_hash(N, X),
   66			   (	X = #(0, V),
   67					functor(V, #, N))).
   68goal_expansion(hash_key_count(H, C), ( arg(1, H, C) )).
   69goal_expansion(hash_key_count_set(H, C), ( setarg(1, H, C) )).
   70goal_expansion(hash_vector(H, V), ( arg(2, H, V) )).
   71goal_expansion(hash_vector_set(H, V), ( setarg(2, H, V) )).
   72:- endif.   73
   74%
   75goal_expansion(hash_of_state(X, H),  ( arg(1, X, A), arg(2, A, H))).
   76goal_expansion(array_hash_of_state(S, A, H), ( arg(1, S, A), arg(2, A, H))).
   77%
   78goal_expansion(vector_of_state(S, Array), ( arg(1, S, Z), arg(3, Z, Array))).
   79goal_expansion(vector_of_state(S, Array, Max),
   80			   ( arg(1, S, Z),
   81				 arg(3, Z, Array),
   82				 arg(1, Z, Max))).
   83goal_expansion(child_state(S, S0),
   84	( arg(4, S, Child),
   85		(	Child == [] -> S0 = S
   86		;	S0 = Child
   87		)
   88	)).
   89%
   90get_child(S, M):- child_state(S, M).

Assuming a totally ordered set of atoms, a state is a collection of families of (finite) sets of (finite) these atoms. In a state, each family of sets (FOS) is given a unique nonnegative integer. 0 is reserved for the empty family {}, and 1 for {{}} = {0} = 1. If a FOS F is neither 0 nor 1, there must be the maximum atom A among those are an element of a set of F. A is called the maximum atom of F. The maximum atom is defined neither for 0 nor 1. Throuhout successive updating process of a state, once the unique id of a FOS is created, this id is kept for the FOS henceforth. cofact/3 is the main bidirectional interface predicate on states to get a FOS id (fact), and to store new FOS (cofact) in a state. A nonnegative integer k is used for the FOS whose id is k, and vice versa.

  106% ?- open_state(S), write(S).
  107%!	open_state(-S) is det.
  108%	S is unified with a new state.
  109open_state(S):- open_state(S, []).
  110%
  111open_state(s(#(1, Hash, Vector), Extra, Compare, [],
  112				 _,		% extra 5th
  113				 _,		% extra 6th
  114				 _,		% extra 7th
  115				 _),	% extra 8th
  116		   Args):-
  117	default_compare(Compare),
  118	( memberchk(hash_size(HsizeExp), Args); 	HsizeExp = 1 ), !,
  119	( memberchk(vector_size(VsizeExp), Args); 	VsizeExp = 1 ), !,
  120	( memberchk(extra(Extra), Args); 	Extra = [varnum-0, varzip-[]] ), !,
  121	Hsize is HsizeExp,
  122	Vsize is VsizeExp,
  123	functor(Vector, #, Vsize),
  124	setarg(1, Vector, 0),
  125	open_hash(Hsize, Hash).

E must be ground, whose main functor is used as a counter name. A unique integer for E is unified with V. This is handy to give a series of integer index to members of a family of ground terms.

  133% ?- open_state(S), memo(a-1, S), memo(a-X, S).
  134% ?- open_state(S), memo_index(x-I, S), memo_index(y-J, S), memo_index(x-K, S).
  135% ?- open_state(S), memo_index(x(1)-I, S), memo_index(x(2)-J, S), memo_index(x(1)-K, S).
  136% ?- open_state(S), memo_index(a(1)-V, S), memo_index(a(1)-U, S).
  137% ?- open_state(S), memo_index(a(1)-V, S), get_key(a, C, S).
  138memo_index(E-V, S):- memo(E-V, S), !,
  139	(	nonvar(V) -> true
  140	;	functor(E, CounterName, _),
  141		memo_index(CounterName, V, S)
  142	).
  143%
  144memo_index(Name, V0, S):- arg(2, S, Extra),
  145	(	select(Name-V, Extra, Extra0) ->
  146		V0 is V+1
  147	;	Extra0 = Extra,
  148		V0 = 1
  149	),
  150	Extra1 = [Name-V0|Extra0],
  151	setarg(2, S, Extra1).
  152
  153% Structure Sharing.
  154setarg_state_extra(X, Y):- arg(3, X, Extra), setarg(3, Y, Extra).
  155%
  156setarg_state_core(X, Y):- arg(1, X, Core), setarg(1, Y, Core).
  157%
  158clear_child(S) :- set_child([], S).
  159%
  160set_child(Child, S):- setarg(4, S, Child).
  161
  162%
  163default_compare(compare).

dump_array(+S) is det: Print all triples stored in the state S.

  168% ?- open_state(S), zdd_eval(pow([a,b,c]), _, S), dump_array(S).
  169% ?- open_state(S), zdd_eval(family([[a],[b],[c]]), X, S), dump_array(S).
  170dump_array(S):- vector_of_state(S, Array, Max),
  171	  forall( between(2, Max, J),
  172			  ( arg(J, Array, T), writeln(J=T))).

close_state(+S) is det: Close the state S. Unused memory is expected to be freed (not sure).

  177% Note: States are nested recursively in a linear way.
  178% ?- open_state(S), close_state(S).
  179close_state(S):- clear_state(S).
  180
  181%
  182clear_state(S):-
  183	nb_setarg(1, S, []),
  184	nb_setarg(2, S, []),
  185	nb_setarg(3, S, []),
  186	nb_setarg(4, S, []).

open_memo(+S) is det: Open a fresh state M, and M is attatched to S. M is called the child state of S. The child state is mainly used as a hash table.

  193% ?- zdd((open_memo, memo(a-1), memo(a-V), close_memo)).
  194% ?- zdd((open_memo, memo(a-1), memo(a-V), close_memo, memo(a-U), var(U))).
  195
  196open_memo(S):- nonvar(S),!,
  197	open_state(S0),
  198	set_child(S0, S).
  199open_memo(S):- open_state(S).

close_memo(+S) is det: Close the chiled state of S.

  204% Close nested memos recursively.
  205close_memo(S):- must_be(nonvar, S),
  206	child_state(S, S0),
  207	clear_child(S),
  208	(	S0 == [] -> true
  209	; 	close_state(S0)		% Note that NOT close_memo.
  210	).

inherit_compare(+S) is det: Set the same compare predicate to the child state of S.

  215inherit_compare(S):- get_compare(CMP_pred, S),
  216	child_state(S, Child),
  217	set_compare(CMP_pred, Child).

inherit_compare(+S, +T) is det: Set the same compare predicate of S to the state T.

  222inherit_compare(S, T):- get_compare(CMP_pred, S),
  223	set_compare(CMP_pred, T).

inherit_compare_opp(+S) is det: Set the oppoiste compare predicate of S to the child state of S.

  228inherit_compare_opp(S):- get_compare(Pred, S),
  229	child_state(S, Sub),
  230	set_compare(pred_compare_opp(Pred), Sub).

inherit_compare_opp(+S, +T) is det: Set the oppoiste compare predicate of S to the state T.

  235inherit_compare_opp(S, T):- get_compare(Pred, S),
  236	set_compare(pred_compare_opp(Pred), T).
  237
  238% ?- zdd((memo(a-1), memoq(a-1))).
  239% ?- zdd((memo(a-1), memochk(a-X))).
  240% ?- zdd((memochk(a-X))).  %@ false.
  241% ?- zdd((memo(a-1), memoq(a-X))).	% false
  242% ?- zdd((memo(a-1), memo(a-X))).
  243% ?- zdd((X<<pow(:numlist(1, 1000)), card(X, C))). % in zdd module.
  244% ?- open_state(S), memo(a-1, S), memo(a-V, S).
  245% ?- open_state(S), memo(a-1, S), memo(a-V, S), set_memo(a-2, S),
  246%	memo(a-U, S).
  247% ?- zdd:zdd((set_memo(a-1), memo(a-X))).
  248
  249% ?- open_hash(2, H), hash(a, H, X), X=3, hash(a, H, Y).
  250% Take time !!
  251% ?- open_hash(2, H), time(repeat(10^8, (hash(a, H, X), X=3, hash(a, H, Y)))).
  252% ?- open_hash(2, H), time(repeat(10^8, (hash(a, H, X), X=3,
  253%	 close_hash(H), hash(a, H, Y)))).
  254% ?- open_hash(2, H), hash(a, H, X), hash(a, H, Y), X==Y.

The input pair X-V is unified with with a member of a bucket of the hash table of the state S. Otherwise, create a new entry for X-V.

  259memo(X-V, S):- child_state(S, S0),
  260	hash_of_state(S0, H),
  261	hash(X, H, V).
  262
  263% ?- zdd((set_memo(a-1), memo(a-Y), set_memo(a-2), memo(a-R))).
  264% ?- zdd((set_memo(a-1), memo(a-Y), set_memo(a-V), memo(a-R), V=2)).
  265set_memo(X-V)	:- shift(=(S)), hash_fresh_entry(X, S, V, _).

Replace old X entry with X-V when X entry exists, otherwise, simply create X-V entry.

  271set_memo(X-V, S)	:- 	hash_fresh_entry(X, S, V, _).
  272
  273% ?- zdd((memo(a-1), update_memo(a-X, Y), X=2, memo(a-U))).

Replace X-Old entry with X-FreshVar entry when the former exists, otherwise simply create X-FreshVar entry with Old left uninstantiated.

  280update_memo(X-FreshVar, OldVal, S):-
  281	hash_fresh_entry(X, S, FreshVar, OldVal).

insert_memo(+Key, +X, +S) is det: Insert X in the zdd associated with the Key when the Key entry exists, otherwise the zdd is assumed to be 1.

  287% ?- zdd((#(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))).
  288
  289insert_memo(Key, X, S):-
  290	update_memo(Key-New, Old, S),
  291	( var(Old) -> Old=1		% empty set
  292	; true
  293	),
  294	zdd_insert(X, Old, New, S).
  295%
  296% :- meta_predicate pred_memo_update(3, ?).
  297% pred_memo_update(Pred, X):- ##(pred_memo_update(Pred, X)).

Replace the pair K-L0 with K-L, where L is obtained by applying Pred to V, L0, by calling Pred(V, L0, L).

  303:- meta_predicate pred_memo_update(3, ?, ?).  304pred_memo_update(Pred, K-V, S):- update_memo(K-L, L0, S),
  305	call(Pred, V, L0, L).
  306
  307% ?- zdd((memo_add_new(a-1), memo(a-X))).
  308% ?- zdd((memo_add_new(a-1), memo_add_new(a-2), memo(a-X))).
  309% ?- zdd((memo_add_new(a-1), memo_add_new(a-2), memo_add_new(a-1), memo(a-X))).
  310memo_add_new(X):-  pred_memo_update(add_new, X).

Insert V in the list associated with the key K only when V is new in the list.

  316memo_add_new(X, S):- pred_memo_update(add_new, X, S).
  317
  318% ?- zdd((pred_memo_update(add_new, a-1), memo(a-X))).
  319add_new(V, [], [V]):-!.
  320add_new(V, L0, L0):- memberchk(V, L0), !.
  321add_new(V, L0, [V|L0]).
  322
  323% ?- zdd((add_child(suc(a), 1), memo(suc(a)-X))).
  324% ?- zdd((add_child(a, 1), add_child(a, 2), memo(a-X))).
  325% ?- zdd((add_child(a, 1), add_child(a, 2), add_child(a, 1), memo(a-X))).
  326% ?- numlist(1, 100000, Ns),
  327%	time(zdd(( maplist(pred([Child]:- add_child(a, Child)), Ns), memo(a-X)))).
  328
  329add_child(X, Child):-  pred_memo_update(add_new, X-Child).
  330%
  331add_child(X, Child, S):- pred_memo_update(add_new, X-Child, S).
  332
  333%
  334memochk(X):- #(memochk(X)).

Unify V with the value of key X only when X entry exists in S, otherwise, fails.

  340memochk(X-V, S):- child_state(S, S0),
  341	hash_of_state(S0, H),
  342	term_bucket_index(X, H, B, _),
  343	memberchk(X-V, B).

memoq(+Q:X-V, +S) is det: Check V with the value of key X compared by == stored in the hash table of S.

  348memoq(X-V, Z):- memochk(X-U, Z), !,  U == V.
  349
  350		/**********************************************
  351		*         index/get_index/set_index           *
  352		**********************************************/
  353
  354% ?- Array = a(#(1,2)), index(2, Array, X), writeln(Array).
  355% ?- Array = a(#(1,2)), index(5, Array, X), writeln(Array).

index(+I, +A, ?X) is det: Unify X with I-th element of the Array when I is less than equal to the current size of Array, otherwise, extend Array enough for I to satisfy the above condition.

  362index(I, Array, X):- arg(1, Array, Vec),
  363		functor(Vec, _, N),
  364		(	I =< N -> arg(I, Vec, X)
  365		;   enlarge_vector(Vec, I, Vec0), !,
  366			nb_setargs(N, Vec, Vec0),
  367			setarg(1, Array, Vec0),
  368			arg(I, Vec0, X)
  369		).
  370
  371% ?- enlarge_vector(#(1,2,3), 5, R), writeln(R).
  372% ?- enlarge_vector(#(1,2,3), 3, R), writeln(R).

enlarge_vector(+A, +I, -B) is det: When vector A has I-th (I>= 1) element then B is unified with A, otherwise, extend A so as to be the minimum array such that new size = 2^n x old size >= I for an integer n, and B is unified with this new A. In the latter case, all entries of of the old A are unified with that of new A in order.

  381enlarge_vector(A, I, B) :-
  382		functor(A, G, N),
  383		(	I =< N -> B = A
  384		;	iterate_double_number(N, I, N0),
  385			functor(B, G, N0),
  386			nb_setargs(N, A, B)
  387		).

get_index(+I, +Array, -X) is det: Equivalent to index(I, Array, X).

  391get_index(I, Array, X):- index(I, Array, X), !.

set_index(+I, +Array, -X) is det: Unify X with I_th element of the Array when I is less than equal to the current size of Array, otherwise, extend Array enough for Array to have I-th emlement, then unify X with the I-th element of extended Array, which is an uninstatiated variable.

  399set_index(I, Array, X):- arg(1, Array, Vec),
  400		functor(Vec, _, N),
  401		(	I =< N -> setarg(I, Vec, X)
  402		;   enlarge_vector(Vec, I, Vec0),
  403			nb_setargs(N, Vec, Vec0),
  404			setarg(1, Array, Vec0),
  405			setarg(I, Vec0, X)
  406		).
  407%
  408iterate_double_number(N, I, N):- I=<N, !.
  409iterate_double_number(N, I, M):- N0 is 2*N,
  410	iterate_double_number(N0, I, M).
  411
  412nb_setargs(0, _, _):-!.
  413nb_setargs(I, X, Y):- arg(I, X, A),
  414		nb_setarg(I, X, 0),				% [2021/10/30]
  415		arg(I, Y, A),
  416		I0 is I - 1,
  417		nb_setargs(I0, X, Y).
  418
  419% NEW style: assuming simple failure for exceeding index.
  420% ?- unify_args(1, f(A, B, C), a).
  421unify_args(I, X, A):- arg(I, X, A), !,
  422	J is I + 1,
  423	unify_args(J, X, A).
  424unify_args(_, _, _).
  425
  426% OLD style of iteration on args.
  427% ?- old_unify_args(3, f(A, B, C), a).
  428old_unify_args(0, _, _):-!.
  429old_unify_args(I, X, A):- arg(I, X, A), !,
  430	J is I - 1,
  431	old_unify_args(J, X, A).
  432
  433%
  434getid_via_global(G, X, I):- b_getval(G, S), cofact(I, X, S).
  435
  436		/***********************************************
  437		*         new_array_elem/get_elem/set_elem     *
  438		***********************************************/

open_hash(+N, -H) is det: Create a new hash table with N entries for buckets, and unify with H. ?- open_hash(3, H), hash(a, H, X), write(H).

  442open_hash(N, H):- initial_hash(N, H),
  443	hash_vector(H, V),
  444	unify_args(1, V, []).  % Buckets are empty at start.

close_hash(+H) is det: close hash table H, to be reclaimed later.

  448close_hash(H):- hash_vector_set(H, []).  % not by nb_setarg, but by setarg.

hash_memo(+X, +R, ?V) is det: Unify X-V with an element in the hash table R. Rehash may be applied to R by check_rehash/1.

  454% ?- open_hash(2, H),
  455%  time(repeat(1000, (hash(a, H, X), X=3, hash(a, H, Y)))).

term_bucket_index(+X, +H, -B, -I) is det: I is unified with the value for X by term_hash/4, and B is unified with I-th bucket of H.

  461% ?- term_bucket_index(b, #(2, 1, #([],[],[])),  B, I).
  462term_bucket_index(X, H, B, I):-
  463	hash_vector(H, Vec),
  464	functor(Vec, _, N),
  465	term_hash(X, 3, N, I0),
  466	I is I0 + 1,
  467	arg(I, Vec, B).

hash(+X, +H, ?E) is det: Put a key-value term X-E on the hash table H.

  472hash(X, H, Val):-
  473	check_rehash(H),
  474	term_bucket_index(X, H, U, I),
  475	(	memberchk(X-V, U) -> Val = V
  476	;	hash_vector(H, Vec),
  477		setarg(I, Vec, [X-Val | U]),
  478		hash_key_count(H, C),
  479		C0 is C + 1,
  480		hash_key_count_set(H, C0)
  481	).

hash_fresh_entry(+X, +S, -Var, -OldVal) is det: If X-OldVal exists in the hash table then the entry is removed, otherwise, OldVal is left uninstantiated. Then X-var is put as a fresh pair on the hash table. Rehash may be performed by check_rehash/1. This predicate is used to calculate value using old value after preparing the entry for the new value.

  491hash_fresh_entry(X, S, FreshVar, OldVal):- hash_of_state(S, H),
  492	check_rehash(H),
  493	term_bucket_index(X, H, U, I),
  494	hash_vector(H, Vec),
  495	(	select(X-OldVal, U, U0)
  496	->	setarg(I, Vec, [X-FreshVar | U0])
  497	;	setarg(I, Vec, [X-FreshVar | U])
  498	).
  499
  500% ?- initial_hash(H), check_rehash(H), writeln(H).
  501% ?- initial_hash(H), check_rehash(H), check_rehash(H),
  502%  check_rehash(H), writeln(H).
  503% ?- listing(check_rehash).
  504:- if(bucket_aware_rehash).  505check_rehash(H):- H = #(C, B, V),
  506		functor(V, _, N),
  507		(	C > B + 1.7 * N -> once(rehash(H))
  508		;	true
  509		).
  510
  511:- else.  512
  513check_rehash(H):- H = #(C, V), !,
  514		functor(V, _, N),
  515		(	C > 1.7 * N -> once(rehash(H))
  516		;	true
  517		).
  518:- endif.

new_array_elem(+X, +Z, -I) is det: Unify I with an integer index for entry X

  524% ?- numlist(1,3, Ns), zdd((X<<pow(Ns), card(X, C))).
  525new_array_elem(X, Z, I):-
  526		arg(1, Z, J),
  527		arg(3, Z, Vec),
  528		I is J + 1,
  529		functor(Vec, _, N),
  530		(	I > N
  531		->	once(double_array(Z)),
  532			arg(3, Z, Vec0)
  533		;	Vec0 = Vec
  534		),
  535		setarg(1, Z, I),
  536		arg(I, Vec0, X).

double_array(+A) is det: Update A by extending array component of A by double. (Destructive update).

  542double_array(A) :- arg(3, A, Z),
  543		functor(Z, G, N),
  544		(	N == 0 -> N0 = 2
  545		; 	N0 is 2*N
  546		),
  547		functor(Z0, G, N0),
  548		nb_setargs(N, Z, Z0),
  549		setarg(3, A, Z0).

get_elem(+X, +Z, -Y) is det: Unify Y with X-th element of ZDD stored in Z.

  554get_elem(X, Z, Y):- arg(3, Z, Vec),
  555	   arg(X, Vec, Y).

set_elem(X, Z, Y) is det: Set X-th element of the vector component of Z to Y.

  559set_elem(X, Z, Y):- arg(3, Z, Vec), setarg(X, Vec, Y).
  560
  561% ?- initial_hash(H), rehash(H), writeln(H), rehash(H), rehash(H), rehash(H), writeln(H).

rehash(H, H0) is det: Extend the hash table H to double-sized H0, and rehash H to H0.

  565rehash(H):-
  566	hash_vector(H, Vec),
  567	functor(Vec, F, N),
  568	N0 is N + N,
  569	functor(Vec0, F, N0),
  570	unify_args(1, Vec0, []),
  571	!,
  572	(	functor(H, _, 2)->
  573		migrate_hash(N, Vec, Vec0),
  574		hash_vector_set(H, Vec0)
  575	;	migrate_hash(N, Vec, Vec0, 0, C),
  576		hash_vector_set(H, Vec0),
  577		hash_bucket_count_set(H, C)
  578	).

migrate_hash(I, V, V0) is det: Rehash all elements of I-th bucket of V into V0.

  581migrate_hash(0, _, _):-!.
  582migrate_hash(I, V, V0):-
  583	arg(I, V, B),
  584	once(migrate_bucket(B, V0)),
  585	I0 is I - 1,
  586	migrate_hash(I0, V, V0).
  587%
  588migrate_bucket([], _):-!.
  589migrate_bucket([Q|U], H):-
  590	(	Q = (X-_) -> E = Q
  591	;   X = Q,
  592		E = Q
  593	),
  594	functor(H, _, S),
  595	term_hash(X, 3, S, K),
  596	K0 is K + 1,
  597	arg(K0, H, D),
  598	setarg(K0, H, [E|D]),
  599	migrate_bucket(U, H).
  600
  601% For buckets number aware rehashing.
  602migrate_hash(0, _, _, C, C):-!.
  603migrate_hash(I, V, V0, C, C0):-
  604	arg(I, V, B),
  605	once(migrate_bucket(B, V0, C, C1)),
  606	I0 is I - 1,
  607	migrate_hash(I0, V, V0, C1, C0).
  608
  609%
  610migrate_bucket([], _, C, C):-!.
  611migrate_bucket([Q|U], H, C, C0):-
  612	(	Q = (X-_) -> E = Q
  613	;   X = Q,
  614		E = Q
  615	),
  616	functor(H, _, S),
  617	term_hash(X, 3, S, K),
  618	K0 is K + 1,
  619	arg(K0, H, D),
  620	setarg(K0, H, [E|D]),
  621	(	D=[] -> C1=C
  622	;	C1 is C+1
  623	),
  624	migrate_bucket(U, H, C1, C0).
  625
  626		/****************
  627		*     cofact    *
  628		****************/
  629
  630% ?- zdd((cofact(X, t(a, 1, 0)))).
  631% ?- zdd((X<<set([a]), psa(X))).

cofact(?X, ?C:t(A,L,R), +State) is det

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.

?- open_state(S), cofact(X, [a,b,d], S), cofact(X, L, S). ?- open_state(S), cofact(X, [a], S), cofact(X, [A|B], S). ?- open_state(S), cofact(X, f(a,b,d), S), cofact(X, L, S).

  655cofact(X, C, S):- nonvar(X), !,   % X>1 assumed.
  656	vector_of_state(S, Vec),
  657    arg(X, Vec, C).
  658cofact(X, t(_, X, 0), _):-!.	 % the famous Minato's zero-suppress rule.
  659cofact(X, C, S):- array_hash_of_state(S, A, H),
  660	hash(C, H, X),		% check C0-X entry in H (hash)
  661	(	nonvar(X) -> true		% exists.
  662	;	new_array_elem(C, A, X)	% new.
  663	).
  664
  665% cofact(X, C, S):- nonvar(X), !,   % X>1 assumed.
  666% 	vector_of_state(S, Vec),
  667%     arg(X, Vec, C0),
  668% 	cofact_extern(C0, C).
  669% cofact(X, t(_, X, 0), _):-!.	 % the famous Minato's zero-suppress rule.
  670% cofact(X, C, S):- array_hash_of_state(S, A, H),
  671% 	cofact_intern(C, C0),
  672% 	hash(C0, H, X),		% check C0-X entry in H (hash)
  673% 	(	nonvar(X) -> true		% exists.
  674% 	;	new_array_elem(C0, A, X)	% new.
  675% 	).
  676
  677% cofact_intern(t(A, 0, R), u(A, R)):-!.
  678% cofact_intern(X, X).
  679
  680% cofact_extern(u(A,B), t(A, 0, B)):-!.
  681% cofact_extern(X, X).
  682
  683
  684		/*****************************************
  685		*     copy, slim, ord_copy, pred_copy    *
  686		*****************************************/

zdd_ord_copy(+X, +S, -Y, +T) is det: Copy zdds in X on S to Y on T. X is a nested lists of integers, which is a unique index of a zdd.

  692zdd_ord_copy(X, S, Y, T):- integer(X), !,
  693	zdd_ord_copy_basic(X, S, Y, T).
  694zdd_ord_copy([], _, [], _):-!.
  695zdd_ord_copy([X|Xs], S, [Y|Ys], T):-!,
  696	zdd_ord_copy(X, S, Y, T),
  697	zdd_ord_copy(Xs, S, Ys, T).

zdd_ord_copy_basic(+X, +S, -Y, +T) is det: Assuming both states S, T shares a same ordering, copy zdds in X on S to Y on T.

  703zdd_ord_copy_basic(X, _, X, _):- X< 2,!.
  704zdd_ord_copy_basic(X, S, Y, S0):- memo(ord_copy(X)-Y, S0),
  705	(	nonvar(Y) -> true
  706	;	cofact(X, t(A, L, R), S),
  707		zdd_ord_copy_basic(L, S, L0, S0),
  708		zdd_ord_copy_basic(R, S, R0, S0),
  709		cofact(Y, t(A, L0, R0), S0)		% Ordering is the same.
  710	).

zdd_copy(+X, +S, -Y, +T) is det: Copy zdds in X on S to Y on T. Sharing orders of S and T is not assumed.

  716zdd_copy(X, S, Y, T):- integer(X), !, zdd_copy_basic(X, S, Y, T).
  717zdd_copy([], _, [], _):-!.
  718zdd_copy([X|Xs], S, [Y|Ys], T):-
  719	zdd_copy(X, S, Y, T),
  720	zdd_copy(Xs, S, Ys, T).
  721%
  722zdd_copy_basic(X, _, X, _):- X< 2,!.
  723zdd_copy_basic(X, S, Y, S0):- memo(copy(X)-Y, S0),
  724	(	nonvar(Y) -> true
  725	;	cofact(X, t(A, L, R), S),
  726		zdd_copy_basic(L, S, L0, S0),
  727		zdd_copy_basic(R, S, R1, S0),
  728		zdd_insert(A, R1, R0, S0),	% Ordering may be different.
  729		zdd_join(L0, R0, Y, S0)
  730	).

zdd_pred_copy(+Pred, +X, +S, -Y, +T) is det: Predicate Pred/2 is to map atoms of S to that of T. Mapping atoms by Pred, copy zdds in X of S to those in Y of T.

  736% ?- open_state(S), open_state(S0), zdd_eval(pow([a,b]), X, S),
  737%	zdd_pred_copy(pred([A, A]), X, S, Y, S0), card(X, C, S), card(Y, D, S0),
  738%	psa(X, S), psa(Y, S0).
  739% ?- open_state(S), zdd_eval(pow([a, b, c]), X, S),
  740% zdd_pred_copy(pred([A,A-A]), X, S, Y, S), psa(X, S), psa(Y, S),
  741% card(X, C, S), card(Y, D, S).
  742
  743:- meta_predicate zdd_pred_copy(2, ?, ?, ?, ?).  744
  745zdd_pred_copy(Pred, X, S, Y, S0):- integer(X), !,
  746	zdd_pred_copy_basic(Pred, X, S, Y, S0).
  747zdd_pred_copy(_, [], _, [], _):-!.
  748zdd_pred_copy(Pred, [X|Xs], S, [Y|Ys], S0):- zdd_pred_copy(Pred, X, S, Y, S0),
  749	zdd_pred_copy(Pred, Xs, S, Ys, S0).
  750%
  751zdd_pred_copy_basic(_, X, _, X, _):- X< 2,!.
  752zdd_pred_copy_basic(Pred, X, S, Y, S0):- memo(pred_copy(X)-Y, S0),
  753	(	nonvar(Y) -> true
  754	;	cofact(X, t(A, L, R), S),
  755		zdd_pred_copy_basic(Pred, L, S, L0, S0),
  756		zdd_pred_copy_basic(Pred, R, S, R1, S0),
  757		call(Pred, A, B),
  758		zdd_insert(B, R1, R0, S0),
  759		zdd_join(L0, R0, Y, S0)
  760	).

?- open_state(S), open_memo(S), zdd_eval(pow([1,2]), X, S), zdd_eval(pow([a,b]), Y, S), zdd_slim(Y, U, S), writeln(S).

zdd_slim(+X, -Y, +S) is det: Remove all redundant zdds that are irrelevant to those specified in X. In fact, perform zdd_ord_copy(X, S, Y, T) for fresh state T, then the content of the orginal S is destructively replaced with that of T by setarg/3. T is closed at exit.

  773zdd_slim(X, Y, S):- open_state(S0),
  774	open_memo(S0),
  775	inherit_compare(S, S0),
  776	setarg_state_extra(S, S0),
  777	clear_child(S),		% clear substate (old memo) of the original state.
  778	zdd_slim(X, S, Y, S0),
  779	setarg_state_core(S0, S),
  780	clear_state(S0).	% Only detaching args for possible sharing.
  781%
  782zdd_slim(X, S, Y, T):- integer(X), !, zdd_ord_copy_basic(X, S, Y, T).
  783zdd_slim([], _, [], _):-!.
  784zdd_slim([X|Xs], S, [Y|Ys], T):- zdd_slim(X, S, Y, T),
  785	zdd_slim(Xs, S, Ys, T)