1 #include <barvinok/util.h>
2 #include "omega/convert.h"
4 #define MAXRAYS POL_NO_DUAL
6 static void max_index(Constraint_Handle c
, varvector
& vv
, varvector
& params
)
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())
16 static void set_constraint(Matrix
*M
, int row
,
17 Constraint_Handle c
, varvector
& vv
, int geq
)
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());
25 Polyhedron
*relation2Domain(Relation
& r
, varvector
& vv
, varvector
& params
)
32 for (int j
= 1; j
<= r
.n_set(); ++j
)
33 vv
.push_back(r
.set_var(j
));
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
));
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]));
45 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
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
]);
54 Matrix
*M
= Matrix_Alloc(c
, vv
.size() + 2);
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
);
62 D
= DomainConcat(P
, D
);
67 Relation
Polyhedron2relation(Polyhedron
*P
,
68 unsigned exist
, unsigned nparam
, char **params
)
70 int nvar
= P
->Dimension
- exist
- nparam
;
74 F_Exists
*e
= r
.add_exists();
75 F_And
*base
= e
->add_and();
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
])));
84 for (int i
= 0; i
< P
->NbConstraints
; ++i
) {
86 if (value_notzero_p(P
->Constraint
[i
][0]))
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
]));