4 #include "count_solutions.h"
6 typedef std::vector
<Variable_ID
> varvector
;
8 static void max_index(Constraint_Handle c
, varvector
& vv
)
10 for (Constr_Vars_Iter
cvi(c
); cvi
; ++cvi
) {
11 Variable_ID var
= (*cvi
).var
;
12 if (find(vv
.begin(), vv
.end(), var
) == vv
.end())
17 double count_solutions(Relation
& r
)
26 for (int j
= 1; j
<= r
.n_set(); ++j
)
27 vv
.push_back(r
.set_var(j
));
29 dim
= r
.n_inp() + r
.n_out();
30 for (int j
= 1; j
<= r
.n_inp(); ++j
)
31 vv
.push_back(r
.input_var(j
));
32 for (int j
= 1; j
<= r
.n_out(); ++j
)
33 vv
.push_back(r
.output_var(j
));
36 int *coeffs
= new int[vv
.size()];
37 int *indices
= new int[vv
.size()];
40 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
43 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
)
45 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
)
48 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
) {
50 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
51 if ((*ei
).get_coef(vv
[i
]) != 0) {
52 coeffs
[j
] = (*ei
).get_coef(vv
[i
]);
56 DFA
*e
= build_DFA_eq(j
, coeffs
, (*ei
).get_const(), indices
);
61 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
66 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
) {
68 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
69 if ((*gi
).get_coef(vv
[i
]) != 0) {
70 coeffs
[j
] = -(*gi
).get_coef(vv
[i
]);
74 DFA
* e
= build_DFA_ineq(j
, coeffs
, -(*gi
).get_const()-1, indices
);
79 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
89 dfa
= dfaMinimize(dfaProduct(dfa
, c
, dfaOR
));
96 for (int i
= dim
; i
< vv
.size(); ++i
) {
98 dfa
= dfaMinimize(dfaProject(dfa
, i
));
102 double c
= count_accepting_paths(dfa
, dfa
->ns
, dim
);