open_state is det

open a new state.

 show_array is det

The same as show_array(zdd_vec). ! show_array(+G) is det. Print all triples in array bound to G.

 memo(+A, +G) is det

A = X-V. 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.

 insert_memo(+Key, +X) is det

Insert X in the zdd associated with the Key when the Key entry exists, otherwise the zdd is assumed to be 1.

 pred_memo_update(+Pred, U) is det

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

 memoq(U) is det

U = X-V, Check V with the value of key X compared by == stored in the hash table of S. ?- zdd. ?- push_memo, memo(a-b), memoq(a-Y). % fail.

 index(?Index, ?Vec, ?Elem) is det

Simple version of index/3. Index-th arg of Vec is unified with Elem. When Index is greater than the size of Vec, Vec is extended by double using the "destructive" operation setarg. Vec is initialized as a special term #(0, #), which means the empty vector, when Vec is unbound.

 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).

 close_hash(+H) is det

close hash table H, to be reclaimed later.

 open_vector(+N, -A) is det

A is unified with a new vector of size N. ?- open_vector(0, H), write(H). ?- open_vector(3, H), write(H).

 hash(+X, +H, ?E) is det

Put a key-value term X-E on the hash table H. ! hash_scan(+X, +Y, ?Val)

 cofact(?X, ?T, +State) is det

T = 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).

 slim_gc(+X, -Y) is det

Do slim_iterms(X, Y), and call garbage_collect.

 slim_iterms(+X, -Y) is det

Remove all redundant iterms (was zdds) that are irrelevant to those specified in X.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 open_state(Arg1)

 close_state

 open_state_core(Arg1)

 open_state_core(Arg1, Arg2)

 memo(Arg1)

 init_memo_stack

 memo_index(Arg1, Arg2)

 push_memo

 pop_memo

 use_memo(Arg1)

 reset_memo_call(Arg1)

 open_memo(Arg1)

 open_memo(Arg1, Arg2)

 close_memo(Arg1)

 set_memo(Arg1)

 update_memo(Arg1, Arg2)

 dump_memo

 dump_memo(Arg1)

 dump_hash(Arg1)

 unify_args(Arg1, Arg2, Arg3)

 add_child(Arg1, Arg2)

 add_child(Arg1, Arg2, Arg3)

 cofact(Arg1, Arg2)

 term(Arg1, Arg2)

 iterm(Arg1, Arg2)

 iterm(Arg1, Arg2, Arg3)

 index(Arg1, Arg2)