Make IAND solver use inference manager. (#5126)

This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.

5 files changed, 28 insertions, 32 deletions

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 7e9fa13e5..a72010bf4 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -28,10 +28,10 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-IAndSolver::IAndSolver(TheoryArith& containing, NlModel& model)
-    : d_containing(containing),
+IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
+    : d_im(im),
       d_model(model),
-      d_initRefine(containing.getUserContext())
+      d_initRefine(state.getUserContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_true = nm->mkConst(true);
@@ -66,10 +66,9 @@ void IAndSolver::initLastCall(const std::vector<Node>& assertions,
   Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl;
 }
 
-std::vector<NlLemma> IAndSolver::checkInitialRefine()
+void IAndSolver::checkInitialRefine()
 {
   Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl;
-  std::vector<NlLemma> lems;
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
   {
@@ -101,17 +100,15 @@ std::vector<NlLemma> IAndSolver::checkInitialRefine()
       Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
       Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
                           << std::endl;
-      lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE);
+      d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_INIT_REFINE);
     }
   }
-  return lems;
 }
 
-std::vector<NlLemma> IAndSolver::checkFullRefine()
+void IAndSolver::checkFullRefine()
 {
   Trace("iand-check") << "IAndSolver::checkFullRefine";
   Trace("iand-check") << "IAND terms: " << std::endl;
-  std::vector<NlLemma> lems;
   for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
   {
     // the reference bitwidth
@@ -163,12 +160,10 @@ std::vector<NlLemma> IAndSolver::checkFullRefine()
         Node lem = valueBasedLemma(i);
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
-        lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE);
+        d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true);
       }
     }
   }
-
-  return lems;
 }
 
 Node IAndSolver::convertToBvK(unsigned k, Node n) const
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 216e1556b..d74365784 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -20,9 +20,10 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "theory/arith/arith_state.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
-#include "theory/arith/theory_arith.h"
 
 namespace CVC4 {
 namespace theory {
@@ -37,7 +38,7 @@ class IAndSolver
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  IAndSolver(TheoryArith& containing, NlModel& model);
+  IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
   ~IAndSolver();
 
   /** init last call
@@ -66,18 +67,18 @@ class IAndSolver
    * This should be a heuristic incomplete check that only introduces a
    * small number of new terms in the lemmas it returns.
    */
-  std::vector<NlLemma> checkInitialRefine();
+  void checkInitialRefine();
   /** check full refine
    *
    * This should be a complete check that returns at least one lemma to
    * rule out the current model.
    */
-  std::vector<NlLemma> checkFullRefine();
+  void checkFullRefine();
 
   //-------------------------------------------- end lemma schemas
  private:
-  // The theory of arithmetic containing this extension.
-  TheoryArith& d_containing;
+  // The inference manager that we push conflicts and lemmas to.
+  InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
   /** commonly used terms */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index b8f69f521..af1f536be 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -19,6 +19,7 @@
 
 #include "options/arith_options.h"
 #include "options/theory_options.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
@@ -32,6 +33,7 @@ namespace arith {
 namespace nl {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
+                                       ArithState& state,
                                        eq::EqualityEngine* ee)
     : d_containing(containing),
       d_im(containing.getInferenceManager()),
@@ -48,7 +50,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_nlSlv(containing, d_model),
       d_cadSlv(d_im, d_model),
       d_icpSlv(d_im),
-      d_iandSlv(containing, d_model),
+      d_iandSlv(d_im, state, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
   d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
@@ -448,13 +450,12 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }
   }
   //-----------------------------------initial lemmas for iand
-  lemmas = d_iandSlv.checkInitialRefine();
-  filterLemmas(lemmas, lems);
-  if (!lems.empty())
+  d_iandSlv.checkInitialRefine();
+  if (d_im.hasUsed())
   {
-    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+    Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " new lemmas."
                     << std::endl;
-    return lems.size();
+    return d_im.numPendingLemmas();
   }
 
   // main calls to nlExt
@@ -583,13 +584,12 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }
   }
   // run the full refinement in the IAND solver
-  lemmas = d_iandSlv.checkFullRefine();
-  filterLemmas(lemmas, wlems);
-
-  Trace("nl-ext") << "  ...finished with "
-                  << (wlems.size() + d_im.numWaitingLemmas())
-                  << " waiting lemmas." << std::endl;
+  d_iandSlv.checkFullRefine();
 
+  Trace("nl-ext") << "  ...finished with " << d_im.numWaitingLemmas() << " waiting lemmas."
+                  << std::endl;
+  Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas() << " lemmas."
+                  << std::endl;
   return 0;
 }
 
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 15beea32c..d09d92c9f 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -74,7 +74,7 @@ class NonlinearExtension
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee);
+  NonlinearExtension(TheoryArith& containing, ArithState& state, eq::EqualityEngine* ee);
   ~NonlinearExtension();
   /**
    * Does non-context dependent setup for a node connected to a theory.
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index abdf6930a..9324c94af 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -83,7 +83,7 @@ void TheoryArith::finishInit()
   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
   {
     d_nonlinearExtension.reset(
-        new nl::NonlinearExtension(*this, d_equalityEngine));
+        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine));
   }
   // finish initialize internally
   d_internal->finishInit();