1 #include <polylib/polylibgmp.h>
2 #include <stdio.h> /* needed for piplib ! */
3 #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
);
51 static int vectorpos2cpos(int v
, int pos
, int n
, int e
, int d
, int j
)
70 * v: total number of variables in original problem
71 * pos: position of minimized variables
72 * n: dimension of space in which minimum was taken
73 * i.e., number of minimized vars in original problem
74 * e: number of extra existential variables
77 * Dimensions in the resulting domain are:
80 static void add_quast(Polyhedron
**D
, Matrix
* M
, PipQuast
*q
,
81 int i
, int v
, int pos
, int n
, int e
, int d
)
85 for (p
= q
->newparm
; p
; p
= p
->next
) {
87 PipVector
*vec
= p
->vector
;
89 value_set_si(M
->p
[i
][0], 1);
90 Vector_Set(M
->p
[i
]+1, 0, d
);
92 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
93 l
= vectorpos2cpos(v
, pos
, n
, e
, d
, j
);
94 value_assign(M
->p
[i
][l
], vec
->the_vector
[j
]);
96 l
= vectorpos2cpos(v
, pos
, n
, e
, d
, p
->rank
);
97 value_oppose(M
->p
[i
][l
], p
->deno
);
98 value_assign(M
->p
[i
][1+d
], vec
->the_vector
[j
]);
101 value_set_si(M
->p
[i
][0], 1);
102 Vector_Set(M
->p
[i
]+1, 0, d
);
104 for (j
= 0; j
< vec
->nb_elements
-1; ++j
) {
105 l
= vectorpos2cpos(v
, pos
, n
, e
, d
, j
);
106 value_oppose(M
->p
[i
][l
], vec
->the_vector
[j
]);
108 l
= vectorpos2cpos(v
, pos
, n
, e
, d
, p
->rank
);
109 value_assign(M
->p
[i
][l
], p
->deno
);
110 value_oppose(M
->p
[i
][1+d
], vec
->the_vector
[j
]);
111 value_addto(M
->p
[i
][1+d
], M
->p
[i
][1+d
], p
->deno
);
112 value_decrement(M
->p
[i
][1+d
], M
->p
[i
][1+d
]);
118 value_set_si(M
->p
[i
][0], 1);
119 Vector_Set(M
->p
[i
]+1, 0, d
);
121 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
122 int l
= vectorpos2cpos(v
, pos
, n
, e
, d
, j
);
123 value_assign(M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
125 value_assign(M
->p
[i
][1+d
], q
->condition
->the_vector
[j
]);
126 add_quast(D
, M
, q
->next_then
, i
+1, v
, pos
, n
, e
, d
);
128 for (j
= 0; j
< q
->condition
->nb_elements
-1; ++j
) {
129 int l
= vectorpos2cpos(v
, pos
, n
, e
, d
, j
);
130 value_oppose(M
->p
[i
][l
], q
->condition
->the_vector
[j
]);
132 value_oppose(M
->p
[i
][1+d
], q
->condition
->the_vector
[j
]);
133 value_decrement(M
->p
[i
][1+d
], M
->p
[i
][1+d
]);
134 add_quast(D
, M
, q
->next_else
, i
+1, v
, pos
, n
, e
, d
);
135 } else if (q
->list
) {
140 for (j
= 0, l
= q
->list
; l
; ++j
, l
= l
->next
) {
141 Vector_Set(M
->p
[i
], 0, d
+1);
142 value_set_si(M
->p
[i
][1+pos
+j
], -1);
144 for (k
= 0; k
< l
->vector
->nb_elements
-1; ++k
) {
145 int ll
= vectorpos2cpos(v
, pos
, n
, e
, d
, k
);
146 value_assign(M
->p
[i
][ll
], l
->vector
->the_vector
[k
]);
148 value_assign(M
->p
[i
][1+d
], l
->vector
->the_vector
[k
]);
152 C
= Matrix_Alloc(i
, 1+d
+1);
153 Vector_Copy(M
->p
[0], C
->p
[0], i
* (1+d
+1));
154 P
= Constraints2Polyhedron(C
, MAXRAYS
);
162 * nvar: total number of variables, including the minimized variables,
163 * but excluding the parameters
164 * pos: position of the first minimized variable
165 * n: number of minimized variables
167 static Polyhedron
*quast2poly(PipQuast
*q
, int nvar
, int pos
, int n
)
176 assert(n
!= 0); /* required ? */
177 nparam
= q
->newparm
? q
->newparm
->rank
:
178 q
->condition
? q
->condition
->nb_elements
-1 :
179 q
->list
->vector
->nb_elements
-1;
181 nexist
= max_new(q
, nparam
-1, 0, &d
) - nparam
+1;
182 rows
= nparam
+ 2 * nexist
+ d
+ n
;
184 /* nparam now refers to the number of parameters in the original polyhedron */
186 M
= Matrix_Alloc(rows
, 1+nvar
+nexist
+nparam
+1);
187 /* All parameters are/should be positive */
188 for (i
= 0; i
< pos
; ++i
) {
189 value_set_si(M
->p
[i
][0], 1);
190 value_set_si(M
->p
[i
][1+i
], 1);
192 for (i
= pos
+n
; i
< nvar
; ++i
) {
193 value_set_si(M
->p
[i
-n
][0], 1);
194 value_set_si(M
->p
[i
-n
][1+i
], 1);
196 for (i
= 0; i
< nparam
; ++i
) {
197 value_set_si(M
->p
[nvar
-n
+i
][0], 1);
198 value_set_si(M
->p
[nvar
-n
+i
][1+nvar
+nexist
+i
], 1);
201 add_quast(&D
, M
, q
, nparam
, nvar
, pos
, n
, nexist
, nvar
+nexist
+nparam
);
206 Polyhedron
*pip_lexmin(Polyhedron
*P
, int pos
, int n
, int nparam
)
210 unsigned int nvar
= P
->Dimension
- nparam
;
211 PipMatrix
*context
= pip_matrix_alloc(0, P
->Dimension
- n
+ 2);
215 POL_ENSURE_INEQUALITIES(P
);
217 domain
= poly2pip(P
, pos
, n
, nparam
);
219 pip_matrix_print(stderr, domain);
220 pip_matrix_print(stderr, context);
223 options
= pip_options_init();
224 sol
= pip_solve(domain
, context
, -1, options
);
227 pip_quast_print(stderr, sol, 0);
230 min
= quast2poly(sol
, nvar
, pos
, n
);
233 pip_matrix_free(context
);
234 pip_matrix_free(domain
);
235 pip_options_free(options
);