Fixes for unconstrained variables in nonlinear model (#5351)

This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0.

This fixes #5348.

1 files changed, 8 insertions, 12 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index a5ac8e3fe..76f37213a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -338,8 +338,7 @@ std::vector<Node> NonlinearExtension::checkModelEval(
   return false_asserts;
 }
 
-bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
-                                    std::vector<Node>& gs)
+bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
 {
   Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
 
@@ -366,7 +365,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   Trace("nl-ext-cm") << "-----" << std::endl;
   unsigned tdegree = d_trSlv.getTaylorDegree();
   std::vector<NlLemma> lemmas;
-  bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
+  bool ret = d_model.checkModel(passertions, tdegree, lemmas);
   for (const auto& al: lemmas)
   {
     d_im.addPendingArithLemma(al);
@@ -539,18 +538,10 @@ bool NonlinearExtension::modelBasedRefinement()
           << std::endl;
       // check the model based on simple solving of equalities and using
       // error bounds on the Taylor approximation of transcendental functions.
-      std::vector<Node> gs;
-      if (checkModel(assertions, gs))
+      if (checkModel(assertions))
       {
         complete_status = 1;
       }
-      for (const Node& mg : gs)
-      {
-        Node mgr = Rewriter::rewrite(mg);
-        mgr = d_containing.getValuation().ensureLiteral(mgr);
-        d_containing.getOutputChannel().requirePhase(mgr, true);
-        d_builtModel = true;
-      }
       if (d_im.hasUsed())
       {
         d_im.clearWaitingLemmas();
@@ -622,6 +613,11 @@ bool NonlinearExtension::modelBasedRefinement()
         d_containing.getOutputChannel().setIncomplete();
       }
     }
+    else
+    {
+      // we have built a model
+      d_builtModel = true;
+    }
     d_im.clearWaitingLemmas();
   } while (needsRecheck);