omega_interface/convert.cc

   1 #include <algorithm>
   2 #include "omega_interface/convert.h"
   3
   4 static void max_index(Constraint_Handle c, varvector& vv, varvector& params)
   5 {
   6     for (Constr_Vars_Iter cvi(c); cvi; ++cvi) {
   7         Variable_ID var = (*cvi).var;
   8         if (find(vv.begin(), vv.end(), var) == vv.end() &&
   9             find(params.begin(), params.end(), var) == params.end())
  10                 vv.push_back(var);
  11     }
  12 }
  13
  14 static void set_constraint(Matrix *M, int row,
  15                            Constraint_Handle c, varvector& vv, int geq)
  16 {
  17     value_set_si(M->p[row][0], geq);
  18     for (int i = 0; i < vv.size(); ++i)
  19         value_set_si(M->p[row][1+i], c.get_coef(vv[i]));
  20     value_set_si(M->p[row][1+vv.size()], c.get_const());
  21 }
  22
  23 Polyhedron *relation2Domain(Relation& r, varvector& vv, varvector& params,
  24                                 unsigned MaxRays)
  25 {
  26     unsigned dim;
  27     unsigned max_size;
  28     Polyhedron *D = NULL;
  29     Polyhedron **next = &D;
  30
  31     r.simplify();
  32
  33     if (r.is_set())
  34         for (int j = 1; j <= r.n_set(); ++j)
  35             vv.push_back(r.set_var(j));
  36     else {
  37         for (int j = 1; j <= r.n_inp(); ++j)
  38             vv.push_back(r.input_var(j));
  39         for (int j = 1; j <= r.n_out(); ++j)
  40             vv.push_back(r.output_var(j));
  41     }
  42     dim = vv.size();
  43
  44     const Variable_ID_Tuple * globals = r.global_decls();
  45     for (int i = 0; i < globals->size(); ++i)
  46         params.push_back(r.get_local((*globals)[i+1]));
  47
  48     max_size = dim;
  49     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  50         vv.resize(dim);
  51         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  52             max_index((*ei), vv, params);
  53         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  54             max_index((*gi), vv, params);
  55         if (vv.size() > max_size)
  56             max_size = vv.size();
  57     }
  58
  59     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  60         int c = 0;
  61
  62         vv.resize(dim);
  63
  64         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei, ++c)
  65             max_index((*ei), vv, params);
  66         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi, ++c)
  67             max_index((*gi), vv, params);
  68         for (int i = 0; i < params.size(); ++i)
  69             vv.push_back(params[i]);
  70
  71         Matrix *M = Matrix_Alloc(c, vv.size() + 2);
  72         int row = 0;
  73         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  74             set_constraint(M, row++, (*ei), vv, 0);
  75         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  76             set_constraint(M, row++, (*gi), vv, 1);
  77         *next = Constraints2Polyhedron(M, MaxRays);
  78         Matrix_Free(M);
  79         next = &(*next)->next;
  80     }
  81     vv.resize(dim);
  82     return D;
  83 }
  84
  85 typedef std::vector<Global_Var_Decl *> globalvector;
  86
  87 static void create_globals(globalvector& globals, unsigned nparam,
  88                                 const char **params)
  89 {
  90     for (int i = 0; i < nparam; ++i)
  91         globals.push_back(new Global_Var_Decl(params[i]));
  92 }
  93
  94 Relation Polyhedron2relation(Polyhedron *P,
  95                           unsigned exist, globalvector& globals)
  96 {
  97     int nvar = P->Dimension - exist - globals.size();
  98     Relation r(nvar);
  99     varvector vars;
 100
 101     F_Exists *e = r.add_exists();
 102     F_And *base = e->add_and();
 103
 104     for (int j = 1; j <= r.n_set(); ++j)
 105         vars.push_back(r.set_var(j));
 106     for (int i = 0; i < exist; ++i)
 107         vars.push_back(e->declare());
 108     for (int i = 0; i < globals.size(); ++i)
 109         vars.push_back(r.get_local(globals[i]));
 110
 111     for (int i = 0; i < P->NbConstraints; ++i) {
 112         Constraint_Handle h;
 113         if (value_notzero_p(P->Constraint[i][0]))
 114             h = base->add_GEQ();
 115         else
 116             h = base->add_EQ();
 117         for (int j = 1; j <= P->Dimension; ++j)
 118             h.update_coef(vars[j-1], VALUE_TO_INT(P->Constraint[i][j]));
 119         h.update_const(VALUE_TO_INT(P->Constraint[i][1+P->Dimension]));
 120     }
 121     r.finalize();
 122     return r;
 123 }
 124
 125 Relation Polyhedron2relation(Polyhedron *P,
 126                           unsigned exist, unsigned nparam, const char **params)
 127 {
 128     globalvector globals;
 129     create_globals(globals, nparam, params);
 130     return Polyhedron2relation(P, exist, globals);
 131 }
 132
 133 Relation Domain2relation(Polyhedron *D, unsigned nvar, unsigned nparam,
 134                          const char **params)
 135 {
 136     globalvector globals;
 137     create_globals(globals, nparam, params);
 138
 139     Relation r = Polyhedron2relation(D, D->Dimension - nvar - nparam,
 140                                         globals);
 141     for (Polyhedron *P = D->next; P; P = P->next) {
 142         Relation s = Polyhedron2relation(P, P->Dimension - nvar - nparam,
 143                                             globals);
 144         r = Union(r, s);
 145     }
 146     return r;
 147 }