A predicate to findall counter examples reinvented?

General
1

The codes findall_counter_examples below is to find all counter examples of a given propositional formula by using ZDD. As it is so simple codes that I am sure that I have reinvented due to my lacking relevant knowledge. Anyway, it has turned out to be handy but tough due to property of ZDD power. I appreciate much for relevant information.

% ?- findall_counter_examples(a, X, S), psa(X, S).
%@  zid = 3
%@ 	[-a]
%@ -------------------
%@ X = 3,
%@ S = .. .

% ?- findall_counter_examples(a->b, X, S), psa(X, S).
%@  zid = 14
%@ 	[a,-b]
%@ -------------------
%@ X = 14,
%@ S = .. .

% ?- findall_counter_examples((a->b)->(b->a), X, S), psa(X, S).
%@  zid = 14
%@ 	[-a,b]
%@ -------------------
%@ X = 14,
%@ S = .. .

ltr_open_state(S):- open_state(S), set_compare(ltr_compare, S).

findall_counter_examples(In, Out, S):-
	ltr_open_state(S),
	zdd_eval(dnf0(In), InZ, S),
	zdd_boole_atoms(InZ, Us, S),
	zdd_sort(Us, Vs, S),
	expand_prefix_dnf(Vs, 1, All, S),
	expand_dnf(Vs, InZ, Y, S),
	zdd_subtr(All, Y, Out, S).