parker/count_solutions.cc

   1 #include <algorithm>
   2 #include <vector>
   3 #include <omega.h>
   4
   5 extern "C" {
   6 /* Erin Parker (parker@cs.unc.edu), March 2004 */
   7
   8 #include "dfa.h"
   9
  10 /* Functions defined in construction.c */
  11 DFA* build_DFA_eq(int, int*, int, int*);
  12 DFA* build_DFA_ineq(int, int*, int, int*);
  13
  14 /* Function defined in count.c */
  15 double count_accepting_paths(DFA*, int, int);
  16 }
  17
  18 #include "count_solutions.h"
  19
  20 typedef std::vector<Variable_ID> varvector;
  21
  22 static void max_index(Constraint_Handle c, varvector& vv)
  23 {
  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);
  28     }
  29 }
  30
  31 double count_solutions(Relation& r)
  32 {
  33     int dim;
  34     int max_size;
  35
  36     r.simplify();
  37
  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));
  49     }
  50
  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();
  60     }
  61
  62     int *coeffs = new int[max_size];
  63     int *indices = new int[max_size];
  64     DFA* dfa = NULL;
  65
  66     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  67         DFA* c = NULL;
  68
  69         vv.resize(dim);
  70
  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);
  75
  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;
  82                 }
  83             }
  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);
  92             }
  93         }
  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;
 100                 }
 101             }
 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);
 110             }
 111         }
 112
 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);
 118         }
 119
 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);
 127         }
 128     }
 129
 130     double c = count_accepting_paths(dfa, dfa->ns, dim);
 131     dfaFree(dfa);
 132
 133     delete [] coeffs;
 134     delete [] indices;
 135
 136     return c;
 137 }