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 |
4890 |
bool hasNewMonomials(Node n, const std::vector<Node>& existing) |
41 |
|
{ |
42 |
9780 |
std::set<Node> visited; |
43 |
|
|
44 |
9780 |
std::vector<Node> worklist; |
45 |
4890 |
worklist.push_back(n); |
46 |
94100 |
while (!worklist.empty()) |
47 |
|
{ |
48 |
92866 |
Node current = worklist.back(); |
49 |
48261 |
worklist.pop_back(); |
50 |
48261 |
if (visited.find(current) == visited.end()) |
51 |
|
{ |
52 |
44339 |
visited.insert(current); |
53 |
44339 |
if (current.getKind() == Kind::NONLINEAR_MULT) |
54 |
|
{ |
55 |
22029 |
if (std::find(existing.begin(), existing.end(), current) |
56 |
22029 |
== existing.end()) |
57 |
|
{ |
58 |
3656 |
return true; |
59 |
|
} |
60 |
|
} |
61 |
|
else |
62 |
|
{ |
63 |
36996 |
worklist.insert(worklist.end(), current.begin(), current.end()); |
64 |
|
} |
65 |
|
} |
66 |
|
} |
67 |
1234 |
return false; |
68 |
|
} |
69 |
|
} // namespace |
70 |
|
|
71 |
9696 |
MonomialBoundsCheck::MonomialBoundsCheck(Env& env, ExtState* data) |
72 |
9696 |
: EnvObj(env), d_data(data), d_cdb(d_data->d_mdb) |
73 |
|
{ |
74 |
9696 |
} |
75 |
|
|
76 |
4364 |
void MonomialBoundsCheck::init() |
77 |
|
{ |
78 |
4364 |
d_ci.clear(); |
79 |
4364 |
d_ci_exp.clear(); |
80 |
4364 |
d_ci_max.clear(); |
81 |
4364 |
} |
82 |
|
|
83 |
788 |
void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts, |
84 |
|
const std::vector<Node>& false_asserts) |
85 |
|
{ |
86 |
|
// sort monomials by degree |
87 |
788 |
Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl; |
88 |
788 |
d_data->d_mdb.sortByDegree(d_data->d_ms); |
89 |
|
// all monomials |
90 |
3152 |
d_data->d_mterms.insert(d_data->d_mterms.end(), |
91 |
788 |
d_data->d_ms_vars.begin(), |
92 |
3152 |
d_data->d_ms_vars.end()); |
93 |
1576 |
d_data->d_mterms.insert( |
94 |
1576 |
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 |
788 |
d_cdb.getConstraints(); |
98 |
|
|
99 |
788 |
NodeManager* nm = NodeManager::currentNM(); |
100 |
|
// register constraints |
101 |
788 |
Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; |
102 |
90358 |
for (const Node& lit : asserts) |
103 |
|
{ |
104 |
89570 |
bool polarity = lit.getKind() != Kind::NOT; |
105 |
179140 |
Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit; |
106 |
89570 |
d_cdb.registerConstraint(atom); |
107 |
|
bool is_false_lit = |
108 |
179140 |
std::find(false_asserts.begin(), false_asserts.end(), lit) |
109 |
268710 |
!= false_asserts.end(); |
110 |
|
// add information about bounds to variables |
111 |
|
std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc = |
112 |
89570 |
cim.find(atom); |
113 |
89570 |
if (itc == cim.end()) |
114 |
|
{ |
115 |
|
continue; |
116 |
|
} |
117 |
250905 |
for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second) |
118 |
|
{ |
119 |
322670 |
Node x = itcc.first; |
120 |
322670 |
Node coeff = itcc.second.d_coeff; |
121 |
322670 |
Node rhs = itcc.second.d_rhs; |
122 |
161335 |
Kind type = itcc.second.d_type; |
123 |
322670 |
Node exp = lit; |
124 |
161335 |
if (!polarity) |
125 |
|
{ |
126 |
|
// reverse |
127 |
79482 |
if (type == Kind::EQUAL) |
128 |
|
{ |
129 |
|
// we will take the strict inequality in the direction of the |
130 |
|
// model |
131 |
56864 |
Node lhs = ArithMSum::mkCoeffTerm(coeff, x); |
132 |
56864 |
Node query = nm->mkNode(Kind::GT, lhs, rhs); |
133 |
56864 |
Node query_mv = d_data->d_model.computeAbstractModelValue(query); |
134 |
28432 |
if (query_mv == d_data->d_true) |
135 |
|
{ |
136 |
17604 |
exp = query; |
137 |
17604 |
type = Kind::GT; |
138 |
|
} |
139 |
|
else |
140 |
|
{ |
141 |
10828 |
Assert(query_mv == d_data->d_false); |
142 |
10828 |
exp = nm->mkNode(Kind::LT, lhs, rhs); |
143 |
10828 |
type = Kind::LT; |
144 |
|
} |
145 |
|
} |
146 |
|
else |
147 |
|
{ |
148 |
51050 |
type = negateKind(type); |
149 |
|
} |
150 |
|
} |
151 |
|
// add to status if maximal degree |
152 |
161335 |
d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x); |
153 |
161335 |
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 |
161335 |
bool updated = true; |
160 |
161335 |
std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs); |
161 |
161335 |
if (its == d_ci[x][coeff].end()) |
162 |
|
{ |
163 |
145601 |
d_ci[x][coeff][rhs] = type; |
164 |
145601 |
d_ci_exp[x][coeff][rhs] = exp; |
165 |
|
} |
166 |
15734 |
else if (type != its->second) |
167 |
|
{ |
168 |
11336 |
Trace("nl-ext-bound-debug2") |
169 |
5668 |
<< "Joining kinds : " << type << " " << its->second << std::endl; |
170 |
5668 |
Kind jk = joinKinds(type, its->second); |
171 |
5668 |
if (jk == Kind::UNDEFINED_KIND) |
172 |
|
{ |
173 |
|
updated = false; |
174 |
|
} |
175 |
5668 |
else if (jk != its->second) |
176 |
|
{ |
177 |
3166 |
if (jk == type) |
178 |
|
{ |
179 |
3154 |
d_ci[x][coeff][rhs] = type; |
180 |
3154 |
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 |
2502 |
updated = false; |
192 |
|
} |
193 |
|
} |
194 |
161335 |
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 |
161335 |
if (d_data->d_env.getOptions().arith.nlExtTangentPlanes) |
211 |
|
{ |
212 |
18339 |
if (is_false_lit) |
213 |
|
{ |
214 |
1845 |
d_data->d_tplane_refine.insert(x); |
215 |
|
} |
216 |
|
} |
217 |
|
} |
218 |
|
} |
219 |
|
// reflexive constraints |
220 |
1576 |
Node null_coeff; |
221 |
8245 |
for (unsigned j = 0; j < d_data->d_mterms.size(); j++) |
222 |
|
{ |
223 |
14914 |
Node n = d_data->d_mterms[j]; |
224 |
7457 |
d_ci[n][null_coeff][n] = Kind::EQUAL; |
225 |
7457 |
d_ci_exp[n][null_coeff][n] = d_data->d_true; |
226 |
7457 |
d_ci_max[n][null_coeff][n] = false; |
227 |
|
} |
228 |
|
|
229 |
788 |
Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; |
230 |
|
const std::map<Node, std::vector<Node> >& cpMap = |
231 |
788 |
d_data->d_mdb.getContainsParentMap(); |
232 |
8245 |
for (unsigned k = 0; k < d_data->d_mterms.size(); k++) |
233 |
|
{ |
234 |
10189 |
Node x = d_data->d_mterms[k]; |
235 |
14914 |
Trace("nl-ext-bound-debug") |
236 |
7457 |
<< "Process bounds for " << x << " : " << std::endl; |
237 |
7457 |
std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x); |
238 |
12182 |
if (itm == cpMap.end()) |
239 |
|
{ |
240 |
4725 |
Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; |
241 |
4725 |
continue; |
242 |
|
} |
243 |
5464 |
Trace("nl-ext-bound-debug") |
244 |
2732 |
<< "...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 |
2732 |
d_ci.find(x); |
248 |
2732 |
if (itc == d_ci.end()) |
249 |
|
{ |
250 |
|
continue; |
251 |
|
} |
252 |
4902 |
for (std::map<Node, std::map<Node, Kind> >::iterator itcc = |
253 |
2732 |
itc->second.begin(); |
254 |
7634 |
itcc != itc->second.end(); |
255 |
|
++itcc) |
256 |
|
{ |
257 |
9804 |
Node coeff = itcc->first; |
258 |
9804 |
Node t = ArithMSum::mkCoeffTerm(coeff, x); |
259 |
59202 |
for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); |
260 |
59202 |
itcr != itcc->second.end(); |
261 |
|
++itcr) |
262 |
|
{ |
263 |
80904 |
Node rhs = itcr->first; |
264 |
|
// only consider this bound if maximal degree |
265 |
54300 |
if (!d_ci_max[x][coeff][rhs]) |
266 |
|
{ |
267 |
27696 |
continue; |
268 |
|
} |
269 |
26604 |
Kind type = itcr->second; |
270 |
162127 |
for (unsigned j = 0; j < itm->second.size(); j++) |
271 |
|
{ |
272 |
259446 |
Node y = itm->second[j]; |
273 |
259446 |
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 |
259446 |
Node mmv = d_data->d_model.computeConcreteModelValue(mult); |
277 |
271046 |
Trace("nl-ext-bound-debug2") |
278 |
135523 |
<< "Model value of " << mult << " is " << mmv << std::endl; |
279 |
136165 |
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 |
134881 |
int mmv_sign = mmv.getConst<Rational>().sgn(); |
287 |
269762 |
Trace("nl-ext-bound-debug2") |
288 |
134881 |
<< " sign of " << mmv << " is " << mmv_sign << std::endl; |
289 |
145839 |
if (mmv_sign == 0) |
290 |
|
{ |
291 |
21916 |
Trace("nl-ext-bound-debug") |
292 |
10958 |
<< " ...coefficient " << mult << " is zero." << std::endl; |
293 |
10958 |
continue; |
294 |
|
} |
295 |
247846 |
Trace("nl-ext-bound-debug") |
296 |
123923 |
<< " from " << x << " * " << mult << " = " << y << " and " << t |
297 |
123923 |
<< " " << type << " " << rhs << ", infer : " << std::endl; |
298 |
123923 |
Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type; |
299 |
247846 |
Node infer_lhs = nm->mkNode(Kind::MULT, mult, t); |
300 |
247846 |
Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs); |
301 |
247846 |
Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs); |
302 |
123923 |
Trace("nl-ext-bound-debug") << " " << infer << std::endl; |
303 |
|
Node infer_mv = |
304 |
247846 |
d_data->d_model.computeAbstractModelValue(rewrite(infer)); |
305 |
247846 |
Trace("nl-ext-bound-debug") |
306 |
123923 |
<< " ...infer model value is " << infer_mv << std::endl; |
307 |
123923 |
if (infer_mv == d_data->d_false) |
308 |
|
{ |
309 |
|
Node exp = nm->mkNode( |
310 |
|
Kind::AND, |
311 |
14670 |
nm->mkNode( |
312 |
9780 |
mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero), |
313 |
19560 |
d_ci_exp[x][coeff][rhs]); |
314 |
9780 |
Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer); |
315 |
9780 |
Node iblem_rw = rewrite(iblem); |
316 |
4890 |
bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms); |
317 |
9780 |
Trace("nl-ext-bound-lemma") |
318 |
4890 |
<< "*** Bound inference lemma : " << iblem_rw |
319 |
4890 |
<< " (pre-rewrite : " << iblem << ")" << std::endl; |
320 |
4890 |
CDProof* proof = nullptr; |
321 |
9780 |
Node orig = d_ci_exp[x][coeff][rhs]; |
322 |
4890 |
if (d_data->isProofEnabled()) |
323 |
|
{ |
324 |
690 |
proof = d_data->getProof(); |
325 |
1380 |
Node simpleeq = nm->mkNode(type, t, rhs); |
326 |
|
// this is iblem, but uses (type t rhs) instead of the original |
327 |
|
// variant (which is identical under rewriting) |
328 |
|
// we first infer the "clean" version of the lemma and then |
329 |
|
// use MACRO_SR_PRED_TRANSFORM to rewrite |
330 |
|
Node tmplem = nm->mkNode(Kind::IMPLIES, |
331 |
1380 |
nm->mkNode(Kind::AND, exp[0], simpleeq), |
332 |
2760 |
infer); |
333 |
2760 |
proof->addStep(tmplem, |
334 |
690 |
mmv_sign == 1 ? PfRule::ARITH_MULT_POS |
335 |
|
: PfRule::ARITH_MULT_NEG, |
336 |
|
{}, |
337 |
1380 |
{mult, simpleeq}); |
338 |
690 |
theory::Rewriter* rew = d_data->d_env.getRewriter(); |
339 |
1380 |
if (type == Kind::EQUAL |
340 |
1380 |
&& (rew->rewrite(simpleeq) != rew->rewrite(exp[1]))) |
341 |
|
{ |
342 |
|
// it is not identical under rewriting and we need to do some work here |
343 |
|
// The proof looks like this: |
344 |
|
// (SCOPE |
345 |
|
// (MODUS_PONENS |
346 |
|
// <tmplem> |
347 |
|
// (AND_INTRO |
348 |
|
// <first premise of iblem> |
349 |
|
// (ARITH_TRICHOTOMY *** |
350 |
|
// (AND_ELIM <second premise of iblem> 1) |
351 |
|
// (AND_ELIM <second premise of iblem> 2) |
352 |
|
// ) |
353 |
|
// ) |
354 |
|
// ) |
355 |
|
// :args <the two premises of iblem> |
356 |
|
// ) |
357 |
|
// ***: the result of the AND_ELIM are rewritten forms of what |
358 |
|
// ARITH_TRICHOTOMY expects, and also their order is not clear. |
359 |
|
// Hence, we apply MACRO_SR_PRED_TRANSFORM to them, and check |
360 |
|
// which corresponds to which subterm of the premise. |
361 |
18 |
proof->addStep(exp[1][0], |
362 |
|
PfRule::AND_ELIM, |
363 |
|
{exp[1]}, |
364 |
24 |
{nm->mkConst(Rational(0))}); |
365 |
18 |
proof->addStep(exp[1][1], |
366 |
|
PfRule::AND_ELIM, |
367 |
|
{exp[1]}, |
368 |
24 |
{nm->mkConst(Rational(1))}); |
369 |
12 |
Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]); |
370 |
12 |
Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]); |
371 |
6 |
if (rew->rewrite(lb) == rew->rewrite(exp[1][0])) |
372 |
|
{ |
373 |
6 |
proof->addStep( |
374 |
4 |
lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {lb}); |
375 |
6 |
proof->addStep( |
376 |
4 |
rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {rb}); |
377 |
|
} |
378 |
|
else |
379 |
|
{ |
380 |
12 |
proof->addStep( |
381 |
8 |
lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {lb}); |
382 |
12 |
proof->addStep( |
383 |
8 |
rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {rb}); |
384 |
|
} |
385 |
24 |
proof->addStep( |
386 |
18 |
simpleeq, PfRule::ARITH_TRICHOTOMY, {lb, rb}, {simpleeq}); |
387 |
18 |
proof->addStep( |
388 |
12 |
tmplem[0], PfRule::AND_INTRO, {exp[0], simpleeq}, {}); |
389 |
18 |
proof->addStep( |
390 |
12 |
tmplem[1], PfRule::MODUS_PONENS, {tmplem[0], tmplem}, {}); |
391 |
24 |
proof->addStep( |
392 |
18 |
iblem, PfRule::SCOPE, {tmplem[1]}, {exp[0], exp[1]}); |
393 |
|
} |
394 |
|
else |
395 |
|
{ |
396 |
2052 |
proof->addStep( |
397 |
1368 |
iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem}); |
398 |
|
} |
399 |
|
} |
400 |
4890 |
d_data->d_im.addPendingLemma(iblem, |
401 |
|
InferenceId::ARITH_NL_INFER_BOUNDS_NT, |
402 |
|
proof, |
403 |
|
introNewTerms); |
404 |
|
} |
405 |
|
} |
406 |
|
} |
407 |
|
} |
408 |
|
} |
409 |
788 |
} |
410 |
|
|
411 |
|
void MonomialBoundsCheck::checkResBounds() |
412 |
|
{ |
413 |
|
NodeManager* nm = NodeManager::currentNM(); |
414 |
|
Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." |
415 |
|
<< std::endl; |
416 |
|
size_t nmterms = d_data->d_mterms.size(); |
417 |
|
for (unsigned j = 0; j < nmterms; j++) |
418 |
|
{ |
419 |
|
Node a = d_data->d_mterms[j]; |
420 |
|
std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = |
421 |
|
d_ci.find(a); |
422 |
|
if (itca == d_ci.end()) |
423 |
|
{ |
424 |
|
continue; |
425 |
|
} |
426 |
|
for (unsigned k = (j + 1); k < nmterms; k++) |
427 |
|
{ |
428 |
|
Node b = d_data->d_mterms[k]; |
429 |
|
std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb = |
430 |
|
d_ci.find(b); |
431 |
|
if (itcb == d_ci.end()) |
432 |
|
{ |
433 |
|
continue; |
434 |
|
} |
435 |
|
Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a |
436 |
|
<< " and " << b << std::endl; |
437 |
|
// if they have common factors |
438 |
|
std::map<Node, Node>::iterator ita = d_data->d_mono_diff[a].find(b); |
439 |
|
if (ita == d_data->d_mono_diff[a].end()) |
440 |
|
{ |
441 |
|
continue; |
442 |
|
} |
443 |
|
Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a |
444 |
|
<< " vs [b] " << b << std::endl; |
445 |
|
std::map<Node, Node>::iterator itb = d_data->d_mono_diff[b].find(a); |
446 |
|
Assert(itb != d_data->d_mono_diff[b].end()); |
447 |
|
Node mv_a = d_data->d_model.computeAbstractModelValue(ita->second); |
448 |
|
Assert(mv_a.isConst()); |
449 |
|
int mv_a_sgn = mv_a.getConst<Rational>().sgn(); |
450 |
|
if (mv_a_sgn == 0) |
451 |
|
{ |
452 |
|
// we don't compare monomials whose current model value is zero |
453 |
|
continue; |
454 |
|
} |
455 |
|
Node mv_b = d_data->d_model.computeAbstractModelValue(itb->second); |
456 |
|
Assert(mv_b.isConst()); |
457 |
|
int mv_b_sgn = mv_b.getConst<Rational>().sgn(); |
458 |
|
if (mv_b_sgn == 0) |
459 |
|
{ |
460 |
|
// we don't compare monomials whose current model value is zero |
461 |
|
continue; |
462 |
|
} |
463 |
|
Trace("nl-ext-rbound") << " [a] factor is " << ita->second |
464 |
|
<< ", sign in model = " << mv_a_sgn << std::endl; |
465 |
|
Trace("nl-ext-rbound") << " [b] factor is " << itb->second |
466 |
|
<< ", sign in model = " << mv_b_sgn << std::endl; |
467 |
|
|
468 |
|
std::vector<Node> exp; |
469 |
|
// bounds of a |
470 |
|
for (std::map<Node, std::map<Node, Kind> >::iterator itcac = |
471 |
|
itca->second.begin(); |
472 |
|
itcac != itca->second.end(); |
473 |
|
++itcac) |
474 |
|
{ |
475 |
|
Node coeff_a = itcac->first; |
476 |
|
for (std::map<Node, Kind>::iterator itcar = itcac->second.begin(); |
477 |
|
itcar != itcac->second.end(); |
478 |
|
++itcar) |
479 |
|
{ |
480 |
|
Node rhs_a = itcar->first; |
481 |
|
Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a); |
482 |
|
rhs_a_res_base = rewrite(rhs_a_res_base); |
483 |
|
if (hasNewMonomials(rhs_a_res_base, d_data->d_ms)) |
484 |
|
{ |
485 |
|
continue; |
486 |
|
} |
487 |
|
Kind type_a = itcar->second; |
488 |
|
exp.push_back(d_ci_exp[a][coeff_a][rhs_a]); |
489 |
|
|
490 |
|
// bounds of b |
491 |
|
for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = |
492 |
|
itcb->second.begin(); |
493 |
|
itcbc != itcb->second.end(); |
494 |
|
++itcbc) |
495 |
|
{ |
496 |
|
Node coeff_b = itcbc->first; |
497 |
|
Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base); |
498 |
|
for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin(); |
499 |
|
itcbr != itcbc->second.end(); |
500 |
|
++itcbr) |
501 |
|
{ |
502 |
|
Node rhs_b = itcbr->first; |
503 |
|
Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b); |
504 |
|
rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res); |
505 |
|
rhs_b_res = rewrite(rhs_b_res); |
506 |
|
if (hasNewMonomials(rhs_b_res, d_data->d_ms)) |
507 |
|
{ |
508 |
|
continue; |
509 |
|
} |
510 |
|
Kind type_b = itcbr->second; |
511 |
|
exp.push_back(d_ci_exp[b][coeff_b][rhs_b]); |
512 |
|
if (Trace.isOn("nl-ext-rbound")) |
513 |
|
{ |
514 |
|
Trace("nl-ext-rbound") << "* try bounds : "; |
515 |
|
debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a); |
516 |
|
Trace("nl-ext-rbound") << std::endl; |
517 |
|
Trace("nl-ext-rbound") << " "; |
518 |
|
debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b); |
519 |
|
Trace("nl-ext-rbound") << std::endl; |
520 |
|
} |
521 |
|
Kind types[2]; |
522 |
|
for (unsigned r = 0; r < 2; r++) |
523 |
|
{ |
524 |
|
Node pivot_factor = r == 0 ? itb->second : ita->second; |
525 |
|
int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn; |
526 |
|
types[r] = r == 0 ? type_a : type_b; |
527 |
|
if (pivot_factor_sign == (r == 0 ? 1 : -1)) |
528 |
|
{ |
529 |
|
types[r] = reverseRelationKind(types[r]); |
530 |
|
} |
531 |
|
if (pivot_factor_sign == 1) |
532 |
|
{ |
533 |
|
exp.push_back( |
534 |
|
nm->mkNode(Kind::GT, pivot_factor, d_data->d_zero)); |
535 |
|
} |
536 |
|
else |
537 |
|
{ |
538 |
|
exp.push_back( |
539 |
|
nm->mkNode(Kind::LT, pivot_factor, d_data->d_zero)); |
540 |
|
} |
541 |
|
} |
542 |
|
Kind jk = transKinds(types[0], types[1]); |
543 |
|
Trace("nl-ext-rbound-debug") |
544 |
|
<< "trans kind : " << types[0] << " + " << types[1] << " = " |
545 |
|
<< jk << std::endl; |
546 |
|
if (jk != Kind::UNDEFINED_KIND) |
547 |
|
{ |
548 |
|
Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res); |
549 |
|
Node conc_mv = d_data->d_model.computeAbstractModelValue(conc); |
550 |
|
if (conc_mv == d_data->d_false) |
551 |
|
{ |
552 |
|
Node rblem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc); |
553 |
|
Trace("nl-ext-rbound-lemma-debug") |
554 |
|
<< "Resolution bound lemma " |
555 |
|
"(pre-rewrite) " |
556 |
|
": " |
557 |
|
<< rblem << std::endl; |
558 |
|
rblem = rewrite(rblem); |
559 |
|
Trace("nl-ext-rbound-lemma") |
560 |
|
<< "Resolution bound lemma : " << rblem << std::endl; |
561 |
|
d_data->d_im.addPendingLemma( |
562 |
|
rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS); |
563 |
|
} |
564 |
|
} |
565 |
|
exp.pop_back(); |
566 |
|
exp.pop_back(); |
567 |
|
exp.pop_back(); |
568 |
|
} |
569 |
|
} |
570 |
|
exp.pop_back(); |
571 |
|
} |
572 |
|
} |
573 |
|
} |
574 |
|
} |
575 |
|
} |
576 |
|
|
577 |
|
} // namespace nl |
578 |
|
} // namespace arith |
579 |
|
} // namespace theory |
580 |
31137 |
} // namespace cvc5 |