1 #include <stdio.h> /* needed for piplib ! */
2 #include <piplib/piplibMP.h>
7 #ifdef HAVE_GROWING_CHERNIKOVA
8 #define MAXRAYS POL_NO_DUAL
13 static PipMatrix
*poly2pip(Polyhedron
*P
, int pos
, int n
, int nparam
)
17 unsigned int extra
= P
->Dimension
- pos
- n
- nparam
;
19 matrix
= pip_matrix_alloc(P
->NbConstraints
, P
->Dimension
+2);
20 for (i
= 0; i
< P
->NbConstraints
; ++i
) {
21 value_assign(matrix
->p
[i
][0], P
->Constraint
[i
][0]);
22 for (j
= 0; j
< n
; ++j
)
23 value_assign(matrix
->p
[i
][1+j
], P
->Constraint
[i
][1+pos
+j
]);
24 for (j
= 0; j
< pos
; ++j
)
25 value_assign(matrix
->p
[i
][1+n
+j
], P
->Constraint
[i
][1+j
]);
26 for (j
= 0; j
< extra
; ++j
)
27 value_assign(matrix
->p
[i
][1+n
+pos
+j
], P
->Constraint
[i
][1+n
+pos
+j
]);
28 for (j
= 1+pos
+n
+extra
; j
< P
->Dimension
+2; ++j
)
29 value_assign(matrix
->p
[i
][j
], P
->Constraint
[i
][j
]);
35 static int max_new(PipQuast
*q
, int max
, int d
, int *maxd
)
39 for (p
= q
->newparm
; p
; p
= p
->next
)
45 max
= max_new(q
->next_else
, max
, d
, maxd
);
46 max
= max_new(q
->next_then
, max
, d
, maxd
);
52 * v: total number of variables in original problem
53 * pos: position of minimized variables
54 * n: dimension of space in which minimum was taken
55 * i.e., number of minimized vars in original problem
56 * e: number of extra existential variables
66 void (*f
)(struct scan_data
*data
, PipQuast
*q
, int i
);
69 static int vectorpos2cpos(struct scan_data
*data
, int j
)
71 int np
= data
->d
- data
->v
- data
->e
;
76 else if (j
< data
->v
- data
->n
)
78 else if (j
< data
->v
-data
->n
+np
)
79 l
= 1+data
->n
+data
->e
+j
;
87 * returns true if some solution exist in the whole quast q
89 static int full_quast(PipQuast
*q
)
91 return q
->condition
? full_quast(q
->next_then
) && full_quast(q
->next_else
)
98 * Dimensions in the resulting domain are:
101 static void scan_quast_r(struct scan_data
*data
, PipQuast
*q
, int i
)
106 /* Skip to a (random) leaf if we are only interested in whether
109 skip
= data
->n
== 0 && full_quast(q
);
110 while (skip
&& q
->condition
)
113 for (p
= q
->newparm
; !skip
&& p
; p
= p
->next
) {
115 PipVector
*vec
= p
->vector
;
117 value_set_si(data
->M
->p
[i
][0], 1);
118 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
120 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
121 l
= vectorpos2cpos(data
, j
);
122 value_assign(data
->M
->p
[i
][l
], vec
->the_vector
[j
]);
124 l
= vectorpos2cpos(data
, p
->rank
);
125 value_oppose(data
->M
->p
[i
][l
], p
->deno
);
126 value_assign(data
->M
->p
[i
][1+data
->d
], vec
->the_vector
[j
]);
129 value_set_si(data
->M
->p
[i
][0], 1);
130 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
132 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
133 l
= vectorpos2cpos(data
, j
);
134 value_oppose(data
->M
->p
[i
][l
], vec
->the_vector
[j
]);
136 l
= vectorpos2cpos(data
, p
->rank
);
137 value_assign(data
->M
->p
[i
][l
], p
->deno
);
138 value_oppose(data
->M
->p
[i
][1+data
->d
], vec
->the_vector
[j
]);
139 value_addto(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
], p
->deno
);
140 value_decrement(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
]);
146 value_set_si(data
->M
->p
[i
][0], 1);
147 Vector_Set(data
->M
->p
[i
]+1, 0, data
->d
);
149 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
150 int l
= vectorpos2cpos(data
, j
);
151 value_assign(data
->M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
153 value_assign(data
->M
->p
[i
][1+data
->d
], q
->condition
->the_vector
[j
]);
154 scan_quast_r(data
, q
->next_then
, i
+1);
156 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
157 int l
= vectorpos2cpos(data
, j
);
158 value_oppose(data
->M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
160 value_oppose(data
->M
->p
[i
][1+data
->d
], q
->condition
->the_vector
[j
]);
161 value_decrement(data
->M
->p
[i
][1+data
->d
], data
->M
->p
[i
][1+data
->d
]);
162 scan_quast_r(data
, q
->next_else
, i
+1);
167 /* if data->n is zero, we are only interested in the domains
168 * where a solution exists and not in the actual solution
170 if (q
->list
&& data
->n
) {
173 for (j
= 0, l
= q
->list
; l
; ++j
, l
= l
->next
) {
174 Vector_Set(data
->M
->p
[i
], 0, data
->d
+1);
175 value_set_si(data
->M
->p
[i
][1+data
->pos
+j
], -1);
177 for (k
= 0; k
< l
->vector
->nb_elements
-1; ++k
) {
178 int ll
= vectorpos2cpos(data
, k
);
179 value_assign(data
->M
->p
[i
][ll
], l
->vector
->the_vector
[k
]);
181 value_assign(data
->M
->p
[i
][1+data
->d
], l
->vector
->the_vector
[k
]);
189 static void scan_quast(struct scan_data
*data
, PipQuast
*q
)
191 int nparam
, nexist
, d
, i
, rows
;
193 nparam
= data
->d
- data
->n
;
196 nexist
= max_new(q
, nparam
-1, 0, &d
) - nparam
+1;
197 rows
= 2 * nexist
+ d
+ data
->n
;
199 /* nparam now refers to the number of parameters in the original polyhedron */
200 nparam
-= data
->v
- data
->n
;
203 data
->d
= data
->v
+ nexist
+ nparam
;
205 data
->M
= Matrix_Alloc(rows
, 1+data
->d
+1);
207 scan_quast_r(data
, q
, 0);
208 Matrix_Free(data
->M
);
211 struct quast2poly_data
{
212 struct scan_data scan
;
216 static void add_quast_base(struct scan_data
*data
, PipQuast
*q
, int i
)
218 struct quast2poly_data
*qdata
= (struct quast2poly_data
*)data
;
222 C
= Matrix_Alloc(i
, 1+data
->d
+1);
223 Vector_Copy(data
->M
->p
[0], C
->p
[0], i
* (1+data
->d
+1));
224 P
= Constraints2Polyhedron(C
, MAXRAYS
);
232 * nvar: total number of variables, including the minimized variables,
233 * but excluding the parameters
234 * nparam: the number of parameters in the PIP problem, excluding the "big parameter"
235 * for maximization problems, i.e., the
236 * total number of variables minus the minimized variables
237 * pos: position of the first minimized variable
238 * n: number of minimized variables
240 static Polyhedron
*quast2poly(PipQuast
*q
, int nvar
, int nparam
, int pos
, int n
)
242 struct quast2poly_data data
;
247 data
.scan
.d
= n
+nparam
;
250 data
.scan
.f
= add_quast_base
;
252 scan_quast(&data
.scan
, q
);
257 Polyhedron
*pip_projectout(Polyhedron
*P
, int pos
, int n
, int nparam
)
261 unsigned int nvar
= P
->Dimension
- nparam
;
262 PipMatrix
*context
= pip_matrix_alloc(0, P
->Dimension
- n
+ 2);
266 POL_ENSURE_INEQUALITIES(P
);
268 domain
= poly2pip(P
, pos
, n
, nparam
);
270 pip_matrix_print(stderr
, domain
);
271 pip_matrix_print(stderr
, context
);
274 options
= pip_options_init();
275 options
->Urs_unknowns
= -1;
276 options
->Urs_parms
= -1;
277 options
->Simplify
= 1;
278 sol
= pip_solve(domain
, context
, -1, options
);
281 pip_quast_print(stderr
, sol
, 0);
284 min
= quast2poly(sol
, nvar
- n
, P
->Dimension
- n
, 0, 0);
287 pip_matrix_free(context
);
288 pip_matrix_free(domain
);
289 pip_options_free(options
);