From 5dcaa28edfa676c57fbbab75767b422e7fab349c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Oct 2020 09:38:45 -0500 Subject: [PATCH] Guard uses of printing approximations for constants (#5247) Errors with these methods were encountered while working on new techniques for arithmetic preprocessing. Also, there is obvious inefficiency since approximations for constants are being computed when certain traces are disabled. --- src/theory/arith/arith_utilities.cpp | 13 +++++- src/theory/arith/nl/nl_model.cpp | 68 ++++++++++++++++++---------- 2 files changed, 54 insertions(+), 27 deletions(-) diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index cbd976b03..1a5bc356f 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -106,7 +106,11 @@ bool isTranscendentalKind(Kind k) Node getApproximateConstant(Node c, bool isLower, unsigned prec) { - Assert(c.isConst()); + if (!c.isConst()) + { + Assert(false) << "getApproximateConstant: non-constant input " << c; + return Node::null(); + } Rational cr = c.getConst(); unsigned lower = 0; @@ -178,7 +182,12 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec) void printRationalApprox(const char* c, Node cr, unsigned prec) { - Assert(cr.isConst()); + if (!cr.isConst()) + { + Assert(false) << "printRationalApprox: non-constant input " << cr; + Trace(c) << cr; + return; + } Node ca = getApproximateConstant(cr, true, prec); if (ca != cr) { diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 711173bc8..b27654b2c 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -260,10 +260,13 @@ bool NlModel::checkModel(const std::vector& assertions, { // set its exact model value in the substitution Node curv = computeConcreteModelValue(cur); - Trace("nl-ext-cm") - << "check-model-bound : exact : " << cur << " = "; - printRationalApprox("nl-ext-cm", curv); - Trace("nl-ext-cm") << std::endl; + if (Trace.isOn("nl-ext-cm")) + { + Trace("nl-ext-cm") + << "check-model-bound : exact : " << cur << " = "; + printRationalApprox("nl-ext-cm", curv); + Trace("nl-ext-cm") << std::endl; + } bool ret = addCheckModelSubstitution(cur, curv); AlwaysAssert(ret); } @@ -591,9 +594,12 @@ bool NlModel::solveEqualitySimple(Node eq, if (uvf.isVar() && !hasCheckModelAssignment(uvf)) { Node uvfv = computeConcreteModelValue(uvf); - Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = "; - printRationalApprox("nl-ext-cm", uvfv); - Trace("nl-ext-cm") << std::endl; + if (Trace.isOn("nl-ext-cm")) + { + Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = "; + printRationalApprox("nl-ext-cm", uvfv); + Trace("nl-ext-cm") << std::endl; + } bool ret = addCheckModelSubstitution(uvf, uvfv); // recurse return ret ? solveEqualitySimple(eq, d, lemmas) : false; @@ -620,9 +626,12 @@ bool NlModel::solveEqualitySimple(Node eq, return false; } Node val = nm->mkConst(-c.getConst() / b.getConst()); - Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = "; - printRationalApprox("nl-ext-cm", val); - Trace("nl-ext-cm") << std::endl; + if (Trace.isOn("nl-ext-cm")) + { + Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = "; + printRationalApprox("nl-ext-cm", val); + Trace("nl-ext-cm") << std::endl; + } bool ret = addCheckModelSubstitution(var, val); if (ret) { @@ -701,31 +710,40 @@ bool NlModel::solveEqualitySimple(Node eq, nm->mkNode(MULT, nm->mkConst(Rational(1) / Rational(2)), nm->mkNode(PLUS, bounds[r][0], bounds[r][1]))); - Trace("nl-ext-cm-debug") << "Bound option #" << r << " : "; - printRationalApprox("nl-ext-cm-debug", bounds[r][0]); - Trace("nl-ext-cm-debug") << "..."; - printRationalApprox("nl-ext-cm-debug", bounds[r][1]); - Trace("nl-ext-cm-debug") << std::endl; + if (Trace.isOn("nl-ext-cm-debug")) + { + Trace("nl-ext-cm-debug") << "Bound option #" << r << " : "; + printRationalApprox("nl-ext-cm-debug", bounds[r][0]); + Trace("nl-ext-cm-debug") << "..."; + printRationalApprox("nl-ext-cm-debug", bounds[r][1]); + Trace("nl-ext-cm-debug") << std::endl; + } diff = Rewriter::rewrite(diff); Assert(diff.isConst()); diff = nm->mkConst(diff.getConst().abs()); diff_bound[r] = diff; - Trace("nl-ext-cm-debug") << "...diff from model value ("; - printRationalApprox("nl-ext-cm-debug", m_var); - Trace("nl-ext-cm-debug") << ") is "; - printRationalApprox("nl-ext-cm-debug", diff_bound[r]); - Trace("nl-ext-cm-debug") << std::endl; + if (Trace.isOn("nl-ext-cm-debug")) + { + Trace("nl-ext-cm-debug") << "...diff from model value ("; + printRationalApprox("nl-ext-cm-debug", m_var); + Trace("nl-ext-cm-debug") << ") is "; + printRationalApprox("nl-ext-cm-debug", diff_bound[r]); + Trace("nl-ext-cm-debug") << std::endl; + } } // take the one that var is closer to in the model Node cmp = nm->mkNode(GEQ, diff_bound[0], diff_bound[1]); cmp = Rewriter::rewrite(cmp); Assert(cmp.isConst()); unsigned r_use_index = cmp == d_true ? 1 : 0; - Trace("nl-ext-cm") << "check-model-bound : approximate (sqrt) : "; - printRationalApprox("nl-ext-cm", bounds[r_use_index][0]); - Trace("nl-ext-cm") << " <= " << var << " <= "; - printRationalApprox("nl-ext-cm", bounds[r_use_index][1]); - Trace("nl-ext-cm") << std::endl; + if (Trace.isOn("nl-ext-cm")) + { + Trace("nl-ext-cm") << "check-model-bound : approximate (sqrt) : "; + printRationalApprox("nl-ext-cm", bounds[r_use_index][0]); + Trace("nl-ext-cm") << " <= " << var << " <= "; + printRationalApprox("nl-ext-cm", bounds[r_use_index][1]); + Trace("nl-ext-cm") << std::endl; + } bool ret = addCheckModelBound(var, bounds[r_use_index][0], bounds[r_use_index][1]); if (ret) -- 2.30.2