1 /*
2 * Scilab ( http://www.scilab.org/ ) - This file is part of Scilab
3 * Copyright (C) 2015 - Scilab Enterprises - Calixte DENIZET
4 *
5 * Copyright (C) 2012 - 2016 - Scilab Enterprises
6 *
7 * This file is hereby licensed under the terms of the GNU GPL v2.0,
8 * pursuant to article 5.3.4 of the CeCILL v.2.1.
9 * This file was originally licensed under the terms of the CeCILL v2.1,
10 * and continues to be available under such terms.
11 * For more information, see the COPYING file which you should have received
12 * along with this program.
13 *
14 */
15
16 #include "gvn/InferenceConstraint.hxx"
17
18 namespace analysis
19 {
check(GVN & gvn,const std::vector<GVN::Value * > & values) const20 InferenceConstraint::Result SameDimsConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
21 {
22 const GVN::Value & R1 = *values[0];
23 const GVN::Value & C1 = *values[1];
24 const GVN::Value & R2 = *values[2];
25 const GVN::Value & C2 = *values[3];
26
27 if (R1.value == R2.value)
28 {
29 if (C1.value == C2.value)
30 {
31 return Result::RESULT_TRUE;
32 }
33
34 MultivariatePolynomial mp = *C1.poly - *C2.poly;
35 if (mp.constant != 0 && mp.isCoeffPositive(false))
36 {
37 return Result::RESULT_FALSE;
38 }
39 }
40 else
41 {
42 MultivariatePolynomial mp = *R1.poly - *R2.poly;
43 if (mp.constant > 0 && mp.isCoeffPositive(false))
44 {
45 return Result::RESULT_FALSE;
46 }
47 }
48 return Result::RESULT_DUNNO;
49 }
50
getMPConstraints(const std::vector<GVN::Value * > & values) const51 MPolyConstraintSet SameDimsConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
52 {
53 MPolyConstraintSet set(2);
54 const GVN::Value & R1 = *values[0];
55 const GVN::Value & C1 = *values[1];
56 const GVN::Value & R2 = *values[2];
57 const GVN::Value & C2 = *values[3];
58
59 set.add(*R1.poly - *R2.poly, MPolyConstraint::Kind::EQ0);
60 set.add(*C1.poly - *C2.poly, MPolyConstraint::Kind::EQ0);
61
62 return set;
63 }
64
applyConstraints(const std::vector<GVN::Value * > & values) const65 void SameDimsConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
66 {
67 GVN::Value & R1 = *values[0];
68 GVN::Value & C1 = *values[1];
69 GVN::Value & R2 = *values[2];
70 GVN::Value & C2 = *values[3];
71
72 applyEquality(R1, R2);
73 applyEquality(C1, C2);
74 }
75
check(GVN & gvn,const std::vector<GVN::Value * > & values) const76 InferenceConstraint::Result EqualConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
77 {
78 const GVN::Value & x = *values[0];
79 const GVN::Value & y = *values[1];
80
81 if (x.value == y.value)
82 {
83 return Result::RESULT_TRUE;
84 }
85 else
86 {
87 MultivariatePolynomial mp = *x.poly - *y.poly;
88 if (mp.constant > 0 && mp.isCoeffPositive(false))
89 {
90 return Result::RESULT_FALSE;
91 }
92 }
93 return Result::RESULT_DUNNO;
94 }
95
applyConstraints(const std::vector<GVN::Value * > & values) const96 void EqualConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
97 {
98 GVN::Value & x = *values[0];
99 GVN::Value & y = *values[1];
100
101 applyEquality(x, y);
102 }
103
getMPConstraints(const std::vector<GVN::Value * > & values) const104 MPolyConstraintSet EqualConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
105 {
106 MPolyConstraintSet set(1);
107 const GVN::Value & x = *values[0];
108 const GVN::Value & y = *values[1];
109
110 set.add(*x.poly - *y.poly, MPolyConstraint::Kind::EQ0);
111
112 return set;
113 }
114
check(GVN & gvn,const std::vector<GVN::Value * > & values) const115 InferenceConstraint::Result MPolyConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
116 {
117 const std::vector<const MultivariatePolynomial *> & args = InferenceConstraint::getArgs(values);
118 MultivariatePolynomial mp;
119
120 if (poly.containsVarsGEq(args.size()))
121 {
122 mp = poly.translateVariables(gvn.getCurrentValue() + 1, args.size()).eval(args);
123 }
124 else
125 {
126 mp = poly.eval(args);
127 }
128
129 switch (kind)
130 {
131 case EQ0:
132 {
133 if (mp.isConstant(0))
134 {
135 // for all X, P(X) == 0
136 return Result::RESULT_TRUE;
137 }
138 else if (mp.constant != 0 && mp.isCoeffPositive(false))
139 {
140 // P(X) = Q(X) + K where K != 0 and Q with positive coeffs
141 return Result::RESULT_FALSE;
142 }
143 else
144 {
145 return Result::RESULT_DUNNO;
146 }
147 }
148 case NEQ0:
149 if (mp.constant != 0 && mp.isCoeffPositive(false))
150 {
151 return Result::RESULT_TRUE;
152 }
153 else if (mp.isConstant(0))
154 {
155 return Result::RESULT_FALSE;
156 }
157 else
158 {
159 return Result::RESULT_DUNNO;
160 }
161 case GT0:
162 if (mp.isCoeffStrictPositive())
163 {
164 return Result::RESULT_TRUE;
165 }
166 else if (mp.constant < 0 && mp.isCoeffNegative(false))
167 {
168 return Result::RESULT_FALSE;
169 }
170 else
171 {
172 return Result::RESULT_DUNNO;
173 }
174 case GEQ0:
175 {
176 if (mp.isCoeffPositive())
177 {
178 return Result::RESULT_TRUE;
179 }
180 else if (mp.isConstant() && mp.constant < 0)
181 {
182 return Result::RESULT_FALSE;
183 }
184 else
185 {
186 return Result::RESULT_DUNNO;
187 }
188 }
189 }
190 }
191
getMPConstraints(const std::vector<GVN::Value * > & values) const192 MPolyConstraintSet MPolyConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
193 {
194 MPolyConstraintSet set(1);
195 set.add(poly.eval(InferenceConstraint::getArgs(values)), kind);
196
197 return set;
198 }
199
applyConstraints(const std::vector<GVN::Value * > & values) const200 void MPolyConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
201 {
202 if (kind == EQ0)
203 {
204 if (poly.constant == 0 && poly.polynomial.size() == 2)
205 {
206 const MultivariateMonomial & m1 = *poly.polynomial.begin();
207 const MultivariateMonomial & m2 = *std::next(poly.polynomial.begin());
208
209 if (((m1.coeff == 1 && m2.coeff == -1) || (m1.coeff == -1 && m2.coeff == 1)) && (m1.monomial.size() == 1 && m2.monomial.size() == 1))
210 {
211 // We have a polynomial P such as P(X,Y)=X-Y
212 GVN::Value & x = *values[m1.monomial.begin()->var];
213 GVN::Value & y = *values[m2.monomial.begin()->var];
214
215 applyEquality(x, y);
216 }
217 }
218 }
219 }
220
check(GVN & gvn,const std::vector<GVN::Value * > & values) const221 InferenceConstraint::Result MPolyConstraintSet::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
222 {
223 for (const auto & constraint : constraints)
224 {
225 Result res = constraint.check(gvn, values);
226 if (res != Result::RESULT_TRUE)
227 {
228 return res;
229 }
230 }
231 return Result::RESULT_TRUE;
232 }
233
getMPConstraints(const std::vector<GVN::Value * > & values) const234 MPolyConstraintSet MPolyConstraintSet::getMPConstraints(const std::vector<GVN::Value *> & values) const
235 {
236 MPolyConstraintSet set(constraints.size());
237 const std::vector<const MultivariatePolynomial *> args = InferenceConstraint::getArgs(values);
238 for (const auto & constraint : constraints)
239 {
240 set.add(constraint.poly.eval(args), constraint.kind);
241 }
242 return set;
243 }
244
applyConstraints(const std::vector<GVN::Value * > & values) const245 void MPolyConstraintSet::applyConstraints(const std::vector<GVN::Value *> & values) const
246 {
247 for (const auto & mpc : constraints)
248 {
249 mpc.applyConstraints(values);
250 }
251 }
252
check(GVN & gvn,const std::vector<GVN::Value * > & values) const253 InferenceConstraint::Result PositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
254 {
255 const GVN::Value & x = *values[0];
256
257 if (x.poly->isCoeffPositive())
258 {
259 return Result::RESULT_TRUE;
260 }
261 else if (x.poly->isConstant() && x.poly->constant < 0)
262 {
263 return Result::RESULT_FALSE;
264 }
265
266 return Result::RESULT_DUNNO;
267 }
268
applyConstraints(const std::vector<GVN::Value * > & values) const269 void PositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
270
getMPConstraints(const std::vector<GVN::Value * > & values) const271 MPolyConstraintSet PositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
272 {
273 MPolyConstraintSet set(1);
274 const GVN::Value & x = *values[0];
275
276 set.add(*x.poly, MPolyConstraint::Kind::GEQ0);
277
278 return set;
279 }
280
check(GVN & gvn,const std::vector<GVN::Value * > & values) const281 InferenceConstraint::Result StrictPositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
282 {
283 const GVN::Value & x = *values[0];
284
285 if (x.poly->isCoeffStrictPositive())
286 {
287 return Result::RESULT_TRUE;
288 }
289 else if (x.poly->isConstant() && x.poly->constant <= 0)
290 {
291 return Result::RESULT_FALSE;
292 }
293
294 return Result::RESULT_DUNNO;
295 }
296
applyConstraints(const std::vector<GVN::Value * > & values) const297 void StrictPositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
298
getMPConstraints(const std::vector<GVN::Value * > & values) const299 MPolyConstraintSet StrictPositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
300 {
301 MPolyConstraintSet set(1);
302 const GVN::Value & x = *values[0];
303
304 set.add(*x.poly, MPolyConstraint::Kind::GT0);
305
306 return set;
307 }
308
check(GVN & gvn,const std::vector<GVN::Value * > & values) const309 InferenceConstraint::Result StrictGreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
310 {
311 const GVN::Value & x = *values[0];
312 const GVN::Value & y = *values[1];
313
314 if (x.value == y.value)
315 {
316 return Result::RESULT_FALSE;
317 }
318
319 MultivariatePolynomial mp = *x.poly - *y.poly;
320 if (mp.constant > 0 && mp.isCoeffPositive(false))
321 {
322 return Result::RESULT_TRUE;
323 }
324 else if (mp.constant < 0 && mp.isCoeffNegative(false))
325 {
326 return Result::RESULT_FALSE;
327 }
328
329 return Result::RESULT_DUNNO;
330 }
331
applyConstraints(const std::vector<GVN::Value * > & values) const332 void StrictGreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
333
getMPConstraints(const std::vector<GVN::Value * > & values) const334 MPolyConstraintSet StrictGreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
335 {
336 MPolyConstraintSet set(1);
337 const GVN::Value & x = *values[0];
338 const GVN::Value & y = *values[1];
339
340 set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GT0);
341
342 return set;
343 }
344
check(GVN & gvn,const std::vector<GVN::Value * > & values) const345 InferenceConstraint::Result GreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
346 {
347 const GVN::Value & x = *values[0];
348 const GVN::Value & y = *values[1];
349
350 if (x.value == y.value)
351 {
352 return Result::RESULT_TRUE;
353 }
354
355 MultivariatePolynomial mp = *x.poly - *y.poly;
356 if (mp.isCoeffPositive(true))
357 {
358 return Result::RESULT_TRUE;
359 }
360 else if (mp.constant < 0 && mp.isCoeffNegative(false))
361 {
362 return Result::RESULT_FALSE;
363 }
364
365 return Result::RESULT_DUNNO;
366 }
367
applyConstraints(const std::vector<GVN::Value * > & values) const368 void GreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
369
getMPConstraints(const std::vector<GVN::Value * > & values) const370 MPolyConstraintSet GreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
371 {
372 MPolyConstraintSet set(1);
373 const GVN::Value & x = *values[0];
374 const GVN::Value & y = *values[1];
375
376 set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GEQ0);
377
378 return set;
379 }
380
check(GVN & gvn,const std::vector<GVN::Value * > & values) const381 InferenceConstraint::Result ValidIndexConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
382 {
383 const GVN::Value & index = *values[0];
384 const GVN::Value & max = *values[1];
385 if (index.poly->constant > 0 && index.poly->isCoeffPositive(false))
386 {
387 // the index is geq than 1
388 MultivariatePolynomial mp = *max.poly - *index.poly;
389 if (mp.isCoeffPositive())
390 {
391 // max - index >= 0
392 return Result::RESULT_TRUE;
393 }
394 else if (mp.isConstant() && mp.constant < 0)
395 {
396 return Result::RESULT_FALSE;
397 }
398 }
399 else if (index.poly->isConstant() && index.poly->constant < 1)
400 {
401 return Result::RESULT_FALSE;
402 }
403
404 return Result::RESULT_DUNNO;
405 }
406
applyConstraints(const std::vector<GVN::Value * > & values) const407 void ValidIndexConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
408
getMPConstraints(const std::vector<GVN::Value * > & values) const409 MPolyConstraintSet ValidIndexConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
410 {
411 MPolyConstraintSet set(2);
412 const GVN::Value & index = *values[0];
413 const GVN::Value & max = *values[1];
414
415 set.add(*max.poly - *index.poly, MPolyConstraint::Kind::GEQ0);
416 set.add(*index.poly - 1, MPolyConstraint::Kind::GEQ0);
417
418 return set;
419 }
420
check(GVN & gvn,const std::vector<GVN::Value * > & values) const421 InferenceConstraint::Result ValidRangeConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
422 {
423 const GVN::Value & index_min = *values[0];
424 const GVN::Value & index_max = *values[1];
425 const GVN::Value & min = *values[2];
426 const GVN::Value & max = *values[3];
427
428 MultivariatePolynomial mp_min = *index_min.poly - *min.poly;
429 if (mp_min.isCoeffPositive())
430 {
431 MultivariatePolynomial mp_max = *max.poly - *index_max.poly;
432 if (mp_max.isCoeffPositive())
433 {
434 return Result::RESULT_TRUE;
435 }
436 else if (mp_max.isConstant() && mp_max.constant < 0)
437 {
438 return Result::RESULT_FALSE;
439 }
440 }
441 else if (mp_min.isConstant() && mp_min.constant < 0)
442 {
443 return Result::RESULT_FALSE;
444 }
445
446 return Result::RESULT_DUNNO;
447 }
448
applyConstraints(const std::vector<GVN::Value * > & values) const449 void ValidRangeConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
450
getMPConstraints(const std::vector<GVN::Value * > & values) const451 MPolyConstraintSet ValidRangeConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
452 {
453 MPolyConstraintSet set(4);
454 const GVN::Value & index_min = *values[0];
455 const GVN::Value & index_max = *values[1];
456 const GVN::Value & min = *values[2];
457 const GVN::Value & max = *values[3];
458
459 set.add(*index_min.poly - *min.poly, MPolyConstraint::Kind::GEQ0);
460 set.add(*max.poly - *index_max.poly, MPolyConstraint::Kind::GEQ0);
461
462 return set;
463 }
464
operator <<(std::wostream & out,const MPolyConstraint & mpc)465 std::wostream & operator<<(std::wostream & out, const MPolyConstraint & mpc)
466 {
467 out << mpc.poly;
468 switch (mpc.kind)
469 {
470 case MPolyConstraint::Kind::EQ0:
471 out << L" = 0";
472 break;
473 case MPolyConstraint::Kind::NEQ0:
474 out << L" != 0";
475 break;
476 case MPolyConstraint::Kind::GT0:
477 out << L" > 0";
478 break;
479 case MPolyConstraint::Kind::GEQ0:
480 out << L" >= 0";
481 break;
482 }
483
484 return out;
485 }
486
operator <<(std::wostream & out,const MPolyConstraintSet & mpcs)487 std::wostream & operator<<(std::wostream & out, const MPolyConstraintSet & mpcs)
488 {
489 tools::printSet(mpcs.constraints, out);
490 return out;
491 }
492 }
493