1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Tim King |
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 |
|
* Check for monomial bound inference lemmas. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/ext/monomial_bounds_check.h" |
17 |
|
|
18 |
|
#include "expr/node.h" |
19 |
|
#include "options/arith_options.h" |
20 |
|
#include "proof/proof.h" |
21 |
|
#include "theory/arith/arith_msum.h" |
22 |
|
#include "theory/arith/arith_utilities.h" |
23 |
|
#include "theory/arith/inference_manager.h" |
24 |
|
#include "theory/arith/nl/ext/ext_state.h" |
25 |
|
#include "theory/arith/nl/nl_model.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace arith { |
31 |
|
namespace nl { |
32 |
|
|
33 |
|
namespace { |
34 |
|
void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) |
35 |
|
{ |
36 |
|
Node t = ArithMSum::mkCoeffTerm(coeff, x); |
37 |
|
Trace(c) << t << " " << type << " " << rhs; |
38 |
|
} |
39 |
|
|
40 |
4195 |
bool hasNewMonomials(Node n, const std::vector<Node>& existing) |
41 |
|
{ |
42 |
8390 |
std::set<Node> visited; |
43 |
|
|
44 |
8390 |
std::vector<Node> worklist; |
45 |
4195 |
worklist.push_back(n); |
46 |
79823 |
while (!worklist.empty()) |
47 |
|
{ |
48 |
78811 |
Node current = worklist.back(); |
49 |
40997 |
worklist.pop_back(); |
50 |
40997 |
if (visited.find(current) == visited.end()) |
51 |
|
{ |
52 |
37955 |
visited.insert(current); |
53 |
37955 |
if (current.getKind() == Kind::NONLINEAR_MULT) |
54 |
|
{ |
55 |
18603 |
if (std::find(existing.begin(), existing.end(), current) |
56 |
18603 |
== existing.end()) |
57 |
|
{ |
58 |
3183 |
return true; |
59 |
|
} |
60 |
|
} |
61 |
|
else |
62 |
|
{ |
63 |
31754 |
worklist.insert(worklist.end(), current.begin(), current.end()); |
64 |
|
} |
65 |
|
} |
66 |
|
} |
67 |
1012 |
return false; |
68 |
|
} |
69 |
|
} // namespace |
70 |
|
|
71 |
9700 |
MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data) |
72 |
9700 |
: d_data(data), d_cdb(d_data->d_mdb) |
73 |
|
{ |
74 |
9700 |
} |
75 |
|
|
76 |
4188 |
void MonomialBoundsCheck::init() |
77 |
|
{ |
78 |
4188 |
d_ci.clear(); |
79 |
4188 |
d_ci_exp.clear(); |
80 |
4188 |
d_ci_max.clear(); |
81 |
4188 |
} |
82 |
|
|
83 |
762 |
void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts, |
84 |
|
const std::vector<Node>& false_asserts) |
85 |
|
{ |
86 |
|
// sort monomials by degree |
87 |
762 |
Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl; |
88 |
762 |
d_data->d_mdb.sortByDegree(d_data->d_ms); |
89 |
|
// all monomials |
90 |
3048 |
d_data->d_mterms.insert(d_data->d_mterms.end(), |
91 |
762 |
d_data->d_ms_vars.begin(), |
92 |
3048 |
d_data->d_ms_vars.end()); |
93 |
1524 |
d_data->d_mterms.insert( |
94 |
1524 |
d_data->d_mterms.end(), d_data->d_ms.begin(), d_data->d_ms.end()); |
95 |
|
|
96 |
|
const std::map<Node, std::map<Node, ConstraintInfo> >& cim = |
97 |
762 |
d_cdb.getConstraints(); |
98 |
|
|
99 |
762 |
NodeManager* nm = NodeManager::currentNM(); |
100 |
|
// register constraints |
101 |
762 |
Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; |
102 |
61586 |
for (const Node& lit : asserts) |
103 |
|
{ |
104 |
60824 |
bool polarity = lit.getKind() != Kind::NOT; |
105 |
121648 |
Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit; |
106 |
60824 |
d_cdb.registerConstraint(atom); |
107 |
|
bool is_false_lit = |
108 |
121648 |
std::find(false_asserts.begin(), false_asserts.end(), lit) |
109 |
182472 |
!= false_asserts.end(); |
110 |
|
// add information about bounds to variables |
111 |
|
std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc = |
112 |
60824 |
cim.find(atom); |
113 |
60824 |
if (itc == cim.end()) |
114 |
|
{ |
115 |
|
continue; |
116 |
|
} |
117 |
167662 |
for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second) |
118 |
|
{ |
119 |
213676 |
Node x = itcc.first; |
120 |
213676 |
Node coeff = itcc.second.d_coeff; |
121 |
213676 |
Node rhs = itcc.second.d_rhs; |
122 |
106838 |
Kind type = itcc.second.d_type; |
123 |
213676 |
Node exp = lit; |
124 |
106838 |
if (!polarity) |
125 |
|
{ |
126 |
|
// reverse |
127 |
60432 |
if (type == Kind::EQUAL) |
128 |
|
{ |
129 |
|
// we will take the strict inequality in the direction of the |
130 |
|
// model |
131 |
48854 |
Node lhs = ArithMSum::mkCoeffTerm(coeff, x); |
132 |
48854 |
Node query = nm->mkNode(Kind::GT, lhs, rhs); |
133 |
48854 |
Node query_mv = d_data->d_model.computeAbstractModelValue(query); |
134 |
24427 |
if (query_mv == d_data->d_true) |
135 |
|
{ |
136 |
15299 |
exp = query; |
137 |
15299 |
type = Kind::GT; |
138 |
|
} |
139 |
|
else |
140 |
|
{ |
141 |
9128 |
Assert(query_mv == d_data->d_false); |
142 |
9128 |
exp = nm->mkNode(Kind::LT, lhs, rhs); |
143 |
9128 |
type = Kind::LT; |
144 |
|
} |
145 |
|
} |
146 |
|
else |
147 |
|
{ |
148 |
36005 |
type = negateKind(type); |
149 |
|
} |
150 |
|
} |
151 |
|
// add to status if maximal degree |
152 |
106838 |
d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x); |
153 |
106838 |
if (Trace.isOn("nl-ext-bound-debug2")) |
154 |
|
{ |
155 |
|
Node t = ArithMSum::mkCoeffTerm(coeff, x); |
156 |
|
Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " " |
157 |
|
<< rhs << " by " << exp << std::endl; |
158 |
|
} |
159 |
106838 |
bool updated = true; |
160 |
106838 |
std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs); |
161 |
106838 |
if (its == d_ci[x][coeff].end()) |
162 |
|
{ |
163 |
93487 |
d_ci[x][coeff][rhs] = type; |
164 |
93487 |
d_ci_exp[x][coeff][rhs] = exp; |
165 |
|
} |
166 |
13351 |
else if (type != its->second) |
167 |
|
{ |
168 |
9024 |
Trace("nl-ext-bound-debug2") |
169 |
4512 |
<< "Joining kinds : " << type << " " << its->second << std::endl; |
170 |
4512 |
Kind jk = joinKinds(type, its->second); |
171 |
4512 |
if (jk == Kind::UNDEFINED_KIND) |
172 |
|
{ |
173 |
|
updated = false; |
174 |
|
} |
175 |
4512 |
else if (jk != its->second) |
176 |
|
{ |
177 |
2757 |
if (jk == type) |
178 |
|
{ |
179 |
2745 |
d_ci[x][coeff][rhs] = type; |
180 |
2745 |
d_ci_exp[x][coeff][rhs] = exp; |
181 |
|
} |
182 |
|
else |
183 |
|
{ |
184 |
12 |
d_ci[x][coeff][rhs] = jk; |
185 |
12 |
d_ci_exp[x][coeff][rhs] = |
186 |
24 |
nm->mkNode(Kind::AND, d_ci_exp[x][coeff][rhs], exp); |
187 |
|
} |
188 |
|
} |
189 |
|
else |
190 |
|
{ |
191 |
1755 |
updated = false; |
192 |
|
} |
193 |
|
} |
194 |
106838 |
if (Trace.isOn("nl-ext-bound")) |
195 |
|
{ |
196 |
|
if (updated) |
197 |
|
{ |
198 |
|
Trace("nl-ext-bound") << "Bound: "; |
199 |
|
debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs); |
200 |
|
Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs]; |
201 |
|
if (d_ci_max[x][coeff][rhs]) |
202 |
|
{ |
203 |
|
Trace("nl-ext-bound") << ", is max degree"; |
204 |
|
} |
205 |
|
Trace("nl-ext-bound") << std::endl; |
206 |
|
} |
207 |
|
} |
208 |
|
// compute if bound is not satisfied, and store what is required |
209 |
|
// for a possible refinement |
210 |
106838 |
if (d_data->d_env.getOptions().arith.nlExtTangentPlanes) |
211 |
|
{ |
212 |
7427 |
if (is_false_lit) |
213 |
|
{ |
214 |
1649 |
d_data->d_tplane_refine.insert(x); |
215 |
|
} |
216 |
|
} |
217 |
|
} |
218 |
|
} |
219 |
|
// reflexive constraints |
220 |
1524 |
Node null_coeff; |
221 |
6063 |
for (unsigned j = 0; j < d_data->d_mterms.size(); j++) |
222 |
|
{ |
223 |
10602 |
Node n = d_data->d_mterms[j]; |
224 |
5301 |
d_ci[n][null_coeff][n] = Kind::EQUAL; |
225 |
5301 |
d_ci_exp[n][null_coeff][n] = d_data->d_true; |
226 |
5301 |
d_ci_max[n][null_coeff][n] = false; |
227 |
|
} |
228 |
|
|
229 |
762 |
Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; |
230 |
|
const std::map<Node, std::vector<Node> >& cpMap = |
231 |
762 |
d_data->d_mdb.getContainsParentMap(); |
232 |
6063 |
for (unsigned k = 0; k < d_data->d_mterms.size(); k++) |
233 |
|
{ |
234 |
7578 |
Node x = d_data->d_mterms[k]; |
235 |
10602 |
Trace("nl-ext-bound-debug") |
236 |
5301 |
<< "Process bounds for " << x << " : " << std::endl; |
237 |
5301 |
std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x); |
238 |
8325 |
if (itm == cpMap.end()) |
239 |
|
{ |
240 |
3024 |
Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; |
241 |
3024 |
continue; |
242 |
|
} |
243 |
4554 |
Trace("nl-ext-bound-debug") |
244 |
2277 |
<< "...has " << itm->second.size() << " parent monomials." << std::endl; |
245 |
|
// check derived bounds |
246 |
|
std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc = |
247 |
2277 |
d_ci.find(x); |
248 |
2277 |
if (itc == d_ci.end()) |
249 |
|
{ |
250 |
|
continue; |
251 |
|
} |
252 |
4170 |
for (std::map<Node, std::map<Node, Kind> >::iterator itcc = |
253 |
2277 |
itc->second.begin(); |
254 |
6447 |
itcc != itc->second.end(); |
255 |
|
++itcc) |
256 |
|
{ |
257 |
8340 |
Node coeff = itcc->first; |
258 |
8340 |
Node t = ArithMSum::mkCoeffTerm(coeff, x); |
259 |
40575 |
for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); |
260 |
40575 |
itcr != itcc->second.end(); |
261 |
|
++itcr) |
262 |
|
{ |
263 |
55440 |
Node rhs = itcr->first; |
264 |
|
// only consider this bound if maximal degree |
265 |
36405 |
if (!d_ci_max[x][coeff][rhs]) |
266 |
|
{ |
267 |
17370 |
continue; |
268 |
|
} |
269 |
19035 |
Kind type = itcr->second; |
270 |
87747 |
for (unsigned j = 0; j < itm->second.size(); j++) |
271 |
|
{ |
272 |
129222 |
Node y = itm->second[j]; |
273 |
129222 |
Node mult = d_data->d_mdb.getContainsDiff(x, y); |
274 |
|
// x <k> t => m*x <k'> t where y = m*x |
275 |
|
// get the sign of mult |
276 |
129222 |
Node mmv = d_data->d_model.computeConcreteModelValue(mult); |
277 |
137424 |
Trace("nl-ext-bound-debug2") |
278 |
68712 |
<< "Model value of " << mult << " is " << mmv << std::endl; |
279 |
69354 |
if (!mmv.isConst()) |
280 |
|
{ |
281 |
1284 |
Trace("nl-ext-bound-debug") |
282 |
642 |
<< " ...coefficient " << mult |
283 |
642 |
<< " is non-constant (probably transcendental)." << std::endl; |
284 |
642 |
continue; |
285 |
|
} |
286 |
68070 |
int mmv_sign = mmv.getConst<Rational>().sgn(); |
287 |
136140 |
Trace("nl-ext-bound-debug2") |
288 |
68070 |
<< " sign of " << mmv << " is " << mmv_sign << std::endl; |
289 |
75630 |
if (mmv_sign == 0) |
290 |
|
{ |
291 |
15120 |
Trace("nl-ext-bound-debug") |
292 |
7560 |
<< " ...coefficient " << mult << " is zero." << std::endl; |
293 |
7560 |
continue; |
294 |
|
} |
295 |
121020 |
Trace("nl-ext-bound-debug") |
296 |
60510 |
<< " from " << x << " * " << mult << " = " << y << " and " << t |
297 |
60510 |
<< " " << type << " " << rhs << ", infer : " << std::endl; |
298 |
60510 |
Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type; |
299 |
121020 |
Node infer_lhs = nm->mkNode(Kind::MULT, mult, t); |
300 |
121020 |
Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs); |
301 |
121020 |
Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs); |
302 |
60510 |
Trace("nl-ext-bound-debug") << " " << infer << std::endl; |
303 |
121020 |
Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer)); |
304 |
121020 |
Trace("nl-ext-bound-debug") |
305 |
60510 |
<< " ...infer model value is " << infer_mv << std::endl; |
306 |
60510 |
if (infer_mv == d_data->d_false) |
307 |
|
{ |
308 |
|
Node exp = nm->mkNode( |
309 |
|
Kind::AND, |
310 |
12585 |
nm->mkNode( |
311 |
8390 |
mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero), |
312 |
16780 |
d_ci_exp[x][coeff][rhs]); |
313 |
8390 |
Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer); |
314 |
8390 |
Node iblem_rw = Rewriter::rewrite(iblem); |
315 |
4195 |
bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms); |
316 |
8390 |
Trace("nl-ext-bound-lemma") |
317 |
4195 |
<< "*** Bound inference lemma : " << iblem_rw |
318 |
4195 |
<< " (pre-rewrite : " << iblem << ")" << std::endl; |
319 |
4195 |
CDProof* proof = nullptr; |
320 |
8390 |
Node orig = d_ci_exp[x][coeff][rhs]; |
321 |
4195 |
if (d_data->isProofEnabled()) |
322 |
|
{ |
323 |
615 |
proof = d_data->getProof(); |
324 |
1230 |
Node simpleeq = nm->mkNode(type, t, rhs); |
325 |
|
// this is iblem, but uses (type t rhs) instead of the original |
326 |
|
// variant (which is identical under rewriting) |
327 |
|
// we first infer the "clean" version of the lemma and then |
328 |
|
// use MACRO_SR_PRED_TRANSFORM to rewrite |
329 |
|
Node tmplem = nm->mkNode(Kind::IMPLIES, |
330 |
1230 |
nm->mkNode(Kind::AND, exp[0], simpleeq), |
331 |
2460 |
infer); |
332 |
2460 |
proof->addStep(tmplem, |
333 |
615 |
mmv_sign == 1 ? PfRule::ARITH_MULT_POS |
334 |
|
: PfRule::ARITH_MULT_NEG, |
335 |
|
{}, |
336 |
1230 |
{mult, simpleeq}); |
337 |
615 |
theory::Rewriter* rew = d_data->d_env.getRewriter(); |
338 |
1230 |
if (type == Kind::EQUAL |
339 |
1230 |
&& (rew->rewrite(simpleeq) != rew->rewrite(exp[1]))) |
340 |
|
{ |
341 |
|
// it is not identical under rewriting and we need to do some work here |
342 |
|
// The proof looks like this: |
343 |
|
// (SCOPE |
344 |
|
// (MODUS_PONENS |
345 |
|
// <tmplem> |
346 |
|
// (AND_INTRO |
347 |
|
// <first premise of iblem> |
348 |
|
// (ARITH_TRICHOTOMY *** |
349 |
|
// (AND_ELIM <second premise of iblem> 1) |
350 |
|
// (AND_ELIM <second premise of iblem> 2) |
351 |
|
// ) |
352 |
|
// ) |
353 |
|
// ) |
354 |
|
// :args <the two premises of iblem> |
355 |
|
// ) |
356 |
|
// ***: the result of the AND_ELIM are rewritten forms of what |
357 |
|
// ARITH_TRICHOTOMY expects, and also their order is not clear. |
358 |
|
// Hence, we apply MACRO_SR_PRED_TRANSFORM to them, and check |
359 |
|
// which corresponds to which subterm of the premise. |
360 |
18 |
proof->addStep(exp[1][0], |
361 |
|
PfRule::AND_ELIM, |
362 |
|
{exp[1]}, |
363 |
24 |
{nm->mkConst(Rational(0))}); |
364 |
18 |
proof->addStep(exp[1][1], |
365 |
|
PfRule::AND_ELIM, |
366 |
|
{exp[1]}, |
367 |
24 |
{nm->mkConst(Rational(1))}); |
368 |
12 |
Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]); |
369 |
12 |
Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]); |
370 |
6 |
if (rew->rewrite(lb) == rew->rewrite(exp[1][0])) |
371 |
|
{ |
372 |
6 |
proof->addStep( |
373 |
4 |
lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {lb}); |
374 |
6 |
proof->addStep( |
375 |
4 |
rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {rb}); |
376 |
|
} |
377 |
|
else |
378 |
|
{ |
379 |
12 |
proof->addStep( |
380 |
8 |
lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {lb}); |
381 |
12 |
proof->addStep( |
382 |
8 |
rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {rb}); |
383 |
|
} |
384 |
24 |
proof->addStep( |
385 |
18 |
simpleeq, PfRule::ARITH_TRICHOTOMY, {lb, rb}, {simpleeq}); |
386 |
18 |
proof->addStep( |
387 |
12 |
tmplem[0], PfRule::AND_INTRO, {exp[0], simpleeq}, {}); |
388 |
18 |
proof->addStep( |
389 |
12 |
tmplem[1], PfRule::MODUS_PONENS, {tmplem[0], tmplem}, {}); |
390 |
24 |
proof->addStep( |
391 |
18 |
iblem, PfRule::SCOPE, {tmplem[1]}, {exp[0], exp[1]}); |
392 |
|
} |
393 |
|
else |
394 |
|
{ |
395 |
1827 |
proof->addStep( |
396 |
1218 |
iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem}); |
397 |
|
} |
398 |
|
} |
399 |
4195 |
d_data->d_im.addPendingLemma(iblem, |
400 |
|
InferenceId::ARITH_NL_INFER_BOUNDS_NT, |
401 |
|
proof, |
402 |
|
introNewTerms); |
403 |
|
} |
404 |
|
} |
405 |
|
} |
406 |
|
} |
407 |
|
} |
408 |
762 |
} |
409 |
|
|
410 |
|
void MonomialBoundsCheck::checkResBounds() |
411 |
|
{ |
412 |
|
NodeManager* nm = NodeManager::currentNM(); |
413 |
|
Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." |
414 |
|
<< std::endl; |
415 |
|
size_t nmterms = d_data->d_mterms.size(); |
416 |
|
for (unsigned j = 0; j < nmterms; j++) |
417 |
|
{ |
418 |
|
Node a = d_data->d_mterms[j]; |
419 |
|
std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = |
420 |
|
d_ci.find(a); |
421 |
|
if (itca == d_ci.end()) |
422 |
|
{ |
423 |
|
continue; |
424 |
|
} |
425 |
|
for (unsigned k = (j + 1); k < nmterms; k++) |
426 |
|
{ |
427 |
|
Node b = d_data->d_mterms[k]; |
428 |
|
std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb = |
429 |
|
d_ci.find(b); |
430 |
|
if (itcb == d_ci.end()) |
431 |
|
{ |
432 |
|
continue; |
433 |
|
} |
434 |
|
Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a |
435 |
|
<< " and " << b << std::endl; |
436 |
|
// if they have common factors |
437 |
|
std::map<Node, Node>::iterator ita = d_data->d_mono_diff[a].find(b); |
438 |
|
if (ita == d_data->d_mono_diff[a].end()) |
439 |
|
{ |
440 |
|
continue; |
441 |
|
} |
442 |
|
Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a |
443 |
|
<< " vs [b] " << b << std::endl; |
444 |
|
std::map<Node, Node>::iterator itb = d_data->d_mono_diff[b].find(a); |
445 |
|
Assert(itb != d_data->d_mono_diff[b].end()); |
446 |
|
Node mv_a = d_data->d_model.computeAbstractModelValue(ita->second); |
447 |
|
Assert(mv_a.isConst()); |
448 |
|
int mv_a_sgn = mv_a.getConst<Rational>().sgn(); |
449 |
|
if (mv_a_sgn == 0) |
450 |
|
{ |
451 |
|
// we don't compare monomials whose current model value is zero |
452 |
|
continue; |
453 |
|
} |
454 |
|
Node mv_b = d_data->d_model.computeAbstractModelValue(itb->second); |
455 |
|
Assert(mv_b.isConst()); |
456 |
|
int mv_b_sgn = mv_b.getConst<Rational>().sgn(); |
457 |
|
if (mv_b_sgn == 0) |
458 |
|
{ |
459 |
|
// we don't compare monomials whose current model value is zero |
460 |
|
continue; |
461 |
|
} |
462 |
|
Trace("nl-ext-rbound") << " [a] factor is " << ita->second |
463 |
|
<< ", sign in model = " << mv_a_sgn << std::endl; |
464 |
|
Trace("nl-ext-rbound") << " [b] factor is " << itb->second |
465 |
|
<< ", sign in model = " << mv_b_sgn << std::endl; |
466 |
|
|
467 |
|
std::vector<Node> exp; |
468 |
|
// bounds of a |
469 |
|
for (std::map<Node, std::map<Node, Kind> >::iterator itcac = |
470 |
|
itca->second.begin(); |
471 |
|
itcac != itca->second.end(); |
472 |
|
++itcac) |
473 |
|
{ |
474 |
|
Node coeff_a = itcac->first; |
475 |
|
for (std::map<Node, Kind>::iterator itcar = itcac->second.begin(); |
476 |
|
itcar != itcac->second.end(); |
477 |
|
++itcar) |
478 |
|
{ |
479 |
|
Node rhs_a = itcar->first; |
480 |
|
Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a); |
481 |
|
rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); |
482 |
|
if (hasNewMonomials(rhs_a_res_base, d_data->d_ms)) |
483 |
|
{ |
484 |
|
continue; |
485 |
|
} |
486 |
|
Kind type_a = itcar->second; |
487 |
|
exp.push_back(d_ci_exp[a][coeff_a][rhs_a]); |
488 |
|
|
489 |
|
// bounds of b |
490 |
|
for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = |
491 |
|
itcb->second.begin(); |
492 |
|
itcbc != itcb->second.end(); |
493 |
|
++itcbc) |
494 |
|
{ |
495 |
|
Node coeff_b = itcbc->first; |
496 |
|
Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base); |
497 |
|
for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin(); |
498 |
|
itcbr != itcbc->second.end(); |
499 |
|
++itcbr) |
500 |
|
{ |
501 |
|
Node rhs_b = itcbr->first; |
502 |
|
Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b); |
503 |
|
rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res); |
504 |
|
rhs_b_res = Rewriter::rewrite(rhs_b_res); |
505 |
|
if (hasNewMonomials(rhs_b_res, d_data->d_ms)) |
506 |
|
{ |
507 |
|
continue; |
508 |
|
} |
509 |
|
Kind type_b = itcbr->second; |
510 |
|
exp.push_back(d_ci_exp[b][coeff_b][rhs_b]); |
511 |
|
if (Trace.isOn("nl-ext-rbound")) |
512 |
|
{ |
513 |
|
Trace("nl-ext-rbound") << "* try bounds : "; |
514 |
|
debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a); |
515 |
|
Trace("nl-ext-rbound") << std::endl; |
516 |
|
Trace("nl-ext-rbound") << " "; |
517 |
|
debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b); |
518 |
|
Trace("nl-ext-rbound") << std::endl; |
519 |
|
} |
520 |
|
Kind types[2]; |
521 |
|
for (unsigned r = 0; r < 2; r++) |
522 |
|
{ |
523 |
|
Node pivot_factor = r == 0 ? itb->second : ita->second; |
524 |
|
int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn; |
525 |
|
types[r] = r == 0 ? type_a : type_b; |
526 |
|
if (pivot_factor_sign == (r == 0 ? 1 : -1)) |
527 |
|
{ |
528 |
|
types[r] = reverseRelationKind(types[r]); |
529 |
|
} |
530 |
|
if (pivot_factor_sign == 1) |
531 |
|
{ |
532 |
|
exp.push_back( |
533 |
|
nm->mkNode(Kind::GT, pivot_factor, d_data->d_zero)); |
534 |
|
} |
535 |
|
else |
536 |
|
{ |
537 |
|
exp.push_back( |
538 |
|
nm->mkNode(Kind::LT, pivot_factor, d_data->d_zero)); |
539 |
|
} |
540 |
|
} |
541 |
|
Kind jk = transKinds(types[0], types[1]); |
542 |
|
Trace("nl-ext-rbound-debug") |
543 |
|
<< "trans kind : " << types[0] << " + " << types[1] << " = " |
544 |
|
<< jk << std::endl; |
545 |
|
if (jk != Kind::UNDEFINED_KIND) |
546 |
|
{ |
547 |
|
Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res); |
548 |
|
Node conc_mv = d_data->d_model.computeAbstractModelValue(conc); |
549 |
|
if (conc_mv == d_data->d_false) |
550 |
|
{ |
551 |
|
Node rblem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc); |
552 |
|
Trace("nl-ext-rbound-lemma-debug") |
553 |
|
<< "Resolution bound lemma " |
554 |
|
"(pre-rewrite) " |
555 |
|
": " |
556 |
|
<< rblem << std::endl; |
557 |
|
rblem = Rewriter::rewrite(rblem); |
558 |
|
Trace("nl-ext-rbound-lemma") |
559 |
|
<< "Resolution bound lemma : " << rblem << std::endl; |
560 |
|
d_data->d_im.addPendingLemma( |
561 |
|
rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS); |
562 |
|
} |
563 |
|
} |
564 |
|
exp.pop_back(); |
565 |
|
exp.pop_back(); |
566 |
|
exp.pop_back(); |
567 |
|
} |
568 |
|
} |
569 |
|
exp.pop_back(); |
570 |
|
} |
571 |
|
} |
572 |
|
} |
573 |
|
} |
574 |
|
} |
575 |
|
|
576 |
|
} // namespace nl |
577 |
|
} // namespace arith |
578 |
|
} // namespace theory |
579 |
31125 |
} // namespace cvc5 |