From 71cab467df779fc1a52e8a5f981132f49d9d3182 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 5 Nov 2021 07:15:49 -0700 Subject: [PATCH] Remove quadratic solving in NlModel (#7542) This PR removes obsolete code from NlModel concerned with solving quadratic equations. This code is only used on nonlinear real problems where the cad solver is not used. --- src/theory/arith/nl/nl_model.cpp | 154 +----------------- src/theory/arith/nl/nl_model.h | 10 -- test/regress/regress0/nl/sqrt2-value.smt2 | 2 +- .../quantifiers/issue6607-witness-te.smt2 | 2 +- 4 files changed, 3 insertions(+), 165 deletions(-) diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 427d203ea..77a3ea530 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -553,117 +553,7 @@ bool NlModel::solveEqualitySimple(Node eq, } return ret; } - Trace("nl-ext-quad") << "Solve quadratic : " << seq << std::endl; - Trace("nl-ext-quad") << " a : " << a << std::endl; - Trace("nl-ext-quad") << " b : " << b << std::endl; - Trace("nl-ext-quad") << " c : " << c << std::endl; - Node two_a = nm->mkNode(MULT, d_two, a); - two_a = Rewriter::rewrite(two_a); - Node sqrt_val = nm->mkNode( - MINUS, nm->mkNode(MULT, b, b), nm->mkNode(MULT, d_two, two_a, c)); - sqrt_val = Rewriter::rewrite(sqrt_val); - Trace("nl-ext-quad") << "Will approximate sqrt " << sqrt_val << std::endl; - Assert(sqrt_val.isConst()); - // if it is negative, then we are in conflict - if (sqrt_val.getConst().sgn() == -1) - { - Node conf = seq.negate(); - Trace("nl-ext-lemma") << "NlModel::Lemma : quadratic no root : " << conf - << std::endl; - lemmas.emplace_back(InferenceId::ARITH_NL_CM_QUADRATIC_EQ, conf); - Trace("nl-ext-cms") << "...fail due to negative discriminant." << std::endl; - return false; - } - if (hasAssignment(var)) - { - Trace("nl-ext-cms") << "...fail due to bounds on variable to solve for." - << std::endl; - // two quadratic equations for same variable, give up - return false; - } - // approximate the square root of sqrt_val - Node l, u; - if (!getApproximateSqrt(sqrt_val, l, u, 15 + d)) - { - Trace("nl-ext-cms") << "...fail, could not approximate sqrt." << std::endl; - return false; - } - d_used_approx = true; - Trace("nl-ext-quad") << "...got " << l << " <= sqrt(" << sqrt_val - << ") <= " << u << std::endl; - Node negb = nm->mkConst(-b.getConst()); - Node coeffa = nm->mkConst(Rational(1) / two_a.getConst()); - // two possible bound regions - Node bounds[2][2]; - Node diff_bound[2]; - Node m_var = computeConcreteModelValue(var); - Assert(m_var.isConst()); - for (unsigned r = 0; r < 2; r++) - { - for (unsigned b2 = 0; b2 < 2; b2++) - { - Node val = b2 == 0 ? l : u; - // (-b +- approx_sqrt( b^2 - 4ac ))/2a - Node approx = nm->mkNode( - MULT, coeffa, nm->mkNode(r == 0 ? MINUS : PLUS, negb, val)); - approx = Rewriter::rewrite(approx); - bounds[r][b2] = approx; - Assert(approx.isConst()); - } - if (bounds[r][0].getConst() > bounds[r][1].getConst()) - { - // ensure bound is (lower, upper) - Node tmp = bounds[r][0]; - bounds[r][0] = bounds[r][1]; - bounds[r][1] = tmp; - } - Node diff = - nm->mkNode(MINUS, - m_var, - nm->mkNode(MULT, - nm->mkConst(Rational(1) / Rational(2)), - nm->mkNode(PLUS, bounds[r][0], bounds[r][1]))); - 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; - 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; - 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 = addBound(var, bounds[r_use_index][0], bounds[r_use_index][1]); - if (ret) - { - d_check_model_solved[eq] = var; - Trace("nl-ext-cms") << "...success, solved quadratic." << std::endl; - } - return ret; + return false; } bool NlModel::simpleCheckModelLit(Node lit) @@ -1118,48 +1008,6 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) return comp == d_true; } -bool NlModel::getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter) const -{ - Assert(c.isConst()); - if (c == d_one || c == d_zero) - { - l = c; - u = c; - return true; - } - Rational rc = c.getConst(); - - Rational rl = rc < Rational(1) ? rc : Rational(1); - Rational ru = rc < Rational(1) ? Rational(1) : rc; - unsigned count = 0; - Rational half = Rational(1) / Rational(2); - while (count < iter) - { - Rational curr = half * (rl + ru); - Rational curr_sq = curr * curr; - if (curr_sq == rc) - { - rl = curr; - ru = curr; - break; - } - else if (curr_sq < rc) - { - rl = curr; - } - else - { - ru = curr; - } - count++; - } - - NodeManager* nm = NodeManager::currentNM(); - l = nm->mkConst(rl); - u = nm->mkConst(ru); - return true; -} - void NlModel::printModelValue(const char* c, Node n, unsigned prec) const { if (Trace.isOn(c)) diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index b3b841eab..7dcd89a4a 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -275,16 +275,6 @@ class NlModel bool simpleCheckModelLit(Node lit); bool simpleCheckModelMsum(const std::map& msum, bool pol); //---------------------------end check model - /** - * This approximates the square root of positive constant c. If this method - * returns true, then l and u are updated to constants such that - * l <= sqrt( c ) <= u - * The argument iter is the number of iterations in the binary search to - * perform. By default, this is set to 15, which is usually enough to be - * precise in the majority of simple cases, whereas not prohibitively - * expensive to compute. - */ - bool getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter = 15) const; /** commonly used terms */ Node d_zero; diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2 index 078d8fcc7..37dcfaf7e 100644 --- a/test/regress/regress0/nl/sqrt2-value.smt2 +++ b/test/regress/regress0/nl/sqrt2-value.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; EXPECT: ((x (witness (set-option :produce-models true) -(set-logic ALL) +(set-logic QF_NRA) (declare-fun x () Real) (assert (= (* x x) 2)) (check-sat) diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 index ff426c139..431512bf2 100644 --- a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 +++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models -(set-logic ALL) +(set-logic NRA) (set-info :status sat) (assert (exists ((skoY Real)) (forall ((skoX Real)) (or (= 0.0 (* skoY skoY)) (and (< skoY 0.0) (or (= skoY skoX) (= 2 (* skoY skoY)))))))) (check-sat) -- 2.30.2