1 #include <polylib/polylibgmp.h>
2 #include <stdio.h> /* needed for piplib ! */
3 #include <piplib/piplibMP.h>
8 #ifdef HAVE_GROWING_CHERNIKOVA
9 #define MAXRAYS POL_NO_DUAL
14 static PipMatrix
*poly2pip(Polyhedron
*P
, int pos
, int n
, int nparam
)
18 unsigned int extra
= P
->Dimension
- pos
- n
- nparam
;
20 matrix
= pip_matrix_alloc(P
->NbConstraints
, P
->Dimension
+2);
21 for (i
= 0; i
< P
->NbConstraints
; ++i
) {
22 value_assign(matrix
->p
[i
][0], P
->Constraint
[i
][0]);
23 for (j
= 0; j
< n
; ++j
)
24 value_assign(matrix
->p
[i
][1+j
], P
->Constraint
[i
][1+pos
+j
]);
25 for (j
= 0; j
< pos
; ++j
)
26 value_assign(matrix
->p
[i
][1+n
+j
], P
->Constraint
[i
][1+j
]);
27 for (j
= 0; j
< extra
; ++j
)
28 value_assign(matrix
->p
[i
][1+n
+pos
+j
], P
->Constraint
[i
][1+n
+pos
+j
]);
29 for (j
= 1+pos
+n
+extra
; j
< P
->Dimension
+2; ++j
)
30 value_assign(matrix
->p
[i
][j
], P
->Constraint
[i
][j
]);
36 static int max_new(PipQuast
*q
, int max
, int d
, int *maxd
)
40 for (p
= q
->newparm
; p
; p
= p
->next
)
46 max
= max_new(q
->next_else
, max
, d
, maxd
);
47 max
= max_new(q
->next_then
, max
, d
, maxd
);
53 * v: total number of variables in original problem
54 * pos: position of minimized variables
55 * n: dimension of space in which minimum was taken
56 * i.e., number of minimized vars in original problem
57 * e: number of extra existential variables
67 void (*f
)(struct scan_data
*data
, PipQuast
*q
, int i
);
70 static int vectorpos2cpos(struct scan_data
*data
, int j
)
72 int np
= data
->d
- data
->v
- data
->e
;
77 else if (j
< data
->v
- data
->n
)
79 else if (j
< data
->v
-data
->n
+np
)
80 l
= 1+data
->n
+data
->e
+j
;
88 * returns true if some solution exist in the whole quast q
90 static int full_quast(PipQuast
*q
)
92 return q
->condition
? full_quast(q
->next_then
) && full_quast(q
->next_else
)
99 * Dimensions in the resulting domain are:
102 static void scan_quast_r(struct scan_data
*data
, PipQuast
*q
, int i
)
107 /* Skip to a (random) leaf if we are only interested in whether
110 skip
= data
->n
== 0 && full_quast(q
);
111 while (skip
&& q
->condition
)
114 for (p
= q
->newparm
; !skip
&& p
; p
= p
->next
) {
116 PipVector
*vec
= p
->vector
;
118 value_set_si(data
->M
->p
[i
][0], 1);
119 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
121 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
122 l
= vectorpos2cpos(data
, j
);
123 value_assign(data
->M
->p
[i
][l
], vec
->the_vector
[j
]);
125 l
= vectorpos2cpos(data
, p
->rank
);
126 value_oppose(data
->M
->p
[i
][l
], p
->deno
);
127 value_assign(data
->M
->p
[i
][1+data
->d
], vec
->the_vector
[j
]);
130 value_set_si(data
->M
->p
[i
][0], 1);
131 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
133 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
134 l
= vectorpos2cpos(data
, j
);
135 value_oppose(data
->M
->p
[i
][l
], vec
->the_vector
[j
]);
137 l
= vectorpos2cpos(data
, p
->rank
);
138 value_assign(data
->M
->p
[i
][l
], p
->deno
);
139 value_oppose(data
->M
->p
[i
][1+data
->d
], vec
->the_vector
[j
]);
140 value_addto(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
], p
->deno
);
141 value_decrement(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
]);
147 value_set_si(data
->M
->p
[i
][0], 1);
148 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
150 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
151 int l
= vectorpos2cpos(data
, j
);
152 value_assign(data
->M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
154 value_assign(data
->M
->p
[i
][1+data
->d
], q
->condition
->the_vector
[j
]);
155 scan_quast_r(data
, q
->next_then
, i
+1);
157 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
158 int l
= vectorpos2cpos(data
, j
);
159 value_oppose(data
->M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
161 value_oppose(data
->M
->p
[i
][1+data
->d
], q
->condition
->the_vector
[j
]);
162 value_decrement(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
]);
163 scan_quast_r(data
, q
->next_else
, i
+1);
168 /* if data->n is zero, we are only interested in the domains
169 * where a solution exists and not in the actual solution
171 if (q
->list
&& data
->n
) {
174 for (j
= 0, l
= q
->list
; l
; ++j
, l
= l
->next
) {
175 Vector_Set(data
->M
->p
[i
], 0, data
->d
+1);
176 value_set_si(data
->M
->p
[i
][1+data
->pos
+j
], -1);
178 for (k
= 0; k
< l
->vector
->nb_elements
-1; ++k
) {
179 int ll
= vectorpos2cpos(data
, k
);
180 value_assign(data
->M
->p
[i
][ll
], l
->vector
->the_vector
[k
]);
182 value_assign(data
->M
->p
[i
][1+data
->d
], l
->vector
->the_vector
[k
]);
190 static void scan_quast(struct scan_data
*data
, PipQuast
*q
)
192 int nparam
, nexist
, d
, i
, rows
;
194 nparam
= data
->d
- data
->n
;
197 nexist
= max_new(q
, nparam
-1, 0, &d
) - nparam
+1;
198 rows
= 2 * nexist
+ d
+ data
->n
;
200 /* nparam now refers to the number of parameters in the original polyhedron */
201 nparam
-= data
->v
- data
->n
;
204 data
->d
= data
->v
+ nexist
+ nparam
;
206 data
->M
= Matrix_Alloc(rows
, 1+data
->d
+1);
208 scan_quast_r(data
, q
, 0);
209 Matrix_Free(data
->M
);
212 struct quast2poly_data
{
213 struct scan_data scan
;
217 static void add_quast_base(struct scan_data
*data
, PipQuast
*q
, int i
)
219 struct quast2poly_data
*qdata
= (struct quast2poly_data
*)data
;
223 C
= Matrix_Alloc(i
, 1+data
->d
+1);
224 Vector_Copy(data
->M
->p
[0], C
->p
[0], i
* (1+data
->d
+1));
225 P
= Constraints2Polyhedron(C
, MAXRAYS
);
233 * nvar: total number of variables, including the minimized variables,
234 * but excluding the parameters
235 * nparam: the number of parameters in the PIP problem, excluding the "big parameter"
236 * for maximization problems, i.e., the
237 * total number of variables minus the minimized variables
238 * pos: position of the first minimized variable
239 * n: number of minimized variables
241 static Polyhedron
*quast2poly(PipQuast
*q
, int nvar
, int nparam
, int pos
, int n
)
243 struct quast2poly_data data
;
248 data
.scan
.d
= n
+nparam
;
251 data
.scan
.f
= add_quast_base
;
253 scan_quast(&data
.scan
, q
);
258 Polyhedron
*pip_projectout(Polyhedron
*P
, int pos
, int n
, int nparam
)
262 unsigned int nvar
= P
->Dimension
- nparam
;
263 PipMatrix
*context
= pip_matrix_alloc(0, P
->Dimension
- n
+ 2);
267 POL_ENSURE_INEQUALITIES(P
);
269 domain
= poly2pip(P
, pos
, n
, nparam
);
271 pip_matrix_print(stderr
, domain
);
272 pip_matrix_print(stderr
, context
);
275 options
= pip_options_init();
276 options
->Urs_unknowns
= -1;
277 options
->Urs_parms
= -1;
278 options
->Simplify
= 1;
279 sol
= pip_solve(domain
, context
, -1, options
);
282 pip_quast_print(stderr
, sol
, 0);
285 min
= quast2poly(sol
, nvar
- n
, P
->Dimension
- n
, 0, 0);
288 pip_matrix_free(context
);
289 pip_matrix_free(domain
);
290 pip_options_free(options
);