1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Arithmetic instantiator. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "options/quantifiers_options.h" |
20 |
|
#include "theory/arith/arith_msum.h" |
21 |
|
#include "theory/arith/partial_model.h" |
22 |
|
#include "theory/arith/theory_arith.h" |
23 |
|
#include "theory/arith/theory_arith_private.h" |
24 |
|
#include "theory/quantifiers/term_util.h" |
25 |
|
#include "theory/rewriter.h" |
26 |
|
#include "util/random.h" |
27 |
|
|
28 |
|
using namespace std; |
29 |
|
using namespace cvc5::kind; |
30 |
|
using namespace cvc5::context; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace quantifiers { |
35 |
|
|
36 |
886 |
ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc) |
37 |
886 |
: Instantiator(env, tn), d_vtc(vtc) |
38 |
|
{ |
39 |
886 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
40 |
886 |
d_one = NodeManager::currentNM()->mkConst(Rational(1)); |
41 |
886 |
} |
42 |
|
|
43 |
15254 |
void ArithInstantiator::reset(CegInstantiator* ci, |
44 |
|
SolvedForm& sf, |
45 |
|
Node pv, |
46 |
|
CegInstEffort effort) |
47 |
|
{ |
48 |
15254 |
d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false); |
49 |
15254 |
d_vts_sym[1] = d_vtc->getVtsDelta(false, false); |
50 |
45762 |
for (unsigned i = 0; i < 2; i++) |
51 |
|
{ |
52 |
30508 |
d_mbp_bounds[i].clear(); |
53 |
30508 |
d_mbp_coeff[i].clear(); |
54 |
91524 |
for (unsigned j = 0; j < 2; j++) |
55 |
|
{ |
56 |
61016 |
d_mbp_vts_coeff[i][j].clear(); |
57 |
|
} |
58 |
30508 |
d_mbp_lit[i].clear(); |
59 |
|
} |
60 |
15254 |
} |
61 |
|
|
62 |
15114 |
bool ArithInstantiator::hasProcessEquality(CegInstantiator* ci, |
63 |
|
SolvedForm& sf, |
64 |
|
Node pv, |
65 |
|
CegInstEffort effort) |
66 |
|
{ |
67 |
15114 |
return true; |
68 |
|
} |
69 |
|
|
70 |
29904 |
bool ArithInstantiator::processEquality(CegInstantiator* ci, |
71 |
|
SolvedForm& sf, |
72 |
|
Node pv, |
73 |
|
std::vector<TermProperties>& term_props, |
74 |
|
std::vector<Node>& terms, |
75 |
|
CegInstEffort effort) |
76 |
|
{ |
77 |
29904 |
NodeManager* nm = NodeManager::currentNM(); |
78 |
59808 |
Node eq_lhs = terms[0]; |
79 |
59808 |
Node eq_rhs = terms[1]; |
80 |
59808 |
Node lhs_coeff = term_props[0].d_coeff; |
81 |
59808 |
Node rhs_coeff = term_props[1].d_coeff; |
82 |
|
// make the same coefficient |
83 |
29904 |
if (rhs_coeff != lhs_coeff) |
84 |
|
{ |
85 |
|
if (!rhs_coeff.isNull()) |
86 |
|
{ |
87 |
|
Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; |
88 |
|
eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs); |
89 |
|
} |
90 |
|
if (!lhs_coeff.isNull()) |
91 |
|
{ |
92 |
|
Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; |
93 |
|
eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs); |
94 |
|
} |
95 |
|
} |
96 |
59808 |
Node eq = eq_lhs.eqNode(eq_rhs); |
97 |
29904 |
eq = rewrite(eq); |
98 |
59808 |
Node val; |
99 |
59808 |
TermProperties pv_prop; |
100 |
59808 |
Node vts_coeff_inf; |
101 |
59808 |
Node vts_coeff_delta; |
102 |
|
// isolate pv in the equality |
103 |
59808 |
CegTermType ires = solve_arith( |
104 |
29904 |
ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); |
105 |
29904 |
if (ires != CEG_TT_INVALID) |
106 |
|
{ |
107 |
9556 |
pv_prop.d_type = CEG_TT_EQUAL; |
108 |
9556 |
if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) |
109 |
|
{ |
110 |
6718 |
return true; |
111 |
|
} |
112 |
|
} |
113 |
23186 |
return false; |
114 |
|
} |
115 |
|
|
116 |
8152 |
bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, |
117 |
|
SolvedForm& sf, |
118 |
|
Node pv, |
119 |
|
CegInstEffort effort) |
120 |
|
{ |
121 |
8152 |
return effort != CEG_INST_EFFORT_FULL; |
122 |
|
} |
123 |
|
|
124 |
241121 |
Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, |
125 |
|
SolvedForm& sf, |
126 |
|
Node pv, |
127 |
|
Node lit, |
128 |
|
CegInstEffort effort) |
129 |
|
{ |
130 |
482242 |
Node atom = lit.getKind() == NOT ? lit[0] : lit; |
131 |
|
// arithmetic inequalities and disequalities |
132 |
482242 |
if (atom.getKind() == GEQ |
133 |
482242 |
|| (atom.getKind() == EQUAL && atom[0].getType().isReal())) |
134 |
|
{ |
135 |
241121 |
return lit; |
136 |
|
} |
137 |
|
return Node::null(); |
138 |
|
} |
139 |
|
|
140 |
6792 |
bool ArithInstantiator::processAssertion(CegInstantiator* ci, |
141 |
|
SolvedForm& sf, |
142 |
|
Node pv, |
143 |
|
Node lit, |
144 |
|
Node alit, |
145 |
|
CegInstEffort effort) |
146 |
|
{ |
147 |
6792 |
NodeManager* nm = NodeManager::currentNM(); |
148 |
13584 |
Node atom = lit.getKind() == NOT ? lit[0] : lit; |
149 |
6792 |
bool pol = lit.getKind() != NOT; |
150 |
|
// arithmetic inequalities and disequalities |
151 |
6792 |
Assert(atom.getKind() == GEQ |
152 |
|
|| (atom.getKind() == EQUAL && atom[0].getType().isReal())); |
153 |
|
// get model value for pv |
154 |
13584 |
Node pv_value = ci->getModelValue(pv); |
155 |
|
// cannot contain infinity? |
156 |
13584 |
Node vts_coeff_inf; |
157 |
13584 |
Node vts_coeff_delta; |
158 |
13584 |
Node val; |
159 |
13584 |
TermProperties pv_prop; |
160 |
|
// isolate pv in the inequality |
161 |
13584 |
CegTermType ires = solve_arith( |
162 |
6792 |
ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); |
163 |
6792 |
if (ires == CEG_TT_INVALID) |
164 |
|
{ |
165 |
269 |
return false; |
166 |
|
} |
167 |
|
// compute how many bounds we will consider |
168 |
6523 |
unsigned rmax = 1; |
169 |
6523 |
if (atom.getKind() == EQUAL && (pol || !options::cegqiModel())) |
170 |
|
{ |
171 |
584 |
rmax = 2; |
172 |
|
} |
173 |
13630 |
for (unsigned r = 0; r < rmax; r++) |
174 |
|
{ |
175 |
7107 |
CegTermType uires = ires; |
176 |
14214 |
Node uval = val; |
177 |
7107 |
if (atom.getKind() == GEQ) |
178 |
|
{ |
179 |
|
// push negation downwards |
180 |
4022 |
if (!pol) |
181 |
|
{ |
182 |
1922 |
uires = mkNegateCTT(ires); |
183 |
1922 |
if (d_type.isInteger()) |
184 |
|
{ |
185 |
1828 |
uval = nm->mkNode( |
186 |
|
PLUS, |
187 |
|
val, |
188 |
3656 |
nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); |
189 |
1828 |
uval = rewrite(uval); |
190 |
|
} |
191 |
|
else |
192 |
|
{ |
193 |
94 |
Assert(d_type.isReal()); |
194 |
|
// now is strict inequality |
195 |
94 |
uires = mkStrictCTT(uires); |
196 |
|
} |
197 |
|
} |
198 |
|
} |
199 |
3085 |
else if (pol) |
200 |
|
{ |
201 |
|
// equalities are both non-strict upper and lower bounds |
202 |
1168 |
uires = r == 0 ? CEG_TT_UPPER : CEG_TT_LOWER; |
203 |
|
} |
204 |
|
else |
205 |
|
{ |
206 |
|
// disequalities are either strict upper or lower bounds |
207 |
|
bool is_upper; |
208 |
1917 |
if (options::cegqiModel()) |
209 |
|
{ |
210 |
|
// disequality is a disjunction : only consider the bound in the |
211 |
|
// direction of the model |
212 |
|
// first check if there is an infinity... |
213 |
1917 |
if (!vts_coeff_inf.isNull()) |
214 |
|
{ |
215 |
|
// coefficient or val won't make a difference, just compare with zero |
216 |
|
Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " |
217 |
|
<< vts_coeff_inf << std::endl; |
218 |
|
Assert(vts_coeff_inf.isConst()); |
219 |
|
is_upper = (vts_coeff_inf.getConst<Rational>().sgn() == 1); |
220 |
|
} |
221 |
|
else |
222 |
|
{ |
223 |
3834 |
Node rhs_value = ci->getModelValue(val); |
224 |
3834 |
Node lhs_value = pv_prop.getModifiedTerm(pv_value); |
225 |
1917 |
if (!pv_prop.isBasic()) |
226 |
|
{ |
227 |
13 |
lhs_value = pv_prop.getModifiedTerm(pv_value); |
228 |
13 |
lhs_value = rewrite(lhs_value); |
229 |
|
} |
230 |
3834 |
Trace("cegqi-arith-debug") |
231 |
1917 |
<< "Disequality : check model values " << lhs_value << " " |
232 |
1917 |
<< rhs_value << std::endl; |
233 |
|
// it generally should be the case that lhs_value!=rhs_value |
234 |
|
// however, this assertion is violated e.g. if non-linear is enabled |
235 |
|
// since the quantifier-free arithmetic solver may pass full |
236 |
|
// effort with no lemmas even when we are not guaranteed to have a |
237 |
|
// model. By convention, we use GEQ to compare the values here. |
238 |
|
// It also may be the case that cmp is non-constant, in the case |
239 |
|
// where lhs or rhs contains a transcendental function. We consider |
240 |
|
// the bound to be an upper bound in this case. |
241 |
3834 |
Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); |
242 |
1917 |
cmp = rewrite(cmp); |
243 |
1917 |
is_upper = !cmp.isConst() || !cmp.getConst<bool>(); |
244 |
|
} |
245 |
|
} |
246 |
|
else |
247 |
|
{ |
248 |
|
// since we are not using the model, we try both. |
249 |
|
is_upper = (r == 0); |
250 |
|
} |
251 |
1917 |
Assert(atom.getKind() == EQUAL && !pol); |
252 |
1917 |
if (d_type.isInteger()) |
253 |
|
{ |
254 |
1887 |
uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; |
255 |
1887 |
uval = nm->mkNode( |
256 |
3774 |
PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); |
257 |
1887 |
uval = rewrite(uval); |
258 |
|
} |
259 |
|
else |
260 |
|
{ |
261 |
30 |
Assert(d_type.isReal()); |
262 |
30 |
uires = is_upper ? CEG_TT_LOWER_STRICT : CEG_TT_UPPER_STRICT; |
263 |
|
} |
264 |
|
} |
265 |
7107 |
if (Trace.isOn("cegqi-arith-bound-inf")) |
266 |
|
{ |
267 |
|
Node pvmod = pv_prop.getModifiedTerm(pv); |
268 |
|
Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : "; |
269 |
|
Trace("cegqi-arith-bound-inf") |
270 |
|
<< pvmod << " -> " << uval << ", styp = " << uires << std::endl; |
271 |
|
} |
272 |
|
// take into account delta |
273 |
7107 |
if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT) |
274 |
|
{ |
275 |
124 |
if (options::cegqiModel()) |
276 |
|
{ |
277 |
|
Node delta_coeff = |
278 |
248 |
nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)); |
279 |
124 |
if (vts_coeff_delta.isNull()) |
280 |
|
{ |
281 |
122 |
vts_coeff_delta = delta_coeff; |
282 |
|
} |
283 |
|
else |
284 |
|
{ |
285 |
2 |
vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff); |
286 |
2 |
vts_coeff_delta = rewrite(vts_coeff_delta); |
287 |
|
} |
288 |
|
} |
289 |
|
else |
290 |
|
{ |
291 |
|
Node delta = d_vtc->getVtsDelta(); |
292 |
|
uval = nm->mkNode( |
293 |
|
uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta); |
294 |
|
uval = rewrite(uval); |
295 |
|
} |
296 |
|
} |
297 |
7107 |
if (options::cegqiModel()) |
298 |
|
{ |
299 |
|
// just store bounds, will choose based on tighest bound |
300 |
7107 |
unsigned index = isUpperBoundCTT(uires) ? 0 : 1; |
301 |
7107 |
d_mbp_bounds[index].push_back(uval); |
302 |
7107 |
d_mbp_coeff[index].push_back(pv_prop.d_coeff); |
303 |
14214 |
Trace("cegqi-arith-debug") |
304 |
7107 |
<< "Store bound " << index << " " << uval << " " << pv_prop.d_coeff |
305 |
7107 |
<< " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit |
306 |
7107 |
<< std::endl; |
307 |
21321 |
for (unsigned t = 0; t < 2; t++) |
308 |
|
{ |
309 |
14214 |
d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf |
310 |
|
: vts_coeff_delta); |
311 |
|
} |
312 |
7107 |
d_mbp_lit[index].push_back(lit); |
313 |
|
} |
314 |
|
else |
315 |
|
{ |
316 |
|
// try this bound |
317 |
|
pv_prop.d_type = isUpperBoundCTT(uires) ? CEG_TT_UPPER : CEG_TT_LOWER; |
318 |
|
if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) |
319 |
|
{ |
320 |
|
return true; |
321 |
|
} |
322 |
|
} |
323 |
|
} |
324 |
6523 |
return false; |
325 |
|
} |
326 |
|
|
327 |
7926 |
bool ArithInstantiator::processAssertions(CegInstantiator* ci, |
328 |
|
SolvedForm& sf, |
329 |
|
Node pv, |
330 |
|
CegInstEffort effort) |
331 |
|
{ |
332 |
7926 |
if (!options::cegqiModel()) |
333 |
|
{ |
334 |
|
return false; |
335 |
|
} |
336 |
7926 |
NodeManager* nm = NodeManager::currentNM(); |
337 |
|
bool use_inf = |
338 |
7926 |
d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal(); |
339 |
7926 |
bool upper_first = Random::getRandom().pickWithProb(0.5); |
340 |
7926 |
if (options::cegqiMinBounds()) |
341 |
|
{ |
342 |
|
upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); |
343 |
|
} |
344 |
|
int best_used[2]; |
345 |
15852 |
std::vector<Node> t_values[3]; |
346 |
15852 |
Node pv_value = ci->getModelValue(pv); |
347 |
|
// try optimal bounds |
348 |
19311 |
for (unsigned r = 0; r < 2; r++) |
349 |
|
{ |
350 |
14096 |
int rr = upper_first ? (1 - r) : r; |
351 |
14096 |
best_used[rr] = -1; |
352 |
14096 |
if (d_mbp_bounds[rr].empty()) |
353 |
|
{ |
354 |
10657 |
if (use_inf) |
355 |
|
{ |
356 |
76 |
Trace("cegqi-arith-bound") |
357 |
38 |
<< "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv |
358 |
38 |
<< " (type=" << d_type << ")" << std::endl; |
359 |
|
// no bounds, we do +- infinity |
360 |
38 |
Node val = d_vtc->getVtsInfinity(d_type); |
361 |
|
// could get rho value for infinity here |
362 |
38 |
if (rr == 0) |
363 |
|
{ |
364 |
24 |
val = nm->mkNode(UMINUS, val); |
365 |
24 |
val = rewrite(val); |
366 |
|
} |
367 |
38 |
TermProperties pv_prop_no_bound; |
368 |
38 |
if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) |
369 |
|
{ |
370 |
38 |
return true; |
371 |
|
} |
372 |
|
else if (!options::cegqiMultiInst()) |
373 |
|
{ |
374 |
|
return false; |
375 |
|
} |
376 |
|
} |
377 |
|
} |
378 |
|
else |
379 |
|
{ |
380 |
6878 |
Trace("cegqi-arith-bound") |
381 |
3439 |
<< (rr == 0 ? "Lower" : "Upper") << " bounds for " << pv |
382 |
3439 |
<< " (type=" << d_type << ") : " << std::endl; |
383 |
3439 |
int best = -1; |
384 |
13756 |
Node best_bound_value[3]; |
385 |
9291 |
for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) |
386 |
|
{ |
387 |
11704 |
Node value[3]; |
388 |
5852 |
if (Trace.isOn("cegqi-arith-bound")) |
389 |
|
{ |
390 |
|
Assert(!d_mbp_bounds[rr][j].isNull()); |
391 |
|
Trace("cegqi-arith-bound") |
392 |
|
<< " " << j << ": " << d_mbp_bounds[rr][j]; |
393 |
|
if (!d_mbp_vts_coeff[rr][0][j].isNull()) |
394 |
|
{ |
395 |
|
Trace("cegqi-arith-bound") |
396 |
|
<< " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)"; |
397 |
|
} |
398 |
|
if (!d_mbp_vts_coeff[rr][1][j].isNull()) |
399 |
|
{ |
400 |
|
Trace("cegqi-arith-bound") |
401 |
|
<< " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)"; |
402 |
|
} |
403 |
|
if (!d_mbp_coeff[rr][j].isNull()) |
404 |
|
{ |
405 |
|
Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")"; |
406 |
|
} |
407 |
|
Trace("cegqi-arith-bound") << ", value = "; |
408 |
|
} |
409 |
5852 |
t_values[rr].push_back(Node::null()); |
410 |
|
// check if it is better than the current best bound : lexicographic |
411 |
|
// order infinite/finite/infinitesimal parts |
412 |
5852 |
bool new_best_set = false; |
413 |
5852 |
bool new_best = true; |
414 |
22613 |
for (unsigned t = 0; t < 3; t++) |
415 |
|
{ |
416 |
|
// get the value |
417 |
17159 |
if (t == 0) |
418 |
|
{ |
419 |
5852 |
value[0] = d_mbp_vts_coeff[rr][0][j]; |
420 |
5852 |
if (!value[0].isNull()) |
421 |
|
{ |
422 |
|
Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + "; |
423 |
|
} |
424 |
|
else |
425 |
|
{ |
426 |
5852 |
value[0] = d_zero; |
427 |
|
} |
428 |
|
} |
429 |
11307 |
else if (t == 1) |
430 |
|
{ |
431 |
11704 |
Node t_value = ci->getModelValue(d_mbp_bounds[rr][j]); |
432 |
5852 |
t_values[rr][j] = t_value; |
433 |
5852 |
value[1] = t_value; |
434 |
5852 |
Trace("cegqi-arith-bound") << value[1]; |
435 |
|
} |
436 |
|
else |
437 |
|
{ |
438 |
5455 |
value[2] = d_mbp_vts_coeff[rr][1][j]; |
439 |
5455 |
if (!value[2].isNull()) |
440 |
|
{ |
441 |
65 |
Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; |
442 |
|
} |
443 |
|
else |
444 |
|
{ |
445 |
5390 |
value[2] = d_zero; |
446 |
|
} |
447 |
|
} |
448 |
|
// multiply by coefficient |
449 |
17159 |
if (value[t] != d_zero && !d_mbp_coeff[rr][j].isNull()) |
450 |
|
{ |
451 |
51 |
Assert(d_mbp_coeff[rr][j].isConst()); |
452 |
204 |
value[t] = nm->mkNode( |
453 |
|
MULT, |
454 |
204 |
nm->mkConst(Rational(1) |
455 |
153 |
/ d_mbp_coeff[rr][j].getConst<Rational>()), |
456 |
51 |
value[t]); |
457 |
51 |
value[t] = rewrite(value[t]); |
458 |
|
} |
459 |
|
// check if new best, if we have not already set it. |
460 |
17159 |
if (best != -1 && !new_best_set) |
461 |
|
{ |
462 |
6176 |
Assert(!value[t].isNull() && !best_bound_value[t].isNull()); |
463 |
6176 |
if (value[t] != best_bound_value[t]) |
464 |
|
{ |
465 |
1065 |
Kind k = rr == 0 ? GEQ : LEQ; |
466 |
1732 |
Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); |
467 |
1065 |
cmp_bound = rewrite(cmp_bound); |
468 |
|
// Should be comparing two constant values which should rewrite |
469 |
|
// to a constant. If a step failed, we assume that this is not |
470 |
|
// the new best bound. We might not be comparing constant |
471 |
|
// values (for instance if transcendental functions are |
472 |
|
// involved), in which case we do update the best bound value. |
473 |
1065 |
if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>()) |
474 |
|
{ |
475 |
398 |
new_best = false; |
476 |
398 |
break; |
477 |
|
} |
478 |
|
// indicate that the value of new_best is now established. |
479 |
667 |
new_best_set = true; |
480 |
|
} |
481 |
|
} |
482 |
|
} |
483 |
5852 |
Trace("cegqi-arith-bound") << std::endl; |
484 |
5852 |
if (new_best) |
485 |
|
{ |
486 |
21816 |
for (unsigned t = 0; t < 3; t++) |
487 |
|
{ |
488 |
16362 |
best_bound_value[t] = value[t]; |
489 |
|
} |
490 |
5454 |
best = j; |
491 |
|
} |
492 |
|
} |
493 |
3439 |
if (best != -1) |
494 |
|
{ |
495 |
3439 |
Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; |
496 |
3439 |
if (best_bound_value[0] != d_zero) |
497 |
|
{ |
498 |
|
Trace("cegqi-arith-bound") |
499 |
|
<< "( " << best_bound_value[0] << " * INF ) + "; |
500 |
|
} |
501 |
3439 |
Trace("cegqi-arith-bound") << best_bound_value[1]; |
502 |
3439 |
if (best_bound_value[2] != d_zero) |
503 |
|
{ |
504 |
108 |
Trace("cegqi-arith-bound") |
505 |
54 |
<< " + ( " << best_bound_value[2] << " * DELTA )"; |
506 |
|
} |
507 |
3439 |
Trace("cegqi-arith-bound") << std::endl; |
508 |
3439 |
best_used[rr] = best; |
509 |
|
// if using cbqiMidpoint, only add the instance based on one bound if |
510 |
|
// the bound is non-strict |
511 |
7995 |
if (!options::cegqiMidpoint() || d_type.isInteger() |
512 |
4212 |
|| d_mbp_vts_coeff[rr][1][best].isNull()) |
513 |
|
{ |
514 |
4153 |
Node val = d_mbp_bounds[rr][best]; |
515 |
17065 |
val = getModelBasedProjectionValue(ci, |
516 |
|
pv, |
517 |
|
val, |
518 |
|
rr == 0, |
519 |
3413 |
d_mbp_coeff[rr][best], |
520 |
|
pv_value, |
521 |
3413 |
t_values[rr][best], |
522 |
6826 |
sf.getTheta(), |
523 |
3413 |
d_mbp_vts_coeff[rr][0][best], |
524 |
3413 |
d_mbp_vts_coeff[rr][1][best]); |
525 |
3413 |
if (!val.isNull()) |
526 |
|
{ |
527 |
4153 |
TermProperties pv_prop_bound; |
528 |
3413 |
pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; |
529 |
3413 |
pv_prop_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER; |
530 |
3413 |
if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) |
531 |
|
{ |
532 |
2400 |
return true; |
533 |
|
} |
534 |
1013 |
else if (!options::cegqiMultiInst()) |
535 |
|
{ |
536 |
273 |
return false; |
537 |
|
} |
538 |
|
} |
539 |
|
} |
540 |
|
} |
541 |
|
} |
542 |
|
} |
543 |
|
// if not using infinity, use model value of zero |
544 |
5215 |
if (!use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty()) |
545 |
|
{ |
546 |
4820 |
Node val = d_zero; |
547 |
4820 |
TermProperties pv_prop_zero; |
548 |
4820 |
Node theta = sf.getTheta(); |
549 |
4820 |
val = getModelBasedProjectionValue(ci, |
550 |
|
pv, |
551 |
|
val, |
552 |
|
true, |
553 |
|
pv_prop_zero.d_coeff, |
554 |
|
pv_value, |
555 |
|
d_zero, |
556 |
9640 |
sf.getTheta(), |
557 |
9640 |
Node::null(), |
558 |
9640 |
Node::null()); |
559 |
4820 |
if (!val.isNull()) |
560 |
|
{ |
561 |
4820 |
if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) |
562 |
|
{ |
563 |
4776 |
return true; |
564 |
|
} |
565 |
44 |
else if (!options::cegqiMultiInst()) |
566 |
|
{ |
567 |
44 |
return false; |
568 |
|
} |
569 |
|
} |
570 |
|
} |
571 |
395 |
if (options::cegqiMidpoint() && !d_type.isInteger()) |
572 |
|
{ |
573 |
1185 |
Node vals[2]; |
574 |
395 |
bool bothBounds = true; |
575 |
395 |
Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; |
576 |
1185 |
for (unsigned rr = 0; rr < 2; rr++) |
577 |
|
{ |
578 |
790 |
int best = best_used[rr]; |
579 |
790 |
if (best == -1) |
580 |
|
{ |
581 |
24 |
bothBounds = false; |
582 |
|
} |
583 |
|
else |
584 |
|
{ |
585 |
766 |
vals[rr] = d_mbp_bounds[rr][best]; |
586 |
4596 |
vals[rr] = getModelBasedProjectionValue(ci, |
587 |
|
pv, |
588 |
|
vals[rr], |
589 |
|
rr == 0, |
590 |
1532 |
Node::null(), |
591 |
|
pv_value, |
592 |
766 |
t_values[rr][best], |
593 |
1532 |
sf.getTheta(), |
594 |
766 |
d_mbp_vts_coeff[rr][0][best], |
595 |
2298 |
Node::null()); |
596 |
|
} |
597 |
790 |
Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; |
598 |
|
} |
599 |
764 |
Node val; |
600 |
395 |
if (bothBounds) |
601 |
|
{ |
602 |
371 |
Assert(!vals[0].isNull() && !vals[1].isNull()); |
603 |
371 |
if (vals[0] == vals[1]) |
604 |
|
{ |
605 |
342 |
val = vals[0]; |
606 |
|
} |
607 |
|
else |
608 |
|
{ |
609 |
87 |
val = nm->mkNode(MULT, |
610 |
58 |
nm->mkNode(PLUS, vals[0], vals[1]), |
611 |
58 |
nm->mkConst(Rational(1) / Rational(2))); |
612 |
29 |
val = rewrite(val); |
613 |
|
} |
614 |
|
} |
615 |
|
else |
616 |
|
{ |
617 |
24 |
if (!vals[0].isNull()) |
618 |
|
{ |
619 |
8 |
val = nm->mkNode(PLUS, vals[0], d_one); |
620 |
8 |
val = rewrite(val); |
621 |
|
} |
622 |
16 |
else if (!vals[1].isNull()) |
623 |
|
{ |
624 |
16 |
val = nm->mkNode(MINUS, vals[1], d_one); |
625 |
16 |
val = rewrite(val); |
626 |
|
} |
627 |
|
} |
628 |
395 |
Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; |
629 |
395 |
if (!val.isNull()) |
630 |
|
{ |
631 |
764 |
TermProperties pv_prop_midpoint; |
632 |
395 |
if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) |
633 |
|
{ |
634 |
18 |
return true; |
635 |
|
} |
636 |
377 |
else if (!options::cegqiMultiInst()) |
637 |
|
{ |
638 |
8 |
return false; |
639 |
|
} |
640 |
|
} |
641 |
|
} |
642 |
|
// generally should not make it to this point, unless we are using a |
643 |
|
// non-monotonic selection function |
644 |
|
|
645 |
369 |
if (!options::cegqiNopt()) |
646 |
|
{ |
647 |
|
// if not trying non-optimal bounds, return |
648 |
|
return false; |
649 |
|
} |
650 |
|
// try non-optimal bounds (heuristic, may help when nested quantification) ? |
651 |
369 |
Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; |
652 |
1107 |
for (unsigned r = 0; r < 2; r++) |
653 |
|
{ |
654 |
738 |
int rr = upper_first ? (1 - r) : r; |
655 |
2243 |
for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) |
656 |
|
{ |
657 |
3010 |
if ((int)j != best_used[rr] |
658 |
1505 |
&& (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull())) |
659 |
|
{ |
660 |
|
Node val = getModelBasedProjectionValue(ci, |
661 |
|
pv, |
662 |
767 |
d_mbp_bounds[rr][j], |
663 |
|
rr == 0, |
664 |
767 |
d_mbp_coeff[rr][j], |
665 |
|
pv_value, |
666 |
767 |
t_values[rr][j], |
667 |
1534 |
sf.getTheta(), |
668 |
767 |
d_mbp_vts_coeff[rr][0][j], |
669 |
5369 |
d_mbp_vts_coeff[rr][1][j]); |
670 |
767 |
if (!val.isNull()) |
671 |
|
{ |
672 |
1534 |
TermProperties pv_prop_nopt_bound; |
673 |
767 |
pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; |
674 |
767 |
pv_prop_nopt_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER; |
675 |
767 |
if (ci->constructInstantiationInc(pv, val, pv_prop_nopt_bound, sf)) |
676 |
|
{ |
677 |
|
return true; |
678 |
|
} |
679 |
767 |
else if (!options::cegqiMultiInst()) |
680 |
|
{ |
681 |
|
return false; |
682 |
|
} |
683 |
|
} |
684 |
|
} |
685 |
|
} |
686 |
|
} |
687 |
369 |
return false; |
688 |
|
} |
689 |
|
|
690 |
20949 |
bool ArithInstantiator::needsPostProcessInstantiationForVariable( |
691 |
|
CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) |
692 |
|
{ |
693 |
41898 |
return std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) |
694 |
62847 |
!= sf.d_non_basic.end(); |
695 |
|
} |
696 |
|
|
697 |
81 |
bool ArithInstantiator::postProcessInstantiationForVariable( |
698 |
|
CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) |
699 |
|
{ |
700 |
81 |
Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) |
701 |
|
!= sf.d_non_basic.end()); |
702 |
81 |
Assert(std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) != sf.d_vars.end()); |
703 |
|
unsigned index = |
704 |
81 |
std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) - sf.d_vars.begin(); |
705 |
81 |
Assert(!sf.d_props[index].isBasic()); |
706 |
162 |
Node eq_lhs = sf.d_props[index].getModifiedTerm(sf.d_vars[index]); |
707 |
81 |
if (Trace.isOn("cegqi-arith-debug")) |
708 |
|
{ |
709 |
|
Trace("cegqi-arith-debug") << "Normalize substitution for "; |
710 |
|
Trace("cegqi-arith-debug") |
711 |
|
<< eq_lhs << " = " << sf.d_subs[index] << std::endl; |
712 |
|
} |
713 |
81 |
Assert(sf.d_vars[index].getType().isInteger()); |
714 |
|
// must ensure that divisibility constraints are met |
715 |
|
// solve updated rewritten equality for vars[index], if coefficient is one, |
716 |
|
// then we are successful |
717 |
162 |
Node eq_rhs = sf.d_subs[index]; |
718 |
162 |
Node eq = eq_lhs.eqNode(eq_rhs); |
719 |
81 |
eq = rewrite(eq); |
720 |
81 |
Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; |
721 |
162 |
std::map<Node, Node> msum; |
722 |
81 |
if (!ArithMSum::getMonomialSumLit(eq, msum)) |
723 |
|
{ |
724 |
9 |
Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; |
725 |
9 |
return false; |
726 |
|
} |
727 |
144 |
Node veq; |
728 |
72 |
if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) == 0) |
729 |
|
{ |
730 |
|
Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; |
731 |
|
return false; |
732 |
|
} |
733 |
144 |
Node veq_c; |
734 |
72 |
if (veq[0] != sf.d_vars[index]) |
735 |
|
{ |
736 |
88 |
Node veq_v; |
737 |
44 |
if (ArithMSum::getMonomial(veq[0], veq_c, veq_v)) |
738 |
|
{ |
739 |
44 |
Assert(veq_v == sf.d_vars[index]); |
740 |
|
} |
741 |
|
} |
742 |
72 |
sf.d_subs[index] = veq[1]; |
743 |
72 |
if (!veq_c.isNull()) |
744 |
|
{ |
745 |
44 |
NodeManager* nm = NodeManager::currentNM(); |
746 |
44 |
sf.d_subs[index] = nm->mkNode(INTS_DIVISION_TOTAL, veq[1], veq_c); |
747 |
88 |
Trace("cegqi-arith-debug") |
748 |
44 |
<< "...bound type is : " << sf.d_props[index].d_type << std::endl; |
749 |
|
// intger division rounding up if from a lower bound |
750 |
88 |
if (sf.d_props[index].d_type == CEG_TT_UPPER |
751 |
44 |
&& options::cegqiRoundUpLowerLia()) |
752 |
|
{ |
753 |
|
sf.d_subs[index] = nm->mkNode( |
754 |
|
PLUS, |
755 |
|
sf.d_subs[index], |
756 |
|
nm->mkNode( |
757 |
|
ITE, |
758 |
|
nm->mkNode( |
759 |
|
EQUAL, nm->mkNode(INTS_MODULUS_TOTAL, veq[1], veq_c), d_zero), |
760 |
|
d_zero, |
761 |
|
d_one)); |
762 |
|
} |
763 |
|
} |
764 |
144 |
Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] |
765 |
72 |
<< " -> " << sf.d_subs[index] << std::endl; |
766 |
72 |
return true; |
767 |
|
} |
768 |
|
|
769 |
36696 |
CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, |
770 |
|
Node pv, |
771 |
|
Node atom, |
772 |
|
Node& veq_c, |
773 |
|
Node& val, |
774 |
|
Node& vts_coeff_inf, |
775 |
|
Node& vts_coeff_delta) |
776 |
|
{ |
777 |
36696 |
NodeManager* nm = NodeManager::currentNM(); |
778 |
73392 |
Trace("cegqi-arith-debug") |
779 |
36696 |
<< "isolate for " << pv << " in " << atom << std::endl; |
780 |
73392 |
std::map<Node, Node> msum; |
781 |
36696 |
if (!ArithMSum::getMonomialSumLit(atom, msum)) |
782 |
|
{ |
783 |
36266 |
Trace("cegqi-arith-debug") |
784 |
18133 |
<< "fail : could not get monomial sum" << std::endl; |
785 |
18133 |
return CEG_TT_INVALID; |
786 |
|
} |
787 |
18563 |
Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; |
788 |
18563 |
if (Trace.isOn("cegqi-arith-debug")) |
789 |
|
{ |
790 |
|
ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug"); |
791 |
|
} |
792 |
37126 |
TypeNode pvtn = pv.getType(); |
793 |
|
// remove vts symbols from polynomial |
794 |
37126 |
Node vts_coeff[2]; |
795 |
55689 |
for (unsigned t = 0; t < 2; t++) |
796 |
|
{ |
797 |
37126 |
if (!d_vts_sym[t].isNull()) |
798 |
|
{ |
799 |
148 |
std::map<Node, Node>::iterator itminf = msum.find(d_vts_sym[t]); |
800 |
148 |
if (itminf != msum.end()) |
801 |
|
{ |
802 |
10 |
vts_coeff[t] = itminf->second; |
803 |
10 |
if (vts_coeff[t].isNull()) |
804 |
|
{ |
805 |
|
vts_coeff[t] = nm->mkConst(Rational(1)); |
806 |
|
} |
807 |
|
// negate if coefficient on variable is positive |
808 |
10 |
std::map<Node, Node>::iterator itv = msum.find(pv); |
809 |
10 |
if (itv != msum.end()) |
810 |
|
{ |
811 |
|
// multiply by the coefficient we will isolate for |
812 |
10 |
if (itv->second.isNull()) |
813 |
|
{ |
814 |
2 |
vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); |
815 |
|
} |
816 |
|
else |
817 |
|
{ |
818 |
8 |
if (!pvtn.isInteger()) |
819 |
|
{ |
820 |
8 |
vts_coeff[t] = nm->mkNode( |
821 |
|
MULT, |
822 |
4 |
nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()), |
823 |
4 |
vts_coeff[t]); |
824 |
2 |
vts_coeff[t] = rewrite(vts_coeff[t]); |
825 |
|
} |
826 |
6 |
else if (itv->second.getConst<Rational>().sgn() == 1) |
827 |
|
{ |
828 |
|
vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); |
829 |
|
} |
830 |
|
} |
831 |
|
} |
832 |
20 |
Trace("cegqi-arith-debug") |
833 |
10 |
<< "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; |
834 |
10 |
msum.erase(d_vts_sym[t]); |
835 |
|
} |
836 |
|
} |
837 |
|
} |
838 |
|
|
839 |
18563 |
int ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); |
840 |
18563 |
if (ires == 0) |
841 |
|
{ |
842 |
1700 |
Trace("cegqi-arith-debug") << "fail : isolate" << std::endl; |
843 |
1700 |
return CEG_TT_INVALID; |
844 |
|
} |
845 |
16863 |
if (Trace.isOn("cegqi-arith-debug")) |
846 |
|
{ |
847 |
|
Trace("cegqi-arith-debug") << "Isolate : "; |
848 |
|
if (!veq_c.isNull()) |
849 |
|
{ |
850 |
|
Trace("cegqi-arith-debug") << veq_c << " * "; |
851 |
|
} |
852 |
|
Trace("cegqi-arith-debug") |
853 |
|
<< pv << " " << atom.getKind() << " " << val << std::endl; |
854 |
|
} |
855 |
|
// when not pure LIA/LRA, we must check whether the lhs contains pv |
856 |
16863 |
if (expr::hasSubterm(val, pv)) |
857 |
|
{ |
858 |
784 |
Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; |
859 |
784 |
return CEG_TT_INVALID; |
860 |
|
} |
861 |
|
// if its type is integer but the substitution is not integer |
862 |
32158 |
if (pvtn.isInteger() |
863 |
48246 |
&& ((!veq_c.isNull() && !veq_c.getType().isInteger()) |
864 |
28398 |
|| !val.getType().isInteger())) |
865 |
|
{ |
866 |
|
// redo, split integer/non-integer parts |
867 |
9 |
bool useCoeff = false; |
868 |
18 |
Integer coeff(1); |
869 |
31 |
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); |
870 |
|
++it) |
871 |
|
{ |
872 |
22 |
if (it->first.isNull() || it->first.getType().isInteger()) |
873 |
|
{ |
874 |
15 |
if (!it->second.isNull()) |
875 |
|
{ |
876 |
9 |
coeff = coeff.lcm(it->second.getConst<Rational>().getDenominator()); |
877 |
9 |
useCoeff = true; |
878 |
|
} |
879 |
|
} |
880 |
|
} |
881 |
|
// multiply everything by this coefficient |
882 |
18 |
Node rcoeff = nm->mkConst(Rational(coeff)); |
883 |
18 |
std::vector<Node> real_part; |
884 |
31 |
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); |
885 |
|
++it) |
886 |
|
{ |
887 |
22 |
if (useCoeff) |
888 |
|
{ |
889 |
18 |
if (it->second.isNull()) |
890 |
|
{ |
891 |
7 |
msum[it->first] = rcoeff; |
892 |
|
} |
893 |
|
else |
894 |
|
{ |
895 |
11 |
msum[it->first] = rewrite(nm->mkNode(MULT, it->second, rcoeff)); |
896 |
|
} |
897 |
|
} |
898 |
22 |
if (!it->first.isNull() && !it->first.getType().isInteger()) |
899 |
|
{ |
900 |
14 |
real_part.push_back(msum[it->first].isNull() |
901 |
28 |
? it->first |
902 |
14 |
: nm->mkNode(MULT, msum[it->first], it->first)); |
903 |
|
} |
904 |
|
} |
905 |
|
// remove delta |
906 |
9 |
vts_coeff[1] = Node::null(); |
907 |
|
// multiply inf |
908 |
9 |
if (!vts_coeff[0].isNull()) |
909 |
|
{ |
910 |
|
vts_coeff[0] = rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0])); |
911 |
|
} |
912 |
9 |
Node realPart = real_part.empty() |
913 |
|
? d_zero |
914 |
14 |
: (real_part.size() == 1 ? real_part[0] |
915 |
32 |
: nm->mkNode(PLUS, real_part)); |
916 |
9 |
Assert(ci->isEligibleForInstantiation(realPart)); |
917 |
|
// re-isolate |
918 |
9 |
Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; |
919 |
9 |
veq_c = Node::null(); |
920 |
9 |
ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); |
921 |
18 |
Trace("cegqi-arith-debug") |
922 |
9 |
<< "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " |
923 |
9 |
<< atom.getKind() << " " << val << std::endl; |
924 |
18 |
Trace("cegqi-arith-debug") |
925 |
9 |
<< " real part : " << realPart << std::endl; |
926 |
9 |
if (ires != 0) |
927 |
|
{ |
928 |
|
int ires_use = |
929 |
9 |
(msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1 |
930 |
9 |
: -1; |
931 |
18 |
val = rewrite( |
932 |
36 |
nm->mkNode(ires_use == -1 ? PLUS : MINUS, |
933 |
18 |
nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart), |
934 |
18 |
nm->mkNode(TO_INTEGER, realPart))); |
935 |
|
// could round up for upper bounds here |
936 |
9 |
Trace("cegqi-arith-debug") << "result : " << val << std::endl; |
937 |
9 |
Assert(val.getType().isInteger()); |
938 |
|
} |
939 |
|
else |
940 |
|
{ |
941 |
|
return CEG_TT_INVALID; |
942 |
|
} |
943 |
|
} |
944 |
16079 |
vts_coeff_inf = vts_coeff[0]; |
945 |
16079 |
vts_coeff_delta = vts_coeff[1]; |
946 |
32158 |
Trace("cegqi-arith-debug") |
947 |
32158 |
<< "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " |
948 |
16079 |
<< val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" |
949 |
16079 |
<< std::endl; |
950 |
16079 |
Assert(ires != 0); |
951 |
16079 |
if (atom.getKind() == EQUAL) |
952 |
|
{ |
953 |
12057 |
return CEG_TT_EQUAL; |
954 |
|
} |
955 |
4022 |
return ires == 1 ? CEG_TT_UPPER : CEG_TT_LOWER; |
956 |
|
} |
957 |
|
|
958 |
9766 |
Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, |
959 |
|
Node e, |
960 |
|
Node t, |
961 |
|
bool isLower, |
962 |
|
Node c, |
963 |
|
Node me, |
964 |
|
Node mt, |
965 |
|
Node theta, |
966 |
|
Node inf_coeff, |
967 |
|
Node delta_coeff) |
968 |
|
{ |
969 |
9766 |
NodeManager* nm = NodeManager::currentNM(); |
970 |
9766 |
Node val = t; |
971 |
9766 |
Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; |
972 |
9766 |
Assert(!e.getType().isInteger() || t.getType().isInteger()); |
973 |
9766 |
Assert(!e.getType().isInteger() || mt.getType().isInteger()); |
974 |
|
// add rho value |
975 |
|
// get the value of c*e |
976 |
19532 |
Node ceValue = me; |
977 |
19532 |
Node new_theta = theta; |
978 |
9766 |
if (!c.isNull()) |
979 |
|
{ |
980 |
53 |
Assert(c.getType().isInteger()); |
981 |
53 |
ceValue = nm->mkNode(MULT, ceValue, c); |
982 |
53 |
ceValue = rewrite(ceValue); |
983 |
53 |
if (new_theta.isNull()) |
984 |
|
{ |
985 |
33 |
new_theta = c; |
986 |
|
} |
987 |
|
else |
988 |
|
{ |
989 |
20 |
new_theta = nm->mkNode(MULT, new_theta, c); |
990 |
20 |
new_theta = rewrite(new_theta); |
991 |
|
} |
992 |
53 |
Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; |
993 |
53 |
Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; |
994 |
|
} |
995 |
9766 |
if (!new_theta.isNull() && e.getType().isInteger()) |
996 |
|
{ |
997 |
208 |
Node rho; |
998 |
104 |
if (isLower) |
999 |
|
{ |
1000 |
56 |
rho = nm->mkNode(MINUS, ceValue, mt); |
1001 |
|
} |
1002 |
|
else |
1003 |
|
{ |
1004 |
48 |
rho = nm->mkNode(MINUS, mt, ceValue); |
1005 |
|
} |
1006 |
104 |
rho = rewrite(rho); |
1007 |
208 |
Trace("cegqi-arith-bound2") |
1008 |
104 |
<< "...rho = " << me << " - " << mt << " = " << rho << std::endl; |
1009 |
208 |
Trace("cegqi-arith-bound2") |
1010 |
104 |
<< "..." << rho << " mod " << new_theta << " = "; |
1011 |
104 |
rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); |
1012 |
104 |
rho = rewrite(rho); |
1013 |
104 |
Trace("cegqi-arith-bound2") << rho << std::endl; |
1014 |
104 |
Kind rk = isLower ? PLUS : MINUS; |
1015 |
104 |
val = nm->mkNode(rk, val, rho); |
1016 |
104 |
val = rewrite(val); |
1017 |
104 |
Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; |
1018 |
|
} |
1019 |
9766 |
if (!inf_coeff.isNull()) |
1020 |
|
{ |
1021 |
|
Assert(!d_vts_sym[0].isNull()); |
1022 |
|
val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); |
1023 |
|
val = rewrite(val); |
1024 |
|
} |
1025 |
9766 |
if (!delta_coeff.isNull()) |
1026 |
|
{ |
1027 |
|
// create delta here if necessary |
1028 |
28 |
val = nm->mkNode( |
1029 |
56 |
PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); |
1030 |
28 |
val = rewrite(val); |
1031 |
|
} |
1032 |
19532 |
return val; |
1033 |
|
} |
1034 |
|
|
1035 |
|
} // namespace quantifiers |
1036 |
|
} // namespace theory |
1037 |
22746 |
} // namespace cvc5 |