1 #include <barvinok/util.h>
2 #include "omega/convert.h"
5 #ifdef HAVE_GROWING_CHERNIKOVA
6 #define MAXRAYS POL_NO_DUAL
11 static void max_index(Constraint_Handle c
, varvector
& vv
, varvector
& params
)
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())
21 static void set_constraint(Matrix
*M
, int row
,
22 Constraint_Handle c
, varvector
& vv
, int geq
)
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());
30 Polyhedron
*relation2Domain(Relation
& r
, varvector
& vv
, varvector
& params
)
37 for (int j
= 1; j
<= r
.n_set(); ++j
)
38 vv
.push_back(r
.set_var(j
));
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
));
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]));
50 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
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
]);
59 Matrix
*M
= Matrix_Alloc(c
, vv
.size() + 2);
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
);
67 D
= DomainConcat(P
, D
);
72 Relation
Polyhedron2relation(Polyhedron
*P
,
73 unsigned exist
, unsigned nparam
, char **params
)
75 int nvar
= P
->Dimension
- exist
- nparam
;
79 F_Exists
*e
= r
.add_exists();
80 F_And
*base
= e
->add_and();
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
])));
89 for (int i
= 0; i
< P
->NbConstraints
; ++i
) {
91 if (value_notzero_p(P
->Constraint
[i
][0]))
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
]));