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

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

 opp_compare(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_disjoint_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)