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.

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 427d203ea68d6e12c38a018e23f8ada99fdb6b31..77a3ea5305699db00934175dec2751c104453d23 100644 (file)
--- 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<Rational>().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<Rational>());
-  Node coeffa = nm->mkConst(Rational(1) / two_a.getConst<Rational>());
-  // 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<Rational>() > bounds[r][1].getConst<Rational>())
-    {
-      // 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<Rational>().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<Node, Node>& 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>();
-
-  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 b3b841eab717e08e17a38296045387a7326d4ba3..7dcd89a4ac39a8abf41d3f14b9b4b5d46c4dc60e 100644 (file)
--- 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<Node, Node>& 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 078d8fcc72ff3c9d35fd343b74c9d308095bffff..37dcfaf7ee09d2c82863998b2ea60373d4b413de 100644 (file)
--- 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 ff426c139bc5c3a131bfd488c03934741571a872..431512bf28b162ea8bf62ee763dd70abadcef46f 100644 (file)
--- 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)