omega/convert.cc

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