Add ArithLemma and arith::InferenceManager (#4960)

This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory.
Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.

15 files changed, 414 insertions, 33 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7a383d0c8..2da04ce66 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -251,6 +251,8 @@ libcvc4_add_sources(
   theory/arith/approx_simplex.h
   theory/arith/arith_ite_utils.cpp
   theory/arith/arith_ite_utils.h
+  theory/arith/arith_lemma.cpp
+  theory/arith/arith_lemma.h
   theory/arith/arith_msum.cpp
   theory/arith/arith_msum.h
   theory/arith/arith_rewriter.cpp
@@ -287,6 +289,8 @@ libcvc4_add_sources(
   theory/arith/fc_simplex.h
   theory/arith/infer_bounds.cpp
   theory/arith/infer_bounds.h
+  theory/arith/inference_manager.cpp
+  theory/arith/inference_manager.h
   theory/arith/linear_equality.cpp
   theory/arith/linear_equality.h
   theory/arith/matrix.cpp
diff --git a/src/theory/arith/arith_lemma.cpp b/src/theory/arith/arith_lemma.cpp
new file mode 100644
index 000000000..9bd4df255
--- /dev/null
+++ b/src/theory/arith/arith_lemma.cpp
@@ -0,0 +1,28 @@
+/*********************                                                        */
+/*! \file arith_lemma.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ArithLemma class, derived from Lemma.
+ **/
+
+#include "theory/arith/arith_lemma.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+std::ostream& operator<<(std::ostream& out, const ArithLemma& al)
+{
+  return out << al.d_node;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h
new file mode 100644
index 000000000..a06cb83f3
--- /dev/null
+++ b/src/theory/arith/arith_lemma.h
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/*! \file arith_lemma.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ArithLemma class, derived from Lemma.
+ **/
+
+#ifndef CVC4__THEORY__ARITH__ARITH_LEMMA_H
+#define CVC4__THEORY__ARITH__ARITH_LEMMA_H
+
+#include <tuple>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/arith/nl/inference.h"
+#include "theory/inference_manager_buffered.h"
+#include "theory/output_channel.h"
+#include "theory/theory_inference.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * The data structure for a single lemma to process by the arithmetic theory,
+ * derived from theory::SimpleTheoryLemma.
+ *
+ * This also includes the inference type that produced this lemma.
+ */
+class ArithLemma : public SimpleTheoryLemma
+{
+ public:
+  ArithLemma(Node n,
+             LemmaProperty p,
+             ProofGenerator* pg,
+             nl::Inference inf = nl::Inference::UNKNOWN)
+      : SimpleTheoryLemma(n, p, pg), d_inference(inf)
+  {
+  }
+  virtual ~ArithLemma() {}
+
+  /** The inference id for the lemma */
+  nl::Inference d_inference;
+};
+/**
+ * Writes an arithmetic lemma to a stream.
+ */
+std::ostream& operator<<(std::ostream& out, const ArithLemma& al);
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__ARITH_LEMMA_H */
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
new file mode 100644
index 000000000..f026aa374
--- /dev/null
+++ b/src/theory/arith/inference_manager.cpp
@@ -0,0 +1,143 @@
+/*********************                                                        */
+/*! \file inference_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of the inference manager for the theory of strings.
+ **/
+
+#include "theory/arith/inference_manager.h"
+
+#include "options/arith_options.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+InferenceManager::InferenceManager(TheoryArith& ta,
+                                   ArithState& astate,
+                                   ProofNodeManager* pnm)
+    : InferenceManagerBuffered(ta, astate, pnm), d_lemmasPp(ta.getUserContext())
+{
+}
+
+void InferenceManager::addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
+                                            bool isWaiting)
+{
+  lemma->d_node = Rewriter::rewrite(lemma->d_node);
+  if (hasCachedLemma(lemma->d_node, lemma->d_property))
+  {
+    return;
+  }
+  if (isEntailedFalse(*lemma))
+  {
+    if (isWaiting)
+    {
+      d_waitingLem.clear();
+    }
+    else
+    {
+      d_pendingLem.clear();
+      d_theoryState.notifyInConflict();
+    }
+  }
+  if (isWaiting)
+  {
+    d_waitingLem.emplace_back(std::move(lemma));
+  }
+  else
+  {
+    addPendingLemma(std::move(lemma));
+  }
+}
+void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
+                                            bool isWaiting)
+{
+  addPendingArithLemma(std::make_shared<ArithLemma>(lemma), isWaiting);
+}
+void InferenceManager::addPendingArithLemma(const Node& lemma,
+                                            nl::Inference inftype,
+                                            bool isWaiting)
+{
+  addPendingArithLemma(std::make_shared<ArithLemma>(
+                           lemma, LemmaProperty::NONE, nullptr, inftype),
+                       isWaiting);
+}
+
+void InferenceManager::flushWaitingLemmas()
+{
+  for (auto& lem : d_waitingLem)
+  {
+    addPendingLemma(std::move(lem));
+  }
+  d_waitingLem.clear();
+}
+
+void InferenceManager::addConflict(const Node& conf, nl::Inference inftype)
+{
+  conflict(Rewriter::rewrite(conf));
+}
+
+std::size_t InferenceManager::numWaitingLemmas() const
+{
+  return d_waitingLem.size();
+}
+
+bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
+{
+  if (isLemmaPropertyPreprocess(p))
+  {
+    return d_lemmasPp.find(lem) != d_lemmasPp.end();
+  }
+  return TheoryInferenceManager::hasCachedLemma(lem, p);
+}
+
+bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
+{
+  if (isLemmaPropertyPreprocess(p))
+  {
+    if (d_lemmasPp.find(lem) != d_lemmasPp.end())
+    {
+      return false;
+    }
+    d_lemmasPp.insert(lem);
+    return true;
+  }
+  return TheoryInferenceManager::cacheLemma(lem, p);
+}
+
+bool InferenceManager::isEntailedFalse(const ArithLemma& lem)
+{
+  if (options::nlExtEntailConflicts())
+  {
+    Node ch_lemma = lem.d_node.negate();
+    ch_lemma = Rewriter::rewrite(ch_lemma);
+    Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
+                               << ch_lemma << "..." << std::endl;
+
+    std::pair<bool, Node> et = d_theory.getValuation().entailmentCheck(
+        options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
+    Trace("arith-inf-manager") << "entailment test result : " << et.first << " "
+                               << et.second << std::endl;
+    if (et.first)
+    {
+      Trace("arith-inf-manager")
+          << "*** Lemma entailed to be in conflict : " << lem.d_node
+          << std::endl;
+      return true;
+    }
+  }
+  return false;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
new file mode 100644
index 000000000..3b7190826
--- /dev/null
+++ b/src/theory/arith/inference_manager.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Customized inference manager for the theory of nonlinear arithmetic
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+
+#include <map>
+#include <vector>
+
+#include "theory/arith/arith_lemma.h"
+#include "theory/arith/arith_state.h"
+#include "theory/arith/nl/inference.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/inference_manager_buffered.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class TheoryArith;
+
+/**
+ * A specialized variant of the InferenceManagerBuffered, tailored to the
+ * arithmetic theory.
+ *
+ * It adds some convenience methods to send ArithLemma and adds a mechanism for
+ * waiting lemmas that can be flushed into the pending lemmas of the this
+ * buffered inference manager.
+ * It also extends the caching mechanism of TheoryInferenceManager to cache
+ * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
+ * it uses the cache provided by the TheoryInferenceManager base class.
+ */
+class InferenceManager : public InferenceManagerBuffered
+{
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+  InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
+
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(std::shared_ptr<ArithLemma> lemma,
+                            bool isWaiting = false);
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
+  /**
+   * Add a lemma as pending lemma to the this inference manager.
+   * If isWaiting is true, the lemma is first stored as waiting lemma and only
+   * added as pending lemma when calling flushWaitingLemmas.
+   */
+  void addPendingArithLemma(const Node& lemma,
+                            nl::Inference inftype,
+                            bool isWaiting = false);
+
+  /**
+   * Flush all waiting lemmas to the this inference manager (as pending
+   * lemmas). To actually send them, call doPendingLemmas() afterwards.
+   */
+  void flushWaitingLemmas();
+
+  /** Add a conflict to the this inference manager. */
+  void addConflict(const Node& conf, nl::Inference inftype);
+
+  /** Returns the number of pending lemmas. */
+  std::size_t numWaitingLemmas() const;
+
+  /** Checks whether the given lemma is already present in the cache. */
+  virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
+
+ protected:
+  /**
+   * Adds the given lemma to the cache. Returns true if it has not been in the
+   * cache yet.
+   */
+  virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
+
+ private:
+  /**
+   * Checks whether the lemma is entailed to be false. In this case, it is a
+   * conflict.
+   */
+  bool isEntailedFalse(const ArithLemma& lem);
+
+  /** The waiting lemmas. */
+  std::vector<std::shared_ptr<ArithLemma>> d_waitingLem;
+
+  /** cache of all preprocessed lemmas sent on the output channel
+   * (user-context-dependent) */
+  NodeSet d_lemmasPp;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index b1f0894fb..ac939c341 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -95,7 +95,7 @@ std::vector<NlLemma> CadSolver::checkFull()
     {
       lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT);
     }
-    Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_lemma << std::endl;
+    Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl;
   }
   return lems;
 #else
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index 49eec186e..58a552815 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -15,20 +15,26 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nonlinear_extension.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
-LemmaProperty NlLemma::getLemmaProperty() const
+bool NlLemma::process(TheoryInferenceManager* im)
 {
-  return d_preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
+  bool res = ArithLemma::process(im);
+  if (d_nlext != nullptr)
+  {
+    d_nlext->processSideEffect(*this);
+  }
+  return res;
 }
 
 std::ostream& operator<<(std::ostream& out, NlLemma& n)
 {
-  out << n.d_lemma;
+  out << n.d_node;
   return out;
 }
 
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index f40857fda..c6c22c3c6 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -17,7 +17,9 @@
 
 #include <tuple>
 #include <vector>
+
 #include "expr/node.h"
+#include "theory/arith/arith_lemma.h"
 #include "theory/arith/nl/inference.h"
 #include "theory/output_channel.h"
 
@@ -27,6 +29,7 @@ namespace arith {
 namespace nl {
 
 class NlModel;
+class NonlinearExtension;
 
 /**
  * The data structure for a single lemma to process by the non-linear solver,
@@ -39,19 +42,24 @@ class NlModel;
  * - A set of secant points to record (for transcendental secant plane
  * inferences).
  */
-struct NlLemma
+class NlLemma : public ArithLemma
 {
-  NlLemma(Node lem, Inference id = Inference::UNKNOWN)
-      : d_id(id), d_lemma(lem), d_preprocess(false)
+ public:
+  NlLemma(Node n,
+          LemmaProperty p,
+          ProofGenerator* pg,
+          nl::Inference inf = nl::Inference::UNKNOWN)
+      : ArithLemma(n, p, pg, inf)
+  {
+  }
+  NlLemma(Node n, nl::Inference inf = nl::Inference::UNKNOWN)
+      : ArithLemma(n, LemmaProperty::NONE, nullptr, inf)
   {
   }
   ~NlLemma() {}
-  /** The inference id for the lemma */
-  Inference d_id;
-  /** The lemma */
-  Node d_lemma;
-  /** Whether to preprocess the lemma */
-  bool d_preprocess;
+
+  bool process(TheoryInferenceManager* im) override;
+
   /** secant points to add
    *
    * A member (tf, d, c) in this vector indicates that point c should be added
@@ -62,8 +70,8 @@ struct NlLemma
    * Cimatti et al., CADE 2017.
    */
   std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
-  /** get lemma property (preprocess or none) */
-  LemmaProperty getLemmaProperty() const;
+
+  NonlinearExtension* d_nlext;
 };
 /**
  * Writes a non-linear lemma to a stream.
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index cfa153a56..fbc38fbc2 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -326,7 +326,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
       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.push_back(pred);
+      lemmas.emplace_back(pred);
     }
   }
   return true;
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp
index 521539674..6c20eec76 100644
--- a/src/theory/arith/nl/nl_solver.cpp
+++ b/src/theory/arith/nl/nl_solver.cpp
@@ -843,7 +843,7 @@ std::vector<NlLemma> NlSolver::checkMonomialMagnitude(unsigned c)
   std::vector<NlLemma> nr_lemmas;
   for (unsigned i = 0; i < lemmas.size(); i++)
   {
-    if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end())
+    if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end())
     {
       nr_lemmas.push_back(lemmas[i]);
     }
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 8535396e7..ada6aa11a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -166,9 +166,9 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
 {
   for (const NlLemma& nlem : out)
   {
-    Node lem = nlem.d_lemma;
-    LemmaProperty p = nlem.getLemmaProperty();
-    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id
+    Node lem = nlem.d_node;
+    LemmaProperty p = nlem.d_property;
+    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference
                           << " : " << lem << std::endl;
     d_containing.getOutputChannel().lemma(lem, p);
     // process the side effect
@@ -182,7 +182,7 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
     {
       d_lemmas.insert(lem);
     }
-    d_stats.d_inferences << nlem.d_id;
+    d_stats.d_inferences << nlem.d_inference;
   }
 }
 
@@ -210,14 +210,15 @@ void NonlinearExtension::computeRelevantAssertions(
 unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
 {
   Trace("nl-ext-lemma-debug")
-      << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl;
-  lem.d_lemma = Rewriter::rewrite(lem.d_lemma);
+      << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl;
+  lem.d_node = Rewriter::rewrite(lem.d_node);
   // get the proper cache
-  NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas;
-  if (lcache.find(lem.d_lemma) != lcache.end())
+  NodeSet& lcache =
+      isLemmaPropertyPreprocess(lem.d_property) ? d_lemmasPp : d_lemmas;
+  if (lcache.find(lem.d_node) != lcache.end())
   {
     Trace("nl-ext-lemma-debug")
-        << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl;
+        << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl;
     return 0;
   }
   out.emplace_back(lem);
@@ -232,7 +233,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
     // check if any are entailed to be false
     for (const NlLemma& lem : lemmas)
     {
-      Node ch_lemma = lem.d_lemma.negate();
+      Node ch_lemma = lem.d_node.negate();
       ch_lemma = Rewriter::rewrite(ch_lemma);
       Trace("nl-ext-et-debug")
           << "Check entailment of " << ch_lemma << "..." << std::endl;
@@ -243,7 +244,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
       if (et.first)
       {
         Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
-                           << lem.d_lemma << std::endl;
+                           << lem.d_node << std::endl;
         // return just this lemma
         if (filterLemma(lem, out) > 0)
         {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index ee58a9e2e..d035b1056 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -172,6 +172,9 @@ class NonlinearExtension
    */
   void presolve();
 
+  /** Process side effect se */
+  void processSideEffect(const NlLemma& se);
+
  private:
   /** Model-based refinement
    *
@@ -274,8 +277,6 @@ class NonlinearExtension
    * Send lemmas in out on the output channel of theory of arithmetic.
    */
   void sendLemmas(const std::vector<NlLemma>& out);
-  /** Process side effect se */
-  void processSideEffect(const NlLemma& se);
 
   /** cache of all lemmas sent on the output channel (user-context-dependent) */
   NodeSet d_lemmas;
diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index 321818b94..b2ef16459 100644
--- a/src/theory/arith/nl/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental_solver.cpp
@@ -212,8 +212,8 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
     // note we must do preprocess on this lemma
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                           << std::endl;
-    NlLemma nlem(lem, Inference::T_PURIFY_ARG);
-    nlem.d_preprocess = true;
+    NlLemma nlem(
+        lem, LemmaProperty::PREPROCESS, nullptr, Inference::T_PURIFY_ARG);
     lems.emplace_back(nlem);
   }
 
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index a1cb9c4e9..df01b4e93 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -121,5 +121,13 @@ void InferenceManagerBuffered::clearPendingPhaseRequirements()
   d_pendingReqPhase.clear();
 }
 
+
+  std::size_t InferenceManagerBuffered::numPendingLemmas() const {
+    return d_pendingLem.size();
+  }
+  std::size_t InferenceManagerBuffered::numPendingFacts() const {
+    return d_pendingFact.size();
+  }
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index e6e7822c5..762b7d4e0 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   InferenceManagerBuffered(Theory& t,
                            TheoryState& state,
                            ProofNodeManager* pnm);
-  ~InferenceManagerBuffered() {}
+  virtual ~InferenceManagerBuffered() {}
   /**
    * Have we processed an inference during this call to check? In particular,
    * this returns true if we have a pending fact or lemma, or have encountered
@@ -124,6 +124,11 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   /** Clear pending phase requirements, without processing */
   void clearPendingPhaseRequirements();
 
+  /** Returns the number of pending lemmas. */
+  std::size_t numPendingLemmas() const;
+  /** Returns the number of pending facts. */
+  std::size_t numPendingFacts() const;
+
  protected:
   /** A set of pending inferences to be processed as lemmas */
   std::vector<std::shared_ptr<TheoryInference>> d_pendingLem;