Collecting choices on family of sets, and bidirectional converter between CNF and DNF

General
1

Let {S1, ..., Sn} be a family of sets. A choice is a set {a1, ..., an} such that ai is in Si (1=< i =<n). By zdd_choices(F, C, S), C is unified with the set of all choices on a given family F of sets.
For example for a family F= {{a,b}, {c,d}}, C is unified with
{{a,c}, {a,d}, {b, c}, {b, d}}.

Note that if the empty set is a member of F, then C is empty, and that if F is empty, then C={{}}. This might be confusing or counter intuitive at first but it is logically sound reading, not convention. Further more, zdd_choices is applied to convert DNF to CNF and vice versa in bidirectional way, which is in zdd.pl in library(pac).

I had written several codes with similar purpose until I came finally to these predicates (zdd_choices and ltr_choices). Fortunately, they are short and fast as seen below and reproducible sample
queries.

`zdd_choices/3`, `ltr_choices/3` 
%!	zdd_choices(+X, -Y, +S) is det.
%   Y = { W | U in W iff all A in U some V in X such that A is in V }.

zdd_choices(0, 1, _):-!.
zdd_choices(1, 0, _):-!.
zdd_choices(X, Y, S):- memo(choices(X)-Y, S),
	(	nonvar(Y)->true
	;	cofact(X, t(A, L, R), S),
		zdd_choices(L, L0, S),
		zdd_choices(R, R0, S),
		cofact(R1, t(A, R0, 1), S),
		zdd_merge(L0, R1, Y, S)
	).

%!	ltr_choices(+InNF,  -OutNF, +S) is det.
% 	OutNF is unified with a set of clauses
%	which is logically equivlalent to OutNF.
%	If InNF is read as DNF, then OutNF must be read
%	as CNF,  an if InNF is read as CNF, then OutNF
%	must be read as DNF.
%
%	REMARK: DNF 0 means false.  DNF 1 means true
%			CNF 0 means true.	CNF 1 means false
%	which is logically sound reading.
%	REMARK: ltr_choices reflects a well-known duality law
%   on disjunction and conjunction.

ltr_choices(0, 1, _):-!.
ltr_choices(1, 0, _):-!.
ltr_choices(X, Y, S):- memo(ltr_choices(X)-Y, S),
	(	nonvar(Y)->true	%, write(.)  % many hits.
	;	cofact(X, t(A, L, R), S),
		ltr_choices(L, L0, S),
		ltr_choices(R, R0, S),
		cofact(R1, t(A, R0, 1), S),
		ltr_merge(L0, R1, Y, S)
	).
Reproducible queries on library(pac) version 1.8.6 
% swipl
?- pack_install(pac). % version 1.8.6
?- use_module(library(pac)).
?- use_module(zdd(zdd)).
?- module(zmod).

zmod:  ?- N=10, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), zdd_choices(Y, Z), card(Y, C), card(Z, D))).
% 9,279 inferences, 0.001 CPU in 0.001 seconds (97% CPU, 14751987 Lips)
N = 10,
Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
X = 11,
Y = 21,
Z = 75,
C = 1023,
D = 1.

mod:  ?- N=1000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), zdd_subtr(X, 1, Y), zdd_choices(Y, Z), card(Y, C), card(Z, D))), C=:= 2^1000-1.
% 59,511,156 inferences, 6.150 CPU in 6.299 seconds (98% CPU, 9675918 Lips)
N = 1000,
Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
X = 1001,
Y = 2001,
Z = 502500,
C = 10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069375,
D = 1.