parker/count_solutions.cc

   1 #include <vector>
   2 #include <omega.h>
   3
   4 extern "C" {
   5 /* Erin Parker (parker@cs.unc.edu), March 2004 */
   6
   7 #include "dfa.h"
   8
   9 /* Functions defined in construction.c */
  10 DFA* build_DFA_eq(int, int*, int, int*);
  11 DFA* build_DFA_ineq(int, int*, int, int*);
  12
  13 /* Function defined in count.c */
  14 double count_accepting_paths(DFA*, int, int);
  15 }
  16
  17 #include "count_solutions.h"
  18
  19 typedef std::vector<Variable_ID> varvector;
  20
  21 static void max_index(Constraint_Handle c, varvector& vv)
  22 {
  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())
  26             vv.push_back(var);
  27     }
  28 }
  29
  30 double count_solutions(Relation& r)
  31 {
  32     int dim;
  33     int max_size;
  34
  35     r.simplify();
  36
  37     varvector vv;
  38     if (r.is_set()) {
  39         dim = r.n_set();
  40         for (int j = 1; j <= r.n_set(); ++j)
  41             vv.push_back(r.set_var(j));
  42     } else {
  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));
  48     }
  49
  50     max_size = dim;
  51     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  52         vv.resize(dim);
  53         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  54             max_index((*ei), vv);
  55         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  56             max_index((*gi), vv);
  57         if (vv.size() > max_size)
  58             max_size = vv.size();
  59     }
  60
  61     int *coeffs = new int[max_size];
  62     int *indices = new int[max_size];
  63     DFA* dfa = NULL;
  64
  65     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  66         DFA* c = NULL;
  67
  68         vv.resize(dim);
  69
  70         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  71             max_index((*ei), vv);
  72         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  73             max_index((*gi), vv);
  74
  75         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei) {
  76             int i, j;
  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]);
  80                     indices[j++] = i;
  81                 }
  82             }
  83             DFA *e = build_DFA_eq(j, coeffs, (*ei).get_const(), indices);
  84             if (!c)
  85                 c = e;
  86             else {
  87                 DFA *t = c;
  88                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
  89                 dfaFree(t);
  90                 dfaFree(e);
  91             }
  92         }
  93         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi) {
  94             int i, j;
  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]);
  98                     indices[j++] = i;
  99                 }
 100             }
 101             DFA* e = build_DFA_ineq(j, coeffs, -(*gi).get_const()-1, indices);
 102             if (!c)
 103                 c = e;
 104             else {
 105                 DFA *t = c;
 106                 c = dfaMinimize(dfaProduct(c, e, dfaAND));
 107                 dfaFree(t);
 108                 dfaFree(e);
 109             }
 110         }
 111
 112         assert(c);
 113         for (int i = dim; i < vv.size(); ++i) {
 114             DFA *t = c;
 115             c = dfaMinimize(dfaProject(c, i));
 116             dfaFree(t);
 117         }
 118
 119         if (!dfa)
 120             dfa = c;
 121         else {
 122             DFA *t = dfa;
 123             dfa = dfaMinimize(dfaProduct(dfa, c, dfaOR));
 124             dfaFree(t);
 125             dfaFree(c);
 126         }
 127     }
 128
 129     double c = count_accepting_paths(dfa, dfa->ns, dim);
 130     dfaFree(dfa);
 131
 132     delete [] coeffs;
 133     delete [] indices;
 134
 135     return c;
 136 }