divide_at(+A, +L, -H, -T) is det

A : ZDD atom. L : sorted list. H,T are unified with lists such that append of reverse(H), [A], and T equals to the given L.

 gf2_solve_zero(+Vs, +X, -P, +S) is det

P is unified with the set of assignments which makes X = 0.

 gf2_poly(+E, -V, +S) is det

E: polynomial over GF2. V is unified with E that is read as a ZDD. GF2 rules applied: e.g. a + a = 0. a*(b+c)=a*b+a*c.

 gf2_insert(+X, +Y, -Z, +S) is det

Insert a literal X into each set of literals in a ZDD Y, and unify Z with the result. For short, Z = X*Y.

 gf2_join(+X, +Y, -Z, +S) is det

X, Y: zdd of GF(2)-polyminals. Z is unified with GF(2)-polynomial addition X + Y.

 gf2_merge(+X, +Y, -Z, +S) is det

X, Y: GF(2)-polyniomials in zdd. Z is unified with GF(2)-polyniomial addition X * Y. Z = X*Y.

Undocumented predicates

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

 gf2_poly_list(Arg1, Arg2, Arg3, Arg4, Arg5)

 gf2_poly_card(Arg1, Arg2, Arg3)

 gf2_card(Arg1, Arg2, Arg3, Arg4)

 gf2_poly_solve(Arg1, Arg2, Arg3)

 gf2_poly_solve_list(Arg1, Arg2, Arg3)

 gf2_solve(Arg1, Arg2, Arg3, Arg4)

 gf2_join_list(Arg1, Arg2, Arg3, Arg4)

 gf2_merge_list(Arg1, Arg2, Arg3, Arg4)

 gf2_subst(Arg1, Arg2, Arg3, Arg4, Arg5)

 collect_atoms(Arg1, Arg2)

 collect_atoms_list(Arg1, Arg2)