5 /* Erin Parker (parker@cs.unc.edu), March 2004 */
9 /* Functions defined in construction.c */
10 DFA
* build_DFA_eq(int, int*, int, int*);
11 DFA
* build_DFA_ineq(int, int*, int, int*);
13 /* Function defined in count.c */
14 double count_accepting_paths(DFA
*, int, int);
17 #include "count_solutions.h"
19 typedef std::vector
<Variable_ID
> varvector
;
21 static void max_index(Constraint_Handle c
, varvector
& vv
)
23 for (Constr_Vars_Iter
cvi(c
); cvi
; ++cvi
) {
24 Variable_ID var
= (*cvi
).var
;
25 if (find(vv
.begin(), vv
.end(), var
) == vv
.end())
30 double count_solutions(Relation
& r
)
40 for (int j
= 1; j
<= r
.n_set(); ++j
)
41 vv
.push_back(r
.set_var(j
));
43 dim
= r
.n_inp() + r
.n_out();
44 for (int j
= 1; j
<= r
.n_inp(); ++j
)
45 vv
.push_back(r
.input_var(j
));
46 for (int j
= 1; j
<= r
.n_out(); ++j
)
47 vv
.push_back(r
.output_var(j
));
51 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
53 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
)
55 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
)
57 if (vv
.size() > max_size
)
61 int *coeffs
= new int[max_size
];
62 int *indices
= new int[max_size
];
65 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
70 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
)
72 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
)
75 for (EQ_Iterator ei
= (*di
)->EQs(); ei
; ++ei
) {
77 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
78 if ((*ei
).get_coef(vv
[i
]) != 0) {
79 coeffs
[j
] = (*ei
).get_coef(vv
[i
]);
83 DFA
*e
= build_DFA_eq(j
, coeffs
, (*ei
).get_const(), indices
);
88 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
93 for (GEQ_Iterator gi
= (*di
)->GEQs(); gi
; ++gi
) {
95 for (i
= 0, j
= 0; i
< vv
.size(); ++i
) {
96 if ((*gi
).get_coef(vv
[i
]) != 0) {
97 coeffs
[j
] = -(*gi
).get_coef(vv
[i
]);
101 DFA
* e
= build_DFA_ineq(j
, coeffs
, -(*gi
).get_const()-1, indices
);
106 c
= dfaMinimize(dfaProduct(c
, e
, dfaAND
));
113 for (int i
= dim
; i
< vv
.size(); ++i
) {
115 c
= dfaMinimize(dfaProject(c
, i
));
123 dfa
= dfaMinimize(dfaProduct(dfa
, c
, dfaOR
));
129 double c
= count_accepting_paths(dfa
, dfa
->ns
, dim
);