Clean up nonlinear extension (#5149)

This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager.

2 files changed, 47 insertions, 80 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 251294d37..a166a5609 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -334,7 +334,6 @@ std::vector<Node> NonlinearExtension::checkModelEval(
 }
 
 bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
-                                    std::vector<NlLemma>& lemmas,
                                     std::vector<Node>& gs)
 {
   Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
@@ -361,19 +360,19 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
 
   Trace("nl-ext-cm") << "-----" << std::endl;
   unsigned tdegree = d_trSlv.getTaylorDegree();
-  bool ret =
-      d_model.checkModel(passertions, tdegree, lemmas, gs);
+  std::vector<NlLemma> lemmas;
+  bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
+  for (const auto& al: lemmas)
+  {
+    d_im.addPendingArithLemma(al);
+  }
   return ret;
 }
 
-int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
-                                      const std::vector<Node>& false_asserts,
-                                      const std::vector<Node>& xts,
-                                      std::vector<NlLemma>& lems,
-                                      std::vector<NlLemma>& wlems)
+void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
+                                       const std::vector<Node>& false_asserts,
+                                       const std::vector<Node>& xts)
 {
-  std::vector<NlLemma> lemmas;
-
   ++(d_stats.d_checkRuns);
 
   if (Trace.isOn("nl-ext"))
@@ -394,7 +393,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       Trace("nl-ext") << "  ...finished with "
                       << d_im.numPendingLemmas() + d_im.numSentLemmas()
                       << " new lemmas from ICP." << std::endl;
-      return d_im.numPendingLemmas() + d_im.numSentLemmas();
+      return;
     }
     Trace("nl-ext") << "Done with ICP" << std::endl;
   }
@@ -406,20 +405,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // initialize the trancendental function solver
     d_trSlv.initLastCall(assertions, false_asserts, xts);
   }
-  if (options::nlCad())
-  {
-    d_cadSlv.initLastCall(assertions);
-  }
 
   // init last call with IAND
   d_iandSlv.initLastCall(assertions, false_asserts, xts);
 
-  if (d_im.hasUsed() || !lems.empty())
+  if (d_im.hasUsed())
   {
-    unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+    std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
     Trace("nl-ext") << "  ...finished with " << count
                     << " new lemmas during registration." << std::endl;
-    return count;
+    return;
   }
 
   //----------------------------------- possibly split on zero
@@ -431,7 +426,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     {
       Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " new lemmas."
                       << std::endl;
-      return d_im.numPendingLemmas();
+      return;
     }
   }
 
@@ -442,10 +437,10 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     d_trSlv.checkTranscendentalInitialRefine();
     if (d_im.hasUsed())
     {
-      unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+      std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
       Trace("nl-ext") << "  ...finished with " << count << " new lemmas."
                       << std::endl;
-      return count;
+      return;
     }
   }
   //-----------------------------------initial lemmas for iand
@@ -454,7 +449,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   {
     Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " new lemmas."
                     << std::endl;
-    return d_im.numPendingLemmas();
+    return;
   }
 
   // main calls to nlExt
@@ -466,17 +461,17 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     {
       Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " new lemmas."
                       << std::endl;
-      return d_im.numPendingLemmas();
+      return;
     }
 
     //-----------------------------------monotonicity of transdental functions
     d_trSlv.checkTranscendentalMonotonic();
     if (d_im.hasUsed())
     {
-      unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+      std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
       Trace("nl-ext") << "  ...finished with " << count << " new lemmas."
                       << std::endl;
-      return count;
+      return;
     }
 
     //------------------------lemmas based on magnitude of non-zero monomials
@@ -488,7 +483,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       {
         Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()
                         << " new lemmas." << std::endl;
-        return d_im.numPendingLemmas();
+        return;
       }
     }
 
@@ -497,7 +492,6 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     d_nlSlv.checkMonomialInferBounds(assertions, false_asserts);
     Trace("nl-ext") << "Bound lemmas : " << d_im.numPendingLemmas() << ", " << d_im.numWaitingLemmas() << std::endl;
     // prioritize lemmas that do not introduce new monomials
-
     if (options::nlExtTangentPlanes()
         && options::nlExtTangentPlanesInterleave())
     {
@@ -508,7 +502,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     {
       Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " new lemmas."
                       << std::endl;
-      return d_im.numPendingLemmas();
+      return;
     }
 
     // from inferred bound inferences : now do ones that introduce new terms
@@ -517,7 +511,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     {
       Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()
                       << " new (monomial-introducing) lemmas." << std::endl;
-      return d_im.numPendingLemmas();
+      return;
     }
 
     //------------------------------------factoring lemmas
@@ -529,7 +523,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       {
         Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()
                         << " new lemmas." << std::endl;
-        return d_im.numPendingLemmas();
+        return;
       }
     }
 
@@ -542,7 +536,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       {
         Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()
                         << " new lemmas." << std::endl;
-        return d_im.numPendingLemmas();
+        return;
       }
     }
 
@@ -559,6 +553,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   if (options::nlCad())
   {
+    d_cadSlv.initLastCall(assertions);
     d_cadSlv.checkFull();
     if (!d_im.hasUsed())
     {
@@ -567,7 +562,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     else
     {
       // checkFull() only adds a single conflict
-      return 1;
+      return;
     }
   }
   // run the full refinement in the IAND solver
@@ -577,7 +572,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                   << std::endl;
   Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " lemmas."
                   << std::endl;
-  return 0;
+  return;
 }
 
 void NonlinearExtension::check(Theory::Effort e)
@@ -610,9 +605,8 @@ void NonlinearExtension::check(Theory::Effort e)
   else
   {
     // If we computed lemmas during collectModelInfo, send them now.
-    if (!d_cmiLemmas.empty() || d_im.hasPendingLemma())
+    if (d_im.hasPendingLemma())
     {
-      sendLemmas(d_cmiLemmas);
       d_im.doPendingFacts();
       d_im.doPendingLemmas();
       d_im.doPendingPhaseRequirements();
@@ -640,7 +634,7 @@ void NonlinearExtension::check(Theory::Effort e)
   }
 }
 
-bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
+bool NonlinearExtension::modelBasedRefinement()
 {
   ++(d_stats.d_mbrRuns);
   d_checkCounter++;
@@ -723,15 +717,13 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
     // complete_status:
     //   1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
     int complete_status = 1;
-    // lemmas that should be sent later
-    std::vector<NlLemma> wlems;
     // We require a check either if an assertion is false or a shared term has
     // a wrong value
     if (!false_asserts.empty() || num_shared_wrong_value > 0)
     {
       complete_status = num_shared_wrong_value > 0 ? -1 : 0;
-      checkLastCall(assertions, false_asserts, xts, mlems, wlems);
-      if (!mlems.empty() || d_im.hasSentLemma() || d_im.hasPendingLemma())
+      checkLastCall(assertions, false_asserts, xts);
+      if (d_im.hasSentLemma() || d_im.hasPendingLemma())
       {
         d_im.clearWaitingLemmas();
         return true;
@@ -748,9 +740,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
           << std::endl;
       // check the model based on simple solving of equalities and using
       // error bounds on the Taylor approximation of transcendental functions.
-      std::vector<NlLemma> lemmas;
       std::vector<Node> gs;
-      if (checkModel(assertions, lemmas, gs))
+      if (checkModel(assertions, gs))
       {
         complete_status = 1;
       }
@@ -761,8 +752,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
         d_containing.getOutputChannel().requirePhase(mgr, true);
         d_builtModel = true;
       }
-      filterLemmas(lemmas, mlems);
-      if (!mlems.empty() || d_im.hasPendingLemma())
+      if (d_im.hasUsed())
       {
         d_im.clearWaitingLemmas();
         return true;
@@ -773,10 +763,9 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
     if (complete_status != 1)
     {
       // flush the waiting lemmas
-      if (!wlems.empty() || d_im.hasWaitingLemma())
+      if (d_im.hasWaitingLemma())
       {
-        std::size_t count = wlems.size() + d_im.numWaitingLemmas();
-        mlems.insert(mlems.end(), wlems.begin(), wlems.end());
+        std::size_t count = d_im.numWaitingLemmas();
         d_im.flushWaitingLemmas();
         Trace("nl-ext") << "...added " << count << " waiting lemmas."
                         << std::endl;
@@ -789,7 +778,6 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
         complete_status = -1;
         if (!shared_term_value_splits.empty())
         {
-          std::vector<NlLemma> stvLemmas;
           for (const Node& eq : shared_term_value_splits)
           {
             Node req = Rewriter::rewrite(eq);
@@ -798,12 +786,12 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
             Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
             Node split = literal.orNode(literal.negate());
             NlLemma nsplit(split, InferenceId::NL_SHARED_TERM_VALUE_SPLIT);
-            filterLemma(nsplit, stvLemmas);
+            d_im.addPendingArithLemma(nsplit, true);
           }
-          if (!stvLemmas.empty())
+          if (d_im.hasWaitingLemma())
           {
-            mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end());
-            Trace("nl-ext") << "...added " << stvLemmas.size()
+            d_im.flushWaitingLemmas();
+            Trace("nl-ext") << "...added " << d_im.numPendingLemmas()
                             << " shared term value split lemmas." << std::endl;
             return true;
           }
@@ -852,11 +840,10 @@ 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
-  d_cmiLemmas.clear();
   if (!d_builtModel.get())
   {
     Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
-    modelBasedRefinement(d_cmiLemmas);
+    modelBasedRefinement();
   }
   if (d_builtModel.get())
   {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index d09d92c9f..f0e61435f 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -115,11 +115,6 @@ class NonlinearExtension
    * constraints are satisfiable, it may "repair" the values in the argument
    * arithModel so that it satisfies certain nonlinear constraints. This may
    * involve e.g. solving for variables in nonlinear equations.
-   *
-   * Notice that in the former case, the lemmas it constructs are not sent out
-   * immediately. Instead, they are put in temporary vector d_cmiLemmas, which
-   * are then sent out (if necessary) when a last call
-   * effort check is issued to this class.
    */
   void interceptModel(std::map<Node, Node>& arithModel);
   /** Does this class need a call to check(...) at last call effort? */
@@ -146,12 +141,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 vector lems.
+   * 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.
    */
-  bool modelBasedRefinement(std::vector<NlLemma>& mlems);
+  bool modelBasedRefinement();
 
   /** check last call
    *
@@ -160,24 +155,15 @@ class NonlinearExtension
    *
    * xts : the list of (non-reduced) extended terms in the current context.
    *
-   * This method adds lemmas to arguments lems and wlems, each of
-   * which are intended to be sent out on the output channel of TheoryArith
-   * under certain conditions.
+   * This method adds lemmas to d_im directly.
    *
    * If the set lems is non-empty, then no further processing is
    * necessary. The last call effort check should terminate and these
    * lemmas should be sent.
-   *
-   * The "waiting" lemmas wlems contain lemmas that should be sent on the
-   * output channel as a last resort. In other words, only if we are not
-   * able to establish SAT via a call to checkModel(...) should wlems be
-   * considered. This set typically contains tangent plane lemmas.
    */
-  int checkLastCall(const std::vector<Node>& assertions,
-                    const std::vector<Node>& false_asserts,
-                    const std::vector<Node>& xts,
-                    std::vector<NlLemma>& lems,
-                    std::vector<NlLemma>& wlems);
+  void checkLastCall(const std::vector<Node>& assertions,
+                     const std::vector<Node>& false_asserts,
+                     const std::vector<Node>& xts);
 
   /** get assertions
    *
@@ -218,7 +204,6 @@ class NonlinearExtension
    * ensureLiteral respectively.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
   //---------------------------end check model
   /** compute relevant assertions */
@@ -291,11 +276,6 @@ class NonlinearExtension
    */
   IAndSolver d_iandSlv;
   /**
-   * The lemmas we computed during collectModelInfo, to be sent out on the
-   * output channel of TheoryArith.
-   */
-  std::vector<NlLemma> d_cmiLemmas;
-  /**
    * The approximations computed during collectModelInfo. For details, see
    * NlModel::getModelValueRepair.
    */