Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Model object for the non-linear extension class.
14 : : */
15 : :
16 : : #include "theory/arith/nl/nl_model.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "options/arith_options.h"
20 : : #include "options/smt_options.h"
21 : : #include "options/theory_options.h"
22 : : #include "theory/arith/arith_msum.h"
23 : : #include "theory/arith/arith_utilities.h"
24 : : #include "theory/arith/nl/nl_lemma_utils.h"
25 : : #include "theory/theory_model.h"
26 : : #include "theory/rewriter.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace arith {
33 : : namespace nl {
34 : :
35 : 32376 : NlModel::NlModel(Env& env) : EnvObj(env), d_used_approx(false)
36 : : {
37 : 32376 : d_true = nodeManager()->mkConst(true);
38 : 32376 : d_false = nodeManager()->mkConst(false);
39 : 32376 : d_zero = nodeManager()->mkConstReal(Rational(0));
40 : 32376 : d_one = nodeManager()->mkConstReal(Rational(1));
41 : 32376 : d_two = nodeManager()->mkConstReal(Rational(2));
42 : 32376 : }
43 : :
44 : 39223 : NlModel::~NlModel() {}
45 : :
46 : 11492 : void NlModel::reset(const std::map<Node, Node>& arithModel)
47 : : {
48 : 11492 : d_concreteModelCache.clear();
49 : 11492 : d_abstractModelCache.clear();
50 : 11492 : d_arithVal = arithModel;
51 : 11492 : }
52 : :
53 : 11524 : void NlModel::resetCheck()
54 : : {
55 : 11524 : d_used_approx = false;
56 : 11524 : d_check_model_solved.clear();
57 : 11524 : d_check_model_bounds.clear();
58 : 11524 : d_substitutions.clear();
59 : 11524 : }
60 : :
61 : 1164440 : Node NlModel::computeConcreteModelValue(TNode n)
62 : : {
63 : 1164440 : return computeModelValue(n, true);
64 : : }
65 : :
66 : 625223 : Node NlModel::computeAbstractModelValue(TNode n)
67 : : {
68 : 625223 : return computeModelValue(n, false);
69 : : }
70 : :
71 : 5710300 : Node NlModel::computeModelValue(TNode n, bool isConcrete)
72 : : {
73 [ + + ]: 5710300 : auto& cache = isConcrete ? d_concreteModelCache : d_abstractModelCache;
74 [ + + ]: 5710300 : if (auto it = cache.find(n); it != cache.end())
75 : : {
76 : 3411400 : return it->second;
77 : : }
78 [ + - ]: 4597800 : Trace("nl-ext-mv-debug") << "computeModelValue " << n
79 : 2298900 : << ", isConcrete=" << isConcrete << std::endl;
80 : 4597800 : Node ret;
81 [ + + ]: 2298900 : if (n.isConst())
82 : : {
83 : 156632 : ret = n;
84 : : }
85 [ + + ][ + + ]: 2142270 : else if (!isConcrete && hasLinearModelValue(n, ret))
[ + + ][ + + ]
[ - - ]
86 : : {
87 : : // use model value for abstraction
88 : : }
89 [ + + ]: 2049140 : else if (n.getNumChildren() == 0)
90 : : {
91 : : // we are interested in the exact value of PI, which cannot be computed.
92 : : // hence, we return PI itself when asked for the concrete value.
93 [ + + ]: 86079 : if (n.getKind() == Kind::PI)
94 : : {
95 : 1506 : ret = n;
96 : : }
97 : : else
98 : : {
99 : 84573 : ret = getValueInternal(n);
100 : : }
101 : : }
102 : : else
103 : : {
104 : : // otherwise, compute true value
105 : 1963060 : TheoryId ctid = theory::kindToTheoryId(n.getKind());
106 [ + + ][ + + ]: 1963060 : if (ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN)
[ + + ]
107 : : {
108 : : // we directly look up terms not belonging to arithmetic
109 : 31415 : ret = getValueInternal(n);
110 : : }
111 : : else
112 : : {
113 : 1931640 : std::vector<Node> children;
114 [ + + ]: 1931640 : if (n.getMetaKind() == metakind::PARAMETERIZED)
115 : : {
116 : 948 : children.emplace_back(n.getOperator());
117 : : }
118 [ + + ]: 5434680 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
119 : : {
120 : 3503040 : children.emplace_back(computeModelValue(n[i], isConcrete));
121 : : }
122 : 1931640 : ret = nodeManager()->mkNode(n.getKind(), children);
123 : 1931640 : ret = rewrite(ret);
124 : : }
125 : : }
126 [ + - ][ - - ]: 4597800 : Trace("nl-ext-mv-debug") << "computed " << (isConcrete ? "M" : "M_A") << "["
127 : 2298900 : << n << "] = " << ret << std::endl;
128 [ - + ][ - + ]: 2298900 : Assert(n.getType() == ret.getType());
[ - - ]
129 : 2298900 : cache[n] = ret;
130 : 2298900 : return ret;
131 : : }
132 : :
133 : 189846 : int NlModel::compare(TNode i, TNode j, bool isConcrete, bool isAbsolute)
134 : : {
135 [ - + ]: 189846 : if (i == j)
136 : : {
137 : 0 : return 0;
138 : : }
139 : 379692 : Node ci = computeModelValue(i, isConcrete);
140 : 379692 : Node cj = computeModelValue(j, isConcrete);
141 [ + - ]: 189846 : if (ci.isConst())
142 : : {
143 [ + - ]: 189846 : if (cj.isConst())
144 : : {
145 : 189846 : return compareValue(ci, cj, isAbsolute);
146 : : }
147 : 0 : return 1;
148 : : }
149 [ - - ]: 0 : return cj.isConst() ? -1 : 0;
150 : : }
151 : :
152 : 227749 : int NlModel::compareValue(TNode i, TNode j, bool isAbsolute) const
153 : : {
154 [ + - ][ + - ]: 455498 : Assert(i.isConst() && j.isConst());
[ - + ][ - - ]
155 [ + + ]: 227749 : if (i == j)
156 : : {
157 : 39067 : return 0;
158 : : }
159 [ + + ]: 188682 : if (!isAbsolute)
160 : : {
161 [ + + ]: 743 : return i.getConst<Rational>() < j.getConst<Rational>() ? -1 : 1;
162 : : }
163 : 375878 : Rational iabs = i.getConst<Rational>().abs();
164 : 375878 : Rational jabs = j.getConst<Rational>().abs();
165 [ + + ]: 187939 : if (iabs == jabs)
166 : : {
167 : 17424 : return 0;
168 : : }
169 [ + + ]: 170515 : return iabs < jabs ? -1 : 1;
170 : : }
171 : :
172 : 1533 : bool NlModel::checkModel(const std::vector<Node>& assertions,
173 : : unsigned d,
174 : : std::vector<NlLemma>& lemmas)
175 : : {
176 [ + - ]: 3066 : Trace("nl-ext-cm-debug") << "NlModel::checkModel: solve for equalities..."
177 : 1533 : << std::endl;
178 [ + + ]: 48771 : for (const Node& atom : assertions)
179 : : {
180 [ + - ]: 47238 : Trace("nl-ext-cm-debug") << "- assertion: " << atom << std::endl;
181 : : // see if it corresponds to a univariate polynomial equation of degree two
182 [ + + ]: 47238 : if (atom.getKind() == Kind::EQUAL)
183 : : {
184 : : // we substitute inside of solve equality simple
185 [ + + ]: 4474 : if (!solveEqualitySimple(atom, d, lemmas))
186 : : {
187 : : // no chance we will satisfy this equality
188 [ + - ]: 5436 : Trace("nl-ext-cm") << "...check-model : failed to solve equality : "
189 : 2718 : << atom << std::endl;
190 : : }
191 : : }
192 : : }
193 : :
194 : : // all remaining variables are constrained to their exact model values
195 [ + - ]: 3066 : Trace("nl-ext-cm-debug") << " set exact bounds for remaining variables..."
196 : 1533 : << std::endl;
197 : 3066 : std::unordered_set<TNode> visited;
198 : 3066 : std::vector<TNode> visit;
199 : 3066 : TNode cur;
200 [ + + ]: 48771 : for (const Node& a : assertions)
201 : : {
202 : 47238 : visit.push_back(a);
203 : 183659 : do
204 : : {
205 : 230897 : cur = visit.back();
206 : 230897 : visit.pop_back();
207 [ + + ]: 230897 : if (visited.find(cur) == visited.end())
208 : : {
209 : 123285 : visited.insert(cur);
210 [ + + ][ + + ]: 123285 : if (cur.getType().isRealOrInt() && !cur.isConst())
[ + - ][ + + ]
[ - - ]
211 : : {
212 : 32744 : Kind k = cur.getKind();
213 [ + + ][ + + ]: 23103 : if (k != Kind::MULT && k != Kind::ADD && k != Kind::NONLINEAR_MULT
214 [ + + ][ + + ]: 7621 : && k != Kind::TO_REAL && !isTranscendentalKind(k)
215 [ + + ][ + + ]: 55847 : && k != Kind::IAND && k != Kind::POW2)
[ + + ][ + + ]
216 : : {
217 : : // if we have not set an approximate bound for it
218 [ + + ]: 6292 : if (!hasAssignment(cur))
219 : : {
220 : : // set its exact model value in the substitution, if we compute
221 : : // a constant value
222 : 8070 : Node curv = computeConcreteModelValue(cur);
223 [ + - ]: 4035 : if (curv.isConst())
224 : : {
225 [ - + ]: 4035 : if (TraceIsOn("nl-ext-cm"))
226 : : {
227 [ - - ]: 0 : Trace("nl-ext-cm")
228 : 0 : << "check-model-bound : exact : " << cur << " = ";
229 : 0 : printRationalApprox("nl-ext-cm", curv);
230 [ - - ]: 0 : Trace("nl-ext-cm") << std::endl;
231 : : }
232 : 4035 : bool ret = addSubstitution(cur, curv);
233 [ - + ][ - + ]: 4035 : AlwaysAssert(ret);
[ - - ]
234 : : }
235 : : }
236 : : }
237 : : }
238 : 123285 : visit.insert(visit.end(), cur.begin(), cur.end());
239 : : }
240 [ + + ]: 230897 : } while (!visit.empty());
241 : : }
242 : :
243 [ + - ]: 1533 : Trace("nl-ext-cm-debug") << " check assertions..." << std::endl;
244 : 3066 : std::vector<Node> check_assertions;
245 [ + + ]: 48771 : for (const Node& a : assertions)
246 : : {
247 [ + + ]: 47238 : if (d_check_model_solved.find(a) == d_check_model_solved.end())
248 : : {
249 : : // apply the substitution to a
250 : 90964 : Node av = getSubstitutedForm(a);
251 [ + - ]: 90964 : Trace("nl-ext-cm") << "simpleCheckModelLit " << av << " (from " << a
252 : 45482 : << ")" << std::endl;
253 : : // simple check literal
254 [ + + ]: 45482 : if (!simpleCheckModelLit(av))
255 : : {
256 [ + - ]: 9776 : Trace("nl-ext-cm") << "...check-model : assertion failed : " << a
257 : 4888 : << std::endl;
258 : 4888 : check_assertions.push_back(av);
259 [ + - ]: 9776 : Trace("nl-ext-cm-debug")
260 : 4888 : << "...check-model : failed assertion, value : " << av << std::endl;
261 : : }
262 : : }
263 : : }
264 : :
265 [ + + ]: 1533 : if (!check_assertions.empty())
266 : : {
267 [ + - ]: 1345 : Trace("nl-ext-cm") << "...simple check failed." << std::endl;
268 : : // TODO (#1450) check model for general case
269 : 1345 : return false;
270 : : }
271 [ + - ]: 188 : Trace("nl-ext-cm") << "...simple check succeeded!" << std::endl;
272 : 188 : return true;
273 : : }
274 : :
275 : 7124 : bool NlModel::addSubstitution(TNode v, TNode s)
276 : : {
277 [ - + ][ - + ]: 7124 : Assert(v.getKind() != Kind::TO_REAL);
[ - - ]
278 [ + - ]: 14248 : Trace("nl-ext-model") << "* check model substitution : " << v << " -> " << s
279 : 7124 : << std::endl;
280 : 7124 : Assert(getSubstitutedForm(s) == s)
281 : 0 : << "Added a substitution whose range is not in substituted form " << s;
282 : : // cannot substitute real for integer
283 : 7124 : Assert(v.getType().isReal() || s.getType().isInteger());
284 : : // should not substitute the same variable twice
285 : : // should not set exact bound more than once
286 [ - + ]: 7124 : if (d_substitutions.contains(v))
287 : : {
288 : 0 : Node cur = d_substitutions.getSubs(v);
289 [ - - ]: 0 : if (cur != s)
290 : : {
291 [ - - ]: 0 : Trace("nl-ext-model")
292 : 0 : << "...warning: already has value: " << cur << std::endl;
293 : : // We set two different substitutions for a variable v. If both are
294 : : // constant, then we throw an error. Otherwise, we ignore the newer
295 : : // substitution and return false here.
296 : 0 : Assert(!cur.isConst() || !s.isConst())
297 : 0 : << "Conflicting exact bounds given for a variable (" << cur << " and "
298 : 0 : << s << ") for " << v;
299 : 0 : return false;
300 : : }
301 : : }
302 : : // Check if the substitution is cyclic when looking inside of abstracted
303 : : // arithmetic terms. This prevents substitutions like:
304 : : // {x -> y, y -> (exp x)}
305 : : // Where note that {x->y}.applyArith((exp x)) = (exp x), but
306 : : // {x->y}.applyArith((exp x)) = (exp y), which is caught here.
307 : 14248 : Node subsFull = d_substitutions.apply(s);
308 [ - + ]: 7124 : if (expr::hasSubterm(subsFull, v))
309 : : {
310 : 0 : return false;
311 : : }
312 : :
313 : : // if we previously had an approximate bound, the exact bound should be in its
314 : : // range
315 : : std::map<Node, std::pair<Node, Node>>::iterator itb =
316 : 7124 : d_check_model_bounds.find(v);
317 [ - + ]: 7124 : if (itb != d_check_model_bounds.end())
318 : : {
319 : 0 : Assert(s.isConst());
320 : 0 : if (s.getConst<Rational>() <= itb->second.first.getConst<Rational>()
321 : 0 : || s.getConst<Rational>() >= itb->second.second.getConst<Rational>())
322 : : {
323 [ - - ]: 0 : Trace("nl-ext-model")
324 : 0 : << "...ERROR: already has bound which is out of range." << std::endl;
325 : 0 : Assert(false) << "Out of bounds exact bound given for a variable with an "
326 : 0 : "approximate bound";
327 : : return false;
328 : : }
329 : : }
330 : 7124 : ArithSubs tmp;
331 : 7124 : tmp.addArith(v, s);
332 [ + + ]: 42502 : for (auto& sub : d_substitutions.d_subs)
333 : : {
334 : 70756 : Node ms = tmp.applyArith(sub);
335 [ + + ]: 35378 : if (ms != sub)
336 : : {
337 : 1104 : sub = rewrite(ms);
338 : : }
339 : : }
340 : 7124 : d_substitutions.addArith(v, s);
341 : 7124 : return true;
342 : : }
343 : :
344 : 1153 : bool NlModel::addBound(TNode v, TNode l, TNode u)
345 : : {
346 [ - + ][ - + ]: 1153 : Assert(l.getType() == v.getType());
[ - - ]
347 [ - + ][ - + ]: 1153 : Assert(u.getType() == v.getType());
[ - - ]
348 [ + - ]: 2306 : Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " "
349 : 1153 : << u << "]" << std::endl;
350 [ + + ]: 1153 : if (l == u)
351 : : {
352 : : // bound is exact, can add as substitution
353 : 348 : return addSubstitution(v, l);
354 : : }
355 : : // should not set a bound for a value that is exact
356 [ - + ]: 805 : if (d_substitutions.contains(v))
357 : : {
358 [ - - ]: 0 : Trace("nl-ext-model")
359 : 0 : << "...ERROR: setting bound for variable that already has exact value."
360 : 0 : << std::endl;
361 : 0 : Assert(false) << "Setting bound for variable that already has exact value.";
362 : : return false;
363 : : }
364 [ - + ][ - + ]: 805 : Assert(l.isConst());
[ - - ]
365 [ - + ][ - + ]: 805 : Assert(u.isConst());
[ - - ]
366 [ - + ][ - + ]: 805 : Assert(l.getConst<Rational>() <= u.getConst<Rational>());
[ - - ]
367 : 805 : d_check_model_bounds[v] = std::pair<Node, Node>(l, u);
368 [ - + ]: 805 : if (TraceIsOn("nl-ext-cm"))
369 : : {
370 [ - - ]: 0 : Trace("nl-ext-cm") << "check-model-bound : approximate : ";
371 : 0 : printRationalApprox("nl-ext-cm", l);
372 [ - - ]: 0 : Trace("nl-ext-cm") << " <= " << v << " <= ";
373 : 0 : printRationalApprox("nl-ext-cm", u);
374 [ - - ]: 0 : Trace("nl-ext-cm") << std::endl;
375 : : }
376 : 805 : return true;
377 : : }
378 : :
379 : 476 : void NlModel::setUsedApproximate() { d_used_approx = true; }
380 : :
381 : 36 : bool NlModel::usedApproximate() const { return d_used_approx; }
382 : :
383 : 5806 : bool NlModel::solveEqualitySimple(Node eq,
384 : : unsigned d,
385 : : std::vector<NlLemma>& lemmas)
386 : : {
387 : 11612 : Node seq = eq;
388 [ + + ]: 5806 : if (!d_substitutions.empty())
389 : : {
390 : 4082 : seq = getSubstitutedForm(eq);
391 [ + + ]: 4082 : if (seq.isConst())
392 : : {
393 [ + + ]: 1687 : if (seq.getConst<bool>())
394 : : {
395 : : // already true
396 : 857 : d_check_model_solved[eq] = Node::null();
397 : 857 : return true;
398 : : }
399 : 830 : return false;
400 : : }
401 : : }
402 [ + - ]: 4119 : Trace("nl-ext-cms") << "simple solve equality " << seq << "..." << std::endl;
403 [ - + ][ - + ]: 4119 : Assert(seq.getKind() == Kind::EQUAL);
[ - - ]
404 : 8238 : std::map<Node, Node> msum;
405 [ - + ]: 4119 : if (!ArithMSum::getMonomialSumLit(seq, msum))
406 : : {
407 [ - - ]: 0 : Trace("nl-ext-cms") << "...fail, could not determine monomial sum."
408 : 0 : << std::endl;
409 : 0 : return false;
410 : : }
411 : 4119 : bool is_valid = true;
412 : : // the variable we will solve a quadratic equation for
413 : 8238 : Node var;
414 : 8238 : Node b = d_zero;
415 : 8238 : Node c = d_zero;
416 : 4119 : NodeManager* nm = nodeManager();
417 : : // the list of variables that occur as a monomial in msum, and whose value
418 : : // is so far unconstrained in the model.
419 : 8238 : std::unordered_set<Node> unc_vars;
420 : : // the list of variables that occur as a factor in a monomial, and whose
421 : : // value is so far unconstrained in the model.
422 : 8238 : std::unordered_set<Node> unc_vars_factor;
423 [ + + ]: 16049 : for (std::pair<const Node, Node>& m : msum)
424 : : {
425 : 23860 : Node v = m.first;
426 [ + + ]: 23860 : Node coeff = m.second.isNull() ? d_one : m.second;
427 [ + + ]: 11930 : if (v.isNull())
428 : : {
429 : 2248 : c = coeff;
430 : : }
431 [ + + ]: 9682 : else if (v.getKind() == Kind::NONLINEAR_MULT)
432 : : {
433 : 3226 : is_valid = false;
434 [ + - ]: 6452 : Trace("nl-ext-cms-debug")
435 : 3226 : << "...invalid due to non-linear monomial " << v << std::endl;
436 : : // may wish to set an exact bound for a factor and repeat
437 [ + + ]: 9698 : for (const Node& vc : v)
438 : : {
439 : 6472 : unc_vars_factor.insert(vc);
440 : : }
441 : : }
442 [ + + ][ + + ]: 6456 : else if (!v.isVar() || (!var.isNull() && var != v))
[ + - ][ + + ]
443 : : {
444 [ + - ]: 7148 : Trace("nl-ext-cms-debug")
445 : 3574 : << "...invalid due to factor " << v << std::endl;
446 : : // cannot solve multivariate
447 [ + + ]: 3574 : if (is_valid)
448 : : {
449 : 2126 : is_valid = false;
450 : : // if b is non-zero, then var is also an unconstrained variable
451 [ + + ]: 2126 : if (b != d_zero)
452 : : {
453 : 1250 : unc_vars.insert(var);
454 : 1250 : unc_vars_factor.insert(var);
455 : : }
456 : : }
457 : : // if v is unconstrained, we may turn this equality into a substitution
458 : 3574 : unc_vars.insert(v);
459 : 3574 : unc_vars_factor.insert(v);
460 : : }
461 : : else
462 : : {
463 : : // set the variable to solve for
464 : 2882 : b = coeff;
465 : 2882 : var = v;
466 : : }
467 : : }
468 [ + + ]: 4119 : if (!is_valid)
469 : : {
470 : : // see if we can solve for a variable?
471 [ + + ]: 6406 : for (const Node& uv : unc_vars)
472 : : {
473 [ + - ]: 4231 : Trace("nl-ext-cm-debug") << "check subs var : " << uv << std::endl;
474 : : // cannot already have a bound
475 [ + + ][ + - ]: 4231 : if (uv.isVar() && !hasAssignment(uv))
[ + + ][ + + ]
[ - - ]
476 : : {
477 : 2567 : Node slv;
478 : 2567 : Node veqc;
479 [ + - ]: 2567 : if (ArithMSum::isolate(uv, msum, veqc, slv, Kind::EQUAL) != 0)
480 : : {
481 [ - + ][ - + ]: 2567 : Assert(!slv.isNull());
[ - - ]
482 : : // must rewrite here to be in substituted form
483 : 2567 : slv = rewrite(slv);
484 : : // Currently do not support substitution-with-coefficients.
485 : : // We also ensure types are correct here, which avoids substituting
486 : : // a term of non-integer type for a variable of integer type.
487 : 4102 : if (veqc.isNull() && !expr::hasSubterm(slv, uv)
488 : 4102 : && slv.getType() == uv.getType())
489 : : {
490 [ + - ]: 1362 : Trace("nl-ext-cm")
491 : 681 : << "check-model-subs : " << uv << " -> " << slv << std::endl;
492 : 681 : bool ret = addSubstitution(uv, slv);
493 [ + - ]: 681 : if (ret)
494 : : {
495 [ + - ]: 1362 : Trace("nl-ext-cms") << "...success, model substitution " << uv
496 : 681 : << " -> " << slv << std::endl;
497 : 681 : d_check_model_solved[eq] = uv;
498 : : }
499 : 681 : return ret;
500 : : }
501 : : }
502 : : }
503 : : }
504 : : // see if we can assign a variable to a constant
505 [ + + ]: 3678 : for (const Node& uvf : unc_vars_factor)
506 : : {
507 [ + - ]: 2835 : Trace("nl-ext-cm-debug") << "check set var : " << uvf << std::endl;
508 : : // cannot already have a bound
509 [ + + ][ + - ]: 2835 : if (uvf.isVar() && !hasAssignment(uvf))
[ + + ][ + + ]
[ - - ]
510 : : {
511 : 2664 : Node uvfv = computeConcreteModelValue(uvf);
512 : : // fail if model value is non-constant
513 [ - + ]: 1332 : if (!uvfv.isConst())
514 : : {
515 : 0 : return false;
516 : : }
517 [ - + ]: 1332 : if (TraceIsOn("nl-ext-cm"))
518 : : {
519 [ - - ]: 0 : Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = ";
520 : 0 : printRationalApprox("nl-ext-cm", uvfv);
521 [ - - ]: 0 : Trace("nl-ext-cm") << std::endl;
522 : : }
523 : 1332 : bool ret = addSubstitution(uvf, uvfv);
524 : : // recurse
525 [ + - ][ + - ]: 1332 : return ret ? solveEqualitySimple(eq, d, lemmas) : false;
[ - - ]
526 : : }
527 : : }
528 [ + - ]: 1686 : Trace("nl-ext-cms") << "...fail due to constrained invalid terms."
529 : 843 : << std::endl;
530 : 843 : return false;
531 : : }
532 [ + - ][ + + ]: 1263 : else if (var.isNull() || var.getType().isInteger())
[ + - ][ + + ]
[ - - ]
533 : : {
534 : : // cannot solve quadratic equations for integer variables
535 [ + - ]: 1045 : Trace("nl-ext-cms") << "...fail due to variable to solve for." << std::endl;
536 : 1045 : return false;
537 : : }
538 : :
539 : : // we are linear, it is simple
540 [ - + ]: 218 : if (b == d_zero)
541 : : {
542 [ - - ]: 0 : Trace("nl-ext-cms") << "...fail due to zero a/b." << std::endl;
543 : 0 : Assert(false);
544 : : return false;
545 : : }
546 : 436 : Node val = nm->mkConstReal(-c.getConst<Rational>() / b.getConst<Rational>());
547 [ - + ]: 218 : if (TraceIsOn("nl-ext-cm"))
548 : : {
549 [ - - ]: 0 : Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = ";
550 : 0 : printRationalApprox("nl-ext-cm", val);
551 [ - - ]: 0 : Trace("nl-ext-cm") << std::endl;
552 : : }
553 : 218 : bool ret = addSubstitution(var, val);
554 [ + - ]: 218 : if (ret)
555 : : {
556 [ + - ]: 218 : Trace("nl-ext-cms") << "...success, solved linear." << std::endl;
557 : 218 : d_check_model_solved[eq] = var;
558 : : }
559 : 218 : return ret;
560 : : }
561 : :
562 : 46780 : bool NlModel::simpleCheckModelLit(Node lit)
563 : : {
564 [ + - ]: 93560 : Trace("nl-ext-cms") << "*** Simple check-model lit for " << lit << "..."
565 : 46780 : << std::endl;
566 [ + + ]: 46780 : if (lit.isConst())
567 : : {
568 [ + - ]: 41560 : Trace("nl-ext-cms") << " return constant." << std::endl;
569 : 41560 : return lit.getConst<bool>();
570 : : }
571 : 5220 : NodeManager* nm = nodeManager();
572 : 5220 : bool pol = lit.getKind() != Kind::NOT;
573 [ + + ]: 10440 : Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
574 : :
575 [ + + ]: 5220 : if (atom.getKind() == Kind::EQUAL)
576 : : {
577 : : // x = a is ( x >= a ^ x <= a )
578 [ + - ]: 1298 : for (unsigned i = 0; i < 2; i++)
579 : : {
580 : 2596 : Node lit2 = nm->mkNode(Kind::GEQ, atom[i], atom[1 - i]);
581 [ + + ]: 1298 : if (!pol)
582 : : {
583 : 1012 : lit2 = lit2.negate();
584 : : }
585 : 1298 : lit2 = rewrite(lit2);
586 : 1298 : bool success = simpleCheckModelLit(lit2);
587 [ + + ]: 1298 : if (success != pol)
588 : : {
589 : : // false != true -> one conjunct of equality is false, we fail
590 : : // true != false -> one disjunct of disequality is true, we succeed
591 : 704 : return success;
592 : : }
593 : : }
594 : : // both checks passed and polarity is true, or both checks failed and
595 : : // polarity is false
596 : 0 : return pol;
597 : : }
598 [ - + ]: 4516 : else if (atom.getKind() != Kind::GEQ)
599 : : {
600 [ - - ]: 0 : Trace("nl-ext-cms") << " failed due to unknown literal." << std::endl;
601 : 0 : return false;
602 : : }
603 : : // get the monomial sum
604 : 9032 : std::map<Node, Node> msum;
605 [ - + ]: 4516 : if (!ArithMSum::getMonomialSumLit(atom, msum))
606 : : {
607 [ - - ]: 0 : Trace("nl-ext-cms") << " failed due to get msum." << std::endl;
608 : 0 : return false;
609 : : }
610 : : // simple interval analysis
611 [ + + ]: 4516 : if (simpleCheckModelMsum(msum, pol))
612 : : {
613 : 3460 : return true;
614 : : }
615 : : // can also try reasoning about univariate quadratic equations
616 [ + - ]: 2112 : Trace("nl-ext-cms-debug")
617 : 1056 : << "* Try univariate quadratic analysis..." << std::endl;
618 : 2112 : std::vector<Node> vs_invalid;
619 : 2112 : std::unordered_set<Node> vs;
620 : 2112 : std::map<Node, Node> v_a;
621 : 2112 : std::map<Node, Node> v_b;
622 : : // get coefficients...
623 [ + + ]: 3075 : for (std::pair<const Node, Node>& m : msum)
624 : : {
625 : 4038 : Node v = m.first;
626 [ + + ]: 2019 : if (!v.isNull())
627 : : {
628 [ - + ]: 1088 : if (v.isVar())
629 : : {
630 [ - - ]: 0 : v_b[v] = m.second.isNull() ? d_one : m.second;
631 : 0 : vs.insert(v);
632 : : }
633 [ - - ]: 0 : else if (v.getKind() == Kind::NONLINEAR_MULT && v.getNumChildren() == 2
634 : 1088 : && v[0] == v[1] && v[0].isVar())
635 : : {
636 [ - - ]: 0 : v_a[v[0]] = m.second.isNull() ? d_one : m.second;
637 : 0 : vs.insert(v[0]);
638 : : }
639 : : else
640 : : {
641 : 1088 : vs_invalid.push_back(v);
642 : : }
643 : : }
644 : : }
645 : : // solve the valid variables...
646 : : Node invalid_vsum =
647 : 1056 : vs_invalid.empty()
648 : 0 : ? d_zero
649 : 2080 : : (vs_invalid.size() == 1 ? vs_invalid[0]
650 [ - + ][ + + ]: 4192 : : nm->mkNode(Kind::ADD, vs_invalid));
651 : : // substitution to try
652 : 2112 : ArithSubs qsub;
653 [ - + ]: 1056 : for (const Node& v : vs)
654 : : {
655 : : // is it a valid variable?
656 : : std::map<Node, std::pair<Node, Node>>::iterator bit =
657 : 0 : d_check_model_bounds.find(v);
658 : 0 : if (!expr::hasSubterm(invalid_vsum, v) && bit != d_check_model_bounds.end())
659 : : {
660 : 0 : std::map<Node, Node>::iterator it = v_a.find(v);
661 [ - - ]: 0 : if (it != v_a.end())
662 : : {
663 : 0 : Node a = it->second;
664 : 0 : Assert(a.isConst());
665 : 0 : int asgn = a.getConst<Rational>().sgn();
666 : 0 : Assert(asgn != 0);
667 : 0 : Node t = nm->mkNode(Kind::MULT, a, v, v);
668 : 0 : Node b = d_zero;
669 : 0 : it = v_b.find(v);
670 [ - - ]: 0 : if (it != v_b.end())
671 : : {
672 : 0 : b = it->second;
673 : 0 : t = nm->mkNode(Kind::ADD, t, nm->mkNode(Kind::MULT, b, v));
674 : : }
675 : 0 : t = rewrite(t);
676 [ - - ]: 0 : Trace("nl-ext-cms-debug") << "Trying to find min/max for quadratic "
677 : 0 : << t << "..." << std::endl;
678 [ - - ]: 0 : Trace("nl-ext-cms-debug") << " a = " << a << std::endl;
679 [ - - ]: 0 : Trace("nl-ext-cms-debug") << " b = " << b << std::endl;
680 : : // find maximal/minimal value on the interval
681 : : Node apex = nm->mkNode(Kind::DIVISION,
682 : 0 : nm->mkNode(Kind::NEG, b),
683 : 0 : nm->mkNode(Kind::MULT, d_two, a));
684 : 0 : apex = rewrite(apex);
685 : 0 : Assert(apex.isConst());
686 : : // for lower, upper, whether we are greater than the apex
687 : : bool cmp[2];
688 : 0 : Node boundn[2];
689 [ - - ]: 0 : for (unsigned r = 0; r < 2; r++)
690 : : {
691 [ - - ]: 0 : boundn[r] = r == 0 ? bit->second.first : bit->second.second;
692 : 0 : Node cmpn = nm->mkNode(Kind::GT, boundn[r], apex);
693 : 0 : cmpn = rewrite(cmpn);
694 : 0 : Assert(cmpn.isConst());
695 : 0 : cmp[r] = cmpn.getConst<bool>();
696 : : }
697 [ - - ]: 0 : Trace("nl-ext-cms-debug") << " apex " << apex << std::endl;
698 [ - - ]: 0 : Trace("nl-ext-cms-debug")
699 : 0 : << " lower " << boundn[0] << ", cmp: " << cmp[0] << std::endl;
700 [ - - ]: 0 : Trace("nl-ext-cms-debug")
701 : 0 : << " upper " << boundn[1] << ", cmp: " << cmp[1] << std::endl;
702 : 0 : Assert(boundn[0].getConst<Rational>()
703 : : <= boundn[1].getConst<Rational>());
704 : 0 : Node s;
705 : 0 : qsub.addArith(v, Node());
706 [ - - ]: 0 : if (cmp[0] != cmp[1])
707 : : {
708 : 0 : Assert(!cmp[0] && cmp[1]);
709 : : // does the sign match the bound?
710 [ - - ]: 0 : if ((asgn == 1) == pol)
711 : : {
712 : : // the apex is the max/min value
713 : 0 : s = apex;
714 [ - - ]: 0 : Trace("nl-ext-cms-debug") << " ...set to apex." << std::endl;
715 : : }
716 : : else
717 : : {
718 : : // it is one of the endpoints, plug in and compare
719 : 0 : Node tcmpn[2];
720 [ - - ]: 0 : for (unsigned r = 0; r < 2; r++)
721 : : {
722 : 0 : qsub.d_subs.back() = boundn[r];
723 : 0 : Node ts = qsub.applyArith(t);
724 : 0 : tcmpn[r] = rewrite(ts);
725 : : }
726 : 0 : Node tcmp = nm->mkNode(Kind::LT, tcmpn[0], tcmpn[1]);
727 [ - - ]: 0 : Trace("nl-ext-cms-debug")
728 : 0 : << " ...both sides of apex, compare " << tcmp << std::endl;
729 : 0 : tcmp = rewrite(tcmp);
730 : 0 : Assert(tcmp.isConst());
731 [ - - ]: 0 : unsigned bindex_use = (tcmp.getConst<bool>() == pol) ? 1 : 0;
732 [ - - ]: 0 : Trace("nl-ext-cms-debug")
733 [ - - ]: 0 : << " ...set to " << (bindex_use == 1 ? "upper" : "lower")
734 : 0 : << std::endl;
735 : 0 : s = boundn[bindex_use];
736 : : }
737 : : }
738 : : else
739 : : {
740 : : // both to one side of the apex
741 : : // we figure out which bound to use (lower or upper) based on
742 : : // three factors:
743 : : // (1) whether a's sign is positive,
744 : : // (2) whether we are greater than the apex of the parabola,
745 : : // (3) the polarity of the constraint, i.e. >= or <=.
746 : : // there are 8 cases of these factors, which we test here.
747 : 0 : unsigned bindex_use = (((asgn == 1) == cmp[0]) == pol) ? 0 : 1;
748 [ - - ]: 0 : Trace("nl-ext-cms-debug")
749 [ - - ]: 0 : << " ...set to " << (bindex_use == 1 ? "upper" : "lower")
750 : 0 : << std::endl;
751 : 0 : s = boundn[bindex_use];
752 : : }
753 : 0 : Assert(!s.isNull());
754 : 0 : qsub.d_subs.back() = s;
755 [ - - ]: 0 : Trace("nl-ext-cms") << "* set bound based on quadratic : " << v
756 : 0 : << " -> " << s << std::endl;
757 : : }
758 : : }
759 : : }
760 [ - + ]: 1056 : if (!qsub.empty())
761 : : {
762 : 0 : Node slit = qsub.applyArith(lit);
763 : 0 : slit = rewrite(slit);
764 : 0 : return simpleCheckModelLit(slit);
765 : : }
766 : 1056 : return false;
767 : : }
768 : :
769 : 4516 : bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol)
770 : : {
771 [ + - ]: 4516 : Trace("nl-ext-cms-debug") << "* Try simple interval analysis..." << std::endl;
772 : 4516 : NodeManager* nm = nodeManager();
773 : : // map from transcendental functions to whether they were set to lower
774 : : // bound
775 : 4516 : bool simpleSuccess = true;
776 : 9032 : std::map<Node, bool> set_bound;
777 : 9032 : std::vector<Node> sum_bound;
778 [ + + ]: 13103 : for (const std::pair<const Node, Node>& m : msum)
779 : : {
780 : 8587 : Node v = m.first;
781 [ + + ]: 8587 : if (v.isNull())
782 : : {
783 [ - + ]: 3719 : sum_bound.push_back(m.second.isNull() ? d_one : m.second);
784 : : }
785 : : else
786 : : {
787 [ + - ]: 4868 : Trace("nl-ext-cms-debug") << "- monomial : " << v << std::endl;
788 : : // --- whether we should set a lower bound for this monomial
789 : : bool set_lower =
790 [ + + ][ - + ]: 4868 : (m.second.isNull() || m.second.getConst<Rational>().sgn() == 1)
791 : 4868 : == pol;
792 [ + - ]: 9736 : Trace("nl-ext-cms-debug")
793 [ - - ]: 4868 : << "set bound to " << (set_lower ? "lower" : "upper") << std::endl;
794 : :
795 : : // --- Collect variables and factors in v
796 : 4868 : std::vector<Node> vars;
797 : 4868 : std::vector<unsigned> factors;
798 [ - + ]: 4868 : if (v.getKind() == Kind::NONLINEAR_MULT)
799 : : {
800 : 0 : unsigned last_start = 0;
801 [ - - ]: 0 : for (unsigned i = 0, nchildren = v.getNumChildren(); i < nchildren; i++)
802 : : {
803 : : // are we at the end?
804 : 0 : if (i + 1 == nchildren || v[i + 1] != v[i])
805 : : {
806 : 0 : unsigned vfact = 1 + (i - last_start);
807 : 0 : last_start = (i + 1);
808 : 0 : vars.push_back(v[i]);
809 : 0 : factors.push_back(vfact);
810 : : }
811 : : }
812 : : }
813 : : else
814 : : {
815 : 4868 : vars.push_back(v);
816 : 4868 : factors.push_back(1);
817 : : }
818 : :
819 : : // --- Get the lower and upper bounds and sign information.
820 : : // Whether we have an (odd) number of negative factors in vars, apart
821 : : // from the variable at choose_index.
822 : 4868 : bool has_neg_factor = false;
823 : 4868 : int choose_index = -1;
824 : 4868 : std::vector<Node> ls;
825 : 4868 : std::vector<Node> us;
826 : : // the relevant sign information for variables with odd exponents:
827 : : // 1: both signs of the interval of this variable are positive,
828 : : // -1: both signs of the interval of this variable are negative.
829 : 4868 : std::vector<int> signs;
830 [ + - ]: 4868 : Trace("nl-ext-cms-debug") << "get sign information..." << std::endl;
831 [ + + ]: 9736 : for (unsigned i = 0, size = vars.size(); i < size; i++)
832 : : {
833 : 4868 : Node vc = vars[i];
834 : 4868 : unsigned vcfact = factors[i];
835 [ - + ]: 4868 : if (TraceIsOn("nl-ext-cms-debug"))
836 : : {
837 [ - - ]: 0 : Trace("nl-ext-cms-debug") << "-- " << vc;
838 [ - - ]: 0 : if (vcfact > 1)
839 : : {
840 [ - - ]: 0 : Trace("nl-ext-cms-debug") << "^" << vcfact;
841 : : }
842 [ - - ]: 0 : Trace("nl-ext-cms-debug") << " ";
843 : : }
844 : : std::map<Node, std::pair<Node, Node>>::iterator bit =
845 : 4868 : d_check_model_bounds.find(vc);
846 : : // if there is a model bound for this term
847 [ + - ]: 4868 : if (bit != d_check_model_bounds.end())
848 : : {
849 : 4868 : Node l = bit->second.first;
850 : 4868 : Node u = bit->second.second;
851 : 4868 : ls.push_back(l);
852 : 4868 : us.push_back(u);
853 : 4868 : int vsign = 0;
854 [ + - ]: 4868 : if (vcfact % 2 == 1)
855 : : {
856 : 4868 : vsign = 1;
857 : 4868 : int lsgn = l.getConst<Rational>().sgn();
858 : 4868 : int usgn = u.getConst<Rational>().sgn();
859 [ + - ]: 9736 : Trace("nl-ext-cms-debug")
860 : 4868 : << "bound_sign(" << lsgn << "," << usgn << ") ";
861 [ + + ]: 4868 : if (lsgn == -1)
862 : : {
863 [ + - ]: 16 : if (usgn < 1)
864 : : {
865 : : // must have a negative factor
866 : 16 : has_neg_factor = !has_neg_factor;
867 : 16 : vsign = -1;
868 : : }
869 [ - - ]: 0 : else if (choose_index == -1)
870 : : {
871 : : // set the choose index to this
872 : 0 : choose_index = i;
873 : 0 : vsign = 0;
874 : : }
875 : : else
876 : : {
877 : : // ambiguous, can't determine the bound
878 [ - - ]: 0 : Trace("nl-ext-cms")
879 : 0 : << " failed due to ambiguious monomial." << std::endl;
880 : 0 : return false;
881 : : }
882 : : }
883 : : }
884 [ + - ]: 4868 : Trace("nl-ext-cms-debug") << " -> " << vsign << std::endl;
885 : 4868 : signs.push_back(vsign);
886 : : }
887 : : else
888 : : {
889 [ - - ]: 0 : Trace("nl-ext-cms-debug") << std::endl;
890 [ - - ]: 0 : Trace("nl-ext-cms")
891 : 0 : << " failed due to unknown bound for " << vc << std::endl;
892 : : // should either assign a model bound or eliminate the variable
893 : : // via substitution
894 : 0 : Assert(false) << "A variable " << vc
895 : 0 : << " is missing a bound/value in the model";
896 : : return false;
897 : : }
898 : : }
899 : : // whether we will try to minimize/maximize (-1/1) the absolute value
900 [ + + ]: 4868 : int setAbs = (set_lower == has_neg_factor) ? 1 : -1;
901 [ + - ]: 9736 : Trace("nl-ext-cms-debug")
902 [ - - ]: 0 : << "set absolute value to " << (setAbs == 1 ? "maximal" : "minimal")
903 : 4868 : << std::endl;
904 : :
905 : 4868 : std::vector<Node> vbs;
906 [ + - ]: 4868 : Trace("nl-ext-cms-debug") << "set bounds..." << std::endl;
907 [ + + ]: 9736 : for (unsigned i = 0, size = vars.size(); i < size; i++)
908 : : {
909 : 4868 : Node vc = vars[i];
910 : 4868 : unsigned vcfact = factors[i];
911 : 4868 : Node l = ls[i];
912 : 4868 : Node u = us[i];
913 : : bool vc_set_lower;
914 : 4868 : int vcsign = signs[i];
915 [ + - ]: 9736 : Trace("nl-ext-cms-debug")
916 : 0 : << "Bounds for " << vc << " : " << l << ", " << u
917 : 4868 : << ", sign : " << vcsign << ", factor : " << vcfact << std::endl;
918 [ - + ]: 4868 : if (l == u)
919 : : {
920 : : // by convention, always say it is lower if they are the same
921 : 0 : vc_set_lower = true;
922 [ - - ]: 0 : Trace("nl-ext-cms-debug")
923 : 0 : << "..." << vc << " equal bound, set to lower" << std::endl;
924 : : }
925 : : else
926 : : {
927 [ - + ]: 4868 : if (vcfact % 2 == 0)
928 : : {
929 : : // minimize or maximize its absolute value
930 : 0 : Rational la = l.getConst<Rational>().abs();
931 : 0 : Rational ua = u.getConst<Rational>().abs();
932 [ - - ]: 0 : if (la == ua)
933 : : {
934 : : // by convention, always say it is lower if abs are the same
935 : 0 : vc_set_lower = true;
936 [ - - ]: 0 : Trace("nl-ext-cms-debug")
937 : 0 : << "..." << vc << " equal abs, set to lower" << std::endl;
938 : : }
939 : : else
940 : : {
941 : 0 : vc_set_lower = (la > ua) == (setAbs == 1);
942 : : }
943 : : }
944 [ - + ]: 4868 : else if (signs[i] == 0)
945 : : {
946 : : // we choose this index to match the overall set_lower
947 : 0 : vc_set_lower = set_lower;
948 : : }
949 : : else
950 : : {
951 : 4868 : vc_set_lower = (signs[i] != setAbs);
952 : : }
953 [ + - ]: 9736 : Trace("nl-ext-cms-debug")
954 [ - - ]: 0 : << "..." << vc << " set to " << (vc_set_lower ? "lower" : "upper")
955 : 4868 : << std::endl;
956 : : }
957 : : // check whether this is a conflicting bound
958 : 4868 : std::map<Node, bool>::iterator itsb = set_bound.find(vc);
959 [ + - ]: 4868 : if (itsb == set_bound.end())
960 : : {
961 : 4868 : set_bound[vc] = vc_set_lower;
962 : : }
963 [ - - ]: 0 : else if (itsb->second != vc_set_lower)
964 : : {
965 [ - - ]: 0 : Trace("nl-ext-cms")
966 : 0 : << " failed due to conflicting bound for " << vc << std::endl;
967 : 0 : return false;
968 : : }
969 : : // must over/under approximate based on vc_set_lower, computed above
970 [ + + ]: 9736 : Node vb = vc_set_lower ? l : u;
971 [ + + ]: 9736 : for (unsigned i2 = 0; i2 < vcfact; i2++)
972 : : {
973 : 4868 : vbs.push_back(vb);
974 : : }
975 : : }
976 [ - + ]: 4868 : if (!simpleSuccess)
977 : : {
978 : 0 : break;
979 : : }
980 [ + - ]: 4868 : Node vbound = vbs.size() == 1 ? vbs[0] : nm->mkNode(Kind::MULT, vbs);
981 : 4868 : sum_bound.push_back(ArithMSum::mkCoeffTerm(m.second, vbound));
982 : : }
983 : : }
984 : : // if the exact bound was computed via simple analysis above
985 : : // make the bound
986 : 9032 : Node bound;
987 [ + + ]: 4516 : if (sum_bound.size() > 1)
988 : : {
989 : 3843 : bound = nm->mkNode(Kind::ADD, sum_bound);
990 : : }
991 [ + - ]: 673 : else if (sum_bound.size() == 1)
992 : : {
993 : 673 : bound = sum_bound[0];
994 : : }
995 : : else
996 : : {
997 : 0 : bound = d_zero;
998 : : }
999 : : // make the comparison
1000 : 13548 : Node comp = nm->mkNode(Kind::GEQ, bound, d_zero);
1001 [ + + ]: 4516 : if (!pol)
1002 : : {
1003 : 2574 : comp = comp.negate();
1004 : : }
1005 [ + - ]: 4516 : Trace("nl-ext-cms") << " comparison is : " << comp << std::endl;
1006 : 4516 : comp = rewrite(comp);
1007 [ - + ][ - + ]: 4516 : Assert(comp.isConst());
[ - - ]
1008 [ + - ]: 4516 : Trace("nl-ext-cms") << " returned : " << comp << std::endl;
1009 : 4516 : return comp == d_true;
1010 : : }
1011 : :
1012 : 86546 : void NlModel::printModelValue(const char* c, Node n, unsigned prec) const
1013 : : {
1014 [ - + ]: 86546 : if (TraceIsOn(c))
1015 : : {
1016 [ - - ]: 0 : Trace(c) << " " << n << " -> ";
1017 : 0 : const Node& aval = d_abstractModelCache.at(n);
1018 [ - - ]: 0 : if (aval.isConst())
1019 : : {
1020 : 0 : printRationalApprox(c, aval, prec);
1021 : : }
1022 : : else
1023 : : {
1024 [ - - ]: 0 : Trace(c) << "?";
1025 : : }
1026 [ - - ]: 0 : Trace(c) << " [actual: ";
1027 : 0 : const Node& cval = d_concreteModelCache.at(n);
1028 [ - - ]: 0 : if (cval.isConst())
1029 : : {
1030 : 0 : printRationalApprox(c, cval, prec);
1031 : : }
1032 : : else
1033 : : {
1034 [ - - ]: 0 : Trace(c) << "?";
1035 : : }
1036 [ - - ]: 0 : Trace(c) << " ]" << std::endl;
1037 : : }
1038 : 86546 : }
1039 : :
1040 : 1368 : void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel)
1041 : : {
1042 : 1368 : NodeManager* nm = nodeManager();
1043 [ + - ]: 1368 : Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
1044 : : // If we extended the model with entries x -> 0 for unconstrained values,
1045 : : // we first update the map to the extended one.
1046 [ + + ]: 1368 : if (d_arithVal.size() > arithModel.size())
1047 : : {
1048 : 12 : arithModel = d_arithVal;
1049 : : }
1050 : : // Record the approximations we used. This code calls the
1051 : : // recordApproximation method of the model, which overrides the model
1052 : : // values for variables that we solved for, using techniques specific to
1053 : : // this class.
1054 : 89 : for (const std::pair<const Node, std::pair<Node, Node>>& cb :
1055 [ + + ]: 1546 : d_check_model_bounds)
1056 : : {
1057 : 178 : Node l = cb.second.first;
1058 : 178 : Node u = cb.second.second;
1059 : 178 : Node v = cb.first;
1060 [ + - ]: 89 : if (l != u)
1061 : : {
1062 [ + - ]: 178 : Trace("nl-model") << v << " is in interval " << l << "..." << u
1063 : 89 : << std::endl;
1064 : : }
1065 : : else
1066 : : {
1067 : : // overwrite, ensure the type is correct
1068 : 0 : Assert(l.isConst());
1069 : 0 : Node ll = nm->mkConstRealOrInt(v.getType(), l.getConst<Rational>());
1070 : 0 : arithModel[v] = ll;
1071 [ - - ]: 0 : Trace("nl-model") << v << " exact approximation is " << ll << std::endl;
1072 : : }
1073 : : }
1074 : : // Also record the exact values we used. An exact value can be seen as a
1075 : : // special kind approximation of the form (witness x. x = exact_value).
1076 : : // Notice that the above term gets rewritten such that the choice function
1077 : : // is eliminated.
1078 [ + + ]: 2337 : for (size_t i = 0; i < d_substitutions.size(); ++i)
1079 : : {
1080 : : // overwrite, ensure the type is correct
1081 : 1938 : Node v = d_substitutions.d_vars[i];
1082 : 1938 : Node s = d_substitutions.d_subs[i];
1083 : 969 : Node ss = s;
1084 : : // If its a rational constant, ensure it has the proper type now. It
1085 : : // also may be a RAN, in which case v should be a real.
1086 [ + + ]: 969 : if (s.isConst())
1087 : : {
1088 : 896 : ss = nm->mkConstRealOrInt(v.getType(), s.getConst<Rational>());
1089 : : }
1090 : 969 : arithModel[v] = ss;
1091 [ + - ]: 969 : Trace("nl-model") << v << " solved is " << ss << std::endl;
1092 : : }
1093 : :
1094 : : // multiplication terms should not be given values; their values are
1095 : : // implied by the monomials that they consist of
1096 : 2736 : std::vector<Node> amErase;
1097 [ + + ]: 21687 : for (const std::pair<const Node, Node>& am : arithModel)
1098 : : {
1099 [ + + ]: 20319 : if (am.first.getKind() == Kind::NONLINEAR_MULT)
1100 : : {
1101 : 3859 : amErase.push_back(am.first);
1102 : : }
1103 : : }
1104 [ + + ]: 5227 : for (const Node& ae : amErase)
1105 : : {
1106 : 3859 : arithModel.erase(ae);
1107 : : }
1108 : 1368 : }
1109 : :
1110 : 115988 : Node NlModel::getValueInternal(TNode n)
1111 : : {
1112 [ - + ]: 115988 : if (n.isConst())
1113 : : {
1114 : 0 : return n;
1115 : : }
1116 [ + + ]: 115988 : if (auto it = d_arithVal.find(n); it != d_arithVal.end())
1117 : : {
1118 [ - + ][ - + ]: 115911 : AlwaysAssert(it->second.isConst());
[ - - ]
1119 : 115911 : return it->second;
1120 : : }
1121 : : // It is unconstrained in the model, return 0. We additionally add it
1122 : : // to mapping from the linear solver. This ensures that if the nonlinear
1123 : : // solver assumes that n = 0, then this assumption is recorded in the overall
1124 : : // model.
1125 : 154 : Node zero = mkZero(n.getType());
1126 : 77 : d_arithVal[n] = zero;
1127 : 77 : return zero;
1128 : : }
1129 : :
1130 : 10191 : bool NlModel::hasAssignment(Node v) const
1131 : : {
1132 [ - + ]: 10191 : if (d_check_model_bounds.find(v) != d_check_model_bounds.end())
1133 : : {
1134 : 0 : return true;
1135 : : }
1136 : 10191 : return (d_substitutions.contains(v));
1137 : : }
1138 : :
1139 : 583878 : bool NlModel::hasLinearModelValue(TNode v, Node& val) const
1140 : : {
1141 : 583878 : auto it = d_arithVal.find(v);
1142 [ + + ]: 583878 : if (it != d_arithVal.end())
1143 : : {
1144 : 93130 : val = it->second;
1145 : 93130 : return true;
1146 : : }
1147 : 490748 : return false;
1148 : : }
1149 : :
1150 : 57044 : Node NlModel::getSubstitutedForm(TNode s) const
1151 : : {
1152 [ + + ]: 57044 : if (d_substitutions.empty())
1153 : : {
1154 : : // no substitutions, just return s
1155 : 2792 : return s;
1156 : : }
1157 : 54252 : return rewrite(d_substitutions.applyArith(s));
1158 : : }
1159 : :
1160 : : } // namespace nl
1161 : : } // namespace arith
1162 : : } // namespace theory
1163 : : } // namespace cvc5::internal
|
