Did you know ... Search Documentation:
Pack pac -- prolog/zdd/zdd.pl
PublicShow source
 obj_id(?X, ?Y, +S) is det
Bidirectional. Y is the atom of the root X. ?- zdd obj_id([a,b,c], Id), obj_id(Obj, Id).
 all_fun(+D, +R, -F, +S) is det
F is unified with the family of functions from D to R.
 all_mono(+D, +R, -F, +S) is det
F is unified with all injections from D to R.
 all_epi(+D, +R, -F, +S) is det
F is unified with the family of functions from D to R.
 zdd_lift(+X, -Y, +S) is det
Y is unified with flatted X: if X = {A1, ..., An} then Y = {B1, ..., Bn} where Bi is the singleton of Ai.
 l_cons(+A, +X, -Y, +S) is det
Y is unified with the family of lists [A|L] for L in X.
 zdd_memberchk(L, Z, G) is det
A list L as a set is a member of a family Z of sets.
 s_map(+F:pred/3, ?Xs, ?Ys, +S) is det
Almost equal to maplist(F(S), Xs, Ys).
 s_map(+F:pred/2, ?Xs, ?Ys, +S) is det
Almost equal to maplist(F(S), Xs).
 zdd_find(+F, +X, -Y, +S) is nondet
Unify Y with an atom in X which satisfies F(X).
 ltr_zdd(+E) is det
Solve E as command on families of clauses.
 opp_compare(-C, +X, +Y) is det
Equivalent to opp_compare(C, Y, X).
 <<(-X, +E, +S) is det
Evaluate expression E in state S then unify obtained value with X.
 zdd_eval(+E, -V, +S) 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 eval E as prolog term with last argument as output. #E eval E as zdd term using state. !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, +S) is det
Evaluate X and unify the value with Y in state S.
 zdd_eval(+E, -V, +S, +M) is det
Evaluate E in state S in context module M, and unify the value with V.
 zdd_family(+L, -X, +S) is det
For a list L of lists of atoms, build a zdd in S whose index is unified with X.
 zdd_join(+X, +Y, -Z, +S) is det
Z is the union of X and Y.
 zdd_cons(+X, +Y, -Z, +S) is det
Short hand for cofact(Z, t(X, 0, Y), S). Having analogy Z = [X|Y] in mind.
 zdd_meet(+X, +Y, -Z, +G) is det
Z is the intersection of X and Y.
 zdd_subtr(+X, +Y, -Z, +G) is det
Z is the subtraction of Y from X: Z = Y \ Z.
 zdd_subtr_1(+X, -Y, +G) is det
Y is the subtraction of 1 (the set {{}}) from X: Y = X \ {{}}.
 zdd_xor(+X, +Y, -Z, +G) is det
Z is the exclusive-or of family X and Y.
 zdd_merge(X, Y, Z, G) is det
Z is the merge of X and Y, that is, Z = { U | U is the union of A in X and B in Y}.
Remark. The merge is associative and commutative, but not idempotent.
 zdd_subfamily(+X, +Y, +S) is det
True if a ZDD X is a subfamily of a ZDD Y.
 zdd_divmod(X, Y, D, M, S) is det
D = { A-B | A in X, B is Y, B is a subset of A }. M = { A in X | forall B in Y B is not a subset of A }. ?- zdd X<< +[*[a,b], [c]], Y<< +[b], zdd_divmod(X, Y, D, M, S), psa(X, S), psa(D, S), psa(M, S).
 zdd_div_div(X, Y, D, D0, S) is det
D is the set of elements in X divisible by an element of Y, D0 is the set A-B (= A//B) s.t. A in X, B in Y and B is subset of A.
 zdd_div(+X, +Y, -Z, +S) is det
Z is the quotient of X divided by Y; Z = { A - B | A in X, B in Y, B is a subset of A }
 zdd_mod(+X, +Y, -Z, +S) is det
Z = { A in X | forall B in Y B is not a subset of A }.
 zdd_mod_by_list(+X, +Y, -Z, +S) is det
Equivalent to zdd_list(Y, U, Z), zdd_mod_by_list(X, U, Z, S).
 zdd_div_by_list(+X, +Y, -Z, +S) is det
Eqivalent to zdd_sets(U, [X], Z, S), zdd_div(Y, U, Z, S).
 zdd_divisible_by_list(X, Y, Z, S) is det
Equivalent to zdd_sets(U, [X], S), zdd_divisible(Y, U, Z, S).
 map_zdd(+F, +X, -Y, +G) is det
Y is the set of all F_S with S running in X, where f_S = { F(a) | a in S}.

map_zdd(F, X, Y) works roughly like maplist(maplist(F), X, Y)) with a list X of lists.

 psa(+X, +S) is det
print all sets of X ?- zdd X<<pow([a]), psa(X). ?- zdd X<<{[a]}, psa(X).
 mp(+M, +X, +S) is det
print all sets of X with message M.
 zdd_list(?X, ?Y, +S) is det
Two way converter between zdd and list. Y is the list of zdd X.
 sets(+X, -Y, +S)
Y is the list in 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))). @ [a,c,e,f] @ X = 8.

 zdd_ord_power(+L, +X, -Y, +S) is det
Y is the merge of powerset of L and X. ?- zdd zdd_ord_power([a,b], 1, X), psa(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_singleton(+X, -P, +G) is det
Unify P with a sigleton ZDD for X.
 zdd_has_1(+X, +G) is det
true if X has 1 (the empty set). ?- zdd0((X<<pow([a,b,c]), zdd_subtr(1, X, Y), card(Y, 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.
 zdd_append(+X, +Y, -Z, +G) is det
Z is result of inserting all elements of X into Y. Y is assumed to have no atom in X.
 card(+I, -C, +S) is det
unify C with the cardinality of a family I of sets.
 max_length(+X, -Max, +S) is det
Unify Max with max of size of members of X.
 ltr_join(+X, +Y, -Z, +S) is det
Unify Z with a ZDD that represents the union of the ZDD X and Y as a family of sets (ltr_invert_free clauses) of literals.
 ltr_merge(+X, +Y, -Z, +S) is det
Z = { U | A in X, B in Y, U is the union of A and B, U is ltr_invert-free }.
 dnf(+X, -Y, +S) is det
Y is a disjuntive normal form of a boolean formula X.
 nnf_dnf(+E, -Z, +S) is det
Z is unified with a dnf for nnf (Negation Normal Form) E.
 cnf(+X, -Y, +S) is det
Y is unified with a conjuntive normal form of a boolean nnf X.
 card_filter_gte(+N, +X, -Y, +S) is det
Y = { A in X | #A >= N }, where #A is the number of elements of A.
 card_filter_lte(+N, +X, -Y, +S) is det
Y = { A in X | #A =< N }, where #A is the cardinality of A.
 card_filter_between(+I, +J, +X, -Y, +S) is det
Y = { A in X | I =< #A =< J }.
 bdd_list_raise(+L, +N, -X, +S) 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.
 bdd_interleave(+X, +Y, -Z, +S) is det
Z = { an interleave of A and B | A in X, B in Y }, where a list M is an interleave of a list A and and a list B if length(M) = length(A)+length(B), and both A and B are sublists of M. A list U is a sublist of a list V if U is a subsequence of V, provided that a list is viewed as a sequence.

Undocumented predicates

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

 Arg1 << Arg2
 fetch_state(Arg1)
 fetch_state(Arg1, Arg2)
 ltr_join_list(Arg1, Arg2, Arg3)
 ltr_join_list(Arg1, Arg2, Arg3, Arg4)
 ltr_card(Arg1, Arg2, Arg3)
 sat(Arg1)
 sat_count(Arg1)
 sat_count(Arg1, Arg2)
 set_at(Arg1, Arg2, Arg3)
 nnf_cnf(Arg1, Arg2, Arg3)
 s_map(Arg1, Arg2, Arg3)
 merge_funs(Arg1, Arg2, Arg3)
 bdd_list(Arg1, Arg2, Arg3)
 bdd_append(Arg1, Arg2, Arg3, Arg4)
 zdd(Arg1)
 zdd0(Arg1)
 zdd_insert(Arg1, Arg2, Arg3, Arg4, Arg5)
 zdd_insert_atoms(Arg1, Arg2, Arg3, Arg4)
 zdd_ord_insert(Arg1, Arg2, Arg3, Arg4)
 zdd_reorder(Arg1, Arg2, Arg3, Arg4)
 zdd_memberchk(Arg1, Arg2)
 zdd_join_1(Arg1, Arg2, Arg3)
 zdd_join_list(Arg1, Arg2, Arg3)
 zdd_join_list(Arg1, Arg2, Arg3, Arg4)
 zdd_merge_list(Arg1, Arg2, Arg3, Arg4)
 zdd_power(Arg1, Arg2, Arg3)
 zdd_rand_path(Arg1, Arg2, Arg3)
 zdd_rand_path(Arg1, Arg2, Arg3, Arg4)
 ltr_meet_filter(Arg1, Arg2, Arg3, Arg4)
 ltr_join_filter(Arg1, Arg2, Arg3, Arg4)
 get_extra(Arg1)
 get_extra(Arg1, Arg2)
 get_key(Arg1, Arg2, Arg3)
 atom_index(Arg1, Arg2)
 set_key(Arg1, Arg2, Arg3)
 update_key(Arg1, Arg2, Arg3, Arg4)
 bump_up(Arg1, Arg2, Arg3)
 set_pred(Arg1, Arg2)
 set_pred(Arg1, Arg2, Arg3)
 set_pred(Arg1, Arg2)
 set_pred(Arg1, Arg2, Arg3)
 zdd_compare(Arg1, Arg2, Arg3, Arg4)
 zdd_sort(Arg1, Arg2, Arg3)
 open_key(Arg1, Arg2, Arg3)
 close_key(Arg1, Arg2)
 set_compare(Arg1)
 set_compare(Arg1, Arg2)
 get_compare(Arg1, Arg2)
 use_zdd(Arg1)
 use_zdd(Arg1, Arg2)
 pred_zdd(Arg1, Arg2)
 pred_zdd(Arg1, Arg2, Arg3)
 zdd_sort_rev(Arg1, Arg2)
 zdd_sort_rev(Arg1, Arg2, Arg3)
 psa
 psa(Arg1, Arg2, Arg3)
 mp(Arg1, Arg2)
 ppoly(Arg1, Arg2)
 poly_term(Arg1, Arg2)
 poly_term(Arg1, Arg2, Arg3)
 eqns(Arg1, Arg2, Arg3)
 significant_length(Arg1, Arg2, Arg3)