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 |
2021 |
ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc) |
37 |
2021 |
: Instantiator(env, tn), d_vtc(vtc) |
38 |
|
{ |
39 |
2021 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
40 |
2021 |
d_one = NodeManager::currentNM()->mkConst(Rational(1)); |
41 |
2021 |
} |
42 |
|
|
43 |
26342 |
void ArithInstantiator::reset(CegInstantiator* ci, |
44 |
|
SolvedForm& sf, |
45 |
|
Node pv, |
46 |
|
CegInstEffort effort) |
47 |
|
{ |
48 |
26342 |
d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false); |
49 |
26342 |
d_vts_sym[1] = d_vtc->getVtsDelta(false, false); |
50 |
79026 |
for (unsigned i = 0; i < 2; i++) |
51 |
|
{ |
52 |
52684 |
d_mbp_bounds[i].clear(); |
53 |
52684 |
d_mbp_coeff[i].clear(); |
54 |
158052 |
for (unsigned j = 0; j < 2; j++) |
55 |
|
{ |
56 |
105368 |
d_mbp_vts_coeff[i][j].clear(); |
57 |
|
} |
58 |
52684 |
d_mbp_lit[i].clear(); |
59 |
|
} |
60 |
26342 |
} |
61 |
|
|
62 |
25984 |
bool ArithInstantiator::hasProcessEquality(CegInstantiator* ci, |
63 |
|
SolvedForm& sf, |
64 |
|
Node pv, |
65 |
|
CegInstEffort effort) |
66 |
|
{ |
67 |
25984 |
return true; |
68 |
|
} |
69 |
|
|
70 |
41014 |
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 |
41014 |
NodeManager* nm = NodeManager::currentNM(); |
78 |
82028 |
Node eq_lhs = terms[0]; |
79 |
82028 |
Node eq_rhs = terms[1]; |
80 |
82028 |
Node lhs_coeff = term_props[0].d_coeff; |
81 |
82028 |
Node rhs_coeff = term_props[1].d_coeff; |
82 |
|
// make the same coefficient |
83 |
41014 |
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 |
82028 |
Node eq = eq_lhs.eqNode(eq_rhs); |
97 |
41014 |
eq = rewrite(eq); |
98 |
82028 |
Node val; |
99 |
82028 |
TermProperties pv_prop; |
100 |
82028 |
Node vts_coeff_inf; |
101 |
82028 |
Node vts_coeff_delta; |
102 |
|
// isolate pv in the equality |
103 |
82028 |
CegTermType ires = solve_arith( |
104 |
41014 |
ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); |
105 |
41014 |
if (ires != CEG_TT_INVALID) |
106 |
|
{ |
107 |
12452 |
pv_prop.d_type = CEG_TT_EQUAL; |
108 |
12452 |
if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) |
109 |
|
{ |
110 |
11670 |
return true; |
111 |
|
} |
112 |
|
} |
113 |
29344 |
return false; |
114 |
|
} |
115 |
|
|
116 |
13532 |
bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, |
117 |
|
SolvedForm& sf, |
118 |
|
Node pv, |
119 |
|
CegInstEffort effort) |
120 |
|
{ |
121 |
13532 |
return effort != CEG_INST_EFFORT_FULL; |
122 |
|
} |
123 |
|
|
124 |
386693 |
Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, |
125 |
|
SolvedForm& sf, |
126 |
|
Node pv, |
127 |
|
Node lit, |
128 |
|
CegInstEffort effort) |
129 |
|
{ |
130 |
773386 |
Node atom = lit.getKind() == NOT ? lit[0] : lit; |
131 |
|
// arithmetic inequalities and disequalities |
132 |
773386 |
if (atom.getKind() == GEQ |
133 |
773386 |
|| (atom.getKind() == EQUAL && atom[0].getType().isReal())) |
134 |
|
{ |
135 |
386693 |
return lit; |
136 |
|
} |
137 |
|
return Node::null(); |
138 |
|
} |
139 |
|
|
140 |
11473 |
bool ArithInstantiator::processAssertion(CegInstantiator* ci, |
141 |
|
SolvedForm& sf, |
142 |
|
Node pv, |
143 |
|
Node lit, |
144 |
|
Node alit, |
145 |
|
CegInstEffort effort) |
146 |
|
{ |
147 |
11473 |
NodeManager* nm = NodeManager::currentNM(); |
148 |
22946 |
Node atom = lit.getKind() == NOT ? lit[0] : lit; |
149 |
11473 |
bool pol = lit.getKind() != NOT; |
150 |
|
// arithmetic inequalities and disequalities |
151 |
11473 |
Assert(atom.getKind() == GEQ |
152 |
|
|| (atom.getKind() == EQUAL && atom[0].getType().isReal())); |
153 |
|
// get model value for pv |
154 |
22946 |
Node pv_value = ci->getModelValue(pv); |
155 |
|
// cannot contain infinity? |
156 |
22946 |
Node vts_coeff_inf; |
157 |
22946 |
Node vts_coeff_delta; |
158 |
22946 |
Node val; |
159 |
22946 |
TermProperties pv_prop; |
160 |
|
// isolate pv in the inequality |
161 |
22946 |
CegTermType ires = solve_arith( |
162 |
11473 |
ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta); |
163 |
11473 |
if (ires == CEG_TT_INVALID) |
164 |
|
{ |
165 |
762 |
return false; |
166 |
|
} |
167 |
|
// compute how many bounds we will consider |
168 |
10711 |
unsigned rmax = 1; |
169 |
10711 |
if (atom.getKind() == EQUAL && (pol || !options().quantifiers.cegqiModel)) |
170 |
|
{ |
171 |
|
rmax = 2; |
172 |
|
} |
173 |
21422 |
for (unsigned r = 0; r < rmax; r++) |
174 |
|
{ |
175 |
10711 |
CegTermType uires = ires; |
176 |
21422 |
Node uval = val; |
177 |
10711 |
if (atom.getKind() == GEQ) |
178 |
|
{ |
179 |
|
// push negation downwards |
180 |
7154 |
if (!pol) |
181 |
|
{ |
182 |
3695 |
uires = mkNegateCTT(ires); |
183 |
3695 |
if (d_type.isInteger()) |
184 |
|
{ |
185 |
3336 |
uval = nm->mkNode( |
186 |
|
PLUS, |
187 |
|
val, |
188 |
6672 |
nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); |
189 |
3336 |
uval = rewrite(uval); |
190 |
|
} |
191 |
|
else |
192 |
|
{ |
193 |
359 |
Assert(d_type.isReal()); |
194 |
|
// now is strict inequality |
195 |
359 |
uires = mkStrictCTT(uires); |
196 |
|
} |
197 |
|
} |
198 |
|
} |
199 |
3557 |
else if (pol) |
200 |
|
{ |
201 |
|
// equalities are both non-strict upper and lower bounds |
202 |
|
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 |
3557 |
if (options().quantifiers.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 |
3557 |
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 |
7114 |
Node rhs_value = ci->getModelValue(val); |
224 |
7114 |
Node lhs_value = pv_prop.getModifiedTerm(pv_value); |
225 |
3557 |
if (!pv_prop.isBasic()) |
226 |
|
{ |
227 |
14 |
lhs_value = pv_prop.getModifiedTerm(pv_value); |
228 |
14 |
lhs_value = rewrite(lhs_value); |
229 |
|
} |
230 |
7114 |
Trace("cegqi-arith-debug") |
231 |
3557 |
<< "Disequality : check model values " << lhs_value << " " |
232 |
3557 |
<< 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 |
7114 |
Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); |
242 |
3557 |
cmp = rewrite(cmp); |
243 |
3557 |
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 |
3557 |
Assert(atom.getKind() == EQUAL && !pol); |
252 |
3557 |
if (d_type.isInteger()) |
253 |
|
{ |
254 |
3446 |
uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; |
255 |
3446 |
uval = nm->mkNode( |
256 |
6892 |
PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); |
257 |
3446 |
uval = rewrite(uval); |
258 |
|
} |
259 |
|
else |
260 |
|
{ |
261 |
111 |
Assert(d_type.isReal()); |
262 |
111 |
uires = is_upper ? CEG_TT_LOWER_STRICT : CEG_TT_UPPER_STRICT; |
263 |
|
} |
264 |
|
} |
265 |
10711 |
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 |
10711 |
if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT) |
274 |
|
{ |
275 |
470 |
if (options().quantifiers.cegqiModel) |
276 |
|
{ |
277 |
|
Node delta_coeff = |
278 |
940 |
nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)); |
279 |
470 |
if (vts_coeff_delta.isNull()) |
280 |
|
{ |
281 |
462 |
vts_coeff_delta = delta_coeff; |
282 |
|
} |
283 |
|
else |
284 |
|
{ |
285 |
8 |
vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff); |
286 |
8 |
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 |
10711 |
if (options().quantifiers.cegqiModel) |
298 |
|
{ |
299 |
|
// just store bounds, will choose based on tighest bound |
300 |
10711 |
unsigned index = isUpperBoundCTT(uires) ? 0 : 1; |
301 |
10711 |
d_mbp_bounds[index].push_back(uval); |
302 |
10711 |
d_mbp_coeff[index].push_back(pv_prop.d_coeff); |
303 |
21422 |
Trace("cegqi-arith-debug") |
304 |
10711 |
<< "Store bound " << index << " " << uval << " " << pv_prop.d_coeff |
305 |
10711 |
<< " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit |
306 |
10711 |
<< std::endl; |
307 |
32133 |
for (unsigned t = 0; t < 2; t++) |
308 |
|
{ |
309 |
21422 |
d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf |
310 |
|
: vts_coeff_delta); |
311 |
|
} |
312 |
10711 |
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 |
10711 |
return false; |
325 |
|
} |
326 |
|
|
327 |
12868 |
bool ArithInstantiator::processAssertions(CegInstantiator* ci, |
328 |
|
SolvedForm& sf, |
329 |
|
Node pv, |
330 |
|
CegInstEffort effort) |
331 |
|
{ |
332 |
12868 |
if (!options().quantifiers.cegqiModel) |
333 |
|
{ |
334 |
|
return false; |
335 |
|
} |
336 |
12868 |
NodeManager* nm = NodeManager::currentNM(); |
337 |
13330 |
bool use_inf = d_type.isInteger() ? options().quantifiers.cegqiUseInfInt |
338 |
13330 |
: options().quantifiers.cegqiUseInfReal; |
339 |
12868 |
bool upper_first = Random::getRandom().pickWithProb(0.5); |
340 |
12868 |
if (options().quantifiers.cegqiMinBounds) |
341 |
|
{ |
342 |
|
upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); |
343 |
|
} |
344 |
|
int best_used[2]; |
345 |
25736 |
std::vector<Node> t_values[3]; |
346 |
25736 |
Node pv_value = ci->getModelValue(pv); |
347 |
|
// try optimal bounds |
348 |
30635 |
for (unsigned r = 0; r < 2; r++) |
349 |
|
{ |
350 |
22574 |
int rr = upper_first ? (1 - r) : r; |
351 |
22574 |
best_used[rr] = -1; |
352 |
22574 |
if (d_mbp_bounds[rr].empty()) |
353 |
|
{ |
354 |
17829 |
if (use_inf) |
355 |
|
{ |
356 |
304 |
Trace("cegqi-arith-bound") |
357 |
152 |
<< "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv |
358 |
152 |
<< " (type=" << d_type << ")" << std::endl; |
359 |
|
// no bounds, we do +- infinity |
360 |
152 |
Node val = d_vtc->getVtsInfinity(d_type); |
361 |
|
// could get rho value for infinity here |
362 |
152 |
if (rr == 0) |
363 |
|
{ |
364 |
96 |
val = nm->mkNode(UMINUS, val); |
365 |
96 |
val = rewrite(val); |
366 |
|
} |
367 |
152 |
TermProperties pv_prop_no_bound; |
368 |
152 |
if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) |
369 |
|
{ |
370 |
152 |
return true; |
371 |
|
} |
372 |
|
else if (!options().quantifiers.cegqiMultiInst) |
373 |
|
{ |
374 |
|
return false; |
375 |
|
} |
376 |
|
} |
377 |
|
} |
378 |
|
else |
379 |
|
{ |
380 |
9490 |
Trace("cegqi-arith-bound") |
381 |
4745 |
<< (rr == 0 ? "Lower" : "Upper") << " bounds for " << pv |
382 |
4745 |
<< " (type=" << d_type << ") : " << std::endl; |
383 |
4745 |
int best = -1; |
384 |
18980 |
Node best_bound_value[3]; |
385 |
12876 |
for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) |
386 |
|
{ |
387 |
16262 |
Node value[3]; |
388 |
8131 |
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 |
8131 |
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 |
8131 |
bool new_best_set = false; |
413 |
8131 |
bool new_best = true; |
414 |
30573 |
for (unsigned t = 0; t < 3; t++) |
415 |
|
{ |
416 |
|
// get the value |
417 |
23423 |
if (t == 0) |
418 |
|
{ |
419 |
8131 |
value[0] = d_mbp_vts_coeff[rr][0][j]; |
420 |
8131 |
if (!value[0].isNull()) |
421 |
|
{ |
422 |
|
Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + "; |
423 |
|
} |
424 |
|
else |
425 |
|
{ |
426 |
8131 |
value[0] = d_zero; |
427 |
|
} |
428 |
|
} |
429 |
15292 |
else if (t == 1) |
430 |
|
{ |
431 |
16262 |
Node t_value = ci->getModelValue(d_mbp_bounds[rr][j]); |
432 |
8131 |
t_values[rr][j] = t_value; |
433 |
8131 |
value[1] = t_value; |
434 |
8131 |
Trace("cegqi-arith-bound") << value[1]; |
435 |
|
} |
436 |
|
else |
437 |
|
{ |
438 |
7161 |
value[2] = d_mbp_vts_coeff[rr][1][j]; |
439 |
7161 |
if (!value[2].isNull()) |
440 |
|
{ |
441 |
216 |
Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; |
442 |
|
} |
443 |
|
else |
444 |
|
{ |
445 |
6945 |
value[2] = d_zero; |
446 |
|
} |
447 |
|
} |
448 |
|
// multiply by coefficient |
449 |
23423 |
if (value[t] != d_zero && !d_mbp_coeff[rr][j].isNull()) |
450 |
|
{ |
451 |
150 |
Assert(d_mbp_coeff[rr][j].isConst()); |
452 |
600 |
value[t] = nm->mkNode( |
453 |
|
MULT, |
454 |
600 |
nm->mkConst(Rational(1) |
455 |
450 |
/ d_mbp_coeff[rr][j].getConst<Rational>()), |
456 |
150 |
value[t]); |
457 |
150 |
value[t] = rewrite(value[t]); |
458 |
|
} |
459 |
|
// check if new best, if we have not already set it. |
460 |
23423 |
if (best != -1 && !new_best_set) |
461 |
|
{ |
462 |
8491 |
Assert(!value[t].isNull() && !best_bound_value[t].isNull()); |
463 |
8491 |
if (value[t] != best_bound_value[t]) |
464 |
|
{ |
465 |
1682 |
Kind k = rr == 0 ? GEQ : LEQ; |
466 |
2383 |
Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); |
467 |
1682 |
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 |
1682 |
if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>()) |
474 |
|
{ |
475 |
981 |
new_best = false; |
476 |
981 |
break; |
477 |
|
} |
478 |
|
// indicate that the value of new_best is now established. |
479 |
701 |
new_best_set = true; |
480 |
|
} |
481 |
|
} |
482 |
|
} |
483 |
8131 |
Trace("cegqi-arith-bound") << std::endl; |
484 |
8131 |
if (new_best) |
485 |
|
{ |
486 |
28600 |
for (unsigned t = 0; t < 3; t++) |
487 |
|
{ |
488 |
21450 |
best_bound_value[t] = value[t]; |
489 |
|
} |
490 |
7150 |
best = j; |
491 |
|
} |
492 |
|
} |
493 |
4745 |
if (best != -1) |
494 |
|
{ |
495 |
4745 |
Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; |
496 |
4745 |
if (best_bound_value[0] != d_zero) |
497 |
|
{ |
498 |
|
Trace("cegqi-arith-bound") |
499 |
|
<< "( " << best_bound_value[0] << " * INF ) + "; |
500 |
|
} |
501 |
4745 |
Trace("cegqi-arith-bound") << best_bound_value[1]; |
502 |
4745 |
if (best_bound_value[2] != d_zero) |
503 |
|
{ |
504 |
330 |
Trace("cegqi-arith-bound") |
505 |
165 |
<< " + ( " << best_bound_value[2] << " * DELTA )"; |
506 |
|
} |
507 |
4745 |
Trace("cegqi-arith-bound") << std::endl; |
508 |
4745 |
best_used[rr] = best; |
509 |
|
// if using cbqiMidpoint, only add the instance based on one bound if |
510 |
|
// the bound is non-strict |
511 |
10281 |
if (!options().quantifiers.cegqiMidpoint || d_type.isInteger() |
512 |
4802 |
|| d_mbp_vts_coeff[rr][1][best].isNull()) |
513 |
|
{ |
514 |
4735 |
Node val = d_mbp_bounds[rr][best]; |
515 |
23475 |
val = getModelBasedProjectionValue(ci, |
516 |
|
pv, |
517 |
|
val, |
518 |
|
rr == 0, |
519 |
4695 |
d_mbp_coeff[rr][best], |
520 |
|
pv_value, |
521 |
4695 |
t_values[rr][best], |
522 |
9390 |
sf.getTheta(), |
523 |
4695 |
d_mbp_vts_coeff[rr][0][best], |
524 |
4695 |
d_mbp_vts_coeff[rr][1][best]); |
525 |
4695 |
if (!val.isNull()) |
526 |
|
{ |
527 |
4735 |
TermProperties pv_prop_bound; |
528 |
4695 |
pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; |
529 |
4695 |
pv_prop_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER; |
530 |
4695 |
if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) |
531 |
|
{ |
532 |
3823 |
return true; |
533 |
|
} |
534 |
872 |
else if (!options().quantifiers.cegqiMultiInst) |
535 |
|
{ |
536 |
832 |
return false; |
537 |
|
} |
538 |
|
} |
539 |
|
} |
540 |
|
} |
541 |
|
} |
542 |
|
} |
543 |
|
// if not using infinity, use model value of zero |
544 |
8061 |
if (!use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty()) |
545 |
|
{ |
546 |
7993 |
Node val = d_zero; |
547 |
7993 |
TermProperties pv_prop_zero; |
548 |
7993 |
Node theta = sf.getTheta(); |
549 |
7993 |
val = getModelBasedProjectionValue(ci, |
550 |
|
pv, |
551 |
|
val, |
552 |
|
true, |
553 |
|
pv_prop_zero.d_coeff, |
554 |
|
pv_value, |
555 |
|
d_zero, |
556 |
15986 |
sf.getTheta(), |
557 |
15986 |
Node::null(), |
558 |
15986 |
Node::null()); |
559 |
7993 |
if (!val.isNull()) |
560 |
|
{ |
561 |
7993 |
if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) |
562 |
|
{ |
563 |
7841 |
return true; |
564 |
|
} |
565 |
152 |
else if (!options().quantifiers.cegqiMultiInst) |
566 |
|
{ |
567 |
152 |
return false; |
568 |
|
} |
569 |
|
} |
570 |
|
} |
571 |
68 |
if (options().quantifiers.cegqiMidpoint && !d_type.isInteger()) |
572 |
|
{ |
573 |
144 |
Node vals[2]; |
574 |
48 |
bool bothBounds = true; |
575 |
48 |
Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; |
576 |
144 |
for (unsigned rr = 0; rr < 2; rr++) |
577 |
|
{ |
578 |
96 |
int best = best_used[rr]; |
579 |
96 |
if (best == -1) |
580 |
|
{ |
581 |
46 |
bothBounds = false; |
582 |
|
} |
583 |
|
else |
584 |
|
{ |
585 |
50 |
vals[rr] = d_mbp_bounds[rr][best]; |
586 |
300 |
vals[rr] = getModelBasedProjectionValue(ci, |
587 |
|
pv, |
588 |
|
vals[rr], |
589 |
|
rr == 0, |
590 |
100 |
Node::null(), |
591 |
|
pv_value, |
592 |
50 |
t_values[rr][best], |
593 |
100 |
sf.getTheta(), |
594 |
50 |
d_mbp_vts_coeff[rr][0][best], |
595 |
150 |
Node::null()); |
596 |
|
} |
597 |
96 |
Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; |
598 |
|
} |
599 |
48 |
Node val; |
600 |
48 |
if (bothBounds) |
601 |
|
{ |
602 |
2 |
Assert(!vals[0].isNull() && !vals[1].isNull()); |
603 |
2 |
if (vals[0] == vals[1]) |
604 |
|
{ |
605 |
|
val = vals[0]; |
606 |
|
} |
607 |
|
else |
608 |
|
{ |
609 |
6 |
val = nm->mkNode(MULT, |
610 |
4 |
nm->mkNode(PLUS, vals[0], vals[1]), |
611 |
4 |
nm->mkConst(Rational(1) / Rational(2))); |
612 |
2 |
val = rewrite(val); |
613 |
|
} |
614 |
|
} |
615 |
|
else |
616 |
|
{ |
617 |
46 |
if (!vals[0].isNull()) |
618 |
|
{ |
619 |
29 |
val = nm->mkNode(PLUS, vals[0], d_one); |
620 |
29 |
val = rewrite(val); |
621 |
|
} |
622 |
17 |
else if (!vals[1].isNull()) |
623 |
|
{ |
624 |
17 |
val = nm->mkNode(MINUS, vals[1], d_one); |
625 |
17 |
val = rewrite(val); |
626 |
|
} |
627 |
|
} |
628 |
48 |
Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; |
629 |
48 |
if (!val.isNull()) |
630 |
|
{ |
631 |
48 |
TermProperties pv_prop_midpoint; |
632 |
48 |
if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) |
633 |
|
{ |
634 |
36 |
return true; |
635 |
|
} |
636 |
12 |
else if (!options().quantifiers.cegqiMultiInst) |
637 |
|
{ |
638 |
12 |
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 |
20 |
if (!options().quantifiers.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 |
20 |
Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; |
652 |
60 |
for (unsigned r = 0; r < 2; r++) |
653 |
|
{ |
654 |
40 |
int rr = upper_first ? (1 - r) : r; |
655 |
100 |
for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) |
656 |
|
{ |
657 |
120 |
if ((int)j != best_used[rr] |
658 |
80 |
&& (!options().quantifiers.cegqiMidpoint |
659 |
|
|| d_mbp_vts_coeff[rr][1][j].isNull())) |
660 |
|
{ |
661 |
|
Node val = getModelBasedProjectionValue(ci, |
662 |
|
pv, |
663 |
20 |
d_mbp_bounds[rr][j], |
664 |
|
rr == 0, |
665 |
20 |
d_mbp_coeff[rr][j], |
666 |
|
pv_value, |
667 |
20 |
t_values[rr][j], |
668 |
40 |
sf.getTheta(), |
669 |
20 |
d_mbp_vts_coeff[rr][0][j], |
670 |
140 |
d_mbp_vts_coeff[rr][1][j]); |
671 |
20 |
if (!val.isNull()) |
672 |
|
{ |
673 |
40 |
TermProperties pv_prop_nopt_bound; |
674 |
20 |
pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; |
675 |
20 |
pv_prop_nopt_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER; |
676 |
20 |
if (ci->constructInstantiationInc(pv, val, pv_prop_nopt_bound, sf)) |
677 |
|
{ |
678 |
|
return true; |
679 |
|
} |
680 |
20 |
else if (!options().quantifiers.cegqiMultiInst) |
681 |
|
{ |
682 |
|
return false; |
683 |
|
} |
684 |
|
} |
685 |
|
} |
686 |
|
} |
687 |
|
} |
688 |
20 |
return false; |
689 |
|
} |
690 |
|
|
691 |
26382 |
bool ArithInstantiator::needsPostProcessInstantiationForVariable( |
692 |
|
CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) |
693 |
|
{ |
694 |
52764 |
return std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) |
695 |
79146 |
!= sf.d_non_basic.end(); |
696 |
|
} |
697 |
|
|
698 |
221 |
bool ArithInstantiator::postProcessInstantiationForVariable( |
699 |
|
CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) |
700 |
|
{ |
701 |
221 |
Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) |
702 |
|
!= sf.d_non_basic.end()); |
703 |
221 |
Assert(std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) != sf.d_vars.end()); |
704 |
|
unsigned index = |
705 |
221 |
std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) - sf.d_vars.begin(); |
706 |
221 |
Assert(!sf.d_props[index].isBasic()); |
707 |
442 |
Node eq_lhs = sf.d_props[index].getModifiedTerm(sf.d_vars[index]); |
708 |
221 |
if (Trace.isOn("cegqi-arith-debug")) |
709 |
|
{ |
710 |
|
Trace("cegqi-arith-debug") << "Normalize substitution for "; |
711 |
|
Trace("cegqi-arith-debug") |
712 |
|
<< eq_lhs << " = " << sf.d_subs[index] << std::endl; |
713 |
|
} |
714 |
221 |
Assert(sf.d_vars[index].getType().isInteger()); |
715 |
|
// must ensure that divisibility constraints are met |
716 |
|
// solve updated rewritten equality for vars[index], if coefficient is one, |
717 |
|
// then we are successful |
718 |
442 |
Node eq_rhs = sf.d_subs[index]; |
719 |
442 |
Node eq = eq_lhs.eqNode(eq_rhs); |
720 |
221 |
eq = rewrite(eq); |
721 |
221 |
Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; |
722 |
442 |
std::map<Node, Node> msum; |
723 |
221 |
if (!ArithMSum::getMonomialSumLit(eq, msum)) |
724 |
|
{ |
725 |
18 |
Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; |
726 |
18 |
return false; |
727 |
|
} |
728 |
406 |
Node veq; |
729 |
203 |
if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) == 0) |
730 |
|
{ |
731 |
|
Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; |
732 |
|
return false; |
733 |
|
} |
734 |
406 |
Node veq_c; |
735 |
203 |
if (veq[0] != sf.d_vars[index]) |
736 |
|
{ |
737 |
174 |
Node veq_v; |
738 |
87 |
if (ArithMSum::getMonomial(veq[0], veq_c, veq_v)) |
739 |
|
{ |
740 |
87 |
Assert(veq_v == sf.d_vars[index]); |
741 |
|
} |
742 |
|
} |
743 |
203 |
sf.d_subs[index] = veq[1]; |
744 |
203 |
if (!veq_c.isNull()) |
745 |
|
{ |
746 |
87 |
NodeManager* nm = NodeManager::currentNM(); |
747 |
87 |
sf.d_subs[index] = nm->mkNode(INTS_DIVISION_TOTAL, veq[1], veq_c); |
748 |
174 |
Trace("cegqi-arith-debug") |
749 |
87 |
<< "...bound type is : " << sf.d_props[index].d_type << std::endl; |
750 |
|
// intger division rounding up if from a lower bound |
751 |
174 |
if (sf.d_props[index].d_type == CEG_TT_UPPER |
752 |
87 |
&& options().quantifiers.cegqiRoundUpLowerLia) |
753 |
|
{ |
754 |
|
sf.d_subs[index] = nm->mkNode( |
755 |
|
PLUS, |
756 |
|
sf.d_subs[index], |
757 |
|
nm->mkNode( |
758 |
|
ITE, |
759 |
|
nm->mkNode( |
760 |
|
EQUAL, nm->mkNode(INTS_MODULUS_TOTAL, veq[1], veq_c), d_zero), |
761 |
|
d_zero, |
762 |
|
d_one)); |
763 |
|
} |
764 |
|
} |
765 |
406 |
Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] |
766 |
203 |
<< " -> " << sf.d_subs[index] << std::endl; |
767 |
203 |
return true; |
768 |
|
} |
769 |
|
|
770 |
52487 |
CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, |
771 |
|
Node pv, |
772 |
|
Node atom, |
773 |
|
Node& veq_c, |
774 |
|
Node& val, |
775 |
|
Node& vts_coeff_inf, |
776 |
|
Node& vts_coeff_delta) |
777 |
|
{ |
778 |
52487 |
NodeManager* nm = NodeManager::currentNM(); |
779 |
104974 |
Trace("cegqi-arith-debug") |
780 |
52487 |
<< "isolate for " << pv << " in " << atom << std::endl; |
781 |
104974 |
std::map<Node, Node> msum; |
782 |
52487 |
if (!ArithMSum::getMonomialSumLit(atom, msum)) |
783 |
|
{ |
784 |
54868 |
Trace("cegqi-arith-debug") |
785 |
27434 |
<< "fail : could not get monomial sum" << std::endl; |
786 |
27434 |
return CEG_TT_INVALID; |
787 |
|
} |
788 |
25053 |
Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; |
789 |
25053 |
if (Trace.isOn("cegqi-arith-debug")) |
790 |
|
{ |
791 |
|
ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug"); |
792 |
|
} |
793 |
50106 |
TypeNode pvtn = pv.getType(); |
794 |
|
// remove vts symbols from polynomial |
795 |
50106 |
Node vts_coeff[2]; |
796 |
75159 |
for (unsigned t = 0; t < 2; t++) |
797 |
|
{ |
798 |
50106 |
if (!d_vts_sym[t].isNull()) |
799 |
|
{ |
800 |
662 |
std::map<Node, Node>::iterator itminf = msum.find(d_vts_sym[t]); |
801 |
662 |
if (itminf != msum.end()) |
802 |
|
{ |
803 |
50 |
vts_coeff[t] = itminf->second; |
804 |
50 |
if (vts_coeff[t].isNull()) |
805 |
|
{ |
806 |
6 |
vts_coeff[t] = nm->mkConst(Rational(1)); |
807 |
|
} |
808 |
|
// negate if coefficient on variable is positive |
809 |
50 |
std::map<Node, Node>::iterator itv = msum.find(pv); |
810 |
50 |
if (itv != msum.end()) |
811 |
|
{ |
812 |
|
// multiply by the coefficient we will isolate for |
813 |
50 |
if (itv->second.isNull()) |
814 |
|
{ |
815 |
20 |
vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); |
816 |
|
} |
817 |
|
else |
818 |
|
{ |
819 |
30 |
if (!pvtn.isInteger()) |
820 |
|
{ |
821 |
32 |
vts_coeff[t] = nm->mkNode( |
822 |
|
MULT, |
823 |
16 |
nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()), |
824 |
16 |
vts_coeff[t]); |
825 |
8 |
vts_coeff[t] = rewrite(vts_coeff[t]); |
826 |
|
} |
827 |
22 |
else if (itv->second.getConst<Rational>().sgn() == 1) |
828 |
|
{ |
829 |
16 |
vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); |
830 |
|
} |
831 |
|
} |
832 |
|
} |
833 |
100 |
Trace("cegqi-arith-debug") |
834 |
50 |
<< "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; |
835 |
50 |
msum.erase(d_vts_sym[t]); |
836 |
|
} |
837 |
|
} |
838 |
|
} |
839 |
|
|
840 |
25053 |
int ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); |
841 |
25053 |
if (ires == 0) |
842 |
|
{ |
843 |
1349 |
Trace("cegqi-arith-debug") << "fail : isolate" << std::endl; |
844 |
1349 |
return CEG_TT_INVALID; |
845 |
|
} |
846 |
23704 |
if (Trace.isOn("cegqi-arith-debug")) |
847 |
|
{ |
848 |
|
Trace("cegqi-arith-debug") << "Isolate : "; |
849 |
|
if (!veq_c.isNull()) |
850 |
|
{ |
851 |
|
Trace("cegqi-arith-debug") << veq_c << " * "; |
852 |
|
} |
853 |
|
Trace("cegqi-arith-debug") |
854 |
|
<< pv << " " << atom.getKind() << " " << val << std::endl; |
855 |
|
} |
856 |
|
// when not pure LIA/LRA, we must check whether the lhs contains pv |
857 |
23704 |
if (expr::hasSubterm(val, pv)) |
858 |
|
{ |
859 |
541 |
Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; |
860 |
541 |
return CEG_TT_INVALID; |
861 |
|
} |
862 |
|
// if its type is integer but the substitution is not integer |
863 |
46326 |
if (pvtn.isInteger() |
864 |
69547 |
&& ((!veq_c.isNull() && !veq_c.getType().isInteger()) |
865 |
45380 |
|| !val.getType().isInteger())) |
866 |
|
{ |
867 |
|
// redo, split integer/non-integer parts |
868 |
58 |
bool useCoeff = false; |
869 |
116 |
Integer coeff(1); |
870 |
184 |
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); |
871 |
|
++it) |
872 |
|
{ |
873 |
126 |
if (it->first.isNull() || it->first.getType().isInteger()) |
874 |
|
{ |
875 |
84 |
if (!it->second.isNull()) |
876 |
|
{ |
877 |
76 |
coeff = coeff.lcm(it->second.getConst<Rational>().getDenominator()); |
878 |
76 |
useCoeff = true; |
879 |
|
} |
880 |
|
} |
881 |
|
} |
882 |
|
// multiply everything by this coefficient |
883 |
116 |
Node rcoeff = nm->mkConst(Rational(coeff)); |
884 |
116 |
std::vector<Node> real_part; |
885 |
184 |
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); |
886 |
|
++it) |
887 |
|
{ |
888 |
126 |
if (useCoeff) |
889 |
|
{ |
890 |
114 |
if (it->second.isNull()) |
891 |
|
{ |
892 |
34 |
msum[it->first] = rcoeff; |
893 |
|
} |
894 |
|
else |
895 |
|
{ |
896 |
80 |
msum[it->first] = rewrite(nm->mkNode(MULT, it->second, rcoeff)); |
897 |
|
} |
898 |
|
} |
899 |
126 |
if (!it->first.isNull() && !it->first.getType().isInteger()) |
900 |
|
{ |
901 |
84 |
real_part.push_back(msum[it->first].isNull() |
902 |
168 |
? it->first |
903 |
84 |
: nm->mkNode(MULT, msum[it->first], it->first)); |
904 |
|
} |
905 |
|
} |
906 |
|
// remove delta |
907 |
58 |
vts_coeff[1] = Node::null(); |
908 |
|
// multiply inf |
909 |
58 |
if (!vts_coeff[0].isNull()) |
910 |
|
{ |
911 |
|
vts_coeff[0] = rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0])); |
912 |
|
} |
913 |
58 |
Node realPart = real_part.empty() |
914 |
|
? d_zero |
915 |
84 |
: (real_part.size() == 1 ? real_part[0] |
916 |
200 |
: nm->mkNode(PLUS, real_part)); |
917 |
58 |
Assert(ci->isEligibleForInstantiation(realPart)); |
918 |
|
// re-isolate |
919 |
58 |
Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; |
920 |
58 |
veq_c = Node::null(); |
921 |
58 |
ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); |
922 |
116 |
Trace("cegqi-arith-debug") |
923 |
58 |
<< "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " |
924 |
58 |
<< atom.getKind() << " " << val << std::endl; |
925 |
116 |
Trace("cegqi-arith-debug") |
926 |
58 |
<< " real part : " << realPart << std::endl; |
927 |
58 |
if (ires != 0) |
928 |
|
{ |
929 |
|
int ires_use = |
930 |
58 |
(msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1 |
931 |
58 |
: -1; |
932 |
116 |
val = rewrite( |
933 |
232 |
nm->mkNode(ires_use == -1 ? PLUS : MINUS, |
934 |
116 |
nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart), |
935 |
116 |
nm->mkNode(TO_INTEGER, realPart))); |
936 |
|
// could round up for upper bounds here |
937 |
58 |
Trace("cegqi-arith-debug") << "result : " << val << std::endl; |
938 |
58 |
Assert(val.getType().isInteger()); |
939 |
|
} |
940 |
|
else |
941 |
|
{ |
942 |
|
return CEG_TT_INVALID; |
943 |
|
} |
944 |
|
} |
945 |
23163 |
vts_coeff_inf = vts_coeff[0]; |
946 |
23163 |
vts_coeff_delta = vts_coeff[1]; |
947 |
46326 |
Trace("cegqi-arith-debug") |
948 |
46326 |
<< "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " |
949 |
23163 |
<< val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" |
950 |
23163 |
<< std::endl; |
951 |
23163 |
Assert(ires != 0); |
952 |
23163 |
if (atom.getKind() == EQUAL) |
953 |
|
{ |
954 |
16009 |
return CEG_TT_EQUAL; |
955 |
|
} |
956 |
7154 |
return ires == 1 ? CEG_TT_UPPER : CEG_TT_LOWER; |
957 |
|
} |
958 |
|
|
959 |
12758 |
Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, |
960 |
|
Node e, |
961 |
|
Node t, |
962 |
|
bool isLower, |
963 |
|
Node c, |
964 |
|
Node me, |
965 |
|
Node mt, |
966 |
|
Node theta, |
967 |
|
Node inf_coeff, |
968 |
|
Node delta_coeff) |
969 |
|
{ |
970 |
12758 |
NodeManager* nm = NodeManager::currentNM(); |
971 |
12758 |
Node val = t; |
972 |
12758 |
Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; |
973 |
12758 |
Assert(!e.getType().isInteger() || t.getType().isInteger()); |
974 |
12758 |
Assert(!e.getType().isInteger() || mt.getType().isInteger()); |
975 |
|
// add rho value |
976 |
|
// get the value of c*e |
977 |
25516 |
Node ceValue = me; |
978 |
25516 |
Node new_theta = theta; |
979 |
12758 |
if (!c.isNull()) |
980 |
|
{ |
981 |
139 |
Assert(c.getType().isInteger()); |
982 |
139 |
ceValue = nm->mkNode(MULT, ceValue, c); |
983 |
139 |
ceValue = rewrite(ceValue); |
984 |
139 |
if (new_theta.isNull()) |
985 |
|
{ |
986 |
90 |
new_theta = c; |
987 |
|
} |
988 |
|
else |
989 |
|
{ |
990 |
49 |
new_theta = nm->mkNode(MULT, new_theta, c); |
991 |
49 |
new_theta = rewrite(new_theta); |
992 |
|
} |
993 |
139 |
Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; |
994 |
139 |
Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; |
995 |
|
} |
996 |
12758 |
if (!new_theta.isNull() && e.getType().isInteger()) |
997 |
|
{ |
998 |
596 |
Node rho; |
999 |
298 |
if (isLower) |
1000 |
|
{ |
1001 |
174 |
rho = nm->mkNode(MINUS, ceValue, mt); |
1002 |
|
} |
1003 |
|
else |
1004 |
|
{ |
1005 |
124 |
rho = nm->mkNode(MINUS, mt, ceValue); |
1006 |
|
} |
1007 |
298 |
rho = rewrite(rho); |
1008 |
596 |
Trace("cegqi-arith-bound2") |
1009 |
298 |
<< "...rho = " << me << " - " << mt << " = " << rho << std::endl; |
1010 |
596 |
Trace("cegqi-arith-bound2") |
1011 |
298 |
<< "..." << rho << " mod " << new_theta << " = "; |
1012 |
298 |
rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); |
1013 |
298 |
rho = rewrite(rho); |
1014 |
298 |
Trace("cegqi-arith-bound2") << rho << std::endl; |
1015 |
298 |
Kind rk = isLower ? PLUS : MINUS; |
1016 |
298 |
val = nm->mkNode(rk, val, rho); |
1017 |
298 |
val = rewrite(val); |
1018 |
298 |
Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; |
1019 |
|
} |
1020 |
12758 |
if (!inf_coeff.isNull()) |
1021 |
|
{ |
1022 |
|
Assert(!d_vts_sym[0].isNull()); |
1023 |
|
val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); |
1024 |
|
val = rewrite(val); |
1025 |
|
} |
1026 |
12758 |
if (!delta_coeff.isNull()) |
1027 |
|
{ |
1028 |
|
// create delta here if necessary |
1029 |
115 |
val = nm->mkNode( |
1030 |
230 |
PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); |
1031 |
115 |
val = rewrite(val); |
1032 |
|
} |
1033 |
25516 |
return val; |
1034 |
|
} |
1035 |
|
|
1036 |
|
} // namespace quantifiers |
1037 |
|
} // namespace theory |
1038 |
31137 |
} // namespace cvc5 |