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

1 files changed, 8 insertions, 4 deletions

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];