parker/count_solutions.cc

   1 #include <vector>
   2 #include <omega.h>
   3
   4 #include "count_solutions.h"
   5
   6 typedef std::vector<Variable_ID> varvector;
   7
   8 static void max_index(Constraint_Handle c, varvector& vv)
   9 {
  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())
  13             vv.push_back(var);
  14     }
  15 }
  16
  17 double count_solutions(Relation& r)
  18 {
  19     int dim;
  20
  21     r.simplify();
  22
  23     varvector vv;
  24     if (r.is_set()) {
  25         dim = r.n_set();
  26         for (int j = 1; j <= r.n_set(); ++j)
  27             vv.push_back(r.set_var(j));
  28     } else {
  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));
  34     }
  35
  36     int *coeffs = new int[vv.size()];
  37     int *indices = new int[vv.size()];
  38     DFA* dfa = NULL;
  39
  40     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  41         DFA* c = NULL;
  42
  43         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  44             max_index((*ei), vv);
  45         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  46             max_index((*gi), vv);
  47
  48         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei) {
  49             int i, j;
  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]);
  53                     indices[j++] = i;
  54                 }
  55             }
  56             DFA *e = build_DFA_eq(j, coeffs, (*ei).get_const(), indices);
  57             if (!c)
  58                 c = e;
  59             else {
  60                 DFA *t = c;
  61                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
  62                 dfaFree(t);
  63                 dfaFree(e);
  64             }
  65         }
  66         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi) {
  67             int i, j;
  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]);
  71                     indices[j++] = i;
  72                 }
  73             }
  74             DFA* e = build_DFA_ineq(j, coeffs, -(*gi).get_const()-1, indices);
  75             if (!c)
  76                 c = e;
  77             else {
  78                 DFA *t = c;
  79                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
  80                 dfaFree(t);
  81                 dfaFree(e);
  82             }
  83         }
  84
  85         if (!dfa)
  86             dfa = c;
  87         else {
  88             DFA *t = dfa;
  89             dfa = dfaMinimize(dfaProduct(dfa, c, dfaOR));
  90             dfaFree(t);
  91             dfaFree(c);
  92         }
  93     }
  94
  95     assert(dfa);
  96     for (int i = dim; i < vv.size(); ++i) {
  97         DFA *t = dfa;
  98         dfa = dfaMinimize(dfaProject(dfa, i));
  99         dfaFree(t);
 100     }
 101
 102     double c = count_accepting_paths(dfa, dfa->ns, dim);
 103     dfaFree(dfa);
 104
 105     delete [] coeffs;
 106     delete [] indices;
 107
 108     return c;
 109 }