Improve non-linear check model error handling (#2497)

2 files changed, 78 insertions, 30 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 9f6608dc5..4cd7896d3 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -888,17 +888,25 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
     Kind k = tfs.first;
     for (const Node& tf : tfs.second)
     {
+      bool success = true;
       // tf is Figure 3 : tf( x )
       Node atf = computeModelValue(tf, 0);
       if (k == PI)
       {
-        addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]);
+        success = addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]);
       }
       else if (isRefineableTfFun(tf))
       {
         d_used_approx = true;
         std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree);
-        addCheckModelBound(atf, bounds.first, bounds.second);
+        success = addCheckModelBound(atf, bounds.first, bounds.second);
+      }
+      if (!success)
+      {
+        Trace("nl-ext-cm-debug")
+            << "...failed to set bound for transcendental function."
+            << std::endl;
+        return false;
       }
       if (Trace.isOn("nl-ext-cm"))
       {
@@ -962,7 +970,8 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
                   << "check-model-bound : exact : " << cur << " = ";
               printRationalApprox("nl-ext-cm", curv);
               Trace("nl-ext-cm") << std::endl;
-              addCheckModelSubstitution(cur, curv);
+              bool ret = addCheckModelSubstitution(cur, curv);
+              AlwaysAssert(ret);
             }
           }
         }
@@ -1036,15 +1045,31 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   return true;
 }
 
-void NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s)
+bool NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s)
 {
   // should not substitute the same variable twice
   Trace("nl-ext-model") << "* check model substitution : " << v << " -> " << s << std::endl;
   // should not set exact bound more than once
   if(std::find(d_check_model_vars.begin(),d_check_model_vars.end(),v)!=d_check_model_vars.end())
   {
+    Trace("nl-ext-model") << "...ERROR: already has value." << std::endl;
+    // this should never happen since substitutions should be applied eagerly
     Assert( false );
-    return;
+    return false;
+  }
+  // if we previously had an approximate bound, the exact bound should be in its
+  // range
+  std::map<Node, std::pair<Node, Node> >::iterator itb =
+      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>())
+    {
+      Trace("nl-ext-model")
+          << "...ERROR: already has bound which is out of range." << std::endl;
+      return false;
+    }
   }
   for (unsigned i = 0, size = d_check_model_subs.size(); i < size; i++)
   {
@@ -1058,23 +1083,32 @@ void NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s)
   }
   d_check_model_vars.push_back(v);
   d_check_model_subs.push_back(s);
+  return true;
 }
 
-void NonlinearExtension::addCheckModelBound(TNode v, TNode l, TNode u)
+bool NonlinearExtension::addCheckModelBound(TNode v, TNode l, TNode u)
 {
   Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " " << u << "]" << std::endl;
   if( l==u )
   {
     // bound is exact, can add as substitution
-    addCheckModelSubstitution(v,l);
-    return;
+    return addCheckModelSubstitution(v, l);
   }
   // should not set a bound for a value that is exact
-  Assert(std::find(d_check_model_vars.begin(),d_check_model_vars.end(),v)==d_check_model_vars.end());
+  if (std::find(d_check_model_vars.begin(), d_check_model_vars.end(), v)
+      != d_check_model_vars.end())
+  {
+    Trace("nl-ext-model")
+        << "...ERROR: setting bound for variable that already has exact value."
+        << std::endl;
+    Assert(false);
+    return false;
+  }
   Assert(l.isConst());
   Assert(u.isConst());
   Assert(l.getConst<Rational>() <= u.getConst<Rational>());
   d_check_model_bounds[v] = std::pair<Node, Node>(l, u);
+  return true;
 }
 
 bool NonlinearExtension::hasCheckModelAssignment(Node v) const
@@ -1203,11 +1237,14 @@ bool NonlinearExtension::solveEqualitySimple(Node eq)
           {
             Trace("nl-ext-cm")
                 << "check-model-subs : " << uv << " -> " << slv << std::endl;
-            addCheckModelSubstitution(uv, slv);
-            Trace("nl-ext-cms") << "...success, model substitution " << uv
-                                << " -> " << slv << std::endl;
-            d_check_model_solved[eq] = uv;
-            return true;
+            bool ret = addCheckModelSubstitution(uv, slv);
+            if (ret)
+            {
+              Trace("nl-ext-cms") << "...success, model substitution " << uv
+                                  << " -> " << slv << std::endl;
+              d_check_model_solved[eq] = uv;
+            }
+            return ret;
           }
         }
       }
@@ -1223,9 +1260,9 @@ bool NonlinearExtension::solveEqualitySimple(Node eq)
         Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = ";
         printRationalApprox("nl-ext-cm", uvfv);
         Trace("nl-ext-cm") << std::endl;
-        addCheckModelSubstitution(uvf, uvfv);
+        bool ret = addCheckModelSubstitution(uvf, uvfv);
         // recurse
-        return solveEqualitySimple(eq);
+        return ret ? solveEqualitySimple(eq) : false;
       }
     }
     Trace("nl-ext-cms") << "...fail due to constrained invalid terms."
@@ -1252,10 +1289,13 @@ bool NonlinearExtension::solveEqualitySimple(Node eq)
     Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = ";
     printRationalApprox("nl-ext-cm", val);
     Trace("nl-ext-cm") << std::endl;
-    addCheckModelSubstitution(var, val);
-    Trace("nl-ext-cms") << "...success, solved linear." << std::endl;
-    d_check_model_solved[eq] = var;
-    return true;
+    bool ret = addCheckModelSubstitution(var, val);
+    if (ret)
+    {
+      Trace("nl-ext-cms") << "...success, solved linear." << std::endl;
+      d_check_model_solved[eq] = var;
+    }
+    return ret;
   }
   Trace("nl-ext-quad") << "Solve quadratic : " << seq << std::endl;
   Trace("nl-ext-quad") << "  a : " << a << std::endl;
@@ -1352,10 +1392,14 @@ bool NonlinearExtension::solveEqualitySimple(Node eq)
   Trace("nl-ext-cm") << " <= " << var << " <= ";
   printRationalApprox("nl-ext-cm", bounds[r_use_index][1]);
   Trace("nl-ext-cm") << std::endl;
-  addCheckModelBound(var, bounds[r_use_index][0], bounds[r_use_index][1]);
-  d_check_model_solved[eq] = var;
-  Trace("nl-ext-cms") << "...success, solved quadratic." << std::endl;
-  return true;
+  bool ret =
+      addCheckModelBound(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;
 }
 
 bool NonlinearExtension::simpleCheckModelLit(Node lit)
@@ -3622,7 +3666,7 @@ std::vector<Node> NonlinearExtension::checkFactoring(
             sum = Rewriter::rewrite( sum );
             Trace("nl-ext-factor")
                 << "* Factored sum for " << x << " : " << sum << std::endl;
-            Node kf = getFactorSkolem( sum, lemmas ); 
+            Node kf = getFactorSkolem(sum, lemmas);
             std::vector< Node > poly;
             poly.push_back(NodeManager::currentNM()->mkNode(MULT, x, kf));
             std::map<Node, std::vector<Node> >::iterator itfo =
@@ -3672,7 +3716,7 @@ Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas )
     return itf->second;
   }  
 }
-                    
+
 std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {            
   std::vector< Node > lemmas; 
   Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." << std::endl;
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index c0af312b3..f2cdea334 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -317,8 +317,10 @@ class NonlinearExtension {
    * Adds the model substitution v -> s. This applies the substitution
    * { v -> s } to each term in d_check_model_subs and adds v,s to
    * d_check_model_vars and d_check_model_subs respectively.
+   * If this method returns false, then the substitution v -> s is inconsistent
+   * with the current substitution and bounds.
    */
-  void addCheckModelSubstitution(TNode v, TNode s);
+  bool addCheckModelSubstitution(TNode v, TNode s);
   /** lower and upper bounds for check model
    *
    * For each term t in the domain of this map, if this stores the pair
@@ -335,9 +337,11 @@ class NonlinearExtension {
   /** add check model bound
    *
    * Adds the bound x -> < l, u > to the map above, and records the
-   * approximation ( x, l <= x <= u ) in the model.
+   * approximation ( x, l <= x <= u ) in the model. This method returns false
+   * if the bound is inconsistent with the current model substitution or
+   * bounds.
    */
-  void addCheckModelBound(TNode v, TNode l, TNode u);
+  bool addCheckModelBound(TNode v, TNode l, TNode u);
   /**
    * The map from literals that our model construction solved, to the variable
    * that was solved for. Examples of such literals are:
@@ -586,7 +590,7 @@ class NonlinearExtension {
   // factor skolems
   std::map< Node, Node > d_factor_skolem;
   Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
-  
+
   // tangent plane bounds
   std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4];