Revising my old codes on ZDD

General
12

Sorry again. I remember that dnf( disjunctive normal form) must be cnf(conjunctive normal form) in refutation procedure.

Correction.

% ?- spy(ltr_refute), zdd((X<<cnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))),
%	psa(X), ltr_refute(X))).
%@ [-a,c]
%@ [-a,-b]
%@ [a,-c]
%@ [a,b]
%@  * Call: (18) zdd:ltr_refute(16) ? no debug
%@ X = 16.

ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(false, _):-!.
ltr_refute(X, S) :- integer(X),
	cofact(X, if(A, L, R), S),
	(	R == true -> true
	;	R == false -> Y = L
	;	cofact(R, if(B, L0, R0), S),
		(	B == -(A)
		->  cnf_merge(L, L0, L1, S),
			cnf_join(R, R0, R1, S),
			cnf_join(L1, R1, Y, S)
		;	cnf_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).

Kuniaki Mukai