From 23eb6c0ab05b6607c14ee33b5c0101381aa0bc41 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Dec 2019 11:58:53 -0600 Subject: [PATCH] Do not substitute beneath arithmetic terms in the non-linear solver (#3324) --- src/theory/arith/arith_utilities.cpp | 78 ++++++++++++++++++++++++ src/theory/arith/arith_utilities.h | 10 +++ src/theory/arith/nl_model.cpp | 19 +++--- src/theory/arith/nonlinear_extension.cpp | 3 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/nl/issue3307.smt2 | 14 +++++ 6 files changed, 112 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress1/nl/issue3307.smt2 diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 3d3078d99..65aaceb80 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -191,6 +191,84 @@ void printRationalApprox(const char* c, Node cr, unsigned prec) } } +Node arithSubstitute(Node n, std::vector& vars, std::vector& subs) +{ + Assert(vars.size() == subs.size()); + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector::iterator itv; + std::vector visit; + TNode cur; + Kind ck; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited[cur] = Node::null(); + ck = cur.getKind(); + itv = std::find(vars.begin(), vars.end(), cur); + if (itv != vars.end()) + { + visited[cur] = subs[std::distance(vars.begin(), itv)]; + } + else if (cur.getNumChildren() == 0) + { + visited[cur] = cur; + } + else + { + TheoryId ctid = theory::kindToTheoryId(ck); + if (ctid != THEORY_ARITH && ctid != THEORY_BOOL + && ctid != THEORY_BUILTIN) + { + // do not traverse beneath applications that belong to another theory + visited[cur] = cur; + } + else + { + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d737fefeb..f87a908b4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -325,6 +325,16 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec); /** print rational approximation of cr with precision prec on trace c */ void printRationalApprox(const char* c, Node cr, unsigned prec = 5); +/** Arithmetic substitute + * + * This computes the substitution n { vars -> subs }, but with the caveat + * that subterms of n that belong to a theory other than arithmetic are + * not traversed. In other words, terms that belong to other theories are + * treated as atomic variables. For example: + * (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3. + */ +Node arithSubstitute(Node n, std::vector& vars, std::vector& subs); + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index fe756e5f7..3274867bb 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -284,10 +284,7 @@ bool NlModel::checkModel(const std::vector& assertions, // apply the substitution to a if (!d_check_model_vars.empty()) { - av = av.substitute(d_check_model_vars.begin(), - d_check_model_vars.end(), - d_check_model_subs.begin(), - d_check_model_subs.end()); + av = arithSubstitute(av, d_check_model_vars, d_check_model_subs); av = Rewriter::rewrite(av); } // simple check literal @@ -360,10 +357,14 @@ bool NlModel::addCheckModelSubstitution(TNode v, TNode s) return false; } } + std::vector varsTmp; + varsTmp.push_back(v); + std::vector subsTmp; + subsTmp.push_back(s); for (unsigned i = 0, size = d_check_model_subs.size(); i < size; i++) { Node ms = d_check_model_subs[i]; - Node mss = ms.substitute(v, s); + Node mss = arithSubstitute(ms, varsTmp, subsTmp); if (mss != ms) { mss = Rewriter::rewrite(mss); @@ -430,10 +431,7 @@ bool NlModel::solveEqualitySimple(Node eq, Node seq = eq; if (!d_check_model_vars.empty()) { - seq = eq.substitute(d_check_model_vars.begin(), - d_check_model_vars.end(), - d_check_model_subs.begin(), - d_check_model_subs.end()); + seq = arithSubstitute(eq, d_check_model_vars, d_check_model_subs); seq = Rewriter::rewrite(seq); if (seq.isConst()) { @@ -866,8 +864,7 @@ bool NlModel::simpleCheckModelLit(Node lit) for (unsigned r = 0; r < 2; r++) { qsubs.push_back(boundn[r]); - Node ts = t.substitute( - qvars.begin(), qvars.end(), qsubs.begin(), qsubs.end()); + Node ts = arithSubstitute(t, qvars, qsubs); tcmpn[r] = Rewriter::rewrite(ts); qsubs.pop_back(); } diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 6e8e7623d..ff2ec412b 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -772,8 +772,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Node pa = a; if (!pvars.empty()) { - pa = - pa.substitute(pvars.begin(), pvars.end(), psubs.begin(), psubs.end()); + pa = arithSubstitute(pa, pvars, psubs); pa = Rewriter::rewrite(pa); } if (!pa.isConst() || !pa.getConst()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index edc44c3d2..814eaab49 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1264,6 +1264,7 @@ set(regress_1_tests regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 + regress1/nl/issue3307.smt2 regress1/nl/issue3441.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 diff --git a/test/regress/regress1/nl/issue3307.smt2 b/test/regress/regress1/nl/issue3307.smt2 new file mode 100644 index 000000000..803bfeb3a --- /dev/null +++ b/test/regress/regress1/nl/issue3307.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(assert + (and + (> b 1) + (< a 0) + (>= (/ 0 (+ (* a b) (/ (- a) 0))) a) + ) + ) +(check-sat) -- 2.30.2