Update sets inference manager to inherit from InferenceManagerBuffered (#5007)

This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.

It matches that base class almost exactly, with cosmetic changes.

Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.

This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.

16 files changed, 109 insertions, 281 deletions

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 8a7713121..3ba41a431 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -29,10 +29,9 @@ InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
 {
 }
 
-bool InferenceManagerBuffered::hasProcessed() const
+bool InferenceManagerBuffered::hasPending() const
 {
-  return d_theoryState.isInConflict() || !d_pendingLem.empty()
-         || !d_pendingFact.empty();
+  return hasPendingFact() || hasPendingLemma();
 }
 
 bool InferenceManagerBuffered::hasPendingFact() const
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 62c3c9b55..e5ad4cb0a 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -37,11 +37,9 @@ class InferenceManagerBuffered : public TheoryInferenceManager
                            ProofNodeManager* pnm);
   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
-   * a conflict.
+   * Do we have a pending fact or lemma?
    */
-  bool hasProcessed() const;
+  bool hasPending() const;
   /**
    * Do we have a pending fact to add as an internal fact to the equality
    * engine?
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 08410943f..a51cee2c3 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -30,13 +30,10 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-CardinalityExtension::CardinalityExtension(SolverState& s,
-                                           InferenceManager& im,
-                                           context::Context* c,
-                                           context::UserContext* u)
+CardinalityExtension::CardinalityExtension(SolverState& s, InferenceManager& im)
     : d_state(s),
       d_im(im),
-      d_card_processed(u),
+      d_card_processed(s.getUserContext()),
       d_finite_type_constants_processed(false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -288,7 +285,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n)
       d_im.assertInference(lem, d_emp_exp, "card", 1);
     }
   }
-  d_im.flushPendingLemmas();
+  d_im.doPendingLemmas();
 }
 
 void CardinalityExtension::checkCardCycles()
@@ -340,7 +337,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       Trace("sets-cycle-debug")
           << "CYCLE: " << fact << " from " << exp << std::endl;
       d_im.assertInference(fact, exp, "card_cycle");
-      d_im.flushPendingLemmas();
+      d_im.doPendingLemmas();
     }
     else
     {
@@ -416,7 +413,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         }
       }
       d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp");
-      d_im.flushPendingLemmas();
+      d_im.doPendingLemmas();
       if (d_im.hasProcessed())
       {
         return;
@@ -448,7 +445,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         Trace("sets-debug") << "  it is empty..." << std::endl;
         Assert(!d_state.areEqual(n, emp_set));
         d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar");
-        d_im.flushPendingLemmas();
+        d_im.doPendingLemmas();
         if (d_im.hasProcessed())
         {
           return;
@@ -495,7 +492,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         Trace("sets-debug")
             << "...derived " << conc.size() << " conclusions" << std::endl;
         d_im.assertInference(conc, n.eqNode(p), "cg_eqpar");
-        d_im.flushPendingLemmas();
+        d_im.doPendingLemmas();
         if (d_im.hasProcessed())
         {
           return;
@@ -547,7 +544,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         {
           Node conc = n.eqNode(cpk);
           d_im.assertInference(conc, exps, "cg_par_sing");
-          d_im.flushPendingLemmas();
+          d_im.doPendingLemmas();
         }
         else
         {
@@ -602,7 +599,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
             }
           }
           d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq");
-          d_im.flushPendingLemmas();
+          d_im.doPendingLemmas();
           if (d_im.hasProcessed())
           {
             return;
@@ -973,7 +970,7 @@ void CardinalityExtension::checkMinCard()
     }
   }
   // flush the lemmas
-  d_im.flushPendingLemmas();
+  d_im.doPendingLemmas();
 }
 
 bool CardinalityExtension::isModelValueBasic(Node eqc)
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index b71af8a43..c257f45c5 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -67,10 +67,7 @@ class CardinalityExtension
    * Constructs a new instance of the cardinality solver w.r.t. the provided
    * contexts.
    */
-  CardinalityExtension(SolverState& s,
-                       InferenceManager& im,
-                       context::Context* c,
-                       context::UserContext* u);
+  CardinalityExtension(SolverState& s, InferenceManager& im);
 
   ~CardinalityExtension() {}
   /** reset
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 8f25f6511..6f0d80b3a 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -15,8 +15,6 @@
 #include "theory/sets/inference_manager.h"
 
 #include "options/sets_options.h"
-#include "theory/sets/theory_sets.h"
-#include "theory/sets/theory_sets_private.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -25,28 +23,15 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-InferenceManager::InferenceManager(TheorySetsPrivate& p,
+InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
-                                   context::Context* c,
-                                   context::UserContext* u)
-    : d_parent(p),
-      d_state(s),
-      d_sentLemma(false),
-      d_addedFact(false),
-      d_lemmas_produced(u),
-      d_keep(c)
+                                   ProofNodeManager* pnm)
+    : InferenceManagerBuffered(t, s, pnm), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-void InferenceManager::reset()
-{
-  d_sentLemma = false;
-  d_addedFact = false;
-  d_pendingLemmas.clear();
-}
-
 bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
 {
   // should we send this fact out as a lemma?
@@ -61,7 +46,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     {
       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
     }
-    d_pendingLemmas.push_back(lem);
+    addPendingLemma(lem);
     return true;
   }
   Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
@@ -96,18 +81,22 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
   }
   bool polarity = fact.getKind() != NOT;
   TNode atom = polarity ? fact : fact[0];
+  if (d_state.isEntailed(atom, polarity))
+  {
+    return false;
+  }
   // things we can assert to equality engine
   if (atom.getKind() == MEMBER
       || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
   {
     // send to equality engine
-    if (d_parent.assertFact(fact, exp))
+    if (assertInternalFact(atom, polarity, exp))
     {
-      d_addedFact = true;
+      // return true if this wasn't redundant
       return true;
     }
   }
-  else if (!d_state.isEntailed(fact, true))
+  else
   {
     // must send as lemma
     Node lem = fact;
@@ -115,7 +104,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType)
     {
       lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact);
     }
-    d_pendingLemmas.push_back(lem);
+    addPendingLemma(lem);
     return true;
   }
   return false;
@@ -125,8 +114,6 @@ void InferenceManager::assertInference(Node fact,
                                        const char* c,
                                        int inferType)
 {
-  d_keep.insert(exp);
-  d_keep.insert(fact);
   if (assertFactRec(fact, exp, inferType))
   {
     Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
@@ -176,67 +163,15 @@ void InferenceManager::split(Node n, int reqPol)
 {
   n = Rewriter::rewrite(n);
   Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
-  flushLemma(lem);
+  // send the lemma
+  lemma(lem);
   Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
   if (reqPol != 0)
   {
     Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
                         << std::endl;
-    d_parent.getOutputChannel()->requirePhase(n, reqPol > 0);
-  }
-}
-void InferenceManager::flushLemmas(std::vector<Node>& lemmas, bool preprocess)
-{
-  if (!d_state.isInConflict())
-  {
-    for (const Node& l : lemmas)
-    {
-      flushLemma(l, preprocess);
-    }
+    requirePhase(n, reqPol > 0);
   }
-  lemmas.clear();
-}
-
-void InferenceManager::flushLemma(Node lem, bool preprocess)
-{
-  if (d_state.isInConflict())
-  {
-    return;
-  }
-  if (d_lemmas_produced.find(lem) != d_lemmas_produced.end())
-  {
-    Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
-    return;
-  }
-  Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
-  d_lemmas_produced.insert(lem);
-  LemmaProperty p =
-      preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
-  d_parent.getOutputChannel()->lemma(lem, p);
-  d_sentLemma = true;
-}
-
-void InferenceManager::flushPendingLemmas(bool preprocess)
-{
-  flushLemmas(d_pendingLemmas, preprocess);
-}
-
-bool InferenceManager::hasLemmaCached(Node lem) const
-{
-  return d_lemmas_produced.find(lem) != d_lemmas_produced.end();
-}
-
-bool InferenceManager::hasProcessed() const
-{
-  return d_state.isInConflict() || d_sentLemma || d_addedFact;
-}
-bool InferenceManager::hasSentLemma() const { return d_sentLemma; }
-bool InferenceManager::hasAddedFact() const { return d_addedFact; }
-
-void InferenceManager::conflict(Node conf)
-{
-  d_parent.getOutputChannel()->conflict(conf);
-  d_state.notifyInConflict();
 }
 
 }  // namespace sets
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index 3278b848e..cc60ea4db 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
 #define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
 
+#include "theory/inference_manager_buffered.h"
 #include "theory/sets/solver_state.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -33,22 +33,12 @@ class TheorySetsPrivate;
  * of theory of sets or internally as literals asserted to the equality engine
  * of theory of sets. The latter literals are referred to as "facts".
  */
-class InferenceManager
+class InferenceManager : public InferenceManagerBuffered
 {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  InferenceManager(TheorySetsPrivate& p,
-                   SolverState& s,
-                   context::Context* c,
-                   context::UserContext* u);
-  /** reset
-   *
-   * Called at the beginning of a full effort check. Resets the information
-   * related to this class regarding whether facts and lemmas have been
-   * processed.
-   */
-  void reset();
+  InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
   /**
    * Add facts corresponding to ( exp => fact ) via calls to the assertFact
    * method of TheorySetsPrivate.
@@ -80,71 +70,23 @@ class InferenceManager
                        const char* c,
                        int inferType = 0);
 
-  /** Flush lemmas
-   *
-   * This sends lemmas on the output channel of the theory of sets.
-   *
-   * The argument preprocess indicates whether preprocessing should be applied
-   * (by TheoryEngine) on each of lemmas.
-   */
-  void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
-  /** singular version of above */
-  void flushLemma(Node lem, bool preprocess = false);
-  /** Do we have pending lemmas? */
-  bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); }
-  /** Applies flushLemmas on d_pendingLemmas */
-  void flushPendingLemmas(bool preprocess = false);
   /** flush the splitting lemma ( n OR (NOT n) )
    *
    * If reqPol is not 0, then a phase requirement for n is requested with
    * polarity ( reqPol>0 ).
    */
   void split(Node n, int reqPol = 0);
-  /** Have we sent a lemma during the current call to a full effort check? */
-  bool hasSentLemma() const;
-  /** Have we added a fact during the current call to a full effort check? */
-  bool hasAddedFact() const;
-  /** Have we processed an inference (fact, lemma, or conflict)? */
-  bool hasProcessed() const;
-  /** Have we sent lem as a lemma in the current user context? */
-  bool hasLemmaCached(Node lem) const;
-
-  /** 
-   * Send conflict.
-   * @param conf The conflict node to be sent on the output channel
-   */
-  void conflict(Node conf);
 
  private:
   /** constants */
   Node d_true;
   Node d_false;
-  /** the theory of sets which owns this */
-  TheorySetsPrivate& d_parent;
-  /** Reference to the state object for the theory of sets */
-  SolverState& d_state;
-  /** pending lemmas */
-  std::vector<Node> d_pendingLemmas;
-  /** sent lemma
-   *
-   * This flag is set to true during a full effort check if this theory
-   * called d_out->lemma(...).
-   */
-  bool d_sentLemma;
-  /** added fact
-   *
-   * This flag is set to true during a full effort check if this theory
-   * added an internal fact to its equality engine.
-   */
-  bool d_addedFact;
-  /** A user-context-dependent cache of all lemmas produced */
-  NodeSet d_lemmas_produced;
   /**
-   * A set of nodes to ref-count. Nodes that are facts or are explanations of
-   * facts must be added to this set since the equality engine does not
-   * ref count nodes.
+   * Reference to the state object for the theory of sets. We store the
+   * (derived) state here, since it has additional methods required in this
+   * class.
    */
-  NodeSet d_keep;
+  SolverState& d_state;
   /** Assert fact recursive
    *
    * This is a helper function for assertInference, which calls assertFact
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 5e5e9d22a..7254bca78 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -25,16 +25,17 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-SolverState::SolverState(TheorySetsPrivate& p,
-                         context::Context* c,
+SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
                          Valuation val)
-    : TheoryState(c, u, val), d_parent(p), d_proxy(u), d_proxy_to_term(u)
+    : TheoryState(c, u, val), d_parent(nullptr), d_proxy(u), d_proxy_to_term(u)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
+void SolverState::setParent(TheorySetsPrivate* p) { d_parent = p; }
+
 void SolverState::reset()
 {
   d_set_eqc.clear();
@@ -249,7 +250,7 @@ bool SolverState::isEntailed(Node n, bool polarity) const
     if (polarity && d_ee->hasTerm(n[1]))
     {
       Node r = d_ee->getRepresentative(n[1]);
-      if (d_parent.isMember(n[0], r))
+      if (d_parent->isMember(n[0], r))
       {
         return true;
       }
@@ -387,13 +388,13 @@ Node SolverState::getProxy(Node n)
   d_proxy_to_term[k] = n;
   Node eq = k.eqNode(n);
   Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
-  d_parent.getOutputChannel()->lemma(eq);
+  d_parent->getOutputChannel()->lemma(eq);
   if (nk == SINGLETON)
   {
     Node slem = nm->mkNode(MEMBER, n[0], k);
     Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton"
                         << std::endl;
-    d_parent.getOutputChannel()->lemma(slem);
+    d_parent->getOutputChannel()->lemma(slem);
   }
   return k;
 }
@@ -452,7 +453,7 @@ Node SolverState::getUnivSet(TypeNode tn)
       Node ulem = nm->mkNode(SUBSET, n1, n2);
       Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type"
                           << std::endl;
-      d_parent.getOutputChannel()->lemma(ulem);
+      d_parent->getOutputChannel()->lemma(ulem);
     }
   }
   d_univset[tn] = n;
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 3a40befbd..1786c414b 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -48,10 +48,9 @@ class SolverState : public TheoryState
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
  public:
-  SolverState(TheorySetsPrivate& p,
-              context::Context* c,
-              context::UserContext* u,
-              Valuation val);
+  SolverState(context::Context* c, context::UserContext* u, Valuation val);
+  /** Set parent */
+  void setParent(TheorySetsPrivate* p);
   //-------------------------------- initialize per check
   /** reset, clears the data structures maintained by this class. */
   void reset();
@@ -204,8 +203,8 @@ class SolverState : public TheoryState
   /** the empty vector and map */
   std::vector<Node> d_emptyVec;
   std::map<Node, Node> d_emptyMap;
-  /** Reference to the parent theory of sets */
-  TheorySetsPrivate& d_parent;
+  /** Pointer to the parent theory of sets */
+  TheorySetsPrivate* d_parent;
   /** The list of all equivalence classes of type set in the current context */
   std::vector<Node> d_set_eqc;
   /** Maps types to the equivalence class containing empty set of that type */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index cb42f09d5..8b969de39 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,16 +34,21 @@ TheorySets::TheorySets(context::Context* c,
                        const LogicInfo& logicInfo,
                        ProofNodeManager* pnm)
     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
-      d_internal(new TheorySetsPrivate(*this, c, u, valuation)),
+      d_state(c, u, valuation),
+      d_im(*this, d_state, pnm),
+      d_internal(new TheorySetsPrivate(*this, d_state, d_im)),
       d_notify(*d_internal.get())
 {
-  // use the state object as the official theory state
-  d_theoryState = d_internal->getSolverState();
+  // use the official theory state and inference manager objects
+  d_theoryState = &d_state;
+  d_inferManager = &d_im;
+
+  // TODO: remove this
+  d_state.setParent(d_internal.get());
 }
 
 TheorySets::~TheorySets()
 {
-  // Do not move me to the header. See explanation in the constructor.
 }
 
 TheoryRewriter* TheorySets::getTheoryRewriter()
@@ -90,12 +95,6 @@ void TheorySets::finishInit()
 
 void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
 
-bool TheorySets::preNotifyFact(
-    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
-{
-  return d_internal->preNotifyFact(atom, polarity, fact);
-}
-
 void TheorySets::notifyFact(TNode atom,
                             bool polarity,
                             TNode fact,
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 7787c0f9b..fed74b1bb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -21,6 +21,8 @@
 
 #include <memory>
 
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -61,12 +63,6 @@ class TheorySets : public Theory
   //--------------------------------- standard check
   /** Post-check, called after the fact queue of the theory is processed. */
   void postCheck(Effort level) override;
-  /** Pre-notify fact, return true if processed. */
-  bool preNotifyFact(TNode atom,
-                     bool pol,
-                     TNode fact,
-                     bool isPrereg,
-                     bool isInternal) override;
   /** Notify fact */
   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
   //--------------------------------- end standard check
@@ -102,6 +98,10 @@ class TheorySets : public Theory
    private:
     TheorySetsPrivate& d_theory;
   };
+  /** The state of the sets solver at full effort */
+  SolverState d_state;
+  /** The inference manager */
+  InferenceManager d_im;
   /** The internal theory */
   std::unique_ptr<TheorySetsPrivate> d_internal;
   /** Instance of the above class */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index c432c8039..7d498a798 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -35,19 +35,17 @@ namespace theory {
 namespace sets {
 
 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
-                                     context::Context* c,
-                                     context::UserContext* u,
-                                     Valuation valuation)
-    : d_members(c),
-      d_deq(c),
-      d_termProcessed(u),
-      d_keep(c),
+                                     SolverState& state,
+                                     InferenceManager& im)
+    : d_members(state.getSatContext()),
+      d_deq(state.getSatContext()),
+      d_termProcessed(state.getUserContext()),
       d_full_check_incomplete(false),
       d_external(external),
-      d_state(*this, c, u, valuation),
-      d_im(*this, d_state, c, u),
-      d_rels(new TheorySetsRels(d_state, d_im, u)),
-      d_cardSolver(new CardinalityExtension(d_state, d_im, c, u)),
+      d_state(state),
+      d_im(im),
+      d_rels(new TheorySetsRels(d_state, d_im)),
+      d_cardSolver(new CardinalityExtension(d_state, d_im)),
       d_rels_enabled(false),
       d_card_enabled(false)
 {
@@ -104,9 +102,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
             // infer equality between elements of singleton
             Node exp = s1.eqNode(s2);
             Node eq = s1[0].eqNode(s2[0]);
-            d_keep.insert(exp);
-            d_keep.insert(eq);
-            assertFact(eq, exp);
+            d_im.assertInternalFact(eq, true, exp);
           }
           else
           {
@@ -166,11 +162,9 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
               if (s1[0] != m2[0])
               {
                 Node eq = s1[0].eqNode(m2[0]);
-                d_keep.insert(exp);
-                d_keep.insert(eq);
                 Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
                                    << " => " << eq << std::endl;
-                assertFact(eq, exp);
+                d_im.assertInternalFact(eq, true, exp);
               }
             }
             else
@@ -270,29 +264,6 @@ bool TheorySetsPrivate::isMember(Node x, Node s)
   return false;
 }
 
-bool TheorySetsPrivate::assertFact(Node fact, Node exp)
-{
-  Trace("sets-assert") << "TheorySets::assertFact : " << fact
-                       << ", exp = " << exp << std::endl;
-  bool polarity = fact.getKind() != kind::NOT;
-  TNode atom = polarity ? fact : fact[0];
-  if (d_state.isEntailed(atom, polarity))
-  {
-    return false;
-  }
-  if (atom.getKind() == kind::EQUAL)
-  {
-    d_equalityEngine->assertEquality(atom, polarity, exp);
-  }
-  else
-  {
-    d_equalityEngine->assertPredicate(atom, polarity, exp);
-  }
-  // call the notify new fact method
-  notifyFact(atom, polarity, exp);
-  return true;
-}
-
 void TheorySetsPrivate::fullEffortReset()
 {
   Assert(d_equalityEngine->consistent());
@@ -305,6 +276,7 @@ void TheorySetsPrivate::fullEffortReset()
   d_state.reset();
   // reset the inference manager
   d_im.reset();
+  d_im.clearPendingLemmas();
   // reset the cardinality solver
   d_cardSolver->reset();
 }
@@ -314,7 +286,7 @@ void TheorySetsPrivate::fullEffortCheck()
   Trace("sets") << "----- Full effort check ------" << std::endl;
   do
   {
-    Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+    Assert(!d_im.hasPendingLemma() || d_im.hasProcessed());
 
     Trace("sets") << "...iterate full effort check..." << std::endl;
     fullEffortReset();
@@ -448,35 +420,35 @@ void TheorySetsPrivate::fullEffortCheck()
     }
     // check subtypes
     checkSubtypes();
-    d_im.flushPendingLemmas(true);
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;
     }
     // check downwards closure
     checkDownwardsClosure();
-    d_im.flushPendingLemmas();
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;
     }
     // check upwards closure
     checkUpwardsClosure();
-    d_im.flushPendingLemmas();
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;
     }
     // check disequalities
     checkDisequalities();
-    d_im.flushPendingLemmas();
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;
     }
     // check reduce comprehensions
     checkReduceComprehensions();
-    d_im.flushPendingLemmas();
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       continue;
@@ -496,8 +468,8 @@ void TheorySetsPrivate::fullEffortCheck()
       d_rels->check(Theory::EFFORT_FULL);
     }
   } while (!d_im.hasSentLemma() && !d_state.isInConflict()
-           && d_im.hasAddedFact());
-  Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
+           && d_im.hasSentFact());
+  Assert(!d_im.hasPendingLemma() || d_im.hasProcessed());
   Trace("sets") << "----- End full effort check, conflict="
                 << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
                 << std::endl;
@@ -854,7 +826,7 @@ void TheorySetsPrivate::checkDisequalities()
     Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
     lem = Rewriter::rewrite(lem);
     d_im.assertInference(lem, d_true, "diseq", 1);
-    d_im.flushPendingLemmas();
+    d_im.doPendingLemmas();
     if (d_im.hasProcessed())
     {
       return;
@@ -893,7 +865,7 @@ void TheorySetsPrivate::checkReduceComprehensions()
         nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
     Trace("sets-comprehension")
         << "Comprehension reduction: " << lem << std::endl;
-    d_im.flushLemma(lem);
+    d_im.lemma(lem);
   }
 }
 
@@ -922,12 +894,6 @@ void TheorySetsPrivate::postCheck(Theory::Effort level)
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
 }
 
-bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact)
-{
-  // use entailment check (is this necessary?)
-  return d_state.isEntailed(atom, polarity);
-}
-
 void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
 {
   if (d_state.isInConflict())
@@ -946,16 +912,14 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
       {
         Node pexp = NodeManager::currentNM()->mkNode(
             kind::AND, atom, atom[1].eqNode(s));
-        d_keep.insert(pexp);
         if (s.getKind() == kind::SINGLETON)
         {
           if (s[0] != atom[0])
           {
             Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
             Node eq = s[0].eqNode(atom[0]);
-            d_keep.insert(eq);
             // triggers an internal inference
-            assertFact(eq, pexp);
+            d_im.assertInternalFact(eq, true, pexp);
           }
         }
         else
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 0df1eabc5..bd1d5f058 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -46,12 +46,6 @@ class TheorySetsPrivate {
   void eqNotifyNewClass(TNode t);
   void eqNotifyMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
-  /** Assert fact holds in the current context with explanation exp.
-   *
-   * exp should be explainable by the equality engine of this class, and fact
-   * should be a literal.
-   */
-  bool assertFact(Node fact, Node exp);
 
  private:
   /** Are a and b trigger terms in the equality engine that may be disequal? */
@@ -122,7 +116,6 @@ class TheorySetsPrivate {
    * context.
    */
   NodeSet d_termProcessed;
-  NodeSet d_keep;
   
   //propagation
   class EqcInfo
@@ -155,9 +148,8 @@ class TheorySetsPrivate {
    * contexts.
    */
   TheorySetsPrivate(TheorySets& external,
-                    context::Context* c,
-                    context::UserContext* u,
-                    Valuation valuation);
+                    SolverState& state,
+                    InferenceManager& im);
 
   ~TheorySetsPrivate();
 
@@ -175,8 +167,6 @@ class TheorySetsPrivate {
   //--------------------------------- standard check
   /** Post-check, called after the fact queue of the theory is processed. */
   void postCheck(Theory::Effort level);
-  /** Preprocess fact, return true if processed. */
-  bool preNotifyFact(TNode atom, bool polarity, TNode fact);
   /** Notify new fact */
   void notifyFact(TNode atom, bool polarity, TNode fact);
   //--------------------------------- end standard check
@@ -237,6 +227,10 @@ class TheorySetsPrivate {
 
  private:
   TheorySets& d_external;
+  /** The state of the sets solver at full effort */
+  SolverState& d_state;
+  /** The inference manager of the sets solver */
+  InferenceManager& d_im;
 
   /** Pointer to the equality engine of theory of sets */
   eq::EqualityEngine* d_equalityEngine;
@@ -256,10 +250,6 @@ class TheorySetsPrivate {
    * given set type, or creates a new one if it does not exist.
    */
   Node getChooseFunction(const TypeNode& setType);
-  /** The state of the sets solver at full effort */
-  SolverState d_state;
-  /** The inference manager of the sets solver */
-  InferenceManager d_im;
   /** subtheory solver for the theory of relations */
   std::unique_ptr<TheorySetsRels> d_rels;
   /** subtheory solver for the theory of sets with cardinality */
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index c8eeece4a..838d29045 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -31,10 +31,8 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator
 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator               TERM_IT;
 typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
 
-TheorySetsRels::TheorySetsRels(SolverState& s,
-                               InferenceManager& im,
-                               context::UserContext* u)
-    : d_state(s), d_im(im), d_shared_terms(u)
+TheorySetsRels::TheorySetsRels(SolverState& s, InferenceManager& im)
+    : d_state(s), d_im(im), d_shared_terms(s.getUserContext())
 {
   d_trueNode = NodeManager::currentNM()->mkConst(true);
   d_falseNode = NodeManager::currentNM()->mkConst(false);
@@ -1103,7 +1101,7 @@ void TheorySetsRels::check(Theory::Effort level)
       // if we are still not in conflict, send lemmas
       if (!d_state.isInConflict())
       {
-        d_im.flushPendingLemmas();
+        d_im.doPendingLemmas();
       }
     }
     d_pending.clear();
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 60715ff57..f48aaf9c5 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -65,9 +65,7 @@ class TheorySetsRels {
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
 public:
- TheorySetsRels(SolverState& s,
-                InferenceManager& im,
-                context::UserContext* u);
+ TheorySetsRels(SolverState& s, InferenceManager& im);
 
  ~TheorySetsRels();
  /**
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 9405a8162..330613e2e 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -56,6 +56,12 @@ void TheoryInferenceManager::reset()
   d_numCurrentFacts = 0;
 }
 
+bool TheoryInferenceManager::hasProcessed() const
+{
+  return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
+         || d_numCurrentFacts > 0;
+}
+
 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
 {
   if (!d_theoryState.isInConflict())
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 7e5ef6dec..080a09ba8 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -87,6 +87,11 @@ class TheoryInferenceManager
    * beginning of this loop and repeat its strategy while hasAddedFact is true.
    */
   void reset();
+  /**
+   * Returns true if we are in conflict, or if we have sent a lemma or fact
+   * since the last call to reset.
+   */
+  bool hasProcessed() const;
   //--------------------------------------- propagations
   /**
    * T-propagate literal lit, possibly encountered by equality engine,