6 /* Erin Parker (parker@cs.unc.edu), March 2004 */
10 /* Functions defined in construction.c */
11 DFA
* build_DFA_eq(int, int*, int, int*);
12 DFA
* build_DFA_ineq(int, int*, int, int*);
14 /* Function defined in count.c */
15 double count_accepting_paths(DFA
*, int, int);
18 #include "count_solutions.h"
20 typedef std::vector
<Variable_ID
> varvector
;
22 static void max_index(Constraint_Handle c
, varvector
& vv
)
24 for (Constr_Vars_Iter
cvi(c
); cvi
; ++cvi
) {
25 Variable_ID var
= (*cvi
).var
;
26 if (find(vv
.begin(), vv
.end(), var
) == vv
.end())
31 double count_solutions(Relation
& r
)
41 for (int j
= 1; j
<= r
.n_set(); ++j
)
42 vv
.push_back(r
.set_var(j
));
44 dim
= r
.n_inp() + r
.n_out();
45 for (int j
= 1; j
<= r
.n_inp(); ++j
)
46 vv
.push_back(r
.input_var(j
));
47 for (int j
= 1; j
<= r
.n_out(); ++j
)
48 vv
.push_back(r
.output_var(j
));
52 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
54 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
)
56 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
)
58 if (vv
.size() > max_size
)
62 int *coeffs
= new int[max_size
];
63 int *indices
= new int[max_size
];
66 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
71 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
)
73 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
)
76 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
) {
78 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
79 if ((*ei
).get_coef(vv
[i
]) != 0) {
80 coeffs
[j
] = (*ei
).get_coef(vv
[i
]);
84 DFA
*e
= build_DFA_eq(j
, coeffs
, (*ei
).get_const(), indices
);
89 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
94 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
) {
96 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
97 if ((*gi
).get_coef(vv
[i
]) != 0) {
98 coeffs
[j
] = -(*gi
).get_coef(vv
[i
]);
102 DFA
* e
= build_DFA_ineq(j
, coeffs
, -(*gi
).get_const()-1, indices
);
107 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
114 for (int i
= dim
; i
< vv
.size(); ++i
) {
116 c
= dfaMinimize(dfaProject(c
, i
));
124 dfa
= dfaMinimize(dfaProduct(dfa
, c
, dfaOR
));
130 double c
= count_accepting_paths(dfa
, dfa
->ns
, dim
);