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.

4 files changed, 28 insertions, 48 deletions

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index b27654b2c..79f2a2350 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -159,7 +159,7 @@ Node NlModel::getRepresentative(Node n) const
   return d_model->getRepresentative(n);
 }
 
-Node NlModel::getValueInternal(Node n) const
+Node NlModel::getValueInternal(Node n)
 {
   if (n.isConst())
   {
@@ -171,7 +171,11 @@ Node NlModel::getValueInternal(Node n) const
     AlwaysAssert(it->second.isConst());
     return it->second;
   }
-  // It is unconstrained in the model, return 0.
+  // It is unconstrained in the model, return 0. We additionally add it
+  // to mapping from the linear solver. This ensures that if the nonlinear
+  // solver assumes that n = 0, then this assumption is recorded in the overall
+  // model.
+  d_arithVal[n] = d_zero;
   return d_zero;
 }
 
@@ -215,8 +219,7 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const
 
 bool NlModel::checkModel(const std::vector<Node>& assertions,
                          unsigned d,
-                         std::vector<NlLemma>& lemmas,
-                         std::vector<Node>& gs)
+                         std::vector<NlLemma>& lemmas)
 {
   Trace("nl-ext-cm-debug") << "  solve for equalities..." << std::endl;
   for (const Node& atom : assertions)
@@ -312,26 +315,6 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
     return false;
   }
   Trace("nl-ext-cm") << "...simple check succeeded!" << std::endl;
-
-  // must assert and re-check if produce models is true
-  if (options::produceModels())
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    // model guard whose semantics is "the model we constructed holds"
-    Node mg = nm->mkSkolem("model", nm->booleanType());
-    gs.push_back(mg);
-    // assert the constructed model as assertions
-    for (const std::pair<const Node, std::pair<Node, Node>> cb :
-         d_check_model_bounds)
-    {
-      Node l = cb.second.first;
-      Node u = cb.second.second;
-      Node v = cb.first;
-      Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
-      pred = nm->mkNode(OR, mg.negate(), pred);
-      lemmas.emplace_back(pred);
-    }
-  }
   return true;
 }
 
@@ -1280,7 +1263,12 @@ void NlModel::getModelValueRepair(
     std::map<Node, Node>& witnesses)
 {
   Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
-
+  // If we extended the model with entries x -> 0 for unconstrained values,
+  // we first update the map to the extended one.
+  if (d_arithVal.size() > arithModel.size())
+  {
+    arithModel = d_arithVal;
+  }
   // Record the approximations we used. This code calls the
   // recordApproximation method of the model, which overrides the model
   // values for variables that we solved for, using techniques specific to
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 7831d78ef..cd2d15563 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -154,8 +154,7 @@ class NlModel
    */
   bool checkModel(const std::vector<Node>& assertions,
                   unsigned d,
-                  std::vector<NlLemma>& lemmas,
-                  std::vector<Node>& gs);
+                  std::vector<NlLemma>& lemmas);
   /**
    * Set that we have used an approximation during this check. This flag is
    * reset on a call to resetCheck. It is set when we use reasoning that
@@ -195,7 +194,7 @@ class NlModel
   /** The current model */
   TheoryModel* d_model;
   /** Get the model value of n from the model object above */
-  Node getValueInternal(Node n) const;
+  Node getValueInternal(Node n);
   /** Does the equality engine of the model have term n? */
   bool hasTerm(Node n) const;
   /** Get the representative of n in the model */
@@ -263,8 +262,10 @@ class NlModel
   Node d_null;
   /**
    * The values that the arithmetic theory solver assigned in the model. This
-   * corresponds to exactly the set of equalities that TheoryArith is currently
-   * sending to TheoryModel during collectModelInfo.
+   * corresponds to the set of equalities that linear solver (via TheoryArith)
+   * is currently sending to TheoryModel during collectModelValues, plus
+   * additional entries x -> 0 for variables that were unassigned by the linear
+   * solver.
    */
   std::map<Node, Node> d_arithVal;
   /**
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);
 
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index cd26a027f..2f4586d78 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -185,13 +185,8 @@ class NonlinearExtension
    *
    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
    * "Detecting Satisfiable Formulas".
-   *
-   * The arguments lemmas and gs store the lemmas and guard literals to be sent
-   * out on the output channel of TheoryArith as lemmas and calls to
-   * ensureLiteral respectively.
    */
-  bool checkModel(const std::vector<Node>& assertions,
-                  std::vector<Node>& gs);
+  bool checkModel(const std::vector<Node>& assertions);
   //---------------------------end check model
   /** compute relevant assertions */
   void computeRelevantAssertions(const std::vector<Node>& assertions,