Did you know ... Search Documentation:
 Pack pac -- prolog/zdd/zdd.pl
zdd_memberchk(L, Z) is det
A list L as a set is a member of a family Z of sets.
zdd_find(+F, +X, -Y) is nondet
Unify Y with an atom in X which satisfies F(X).
opp_compare(-C, +X, +Y) is det
This is almost the standar compare/3 except "a - b" < "a -> b". ?- `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))`.
zdd_eval(+E, -V) is det
Evaluate E recursively and unify the obtained value with V in state S.

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

--- zdd 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,```
zdd_eval(+X, -Y) is det
Evaluate X and unify the value with Y.
zdd_eval(+E, -V, +M) is det
Evaluate E in module M, and unify the value with V.
bdd_cons(+X, +Y, -Z) is det
Short hand for `cofact(Z, t(X, 0, Y), S)`. Having analogy Z = [X|Y] in mind.
zdd_disjoint_merge(+X, +Y, -Z) is det
Z is unified with the family of sets that is union of disjoint set A in X and B in Y. For example, if X ={[a, b], [b]} and Y={[a,c],[c]} then Z = {[a,b,c], [b,c]}.
zdd_subfamily(+X, +Y) is nondet
True if a ZDD X is a subfamily of a ZDD Y.
psa(+X) is det
print all sets of X ?- X<<`pow([a])`, `psa(X)`. ?- X<<{[a]}, `psa(X)`.
zdd_rand_path(+I, +S) is det
Print a set at random in In.

?- `zdd((X << pow([a, b, c]), zdd_rand_path(X)))`. ?- `zdd((X << {[a], [b], [c]}, zdd_rand_path(X)))`. ?- `zdd((X << pow([a, b, c, d, e, f, g]), zdd_rand_path(X)))`.

atomlist(+T, -A) is det
T is a term of the form `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.
charlist(+U, -I) is det
U = A-B. I is unified with the list of characters X such that A @=< X @=< B.
charlist(+A, +B, X) is det
Equivalent to `charlist(A-B, X)`. ?- `charlist(a, c, X)`. @ X = [a, b, c].
zdd_insert(+A, +Y, -Z, +S) is det
Insert A to each set in a ZDD Y, and unify Z. Z = { union of U and {A} | U in Y }.

?- `zdd((zdd_insert(a, 1, X), zdd_insert(b, X, X1), prz(X1)))`. ?- `zdd((X<<pow([a,b,c]), zdd_insert(x, X, X1), psa(X1)))`.

zdd_insert_atoms(+As, +X, -Y) is det
Insert all atoms in As to X to get the result Y.
card(+I, -C) is det
unify C with the cardinality of a family I of sets.
max_length(+X, -Max) is det
Unify Max with max of size of members of X.
dnf(+X, -Y) is det
Y is a disjuntive normal form of a boolean formula X.
nnf_dnf(+E, -Z) is det
Z is unified with a dnf for nnf (Negation Normal Form) E.
cnf(+X, -Y) is det
Y is unified with a conjuntive normal form of a boolean nnf X.
card_filter_gte(+N, +X, -Y) is det
Y = { A in X | #A >= N }, where #A is the number of elements of A.
card_filter_between(+I, +J, +X, -Y) is det
Y = { A in X | I =< #A =< J }. ?- `time(( N = 100, numlist(1, N, Ns), X<<pow(Ns), card_filter_between(50, 51, X, Y), card(Y, C)))`.
bdd_list_raise(+L, +N, -X) is det
L: list of atoms. N: integer exponent. X is unified with a BDD L^N=LL...L (N times), i.e., the set of lists of lenghth N which consists of elements of L.

## Undocumented predicates

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

Arg1 << Arg2
zdd
ltr
ltr_join(Arg1, Arg2, Arg3)
ltr_join_list(Arg1, Arg2)
ltr_join_list(Arg1, Arg2, Arg3)
ltr_merge(Arg1, Arg2, Arg3)
ltr_card(Arg1, Arg2)
card_filter_lte(Arg1, Arg2, Arg3)
sat
sat(Arg1)
sat_count(Arg1)
set_at(Arg1, Arg2)
obj_id(Arg1, Arg2)
nnf_cnf(Arg1, Arg2)
all_fun(Arg1, Arg2, Arg3)
all_mono(Arg1, Arg2, Arg3)
all_epi(Arg1, Arg2, Arg3)
merge_funs(Arg1, Arg2)
bdd_list(Arg1, Arg2)
bdd_append(Arg1, Arg2, Arg3)
bdd_interleave(Arg1, Arg2, Arg3)
zdd_div_by_list(Arg1, Arg2, Arg3)
bdd_sort_append(Arg1, Arg2, Arg3)
bdd_append(Arg1, Arg2, Arg3)
zdd_insert(Arg1, Arg2, Arg3)
l_cons(Arg1, Arg2, Arg3)
zdd_ord_insert(Arg1, Arg2, Arg3)
zdd_reorder(Arg1, Arg2, Arg3)
zdd_has_1(Arg1)
zdd_family(Arg1, Arg2)
zdd_join(Arg1, Arg2, Arg3)
zdd_join_1(Arg1, Arg2)
zdd_join_list(Arg1, Arg2)
zdd_singleton(Arg1, Arg2)
zdd_merge(Arg1, Arg2, Arg3)
zdd_merge_list(Arg1, Arg2, Arg3)
zdd_meet(Arg1, Arg2, Arg3)
zdd_subtr(Arg1, Arg2, Arg3)
zdd_subtr_1(Arg1, Arg2)
zdd_xor(Arg1, Arg2, Arg3)
zdd_div(Arg1, Arg2, Arg3)
zdd_mod(Arg1, Arg2, Arg3)
zdd_divmod(Arg1, Arg2, Arg3, Arg4)
zdd_div_div(Arg1, Arg2, Arg3, Arg4)
zdd_divisible_by_list(Arg1, Arg2, Arg3)
zdd_power(Arg1, Arg2)
zdd_ord_power(Arg1, Arg2, Arg3)
zdd_rand_path(Arg1)
zdd_rand_path(Arg1, Arg2, Arg3)
ltr_meet_filter(Arg1, Arg2, Arg3)
ltr_join_filter(Arg1, Arg2, Arg3)
get_key(Arg1, Arg2)
atom_index(Arg1)
set_key(Arg1, Arg2)
update_key(Arg1, Arg2, Arg3)
set_pred(Arg1, Arg2)
zdd_compare(Arg1, Arg2, Arg3)
zdd_sort(Arg1, Arg2)
open_key(Arg1, Arg2)
close_key(Arg1)
set_compare(Arg1)
get_compare(Arg1)
map_zdd(Arg1, Arg2, Arg3)
psa
psa(Arg1, Arg2)
mp(Arg1, Arg2)
sets(Arg1, Arg2)
ppoly(Arg1)
poly_term(Arg1, Arg2)
eqns(Arg1, Arg2)
zdd_list(Arg1, Arg2)
significant_length(Arg1, Arg2, Arg3)