From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Feb 2021 22:50:16 +0000 (-0600)
Subject: Use quantifiers inference manager for lemma management (#5867)
X-Git-Tag: cvc5-1.0.0~2305
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c198f374972e62db0cebc93d3977fd1e414f431b;p=cvc5.git

Use quantifiers inference manager for lemma management (#5867)

Towards eliminating dependencies on quantifiers engine.

This replaces the custom implementation of lemma management in quantifiers engine with the standard one.

It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.

Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
---

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 835dbe798..f17029618 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -33,8 +33,8 @@ namespace CVC4 {
 class Command;
 class CommandStatus;
 class UnsatCore;
-class InstantiationList;
-class SkolemList;
+struct InstantiationList;
+struct SkolemList;
 
 class Printer
 {
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index cdba5dfd6..bc038a149 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -44,12 +44,23 @@ bool InferenceManagerBuffered::hasPendingLemma() const
   return !d_pendingLem.empty();
 }
 
-void InferenceManagerBuffered::addPendingLemma(Node lem,
+bool InferenceManagerBuffered::addPendingLemma(Node lem,
                                                LemmaProperty p,
-                                               ProofGenerator* pg)
+                                               ProofGenerator* pg,
+                                               bool checkCache)
 {
+  if (checkCache)
+  {
+    // check if it is unique up to rewriting
+    Node lemr = Rewriter::rewrite(lem);
+    if (hasCachedLemma(lemr, p))
+    {
+      return false;
+    }
+  }
   // make the simple theory lemma
   d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg));
+  return true;
 }
 
 void InferenceManagerBuffered::addPendingLemma(
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 6edc0298f..28014ce8e 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -52,10 +52,19 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * non-null, pg must be able to provide a proof for lem for the remainder
    * of the user context. Pending lemmas are sent to the output channel using
    * doPendingLemmas.
+   *
+   * @param lem The lemma to send
+   * @param p The property of the lemma
+   * @param pg The proof generator which can provide a proof for lem
+   * @param checkCache Whether we want to check that the lemma is already in
+   * the cache.
+   * @return true if the lemma was added to the list of pending lemmas and
+   * false if the lemma is already cached.
    */
-  void addPendingLemma(Node lem,
+  bool addPendingLemma(Node lem,
                        LemmaProperty p = LemmaProperty::NONE,
-                       ProofGenerator* pg = nullptr);
+                       ProofGenerator* pg = nullptr,
+                       bool checkCache = true);
   /**
    * Add pending lemma, where lemma can be a (derived) class of the
    * theory inference base class.
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 411ab36b9..b2fff012e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1082,8 +1082,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
   }
   Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
   bool ret = d_parent->doAddInstantiation(subs);
-  for( unsigned i=0; i<lemmas.size(); i++ ){
-    d_parent->addLemma(lemmas[i]);
+  for (const Node& l : lemmas)
+  {
+    d_parent->addPendingLemma(l);
   }
   return ret;
 }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 037cb74d7..208933456 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -108,7 +108,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       //add counterexample lemma
       Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
       //require any decision on cel to be phase=true
-      d_quantEngine->addRequirePhase( ceLit, true );
+      d_qim.addPendingPhaseRequirement(ceLit, true);
       Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
       //add counterexample lemma
       lem = Rewriter::rewrite( lem );
@@ -259,7 +259,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
       clSet = double(clock())/double(CLOCKS_PER_SEC);
       Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
     }
-    unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+    size_t lastWaiting = d_qim.numPendingLemmas();
     for( int ee=0; ee<=1; ee++ ){
       //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
@@ -273,15 +273,17 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
           break;
         }
       }
-      if (d_qstate.isInConflict()
-          || d_quantEngine->getNumLemmasWaiting() > lastWaiting)
+      if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting)
       {
         break;
       }
     }
     if( Trace.isOn("cegqi-engine") ){
-      if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
-        Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+      if (d_qim.numPendingLemmas() > lastWaiting)
+      {
+        Trace("cegqi-engine")
+            << "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting)
+            << std::endl;
       }
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
       Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
@@ -392,7 +394,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   {
     Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
                          << std::endl;
-    d_quantEngine->addLemma(auxLems[i], false);
+    d_qim.addPendingLemma(auxLems[i]);
   }
 }
 
@@ -491,11 +493,11 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   }
 }
 
-bool InstStrategyCegqi::addLemma( Node lem ) {
-  return d_quantEngine->addLemma( lem );
+bool InstStrategyCegqi::addPendingLemma(Node lem) const
+{
+  return d_qim.addPendingLemma(lem);
 }
 
-
 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
       d_cinst.find(q);
@@ -534,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
       // add lemmas to process
       for (const Node& lem : lems)
       {
-        d_quantEngine->addLemma(lem);
+        d_qim.addPendingLemma(lem);
       }
       // don't need to process this, since it has been reduced
       return true;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index a6a3c36cd..7d39efc6b 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -123,8 +123,8 @@ class InstStrategyCegqi : public QuantifiersModule
   //------------------- interface for CegqiOutputInstStrategy
   /** Instantiate the current quantified formula forall x. Q with x -> subs. */
   bool doAddInstantiation(std::vector<Node>& subs);
-  /** Add lemma lem via the output channel of this class. */
-  bool addLemma(Node lem);
+  /** Add pending lemma lem via the inference manager of this class. */
+  bool addPendingLemma(Node lem) const;
   //------------------- end interface for CegqiOutputInstStrategy
 
  protected:
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 83a102633..bfaf0b83c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -347,10 +347,11 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
       std::vector< Node > lem;
       getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
       if( !lem.empty() ){
-        for( unsigned j=0; j<lem.size(); j++ ){
-          d_quantEngine->addLemma( lem[j], false );
-          d_hasAddedLemma = true;
+        for (const Node& l : lem)
+        {
+          d_qim.addPendingLemma(l);
         }
+        d_hasAddedLemma = true;
         return false;
       }
     }
@@ -929,8 +930,8 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
               d_eq_conjectures[rhs].push_back( lhs );
 
               Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg );
-              d_quantEngine->addLemma( lem, false );
-              d_quantEngine->addRequirePhase( rsg, false );
+              d_qim.addPendingLemma(lem);
+              d_qim.addPendingPhaseRequirement(rsg, false);
               addedLemmas++;
               if( (int)addedLemmas>=options::conjectureGenPerRound() ){
                 break;
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 7479d005a..7cc1074aa 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -30,10 +30,11 @@ namespace inst {
 
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
+    quantifiers::QuantifiersInferenceManager& qim,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
@@ -497,7 +498,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
           {
             Node u = tdb->getHoTypeMatchPredicate(tn);
             Node au = nm->mkNode(kind::APPLY_UF, u, f);
-            if (d_quantEngine->addLemma(au))
+            if (d_qim.addPendingLemma(au))
             {
               // this forces f to be a first-class member of the quantifier-free
               // equality engine, which in turn forces the quantifier-free
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index d9636cd65..e424f69d1 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -93,6 +93,7 @@ class HigherOrderTrigger : public Trigger
 
  private:
   HigherOrderTrigger(QuantifiersEngine* qe,
+                     quantifiers::QuantifiersInferenceManager& qim,
                      Node q,
                      std::vector<Node>& nodes,
                      std::map<Node, std::vector<Node> >& ho_apps);
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 916790d9c..3baa25fa0 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -29,6 +29,7 @@ class QuantifiersEngine;
 namespace quantifiers {
 
 class QuantifiersState;
+class QuantifiersInferenceManager;
 
 /** A status response to process */
 enum class InstStrategyStatus
@@ -45,8 +46,10 @@ enum class InstStrategyStatus
 class InstStrategy
 {
  public:
-  InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs)
-      : d_quantEngine(qe), d_qstate(qs)
+  InstStrategy(QuantifiersEngine* qe,
+               QuantifiersState& qs,
+               QuantifiersInferenceManager& qim)
+      : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
   {
   }
   virtual ~InstStrategy() {}
@@ -64,6 +67,8 @@ class InstStrategy
   QuantifiersEngine* d_quantEngine;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
+  /** The quantifiers inference manager object */
+  QuantifiersInferenceManager& d_qim;
 }; /* class InstStrategy */
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 7c302e68c..7c8ab5ec2 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -58,10 +58,12 @@ struct sortTriggers {
   }
 };
 
-InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
-                                                         QuantifiersState& qs,
-                                                         QuantRelevance* qr)
-    : InstStrategy(qe, qs), d_quant_rel(qr)
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
+    QuantifiersEngine* qe,
+    QuantifiersState& qs,
+    QuantifiersInferenceManager& qim,
+    QuantRelevance* qr)
+    : InstStrategy(qe, qs, qim), d_quant_rel(qr)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -280,6 +282,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     if (d_is_single_trigger[patTerms[0]])
     {
       tr = Trigger::mkTrigger(d_quantEngine,
+                              d_qim,
                               f,
                               patTerms[0],
                               false,
@@ -316,6 +319,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       }
       // will possibly want to get an old trigger
       tr = Trigger::mkTrigger(d_quantEngine,
+                              d_qim,
                               f,
                               patTerms,
                               false,
@@ -357,6 +361,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         {
           d_single_trigger_gen[patTerms[index]] = true;
           Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
+                                            d_qim,
                                             f,
                                             patTerms[index],
                                             false,
@@ -627,7 +632,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
         << "Make partially specified user pattern: " << std::endl;
     Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
     Node lem = nm->mkNode(OR, q.negate(), qq);
-    d_quantEngine->addLemma(lem);
+    d_qim.addPendingLemma(lem);
     return;
   }
   unsigned tindex;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index ac3c60ffe..81b40f067 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -87,6 +87,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy
  public:
   InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
                               QuantifiersState& qs,
+                              QuantifiersInferenceManager& qim,
                               QuantRelevance* qr);
   ~InstStrategyAutoGenTriggers() {}
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index c9165c648..9d730e055 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -24,9 +24,11 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie,
-                                                   QuantifiersState& qs)
-    : InstStrategy(ie, qs)
+InstStrategyUserPatterns::InstStrategyUserPatterns(
+    QuantifiersEngine* ie,
+    QuantifiersState& qs,
+    QuantifiersInferenceManager& qim)
+    : InstStrategy(ie, qs, qim)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
@@ -104,7 +106,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     for (size_t i = 0, usize = ugw.size(); i < usize; i++)
     {
       Trigger* t = Trigger::mkTrigger(
-          d_quantEngine, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+          d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL);
       if (t)
       {
         d_user_gen[q].push_back(t);
@@ -162,8 +164,8 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
     d_user_gen_wait[q].push_back(nodes);
     return;
   }
-  Trigger* t =
-      Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
+  Trigger* t = Trigger::mkTrigger(
+      d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW);
   if (t)
   {
     d_user_gen[q].push_back(t);
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index 3d7ddd97b..92b427621 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -33,7 +33,9 @@ namespace quantifiers {
 class InstStrategyUserPatterns : public InstStrategy
 {
  public:
-  InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs);
+  InstStrategyUserPatterns(QuantifiersEngine* qe,
+                           QuantifiersState& qs,
+                           QuantifiersInferenceManager& qim);
   ~InstStrategyUserPatterns();
   /** add pattern */
   void addUserPattern(Node q, Node pat);
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 96b3bd0b0..4f3b207be 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs));
+      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
-    d_i_ag.reset(
-        new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get()));
+    d_i_ag.reset(new InstStrategyAutoGenTriggers(
+        d_quantEngine, qs, qim, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
@@ -73,7 +73,7 @@ void InstantiationEngine::presolve() {
 }
 
 void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
-  unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+  size_t lastWaiting = d_qim.numPendingLemmas();
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -111,7 +111,8 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       }
     }
     //do not consider another level if already added lemma at this level
-    if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+    if (d_qim.numPendingLemmas() > lastWaiting)
+    {
       finished = true;
     }
     e++;
@@ -164,21 +165,19 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
   Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
   if (quantActive)
   {
-    unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+    size_t lastWaiting = d_qim.numPendingLemmas();
     doInstantiationRound(e);
     if (d_qstate.isInConflict())
     {
-      Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
+      Assert(d_qim.numPendingLemmas() > lastWaiting);
       Trace("inst-engine") << "Conflict, added lemmas = "
-                           << (d_quantEngine->getNumLemmasWaiting()
-                               - lastWaiting)
+                           << (d_qim.numPendingLemmas() - lastWaiting)
                            << std::endl;
     }
-    else if (d_quantEngine->hasAddedLemma())
+    else if (d_qim.hasPendingLemma())
     {
       Trace("inst-engine") << "Added lemmas = "
-                           << (d_quantEngine->getNumLemmasWaiting()
-                               - lastWaiting)
+                           << (d_qim.numPendingLemmas() - lastWaiting)
                            << std::endl;
     }
   }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index b1caa739e..58d94a11d 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
@@ -33,8 +34,11 @@ namespace theory {
 namespace inst {
 
 /** trigger class constructor */
-Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
-    : d_quantEngine(qe), d_quant(q)
+Trigger::Trigger(QuantifiersEngine* qe,
+                 quantifiers::QuantifiersInferenceManager& qim,
+                 Node q,
+                 std::vector<Node>& nodes)
+    : d_quantEngine(qe), d_qim(qim), d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -119,7 +123,7 @@ uint64_t Trigger::addInstantiations()
         Node eq = k.eqNode(gt);
         Trace("trigger-gt-lemma")
             << "Trigger: ground term purify lemma: " << eq << std::endl;
-        d_quantEngine->addLemma(eq);
+        d_qim.addPendingLemma(eq);
         gtAddedLemmas++;
       }
     }
@@ -228,6 +232,7 @@ bool Trigger::mkTriggerTerms(Node q,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersInferenceManager& qim,
                             Node f,
                             std::vector<Node>& nodes,
                             bool keepAll,
@@ -268,11 +273,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   Trigger* t;
   if (!ho_apps.empty())
   {
-    t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
+    t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps);
   }
   else
   {
-    t = new Trigger(qe, f, trNodes);
+    t = new Trigger(qe, qim, f, trNodes);
   }
 
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
@@ -280,6 +285,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersInferenceManager& qim,
                             Node f,
                             Node n,
                             bool keepAll,
@@ -288,7 +294,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 {
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars);
+  return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars);
 }
 
 int Trigger::getActiveScore() {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index e2d3f7788..e2ce61bd1 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -29,11 +29,14 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace quantifiers {
+class QuantifiersInferenceManager;
+}
+
 namespace inst {
 
 class IMGenerator;
 class InstMatchGenerator;
-
 /** A collection of nodes representing a trigger.
 *
 * This class encapsulates all implementations of E-matching in CVC4.
@@ -159,6 +162,7 @@ class Trigger {
     TR_RETURN_NULL  //return null if a duplicate is found
   };
   static Trigger* mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersInferenceManager& qim,
                             Node q,
                             std::vector<Node>& nodes,
                             bool keepAll = true,
@@ -166,6 +170,7 @@ class Trigger {
                             size_t useNVars = 0);
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersInferenceManager& qim,
                             Node q,
                             Node n,
                             bool keepAll = true,
@@ -187,7 +192,10 @@ class Trigger {
 
  protected:
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
-  Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes);
+  Trigger(QuantifiersEngine* ie,
+          quantifiers::QuantifiersInferenceManager& qim,
+          Node q,
+          std::vector<Node>& nodes);
   /** add an instantiation (called by InstMatchGenerator)
    *
    * This calls Instantiate::addInstantiation(...) for instantiations
@@ -233,6 +241,8 @@ class Trigger {
   std::vector<Node> d_groundTerms;
   /** The quantifiers engine associated with this trigger. */
   QuantifiersEngine* d_quantEngine;
+  /** Reference to the quantifiers inference manager */
+  quantifiers::QuantifiersInferenceManager& d_qim;
   /** The quantified formula this trigger is for. */
   Node d_quant;
   /** match generator
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index a6862f513..0a0d155f9 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -294,7 +294,7 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
     {
       Trace("bound-int-lemma")
           << "*** bound int : proxy lemma : " << prangeLem << std::endl;
-      d_quantEngine->addLemma(prangeLem);
+      d_qim.addPendingLemma(prangeLem);
       addedLemma = true;
     }
   }
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 618a72047..428c435df 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -70,7 +70,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
 {
   bool doCheck = false;
   if( options::mbqiInterleave() ){
-    doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+    doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
   }
   if( !doCheck ){
     doCheck = quant_e == QEFFORT_MODEL;
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index f22e67815..1b011481b 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -77,7 +77,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
     if (options::fullSaturateInterleave())
     {
       // we only add when interleaved with other strategies
-      doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+      doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
     }
     if (options::fullSaturateQuant() && !doCheck)
     {
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 49f1fe116..4db53c4b7 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -38,9 +38,11 @@ namespace quantifiers {
 
 Instantiate::Instantiate(QuantifiersEngine* qe,
                          QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim,
                          ProofNodeManager* pnm)
     : d_qe(qe),
       d_qstate(qs),
+      d_qim(qim),
       d_pnm(pnm),
       d_term_db(nullptr),
       d_term_util(nullptr),
@@ -321,13 +323,12 @@ bool Instantiate::addInstantiation(
   bool addedLem = false;
   if (hasProof)
   {
-    // use trust interface
-    TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get());
-    addedLem = d_qe->addTrustedLemma(tlem, true, false);
+    // use proof generator
+    addedLem = d_qim.addPendingLemma(lem, LemmaProperty::NONE, d_pfInst.get());
   }
   else
   {
-    addedLem = d_qe->addLemma(lem, true, false);
+    addedLem = d_qim.addPendingLemma(lem);
   }
 
   if (!addedLem)
@@ -400,18 +401,6 @@ bool Instantiate::addInstantiation(
   return true;
 }
 
-bool Instantiate::removeInstantiation(Node q,
-                                      Node lem,
-                                      std::vector<Node>& terms)
-{
-  // lem must occur in d_waiting_lemmas
-  if (d_qe->removeLemma(lem))
-  {
-    return removeInstantiationInternal(q, terms);
-  }
-  return false;
-}
-
 bool Instantiate::recordInstantiation(Node q,
                                       std::vector<Node>& terms,
                                       bool modEq,
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index bbb1a0a44..154cda681 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -78,7 +78,7 @@ class InstantiationRewriter
  *
  * Its main interface is ::addInstantiation(...), which is called by many of
  * the quantifiers modules, which enqueues instantiation lemmas in quantifiers
- * engine via calls to QuantifiersEngine::addLemma.
+ * engine via calls to QuantifiersInferenceManager::addPendingLemma.
  *
  * It also has utilities for constructing instantiations, and interfaces for
  * getting the results of the instantiations produced during check-sat calls.
@@ -90,6 +90,7 @@ class Instantiate : public QuantifiersUtil
  public:
   Instantiate(QuantifiersEngine* qe,
               QuantifiersState& qs,
+              QuantifiersInferenceManager& qim,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -117,7 +118,7 @@ class Instantiate : public QuantifiersUtil
    *
    * This function returns true if the instantiation lemma for quantified
    * formula q for the substitution specified by m is successfully enqueued
-   * via a call to QuantifiersEngine::addLemma.
+   * via a call to QuantifiersInferenceManager::addPendingLemma.
    *   mkRep : whether to take the representatives of the terms in the range of
    *           the substitution m,
    *   modEq : whether to check for duplication modulo equality in instantiation
@@ -326,6 +327,8 @@ class Instantiate : public QuantifiersUtil
   QuantifiersEngine* d_qe;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** cache of term database for quantifiers engine */
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 5ffe4426a..086d492f4 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -249,7 +249,7 @@ private:  //for equivalence classes
    *
    * This method attempts to construct a conflicting or propagating instance.
    * If such an instance exists, then it makes a call to
-   * Instantiation::addInstantiation or QuantifiersEngine::addLemma.
+   * Instantiation::addInstantiation.
    */
   void check(Theory::Effort level, QEffort quant_e) override;
 
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index a1dc5acf3..f782ae7ef 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -198,7 +198,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
   for (const Node& lem : lemmas)
   {
     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
-    d_quantEngine->addLemma(lem, false);
+    d_qim.addPendingLemma(lem);
   }
   Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
 }
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 9037e94fa..551143e40 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -185,10 +185,10 @@ public:
   QuantifiersUtil(){}
   virtual ~QuantifiersUtil(){}
   /* reset
-  * Called at the beginning of an instantiation round
-  * Returns false if the reset failed. When reset fails, the utility should have
-  * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163
-  */
+   * Called at the beginning of an instantiation round
+   * Returns false if the reset failed. When reset fails, the utility should
+   * have added a lemma via a call to d_qim.addPendingLemma.
+   */
   virtual bool reset( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
   virtual void registerQuantifier(Node q) = 0;
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index f456dd407..652c42839 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -26,6 +26,12 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
 
 QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
 
+void QuantifiersInferenceManager::doPending()
+{
+  doPendingLemmas();
+  doPendingPhaseRequirements();
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index f89606d75..afdcfbdeb 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -34,6 +34,10 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
                               QuantifiersState& state,
                               ProofNodeManager* pnm);
   ~QuantifiersInferenceManager();
+  /**
+   * Do all pending lemmas, then do all pending phase requirements.
+   */
+  void doPending();
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index c1333b85f..7bae92184 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -42,9 +42,11 @@ namespace quantifiers {
 
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
+                                 QuantifiersInferenceManager& qim,
                                  SygusStatistics& s)
     : d_qe(qe),
       d_qstate(qs),
+      d_qim(qim),
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
@@ -721,7 +723,7 @@ bool SynthConjecture::doRefine()
   {
     Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem
                          << std::endl;
-    bool res = d_qe->addLemma(lem);
+    bool res = d_qim.addPendingLemma(lem);
     if (res)
     {
       ++(d_stats.d_cegqi_lemmas_refine);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 1d43e30ff..ca3f2983b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -84,6 +84,7 @@ class SynthConjecture
  public:
   SynthConjecture(QuantifiersEngine* qe,
                   QuantifiersState& qs,
+                  QuantifiersInferenceManager& qim,
                   SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
@@ -203,6 +204,8 @@ class SynthConjecture
   QuantifiersEngine* d_qe;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 869d22737..c12f387bc 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -39,7 +39,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe,
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, qs, d_statistics)));
+      new SynthConjecture(d_quantEngine, qs, qim, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -160,7 +160,7 @@ void SynthEngine::assignConjecture(Node q)
   if (d_conjs.back()->isAssigned())
   {
     d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-        new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
+        new SynthConjecture(d_quantEngine, d_qstate, d_qim, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
@@ -224,7 +224,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
-      if (d_quantEngine->addLemma(lem))
+      if (d_qim.addPendingLemma(lem))
       {
         ++(d_statistics.d_cegqi_lemmas_ce);
         addedLemma = true;
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 69836feba..f6827d1c4 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -309,7 +309,7 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
   for (const Node& lem : lemmas)
   {
     Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
-    added_lemma |= d_quantEngine->addLemma(lem);
+    added_lemma |= d_qim.addPendingLemma(lem);
   }
   return added_lemma;
 }
@@ -511,7 +511,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
   d_var_eval.emplace(q, evals);
 
   Node lit = getCeLiteral(q);
-  d_quantEngine->addRequirePhase(lit, true);
+  d_qim.addPendingPhaseRequirement(lit, true);
 
   /* The decision strategy for quantified formula 'q' ensures that its
    * counterexample literal is decided on first. It is user-context dependent.
@@ -545,7 +545,7 @@ void SygusInst::addCeLemma(Node q)
   if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
 
   Node lem = d_ce_lemmas[q];
-  d_quantEngine->addLemma(lem, false);
+  d_qim.addPendingLemma(lem);
   d_ce_lemma_added.insert(q);
   Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 1498c29b7..56f85e99e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -405,7 +405,7 @@ void TermDb::computeUfTerms( TNode f ) {
             }
             Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
           }
-          d_quantEngine->addLemma(lem);
+          d_qim.addPendingLemma(lem);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return;
@@ -1015,7 +1015,7 @@ bool TermDb::reset( Theory::Effort effort ){
           // equality is sent out as a lemma here.
           Trace("term-db-lemma")
               << "Purify equality lemma: " << eq << std::endl;
-          d_quantEngine->addLemma(eq);
+          d_qim.addPendingLemma(eq);
           d_qstate.notifyInConflict();
           d_consistent_ee = false;
           return false;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0e28cab76..bdc12cdaa 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -49,12 +49,11 @@ QuantifiersEngine::QuantifiersEngine(
       d_eq_query(nullptr),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes),
-      d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
+      d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)),
       d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
       d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext()),
-      d_lemmas_produced_c(qstate.getUserContext()),
       d_ierCounter_c(qstate.getSatContext()),
       d_presolve(qstate.getUserContext(), true),
       d_presolve_in(qstate.getUserContext()),
@@ -73,10 +72,6 @@ QuantifiersEngine::QuantifiersEngine(
 
   d_util.push_back(d_instantiate.get());
 
-  d_hasAddedLemma = false;
-  //don't add true lemma
-  d_lemmas_produced_c[d_term_util->d_true] = true;
-
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
@@ -261,8 +256,7 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
-  d_lemmas_waiting.clear();
-  d_phase_req_waiting.clear();
+  d_qim.clearPending();
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
@@ -342,7 +336,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     // proceed with the check.
     Assert(false);
   }
-  bool needsCheck = !d_lemmas_waiting.empty();
+  bool needsCheck = d_qim.hasPendingLemma();
   QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
@@ -362,14 +356,15 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
   }
 
-  d_hasAddedLemma = false;
+  d_qim.reset();
   bool setIncomplete = false;
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
     //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
-    flushLemmas();
-    if( d_hasAddedLemma ){
+    d_qim.doPending();
+    if (d_qim.hasSentLemma())
+    {
       return;
     }
 
@@ -388,8 +383,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       Trace("quant-engine-debug") << std::endl;
       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
-      if( !d_lemmas_waiting.empty() ){
-        Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+      if (d_qim.hasPendingLemma())
+      {
+        Trace("quant-engine-debug")
+            << "  lemmas waiting = " << d_qim.numPendingLemmas() << std::endl;
       }
       Trace("quant-engine-debug")
           << "  Theory engine finished : "
@@ -415,8 +412,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
                                    << "..." << std::endl;
       if (!util->reset(e))
       {
-        flushLemmas();
-        if( d_hasAddedLemma ){
+        d_qim.doPending();
+        if (d_qim.hasSentLemma())
+        {
           return;
         }else{
           //should only fail reset if added a lemma
@@ -444,8 +442,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
     //reset may have added lemmas
-    flushLemmas();
-    if( d_hasAddedLemma ){
+    d_qim.doPending();
+    if (d_qim.hasSentLemma())
+    {
       return;
     }
 
@@ -469,11 +468,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
         {
           // If we failed to build the model, flush all pending lemmas and
           // finish.
-          flushLemmas();
+          d_qim.doPending();
           break;
         }
       }
-      if( !d_hasAddedLemma ){
+      if (!d_qim.hasSentLemma())
+      {
         //check each module
         for (QuantifiersModule*& mdl : qm)
         {
@@ -488,10 +488,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
           }
         }
         //flush all current lemmas
-        flushLemmas();
+        d_qim.doPending();
       }
       //if we have added one, stop
-      if( d_hasAddedLemma ){
+      if (d_qim.hasSentLemma())
+      {
         break;
       }else{
         Assert(!d_qstate.isInConflict());
@@ -580,7 +581,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
     // debug print
-    if (d_hasAddedLemma)
+    if (d_qim.hasSentLemma())
     {
       bool debugInstTrace = Trace.isOn("inst-per-quant-round");
       if (options::debugInst() || debugInstTrace)
@@ -593,7 +594,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     if( Trace.isOn("quant-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
       Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
-      Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
+      Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma();
       Trace("quant-engine") << std::endl;
     }
 
@@ -603,7 +604,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 
   //SAT case
-  if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+  if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma())
+  {
     if( setIncomplete ){
       Trace("quant-engine") << "Set incomplete flag." << std::endl;
       getOutputChannel().setIncomplete();
@@ -656,7 +658,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f)
   if( it==d_quants.end() ){
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
     Trace("quant") << " : " << f << std::endl;
-    unsigned prev_lemma_waiting = d_lemmas_waiting.size();
+    size_t prev_lemma_waiting = d_qim.numPendingLemmas();
     ++(d_statistics.d_num_quant);
     Assert(f.getKind() == FORALL);
     // register with utilities
@@ -684,11 +686,11 @@ void QuantifiersEngine::registerQuantifierInternal(Node f)
       mdl->registerQuantifier(f);
       // since this is context-independent, we should not add any lemmas during
       // this call
-      Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
+      Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
     }
     Trace("quant-debug") << "...finish." << std::endl;
     d_quants[f] = true;
-    AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
+    AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
   }
 }
 
@@ -717,7 +719,7 @@ void QuantifiersEngine::preRegisterQuantifier(Node q)
     mdl->preRegisterQuantifier(q);
   }
   // flush the lemmas
-  flushLemmas();
+  d_qim.doPending();
   Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
 }
 
@@ -780,66 +782,10 @@ void QuantifiersEngine::eqNotifyNewClass(TNode t) {
   addTermToDatabase( t );
 }
 
-bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
-  if( doCache ){
-    if( doRewrite ){
-      lem = Rewriter::rewrite(lem);
-    }
-    Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
-    BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
-    if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
-      d_lemmas_produced_c[ lem ] = true;
-      d_lemmas_waiting.push_back( lem );
-      Trace("inst-add-debug") << "Added lemma" << std::endl;
-      return true;
-    }else{
-      Trace("inst-add-debug") << "Duplicate." << std::endl;
-      return false;
-    }
-  }else{
-    //do not need to rewrite, will be rewritten after sending
-    d_lemmas_waiting.push_back( lem );
-    return true;
-  }
-}
-
-bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
-                                        bool doCache,
-                                        bool doRewrite)
-{
-  Node lem = tlem.getProven();
-  if (!addLemma(lem, doCache, doRewrite))
-  {
-    return false;
-  }
-  d_lemmasWaitingPg[lem] = tlem.getGenerator();
-  return true;
-}
-
-bool QuantifiersEngine::removeLemma( Node lem ) {
-  std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
-  if( it!=d_lemmas_waiting.end() ){
-    d_lemmas_waiting.erase( it, it + 1 );
-    d_lemmas_produced_c[ lem ] = false;
-    return true;
-  }else{
-    return false;
-  }
-}
-
-void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
-  d_phase_req_waiting[lit] = req;
-}
-
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
 
-bool QuantifiersEngine::hasAddedLemma() const
-{
-  return !d_lemmas_waiting.empty() || d_hasAddedLemma;
-}
-
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
@@ -889,41 +835,6 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode()
   }
 }
 
-void QuantifiersEngine::flushLemmas(){
-  OutputChannel& out = getOutputChannel();
-  if( !d_lemmas_waiting.empty() ){
-    //take default output channel if none is provided
-    d_hasAddedLemma = true;
-    std::map<Node, ProofGenerator*>::iterator itp;
-    // Note: Do not use foreach loop here and do not cache size() call.
-    // New lemmas can be added while iterating over d_lemmas_waiting.
-    for (size_t i = 0; i < d_lemmas_waiting.size(); ++i)
-    {
-      const Node& lemw = d_lemmas_waiting[i];
-      Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
-      itp = d_lemmasWaitingPg.find(lemw);
-      LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY;
-      if (itp != d_lemmasWaitingPg.end())
-      {
-        TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
-        out.trustedLemma(tlemw, p);
-      }
-      else
-      {
-        out.lemma(lemw, p);
-      }
-    }
-    d_lemmas_waiting.clear();
-  }
-  if( !d_phase_req_waiting.empty() ){
-    for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
-      Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
-      out.requirePhase(it->first, it->second);
-    }
-    d_phase_req_waiting.clear();
-  }
-}
-
 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
   d_instantiate->getInstantiationTermVectors(q, tvecs);
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 83e01e9e6..cab452e2b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -173,36 +173,11 @@ private:
  void registerQuantifierInternal(Node q);
  /** reduceQuantifier, return true if reduced */
  bool reduceQuantifier(Node q);
- /** flush lemmas */
- void flushLemmas();
 
 public:
- /**
-  * Add lemma to the lemma buffer of this quantifiers engine.
-  * @param lem The lemma to send
-  * @param doCache Whether to cache the lemma (to check for duplicate lemmas)
-  * @param doRewrite Whether to rewrite the lemma
-  * @return true if the lemma was successfully added to the buffer
-  */
- bool addLemma(Node lem, bool doCache = true, bool doRewrite = true);
- /**
-  * Add trusted lemma lem, same as above, but where a proof generator may be
-  * provided along with the lemma.
-  */
- bool addTrustedLemma(TrustNode tlem,
-                      bool doCache = true,
-                      bool doRewrite = true);
- /** remove pending lemma */
- bool removeLemma(Node lem);
- /** add require phase */
- void addRequirePhase(Node lit, bool req);
  /** mark relevant quantified formula, this will indicate it should be checked
   * before the others */
  void markRelevant(Node q);
- /** has added lemma */
- bool hasAddedLemma() const;
- /** get number of waiting lemmas */
- unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
  /** get needs check */
  bool getInstWhenNeedsCheck(Theory::Effort e);
  /** get user pat mode */
@@ -345,9 +320,6 @@ public:
    * The modules utility, which contains all of the quantifiers modules.
    */
   std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
-  //------------- temporary information during check
-  /** has added lemma this round */
-  bool d_hasAddedLemma;
   //------------- end temporary information during check
  private:
   /** list of all quantifiers seen */
@@ -357,15 +329,6 @@ public:
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map<Node, Node> d_quants_red_lem;
-  /** list of all lemmas produced */
-  // std::map< Node, bool > d_lemmas_produced;
-  BoolMap d_lemmas_produced_c;
-  /** lemmas waiting */
-  std::vector<Node> d_lemmas_waiting;
-  /** map from waiting lemmas to their proof generators */
-  std::map<Node, ProofGenerator*> d_lemmasWaitingPg;
-  /** phase requirements waiting */
-  std::map<Node, bool> d_phase_req_waiting;
   /** inst round counters TODO: make context-dependent? */
   context::CDO<int> d_ierCounter_c;
   int d_ierCounter;
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index ebd68a982..58a8b86a4 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -36,6 +36,9 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
       d_numCurrentLemmas(0),
       d_numCurrentFacts(0)
 {
+  // don't add true lemma
+  Node truen = NodeManager::currentNM()->mkConst(true);
+  d_lemmasSent.insert(truen);
 }
 
 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)