1:- module(count_zdd, [ count_all/0, eval_count_one/1 ]). 2
3:- use_module(zdd(zdd)). 4
5count_all:- forall(zdd_term(E), (zmod:zdd, once(count_one(E)))).
7count_one(E):-
8 call_with_time_limit(10, (X<< E, card(X, C))),
9 writeln(#(E)=C).
10
11eval_count_one(E):- zmod:zdd, count_one(E).
12
14zdd_term( a ).
15zdd_term( (a+b)*(a+c)).
16zdd_term( (a+b)*(c+d)).
17zdd_term( a*b*c*a*b).
18zdd_term( a*b + c).
19zdd_term( (a+b)-(c+d)).
20zdd_term( (a+b)/a).
21zdd_term( (a+b)//a).
22zdd_term( (a*c+b)//a).
23zdd_term( *(numlist(1, 5))).
24zdd_term( *([1,2,3])).
25zdd_term( +[0, 1, 2]* (+[0, 1, 2])).
26zdd_term( +[1,b,1,1] * (+[1,a])).
27zdd_term( +[1,2,3,4]).
28zdd_term( +(numlist(1,100)) * +(numlist(1,100))).
29zdd_term( (a+b)*(a+c) +(a*b)).
30zdd_term( pow([a,b])-(c+d)).
31zdd_term( pow([a,b])//(a+b)).
32zdd_term( pow([a,b])/(a+b)).
33zdd_term( pow(charlist(a, c))).
34zdd_term( pow(append([1,2],[a, b]))).
35zdd_term( pow(subtract([1,2,3], [1,2,a]))).
36zdd_term( +(atomlist($a(1,10)))).
37zdd_term( pow(atomlist($a(1,10))))