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.

1 files changed, 6 insertions, 26 deletions

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.
    */