omega/convert.cc

   1 #include <barvinok/util.h>
   2 #include "omega/convert.h"
   3 #include "config.h"
   4
   5 #ifdef HAVE_GROWING_CHERNIKOVA
   6 #define MAXRAYS    POL_NO_DUAL
   7 #else
   8 #define MAXRAYS  600
   9 #endif
  10
  11 static void max_index(Constraint_Handle c, varvector& vv, varvector& params)
  12 {
  13     for (Constr_Vars_Iter cvi(c); cvi; ++cvi) {
  14         Variable_ID var = (*cvi).var;
  15         if (find(vv.begin(), vv.end(), var) == vv.end() &&
  16             find(params.begin(), params.end(), var) == params.end())
  17                 vv.push_back(var);
  18     }
  19 }
  20
  21 static void set_constraint(Matrix *M, int row,
  22                            Constraint_Handle c, varvector& vv, int geq)
  23 {
  24     value_set_si(M->p[row][0], geq);
  25     for (int i = 0; i < vv.size(); ++i)
  26         value_set_si(M->p[row][1+i], c.get_coef(vv[i]));
  27     value_set_si(M->p[row][1+vv.size()], c.get_const());
  28 }
  29
  30 Polyhedron *relation2Domain(Relation& r, varvector& vv, varvector& params)
  31 {
  32     Polyhedron *D = NULL;
  33
  34     r.simplify();
  35
  36     if (r.is_set())
  37         for (int j = 1; j <= r.n_set(); ++j)
  38             vv.push_back(r.set_var(j));
  39     else {
  40         for (int j = 1; j <= r.n_inp(); ++j)
  41             vv.push_back(r.input_var(j));
  42         for (int j = 1; j <= r.n_out(); ++j)
  43             vv.push_back(r.output_var(j));
  44     }
  45
  46     const Variable_ID_Tuple * globals = r.global_decls();
  47     for (int i = 0; i < globals->size(); ++i)
  48         params.push_back(r.get_local((*globals)[i+1]));
  49
  50     for (DNF_Iterator di(r.query_DNF()); di; ++di) {
  51         int c = 0;
  52         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei, ++c)
  53             max_index((*ei), vv, params);
  54         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi, ++c)
  55             max_index((*gi), vv, params);
  56         for (int i = 0; i < params.size(); ++i)
  57             vv.push_back(params[i]);
  58
  59         Matrix *M = Matrix_Alloc(c, vv.size() + 2);
  60         int row = 0;
  61         for (EQ_Iterator ei = (*di)->EQs(); ei; ++ei)
  62             set_constraint(M, row++, (*ei), vv, 0);
  63         for (GEQ_Iterator gi = (*di)->GEQs(); gi; ++gi)
  64             set_constraint(M, row++, (*gi), vv, 1);
  65         Polyhedron *P = Constraints2Polyhedron(M, MAXRAYS);
  66         Matrix_Free(M);
  67         D = DomainConcat(P, D);
  68     }
  69     return D;
  70 }
  71
  72 Relation Polyhedron2relation(Polyhedron *P,
  73                           unsigned exist, unsigned nparam, char **params)
  74 {
  75     int nvar = P->Dimension - exist - nparam;
  76     Relation r(nvar);
  77     varvector vars;
  78
  79     F_Exists *e = r.add_exists();
  80     F_And *base = e->add_and();
  81
  82     for (int j = 1; j <= r.n_set(); ++j)
  83         vars.push_back(r.set_var(j));
  84     for (int i = 0; i < exist; ++i)
  85         vars.push_back(e->declare());
  86     for (int i = 0; i < nparam; ++i)
  87         vars.push_back(r.get_local(new Global_Var_Decl(params[i])));
  88
  89     for (int i = 0; i < P->NbConstraints; ++i) {
  90         Constraint_Handle h;
  91         if (value_notzero_p(P->Constraint[i][0]))
  92             h = base->add_GEQ();
  93         else
  94             h = base->add_EQ();
  95         for (int j = 1; j <= P->Dimension; ++j)
  96             h.update_coef(vars[j-1], VALUE_TO_INT(P->Constraint[i][j]));
  97         h.update_const(VALUE_TO_INT(P->Constraint[i][1+P->Dimension]));
  98     }
  99     r.finalize();
 100     return r;
 101 }