close_state(+S) is det

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

 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.

 close_memo(+S) is det

Close the chiled state of S.

 inherit_compare(+S, +T) is det

Set the same compare predicate of S to the state T.

 inherit_compare_opp(+S, +T) is det

Set the oppoiste compare predicate of S to the state T.

 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.

 memoq(+Q:X-V, +S) is det

Check V with the value of key X compared by == stored in the hash table of S.

 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.

 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.

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

Put a key-value term X-E on the hash table H.

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

 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.

 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.

 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.

 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.

Undocumented predicates

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

 open_state(Arg1)

 open_state(Arg1, Arg2)

 memo(Arg1, Arg2)

 memochk(Arg1, Arg2)

 memo_index(Arg1, Arg2)

 set_memo(Arg1, Arg2)

 update_memo(Arg1, Arg2, Arg3)

 get_child(Arg1, Arg2)

 unify_args(Arg1, Arg2, Arg3)

 add_child(Arg1, Arg2)

 add_child(Arg1, Arg2, Arg3)

 pred_memo_update(Arg1, Arg2, Arg3)