Did you know ... Search Documentation:
Pack pac -- prolog/zdd/zdd.pl
PublicShow source
 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)