Ensure nonlinear extensions properly reconsiders its model (#6204)

In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.

3 files changed, 19 insertions, 30 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 25aebf6d4..781fb0c71 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -57,8 +57,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_tangentPlaneSlv(&d_extState),
       d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
       d_icpSlv(d_im),
-      d_iandSlv(d_im, state, d_model),
-      d_builtModel(containing.getSatContext(), false)
+      d_iandSlv(d_im, state, d_model)
 {
   d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
   d_extTheory.addFunctionKind(kind::EXPONENTIAL);
@@ -246,8 +245,7 @@ void NonlinearExtension::check(Theory::Effort e)
 {
   d_im.reset();
   Trace("nl-ext") << std::endl;
-  Trace("nl-ext") << "NonlinearExtension::check, effort = " << e
-                  << ", built model = " << d_builtModel.get() << std::endl;
+  Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl;
   if (e == Theory::EFFORT_FULL)
   {
     d_extTheory.clearCache();
@@ -301,7 +299,7 @@ void NonlinearExtension::check(Theory::Effort e)
   }
 }
 
-bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
+Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
 {
   ++(d_stats.d_mbrRuns);
   d_checkCounter++;
@@ -403,7 +401,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
       if (d_im.hasSentLemma() || d_im.hasPendingLemma())
       {
         d_im.clearWaitingLemmas();
-        return true;
+        return Result::Sat::UNSAT;
       }
     }
     Trace("nl-ext") << "Finished check with status : " << complete_status
@@ -424,7 +422,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
       if (d_im.hasUsed())
       {
         d_im.clearWaitingLemmas();
-        return true;
+        return Result::Sat::UNSAT;
       }
     }
 
@@ -438,7 +436,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
         d_im.flushWaitingLemmas();
         Trace("nl-ext") << "...added " << count << " waiting lemmas."
                         << std::endl;
-        return true;
+        return Result::Sat::UNSAT;
       }
       // resort to splitting on shared terms with their model value
       // if we did not add any lemmas
@@ -464,7 +462,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
             d_im.flushWaitingLemmas();
             Trace("nl-ext") << "...added " << d_im.numPendingLemmas()
                             << " shared term value split lemmas." << std::endl;
-            return true;
+            return Result::Sat::UNSAT;
           }
         }
         else
@@ -494,16 +492,11 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
         d_containing.getOutputChannel().setIncomplete();
       }
     }
-    else
-    {
-      // we have built a model
-      d_builtModel = true;
-    }
     d_im.clearWaitingLemmas();
   } while (needsRecheck);
 
   // did not add lemmas
-  return false;
+  return Result::Sat::SAT;
 }
 
 void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
@@ -517,12 +510,9 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
   Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
   d_model.reset(d_containing.getValuation().getModel(), arithModel);
   // run a last call effort check
-  if (!d_builtModel.get())
-  {
-    Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
-    modelBasedRefinement(termSet);
-  }
-  if (d_builtModel.get())
+  Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
+  Result::Sat res = modelBasedRefinement(termSet);
+  if (res == Result::Sat::SAT)
   {
     Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
     d_approximations.clear();
@@ -535,7 +525,6 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
 void NonlinearExtension::presolve()
 {
   Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
-  d_builtModel = false;
 }
 
 void NonlinearExtension::runStrategy(Theory::Effort effort,
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 820c317c5..bc8f48c26 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -39,6 +39,7 @@
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
 #include "theory/theory.h"
+#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {
@@ -154,12 +155,12 @@ class NonlinearExtension
    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
    * the current candidate model.
    *
-   * This function returns true if a lemma was added to the inference manager.
-   * Otherwise, it returns false. In the latter case, the model object d_model
-   * may have information regarding how to construct a model, in the case that
-   * we determined the problem is satisfiable.
+   * This function returns whether we found a satisfying assignment
+   * (Result::Sat::SAT), or not (Result::Sat::UNSAT). Note that UNSAT does not
+   * necessarily means the whole query is UNSAT, but that the linear model was
+   * refuted by a lemma.
    */
-  bool modelBasedRefinement(const std::set<Node>& termSet);
+  Result::Sat modelBasedRefinement(const std::set<Node>& termSet);
 
   /** get assertions
    *
@@ -290,8 +291,6 @@ class NonlinearExtension
    * NlModel::getModelValueRepair.
    */
   std::map<Node, Node> d_witnesses;
-  /** have we successfully built the model in this SAT context? */
-  context::CDO<bool> d_builtModel;
 }; /* class NonlinearExtension */
 
 }  // namespace nl
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 36b2d3eb8..a179336af 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -270,7 +270,8 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
     {
       Node eq = p.first.eqNode(p.second);
       Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
-      d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
+      bool added = d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL);
+      AlwaysAssert(added) << "The lemma was already in cache. Probably there is something wrong with theory combination...";
     }
     return false;
   }