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     int max_size;
  21
  22     r.simplify();
  23
  24     varvector vv;
  25     if (r.is_set()) {
  26         dim = r.n_set();
  27         for (int j = 1; j <= r.n_set(); ++j)
  28             vv.push_back(r.set_var(j));
  29     } else {
  30         dim = r.n_inp() + r.n_out();
  31         for (int j = 1; j <= r.n_inp(); ++j)
  32             vv.push_back(r.input_var(j));
  33         for (int j = 1; j <= r.n_out(); ++j)
  34             vv.push_back(r.output_var(j));
  35     }
  36
  37     max_size = dim;
  38     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  39         vv.resize(dim);
  40         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  41             max_index((*ei), vv);
  42         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  43             max_index((*gi), vv);
  44         if (vv.size() > max_size)
  45             max_size = vv.size();
  46     }
  47
  48     int *coeffs = new int[max_size];
  49     int *indices = new int[max_size];
  50     DFA* dfa = NULL;
  51
  52     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  53         DFA* c = NULL;
  54
  55         vv.resize(dim);
  56
  57         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  58             max_index((*ei), vv);
  59         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  60             max_index((*gi), vv);
  61
  62         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei) {
  63             int i, j;
  64             for (i = 0, j = 0; i < vv.size(); ++i) {
  65                 if ((*ei).get_coef(vv[i]) != 0) {
  66                     coeffs[j] = (*ei).get_coef(vv[i]);
  67                     indices[j++] = i;
  68                 }
  69             }
  70             DFA *e = build_DFA_eq(j, coeffs, (*ei).get_const(), indices);
  71             if (!c)
  72                 c = e;
  73             else {
  74                 DFA *t = c;
  75                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
  76                 dfaFree(t);
  77                 dfaFree(e);
  78             }
  79         }
  80         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi) {
  81             int i, j;
  82             for (i = 0, j = 0; i < vv.size(); ++i) {
  83                 if ((*gi).get_coef(vv[i]) != 0) {
  84                     coeffs[j] = -(*gi).get_coef(vv[i]);
  85                     indices[j++] = i;
  86                 }
  87             }
  88             DFA* e = build_DFA_ineq(j, coeffs, -(*gi).get_const()-1, indices);
  89             if (!c)
  90                 c = e;
  91             else {
  92                 DFA *t = c;
  93                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
  94                 dfaFree(t);
  95                 dfaFree(e);
  96             }
  97         }
  98
  99         assert(c);
 100         for (int i = dim; i < vv.size(); ++i) {
 101             DFA *t = c;
 102             c = dfaMinimize(dfaProject(c, i));
 103             dfaFree(t);
 104         }
 105
 106         if (!dfa)
 107             dfa = c;
 108         else {
 109             DFA *t = dfa;
 110             dfa = dfaMinimize(dfaProduct(dfa, c, dfaOR));
 111             dfaFree(t);
 112             dfaFree(c);
 113         }
 114     }
 115
 116     double c = count_accepting_paths(dfa, dfa->ns, dim);
 117     dfaFree(dfa);
 118
 119     delete [] coeffs;
 120     delete [] indices;
 121
 122     return c;
 123 }