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