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.

diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp
index 2ec366d2a102451dd526a6f74b4a1122174372d5..062a9213b04cfc42968abfbe72030057d738d187 100644 (file)
--- 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<Node>& 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 c566758bea8e24502577c000e575f11eaef0775f..3c9458ae3e24069ba584d5bd856343f3c98285fc 100644 (file)
--- 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<Node>& assertions,
                          unsigned d,
                          std::vector<NlLemma>& 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<Node>& 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<Node>& 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<Node>& 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<Rational>() >= itb->second.first.getConst<Rational>()
-        || s.getConst<Rational>() <= itb->second.second.getConst<Rational>())
+    Assert(s.isConst());
+    if (s.getConst<Rational>() <= itb->second.first.getConst<Rational>()
+        || s.getConst<Rational>() >= itb->second.second.getConst<Rational>())
     {
       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<bool>())
@@ -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<Rational>() / b.getConst<Rational>());
-    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<Rational>() / b.getConst<Rational>());
+  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<Node, Node>& 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 265e270dbd28bbcbdf182182853ff4ea131bb3cd..a9cc38b36e699d4dfa7b7af59ad858f5c3a1b04a 100644 (file)
--- 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<Node, Node>& arithModel);
 
+  /** Return the substituted form of s */
+  Node getSubstitutedForm(TNode s) const;
+
  private:
   /** Cache for concrete model values */
   std::map<Node, Node> d_concreteModelCache;

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 6645589e2c288302d151378e265dbfc0b842f3c6..b937dcb99f13c222a9d9be0afcf67749f810f647 100644 (file)
--- 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 61fd9a13e015c47a1821947c4344e18428c066b8..45d3701fc3ebcca9297411957f3470dd7c7da6a3 100644 (file)
--- 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 (file)
index 0000000..fb903fb
--- /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)