1 #include "omega/convert.h"
3 static void max_index(Constraint_Handle c
, varvector
& vv
, varvector
& params
)
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())
13 static void set_constraint(Matrix
*M
, int row
,
14 Constraint_Handle c
, varvector
& vv
, int geq
)
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());
22 Polyhedron
*relation2Domain(Relation
& r
, varvector
& vv
, varvector
& params
,
28 Polyhedron
**next
= &D
;
33 for (int j
= 1; j
<= r
.n_set(); ++j
)
34 vv
.push_back(r
.set_var(j
));
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
));
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]));
48 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
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
)
58 for (DNF_Iterator
di(r
.query_DNF()); di
; ++di
) {
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
]);
70 Matrix
*M
= Matrix_Alloc(c
, vv
.size() + 2);
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
);
78 next
= &(*next
)->next
;
84 typedef std::vector
<Global_Var_Decl
*> globalvector
;
86 static void create_globals(globalvector
& globals
, unsigned nparam
,
89 for (int i
= 0; i
< nparam
; ++i
)
90 globals
.push_back(new Global_Var_Decl(params
[i
]));
93 Relation
Polyhedron2relation(Polyhedron
*P
,
94 unsigned exist
, globalvector
& globals
)
96 int nvar
= P
->Dimension
- exist
- globals
.size();
100 F_Exists
*e
= r
.add_exists();
101 F_And
*base
= e
->add_and();
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
]));
110 for (int i
= 0; i
< P
->NbConstraints
; ++i
) {
112 if (value_notzero_p(P
->Constraint
[i
][0]))
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
]));
124 Relation
Polyhedron2relation(Polyhedron
*P
,
125 unsigned exist
, unsigned nparam
, char **params
)
127 globalvector globals
;
128 create_globals(globals
, nparam
, params
);
129 return Polyhedron2relation(P
, exist
, globals
);
132 Relation
Domain2relation(Polyhedron
*D
, unsigned nvar
, unsigned nparam
,
135 globalvector globals
;
136 create_globals(globals
, nparam
, params
);
138 Relation r
= Polyhedron2relation(D
, D
->Dimension
- nvar
- nparam
,
140 for (Polyhedron
*P
= D
->next
; P
; P
= P
->next
) {
141 Relation s
= Polyhedron2relation(P
, P
->Dimension
- nvar
- nparam
,
148 void dump(Relation
& r
)
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();
157 fprintf(stderr
, "Unions not supported\n");
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");
168 barvinok_options_free(options
);