barvinok 0.41.7
[barvinok.git] / parker / count_solutions.cc
blob2e065443c5a68551ee301fd368766a784a1170f2
1 #include <algorithm>
2 #include <vector>
3 #include <omega.h>
5 extern "C" {
6 /* Erin Parker (parker@cs.unc.edu), March 2004 */
8 #include "dfa.h"
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())
27 vv.push_back(var);
31 double count_solutions(Relation& r)
33 int dim;
34 int max_size;
36 r.simplify();
38 varvector vv;
39 if (r.is_set()) {
40 dim = r.n_set();
41 for (int j = 1; j <= r.n_set(); ++j)
42 vv.push_back(r.set_var(j));
43 } else {
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));
51 max_size = dim;
52 for (DNF_Iterator di(r.query_DNF()); di; ++di) {
53 vv.resize(dim);
54 for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
55 max_index((*ei), vv);
56 for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
57 max_index((*gi), vv);
58 if (vv.size() > max_size)
59 max_size = vv.size();
62 int *coeffs = new int[max_size];
63 int *indices = new int[max_size];
64 DFA* dfa = NULL;
66 for (DNF_Iterator di(r.query_DNF()); di; ++di) {
67 DFA* c = NULL;
69 vv.resize(dim);
71 for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
72 max_index((*ei), vv);
73 for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
74 max_index((*gi), vv);
76 for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei) {
77 int i, j;
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]);
81 indices[j++] = i;
84 DFA *e = build_DFA_eq(j, coeffs, (*ei).get_const(), indices);
85 if (!c)
86 c = e;
87 else {
88 DFA *t = c;
89 c = dfaMinimize(dfaProduct(c, e, dfaAND));
90 dfaFree(t);
91 dfaFree(e);
94 for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi) {
95 int i, j;
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]);
99 indices[j++] = i;
102 DFA* e = build_DFA_ineq(j, coeffs, -(*gi).get_const()-1, indices);
103 if (!c)
104 c = e;
105 else {
106 DFA *t = c;
107 c = dfaMinimize(dfaProduct(c, e, dfaAND));
108 dfaFree(t);
109 dfaFree(e);
113 assert(c);
114 for (int i = dim; i < vv.size(); ++i) {
115 DFA *t = c;
116 c = dfaMinimize(dfaProject(c, i));
117 dfaFree(t);
120 if (!dfa)
121 dfa = c;
122 else {
123 DFA *t = dfa;
124 dfa = dfaMinimize(dfaProduct(dfa, c, dfaOR));
125 dfaFree(t);
126 dfaFree(c);
130 double c = count_accepting_paths(dfa, dfa->ns, dim);
131 dfaFree(dfa);
133 delete [] coeffs;
134 delete [] indices;
136 return c;