Fixing a small gap in preprocessing for ZDD based propositional refutation

Nice to know
1

EDIT: 2022-9-27
I have updated the package pac to pac-1.6.7 as it is. I think ZDD library is almost final as I planned when I started to develop, though it is still a toy. Now I will play it around with the library from time to time for problems which I am interested in.

During this work, I am getting interested in Knuth’s frontier
based computation, though still I have only partial information from some article by Minato’s group on ZDD. IMO, frontier based computation should be interesting for Prolog programing. I was surprised often to find that the standard “divide and conqure”, “recursive call”, etc with which we are familiar could not be applied well to massive computation which ZDD is aimed at. In fact I really experinced that Knuth’s insight is to the point. Now it is time for me to think again how to introduce ZDD with frontier based computation so as to fit it to the Prolog programming. If you feel sharing the same interest with me, write to me.
EDIT end

I am pleased to share with my small idea of completion to fill a gap for ZDD based provers of mine. The gap was related to preprocessing given formulae into C(onjunctive)N(ormal)F(form) in ZDD, which must be complementary free. This is not good for e.g. a\land \neg a,
though details is omitted here. To fix this gap, I apply the recent posted counting method for solutions of D(isjuntive)NF,
assuming that formula which gets to the empty CNF is almost trivial, though I am not sure this assumption is justified.
I would like to upload this codes as in pack pac 1.6.7 after
polishing many other small revision scattered in the package.

New codes for hybrid of refutation and counting solutions:

prove(X):- prove(X, [time_limit(60)]).
%
prove(X, Opts):-
	(	memberchk(time_limit(Limit), Opts) -> true
	;	Limit = 60
	),
	open_state(S),
	set_compare(ltr_compare, S),
	(	call_with_time_limit(Limit, prove_boole(X, S))
	->	writeln('VALID')
	;	writeln('INVALID')
	),
	close_state(S).
%
prove_boole(X, S):- cnf(-X, CNF, S),
	card(CNF, C, S),
	!,
	format("CNF has ~w clauses.\n", [C]),
	(	C > 0	->  resolve(CNF, S)
	;	dnf(X, DNF, S),
		ltr_card(DNF, Count, N, S),
		Count is 1<< N
	).

Valid formula samples:

valid_formula( (a * b) + (a * -b) + (-a * b) + (-a * -b)).
valid_formula((-(-a) -> a) * (a -> -(-a))).		% Double Negation
valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morgan’s Law
valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b).
valid_formula(a + -a).
valid_formula(((a -> b) -> a) -> a).  % Peirce’s Law
valid_formula(-(-a)->a).
valid_formula(a -> a).
valid_formula(a -> (b -> a)).
valid_formula((a->b)->((b->c)->(a->c))).
valid_formula(a->((a->b)->b)).
valid_formula((a*(a->b))->b).
valid_formula((a->b)->(-b -> -a)).
valid_formula((a->b)->((b->c)->(a->c))).
valid_formula((((((((p3<=> p2) <=> p1) <=> p0) <=> p3) <=> p2) <=> p1) <=> p0)).

Invalid formula samples

% ?- forall(invalid_formula(A), prove(A)).
invalid_formula(a).
invalid_formula((a->b)->a).
invalid_formula((a->b)->(b->a)).
invalid_formula(a -> (b -> c)).
invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)).
invalid_formula( -((-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f))).