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.

1 files changed, 11 insertions, 22 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,