From 509ecd23cff74a68ba5971308cfc5313bc6c202f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Mar 2022 16:12:55 -0500 Subject: [PATCH] Fix issues involving multiple sources of model substitutions in NL (#8300) Fixes #8294. The first benchmark times out, the second is added as a regression. The issues center around 2 sources of substitutions (coverings and sine solvers) for model substitutions. Also does minor cleanup to nl model. --- src/theory/arith/nl/coverings_solver.cpp | 8 +- src/theory/arith/nl/nl_model.cpp | 125 +++++++++--------- src/theory/arith/nl/nl_model.h | 3 + .../arith/nl/transcendental/sine_solver.cpp | 2 + test/regress/CMakeLists.txt | 1 + .../nl/nta/issue8294-2-double-solve.smt2 | 8 ++ 6 files changed, 85 insertions(+), 62 deletions(-) create mode 100644 test/regress/regress0/nl/nta/issue8294-2-double-solve.smt2 diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp index 2ec366d2a..062a9213b 100644 --- a/src/theory/arith/nl/coverings_solver.cpp +++ b/src/theory/arith/nl/coverings_solver.cpp @@ -244,9 +244,13 @@ bool CoveringsSolver::constructModelIfAvailable(std::vector& assertions) void CoveringsSolver::addToModel(TNode var, TNode value) const { - Trace("nl-cov") << "-> " << var << " = " << value << std::endl; Assert(value.getType().isRealOrInt()); - d_model.addSubstitution(var, value); + // we must take its substituted form here, since other solvers (e.g. the + // reductions inference of the sine solver) may have introduced substitutions + // internally during check. + Node svalue = d_model.getSubstitutedForm(value); + Trace("nl-cov") << "-> " << var << " = " << svalue << std::endl; + d_model.addSubstitution(var, svalue); } } // namespace nl diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index c566758be..3c9458ae3 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -173,12 +173,15 @@ bool NlModel::checkModel(const std::vector& assertions, unsigned d, std::vector& lemmas) { - Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl; + Trace("nl-ext-cm-debug") << "NlModel::checkModel: solve for equalities..." + << std::endl; for (const Node& atom : assertions) { + Trace("nl-ext-cm-debug") << "- assertion: " << atom << std::endl; // see if it corresponds to a univariate polynomial equation of degree two if (atom.getKind() == EQUAL) { + // we substitute inside of solve equality simple if (!solveEqualitySimple(atom, d, lemmas)) { // no chance we will satisfy this equality @@ -227,10 +230,7 @@ bool NlModel::checkModel(const std::vector& assertions, } } } - for (const Node& cn : cur) - { - visit.push_back(cn); - } + visit.insert(visit.end(), cur.begin(), cur.end()); } } while (!visit.empty()); } @@ -241,12 +241,10 @@ bool NlModel::checkModel(const std::vector& assertions, { if (d_check_model_solved.find(a) == d_check_model_solved.end()) { - Node av = a; // apply the substitution to a - if (!d_substitutions.empty()) - { - av = rewrite(arithSubstitute(av, d_substitutions)); - } + Node av = getSubstitutedForm(a); + Trace("nl-ext-cm") << "simpleCheckModelLit " << av << " (from " << a + << ")" << std::endl; // simple check literal if (!simpleCheckModelLit(av)) { @@ -271,18 +269,25 @@ bool NlModel::checkModel(const std::vector& assertions, bool NlModel::addSubstitution(TNode v, TNode s) { - // should not substitute the same variable twice Trace("nl-ext-model") << "* check model substitution : " << v << " -> " << s << std::endl; + Assert(getSubstitutedForm(s) == s) + << "Added a substitution whose range is not in substituted form " << s; + // should not substitute the same variable twice // should not set exact bound more than once if (d_substitutions.contains(v)) { Node cur = d_substitutions.getSubs(v); if (cur != s) { - Trace("nl-ext-model") << "...ERROR: already has value: " << cur << std::endl; - // this should never happen since substitutions should be applied eagerly - Assert(false); + Trace("nl-ext-model") + << "...warning: already has value: " << cur << std::endl; + // We set two different substitutions for a variable v. If both are + // constant, then we throw an error. Otherwise, we ignore the newer + // substitution and return false here. + Assert(!cur.isConst() || !s.isConst()) + << "Conflicting exact bounds given for a variable (" << cur << " and " + << s << ") for " << v; return false; } } @@ -292,11 +297,14 @@ bool NlModel::addSubstitution(TNode v, TNode s) d_check_model_bounds.find(v); if (itb != d_check_model_bounds.end()) { - if (s.getConst() >= itb->second.first.getConst() - || s.getConst() <= itb->second.second.getConst()) + Assert(s.isConst()); + if (s.getConst() <= itb->second.first.getConst() + || s.getConst() >= itb->second.second.getConst()) { Trace("nl-ext-model") << "...ERROR: already has bound which is out of range." << std::endl; + Assert(false) << "Out of bounds exact bound given for a variable with an " + "approximate bound"; return false; } } @@ -329,7 +337,7 @@ bool NlModel::addBound(TNode v, TNode l, TNode u) Trace("nl-ext-model") << "...ERROR: setting bound for variable that already has exact value." << std::endl; - Assert(false); + Assert(false) << "Setting bound for variable that already has exact value."; return false; } Assert(l.isConst()); @@ -358,8 +366,7 @@ bool NlModel::solveEqualitySimple(Node eq, Node seq = eq; if (!d_substitutions.empty()) { - seq = arithSubstitute(eq, d_substitutions); - seq = rewrite(seq); + seq = getSubstitutedForm(eq); if (seq.isConst()) { if (seq.getConst()) @@ -383,7 +390,6 @@ bool NlModel::solveEqualitySimple(Node eq, bool is_valid = true; // the variable we will solve a quadratic equation for Node var; - Node a = d_zero; Node b = d_zero; Node c = d_zero; NodeManager* nm = NodeManager::currentNM(); @@ -403,23 +409,13 @@ bool NlModel::solveEqualitySimple(Node eq, } else if (v.getKind() == NONLINEAR_MULT) { - if (v.getNumChildren() == 2 && v[0].isVar() && v[0] == v[1] - && (var.isNull() || var == v[0])) - { - // may solve quadratic - a = coeff; - var = v[0]; - } - else + is_valid = false; + Trace("nl-ext-cms-debug") + << "...invalid due to non-linear monomial " << v << std::endl; + // may wish to set an exact bound for a factor and repeat + for (const Node& vc : v) { - is_valid = false; - Trace("nl-ext-cms-debug") - << "...invalid due to non-linear monomial " << v << std::endl; - // may wish to set an exact bound for a factor and repeat - for (const Node& vc : v) - { - unc_vars_factor.insert(vc); - } + unc_vars_factor.insert(vc); } } else if (!v.isVar() || (!var.isNull() && var != v)) @@ -462,6 +458,8 @@ bool NlModel::solveEqualitySimple(Node eq, if (ArithMSum::isolate(uv, msum, veqc, slv, EQUAL) != 0) { Assert(!slv.isNull()); + // must rewrite here to be in substituted form + slv = rewrite(slv); // Currently do not support substitution-with-coefficients. // We also ensure types are correct here, which avoids substituting // a term of non-integer type for a variable of integer type. @@ -513,31 +511,27 @@ bool NlModel::solveEqualitySimple(Node eq, } // we are linear, it is simple - if (a == d_zero) + if (b == d_zero) { - if (b == d_zero) - { - Trace("nl-ext-cms") << "...fail due to zero a/b." << std::endl; - Assert(false); - return false; - } - Node val = nm->mkConst(CONST_RATIONAL, - -c.getConst() / b.getConst()); - 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 = addSubstitution(var, val); - if (ret) - { - Trace("nl-ext-cms") << "...success, solved linear." << std::endl; - d_check_model_solved[eq] = var; - } - return ret; + Trace("nl-ext-cms") << "...fail due to zero a/b." << std::endl; + Assert(false); + return false; } - return false; + Node val = nm->mkConst(CONST_RATIONAL, + -c.getConst() / b.getConst()); + 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 = addSubstitution(var, val); + if (ret) + { + Trace("nl-ext-cms") << "...success, solved linear." << std::endl; + d_check_model_solved[eq] = var; + } + return ret; } bool NlModel::simpleCheckModelLit(Node lit) @@ -870,7 +864,8 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) << " failed due to unknown bound for " << vc << std::endl; // should either assign a model bound or eliminate the variable // via substitution - Assert(false); + Assert(false) << "A variable " << vc + << " is missing a bound/value in the model"; return false; } } @@ -1113,6 +1108,16 @@ bool NlModel::hasLinearModelValue(TNode v, Node& val) const return false; } +Node NlModel::getSubstitutedForm(TNode s) const +{ + if (d_substitutions.empty()) + { + // no substitutions, just return s + return s; + } + return rewrite(arithSubstitute(s, d_substitutions)); +} + } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 265e270db..a9cc38b36 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -176,6 +176,9 @@ class NlModel : protected EnvObj */ void getModelValueRepair(std::map& arithModel); + /** Return the substituted form of s */ + Node getSubstitutedForm(TNode s) const; + private: /** Cache for concrete model values */ std::map d_concreteModelCache; diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 6645589e2..b937dcb99 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -138,6 +138,8 @@ void SineSolver::doReductions() else { // remember that the argument is equal to the boundary point + Trace("nl-ext") << "SineSolver::doReductions: substitution: " << tf[0] + << " -> " << itv->second << std::endl; d_data->d_model.addSubstitution(tf[0], itv->second); // all congruent transcendental functions are exactly equal to its // value diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 61fd9a13e..45d3701fc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -809,6 +809,7 @@ set(regress_0_tests regress0/nl/nta/issue8182-2-exact-mv-keep.smt2 regress0/nl/nta/issue8183-tc-pi.smt2 regress0/nl/nta/issue8208-red-nred.smt2 + regress0/nl/nta/issue8294-2-double-solve.smt2 regress0/nl/nta/proj-issue376.smt2 regress0/nl/nta/proj-issue403.smt2 regress0/nl/nta/proj-issue460-pi-value.smt2 diff --git a/test/regress/regress0/nl/nta/issue8294-2-double-solve.smt2 b/test/regress/regress0/nl/nta/issue8294-2-double-solve.smt2 new file mode 100644 index 000000000..fb903fb9f --- /dev/null +++ b/test/regress/regress0/nl/nta/issue8294-2-double-solve.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_NRAT) +(set-info :status sat) +(set-option :re-elim-agg true) +(declare-fun r3 () Real) +(assert (= 0.0 (+ (- r3) (cos r3) (- 1.0)))) +(check-sat) -- 2.30.2