omega/convert.cc

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