(new theory) Update TheoryDatatypes to the new standard (#4986)

Updates it to use the new inference manager as well as updating its check to the standard callbacks.

4 files changed, 133 insertions, 304 deletions

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 3dc16355b..762cdfd8b 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -108,6 +108,19 @@ void InferenceManager::process()
   doPendingFacts();
 }
 
+bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
+{
+  bool ret = false;
+  for (const Node& lem : lemmas)
+  {
+    if (lemma(lem))
+    {
+      ret = true;
+    }
+  }
+  return ret;
+}
+
 }  // namespace datatypes
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 0dda3259e..0dfdfb281 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -81,6 +81,11 @@ class InferenceManager : public InferenceManagerBuffered
    * or processed internally.
    */
   void process();
+  /**
+   * Send lemmas with property NONE on the output channel immediately.
+   * Returns true if any lemma was sent.
+   */
+  bool sendLemmas(const std::vector<Node>& lemmas);
 };
 
 }  // namespace datatypes
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4c8fa87ba..78b6d81c2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -47,22 +47,18 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
                                  const LogicInfo& logicInfo,
                                  ProofNodeManager* pnm)
     : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
-      d_infer(c),
-      d_infer_exp(c),
       d_term_sk(u),
       d_notify(*this),
       d_labels(c),
       d_selector_apps(c),
-      d_conflict(c, false),
-      d_addedLemma(false),
-      d_addedFact(false),
       d_collectTermsCache(c),
       d_collectTermsCacheU(u),
       d_functionTerms(c),
       d_singleton_eq(u),
       d_lemmas_produced_c(u),
       d_sygusExtension(nullptr),
-      d_state(c, u, valuation)
+      d_state(c, u, valuation),
+      d_im(*this, d_state, pnm)
 {
 
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -71,6 +67,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
 
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
+  d_inferManager = &d_im;
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -156,64 +153,43 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
   }
 }
 
-void TheoryDatatypes::check(Effort e) {
-  if (done() && e<EFFORT_FULL) {
-    return;
-  }
-  Assert(d_pending.empty());
-  d_addedLemma = false;
-  
-  if( e == EFFORT_LAST_CALL ){
+bool TheoryDatatypes::preCheck(Effort level)
+{
+  d_im.reset();
+  return false;
+}
+
+void TheoryDatatypes::postCheck(Effort level)
+{
+  if (level == EFFORT_LAST_CALL)
+  {
     Assert(d_sygusExtension != nullptr);
-    std::vector< Node > lemmas;
+    std::vector<Node> lemmas;
     d_sygusExtension->check(lemmas);
-    doSendLemmas( lemmas );
+    d_im.sendLemmas(lemmas);
     return;
   }
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  Trace("datatypes-check") << "Check effort " << e << std::endl;
-  while(!done() && !d_conflict) {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.d_assertion;
-    Trace("datatypes-assert") << "Assert " << fact << std::endl;
-
-    TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
-
-    // extra debug check to make sure that the rewriter did its job correctly
-    Assert(atom.getKind() != kind::EQUAL
-           || (atom[0].getKind() != kind::TUPLE_UPDATE
-               && atom[1].getKind() != kind::TUPLE_UPDATE
-               && atom[0].getKind() != kind::RECORD_UPDATE
-               && atom[1].getKind() != kind::RECORD_UPDATE))
-        << "tuple/record escaped into datatypes decision procedure; should "
-           "have been rewritten away";
-
-    //assert the fact
-    assertFact( fact, fact );
-    flushPendingFacts();
-  }
-
-  if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) {
+  else if (level == EFFORT_FULL && !d_state.isInConflict()
+           && !d_im.hasAddedLemma() && !d_valuation.needCheck())
+  {
     //check for cycles
-    Assert(d_pending.empty());
+    Assert(!d_im.hasPendingFact());
     do {
-      d_addedFact = false;
+      d_im.reset();
       Trace("datatypes-proc") << "Check cycles..." << std::endl;
       checkCycles();
       Trace("datatypes-proc") << "...finish check cycles" << std::endl;
-      flushPendingFacts();
-      if( d_conflict || d_addedLemma ){
+      d_im.process();
+      if (d_state.isInConflict() || d_im.hasAddedLemma())
+      {
         return;
       }
-    }while( d_addedFact );
-  
+    } while (d_im.hasAddedFact());
+
     //check for splits
-    Trace("datatypes-debug") << "Check for splits " << e << endl;
+    Trace("datatypes-debug") << "Check for splits " << endl;
     do {
-      d_addedFact = false;
+      d_im.reset();
       std::map< TypeNode, Node > rec_singletons;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
       while( !eqcs_i.isFinished() ){
@@ -265,7 +241,7 @@ void TheoryDatatypes::check(Effort e) {
                     assumptions.push_back(assumption);
                     Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
                     Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
-                    doSendLemma( lemma );
+                    d_im.lemma(lemma);
                   }
                 }
               }else{
@@ -279,8 +255,6 @@ void TheoryDatatypes::check(Effort e) {
               //all other cases
               std::vector< bool > pcons;
               getPossibleCons( eqc, n, pcons );
-              //std::map< int, bool > sel_apps;
-              //getSelectorsForCons( n, sel_apps );
               //check if we do not need to resolve the constructor type for this equivalence class.
               // this is if there are no selectors for this equivalence class, and its possible values are infinite,
               //  then do not split.
@@ -322,10 +296,8 @@ void TheoryDatatypes::check(Effort e) {
                   //this may not be necessary?
                   //if only one constructor, then this term must be this constructor
                   Node t = utils::mkTester(n, 0, dt);
-                  d_pending.push_back( t );
-                  d_pending_exp[ t ] = d_true;
+                  d_im.addPendingInference(t, d_true);
                   Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
-                  d_infer.push_back( t );
                 }else{
                   Assert(consIndex != -1 || dt.isSygus());
                   if( options::dtBinarySplit() && consIndex!=-1 ){
@@ -335,14 +307,13 @@ void TheoryDatatypes::check(Effort e) {
                     NodeBuilder<> nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
-                    doSendLemma( lemma );
+                    d_im.lemma(lemma);
                     d_out->requirePhase( test, true );
                   }else{
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                     Node lemma = utils::mkSplit(n, dt);
                     Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                    d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
-                    d_addedLemma = true;
+                    d_im.lemma(lemma, LemmaProperty::SEND_ATOMS, false);
                   }
                   if( !options::dtBlastSplits() ){
                     break;
@@ -358,29 +329,32 @@ void TheoryDatatypes::check(Effort e) {
         }
         ++eqcs_i;
       }
-      if (d_addedLemma)
+      if (d_im.hasAddedLemma())
       {
         // clear pending facts: we added a lemma, so internal inferences are
         // no longer necessary
-        d_pending.clear();
-        d_pending_exp.clear();
+        d_im.clearPendingFacts();
       }
       else
       {
         // we did not add a lemma, process internal inferences. This loop
         // will repeat.
         Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
-        flushPendingFacts();
+        d_im.process();
       }
-    }while( !d_conflict && !d_addedLemma && d_addedFact );
-    Trace("datatypes-debug") << "Finished, conflict=" << d_conflict << ", lemmas=" << d_addedLemma << std::endl;
-    if( !d_conflict ){
+    } while (!d_state.isInConflict() && !d_im.hasAddedLemma()
+             && d_im.hasAddedFact());
+    Trace("datatypes-debug")
+        << "Finished, conflict=" << d_state.isInConflict()
+        << ", lemmas=" << d_im.hasAddedLemma() << std::endl;
+    if (!d_state.isInConflict())
+    {
       Trace("dt-model-debug") << std::endl;
       printModelDebug("dt-model-debug");
     }
   }
 
-  Trace("datatypes-check") << "Finished check effort " << e << std::endl;
+  Trace("datatypes-check") << "Finished check effort " << level << std::endl;
   if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
     Notice() << "TheoryDatatypes::check(): done" << endl;
   }
@@ -390,100 +364,17 @@ bool TheoryDatatypes::needsCheckLastEffort() {
   return d_sygusExtension != nullptr;
 }
 
-void TheoryDatatypes::flushPendingFacts(){
-  //pending lemmas: used infrequently, only for definitional lemmas
-  if( !d_pending_lem.empty() ){
-    int i = 0;
-    while( i<(int)d_pending_lem.size() ){
-      doSendLemma( d_pending_lem[i] );
-      i++;
-    }
-    d_pending_lem.clear();
-  }
-  int i = 0;
-  while( !d_conflict && i<(int)d_pending.size() ){
-    Node fact = d_pending[i];
-    Node exp = d_pending_exp[ fact ];
-    Trace("datatypes-debug") << "Assert fact (#" << (i+1) << "/" << d_pending.size() << ") " << fact << " with explanation " << exp << std::endl;
-    //check to see if we have to communicate it to the rest of the system
-    if( mustCommunicateFact( fact, exp ) ){
-      Node lem = fact;
-      if( exp.isNull() || exp==d_true ){
-        Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
-      }else{
-        Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
-        std::vector< TNode > assumptions;
-        //if( options::dtRExplainLemmas() ){
-        explain( exp, assumptions );
-        //}else{
-        //  ee_exp = exp;
-        //}
-        //Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
-        if( assumptions.empty() ){
-          lem = fact;
-        }else{
-          std::vector< Node > children;
-          for (const TNode& assumption : assumptions)
-          {
-            children.push_back(assumption.negate());
-          }
-          children.push_back( fact );
-          lem = NodeManager::currentNM()->mkNode( OR, children );
-        }
-      }
-      Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
-      doSendLemma( lem );
-    }else{
-      assertFact( fact, exp );
-      d_addedFact = true;
-    }
-    Trace("datatypes-debug") << "Finished fact " << fact << ", now = " << d_conflict << " " << d_pending.size() << std::endl;
-    i++;
-  }
-  d_pending.clear();
-  d_pending_exp.clear();
-}
-
-bool TheoryDatatypes::doSendLemma( Node lem ) {
-  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
-    Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : " << lem << std::endl;
-    d_lemmas_produced_c[lem] = true;
-    d_out->lemma( lem );
-    d_addedLemma = true;
-    return true;
-  }else{
-    Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : duplicate : "
-                           << lem << std::endl;
-    return false;
-  }
-}
-bool TheoryDatatypes::doSendLemmas( std::vector< Node >& lemmas ){
-  bool ret = false;
-  for (const Node& lem : lemmas)
-  {
-    bool cret = doSendLemma(lem);
-    ret = ret || cret;
-  }
-  lemmas.clear();
-  return ret;
-}
-        
-void TheoryDatatypes::assertFact( Node fact, Node exp)
+void TheoryDatatypes::notifyFact(TNode atom,
+                                 bool polarity,
+                                 TNode fact,
+                                 bool isInternal)
 {
-  Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact << std::endl;
-  bool polarity = fact.getKind() != kind::NOT;
-  TNode atom = polarity ? fact : fact[0];
-  if (atom.getKind() == kind::EQUAL) {
-    d_equalityEngine->assertEquality(atom, polarity, exp);
-  }else{
-    d_equalityEngine->assertPredicate(atom, polarity, exp);
-  }
   // could be sygus-specific
   if (d_sygusExtension)
   {
     std::vector< Node > lemmas;
     d_sygusExtension->assertFact(atom, polarity, lemmas);
-    doSendLemmas( lemmas );
+    d_im.sendLemmas(lemmas);
   }
   //add to tester if applicable
   Node t_arg;
@@ -493,28 +384,37 @@ void TheoryDatatypes::assertFact( Node fact, Node exp)
     Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
     Node rep = getRepresentative( t_arg );
     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-    addTester( tindex, fact, eqc, rep, t_arg );
+    Node tst =
+        isInternal ? (polarity ? Node(atom) : atom.notNode()) : Node(fact);
+    addTester(tindex, tst, eqc, rep, t_arg);
     Trace("dt-tester") << "Done assert tester." << std::endl;
     Trace("dt-tester") << "Done pending merges." << std::endl;
-    if( !d_conflict && polarity ){
+    if (!d_state.isInConflict() && polarity)
+    {
       if (d_sygusExtension)
       {
         Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
-        //Assert( !d_sygus_util->d_conflict );
         std::vector< Node > lemmas;
         d_sygusExtension->assertTester(tindex, t_arg, atom, lemmas);
         Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
-        doSendLemmas( lemmas );
+        d_im.sendLemmas(lemmas);
       }
     }
   }else{
     Trace("dt-tester-debug") << "Assert (non-tester) : " << atom << std::endl;
   }
   Trace("datatypes-debug") << "TheoryDatatypes::assertFact : finished " << fact << std::endl;
+  // now, flush pending facts if this wasn't an internal call
+  if (!isInternal)
+  {
+    d_im.process();
+  }
 }
 
-void TheoryDatatypes::preRegisterTerm(TNode n) {
-  Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+void TheoryDatatypes::preRegisterTerm(TNode n)
+{
+  Debug("datatypes-prereg")
+      << "TheoryDatatypes::preRegisterTerm() " << n << endl;
   collectTerms( n );
   switch (n.getKind()) {
   case kind::EQUAL:
@@ -530,12 +430,11 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
     {
       std::vector< Node > lemmas;
       d_sygusExtension->preRegisterTerm(n, lemmas);
-      doSendLemmas( lemmas );
+      d_im.sendLemmas(lemmas);
     }
-    // d_equalityEngine->addTriggerTerm(n, THEORY_DATATYPES);
     break;
   }
-  flushPendingFacts();
+  d_im.process();
 }
 
 TrustNode TheoryDatatypes::expandDefinition(Node n)
@@ -699,21 +598,13 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in)
   return TrustNode::null();
 }
 
-void TheoryDatatypes::notifySharedTerm(TNode t)
-{
-  Debug("datatypes") << "TheoryDatatypes::notifySharedTerm(): " << t << " "
-                     << t.getType().isBoolean() << endl;
-  d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES);
-  Debug("datatypes") << "TheoryDatatypes::notifySharedTerm() finished"
-                     << std::endl;
-}
-
 bool TheoryDatatypes::propagateLit(TNode literal)
 {
   Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")"
                          << std::endl;
   // If already in conflict, no more propagation
-  if (d_conflict) {
+  if (d_state.isInConflict())
+  {
     Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal
                            << "): already in conflict" << std::endl;
     return false;
@@ -723,7 +614,7 @@ bool TheoryDatatypes::propagateLit(TNode literal)
   bool ok = d_out->propagate(literal);
   if (!ok) {
     Trace("dt-conflict") << "CONFLICT: Eq engine propagate conflict " << std::endl;
-    d_conflict = true;
+    d_state.notifyInConflict();
   }
   return ok;
 }
@@ -805,7 +696,7 @@ void TheoryDatatypes::conflict(TNode a, TNode b){
   d_conflictNode = explainLit(eq);
   Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
   d_out->conflict( d_conflictNode );
-  d_conflict = true;
+  d_state.notifyInConflict();
 }
 
 /** called when a new equivalance class is created */
@@ -826,7 +717,8 @@ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
 }
 
 void TheoryDatatypes::merge( Node t1, Node t2 ){
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     TNode trep1 = t1;
     TNode trep2 = t2;
     Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
@@ -855,7 +747,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             d_conflictNode = explainLit(unifEq);
             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
-            d_conflict = true;
+            d_state.notifyInConflict();
             return;
           }
           else
@@ -864,22 +756,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( !areEqual( cons1[i], cons2[i] ) ){
                 Node eq = cons1[i].eqNode( cons2[i] );
-                d_pending.push_back( eq );
-                d_pending_exp[ eq ] = unifEq;
+                d_im.addPendingInference(eq, unifEq);
                 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
-                d_infer.push_back( eq );
-                d_infer_exp.push_back( unifEq );
               }
             }
-/*
-            for( unsigned i=0; i<rew.size(); i++ ){
-              d_pending.push_back( rew[i] );
-              d_pending_exp[ rew[i] ] = unifEq;
-              Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
-              d_infer.push_back( rew[i] );
-              d_infer_exp.push_back( unifEq );
-            }
-*/
           }
         }
         Trace("datatypes-debug") << "  instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
@@ -889,7 +769,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             Trace("datatypes-debug") << "  must check if it is okay to set the constructor." << std::endl;
             checkInst = true;
             addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
-            if( d_conflict ){
+            if (d_state.isInConflict())
+            {
               return;
             }
           }
@@ -916,7 +797,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           Node t_arg = d_labels_args[t2][i];
           unsigned tindex = d_labels_tindex[t2][i];
           addTester( tindex, t, eqc1, t1, t_arg );
-          if( d_conflict ){
+          if (d_state.isInConflict())
+          {
             Trace("datatypes-debug") << "  conflict!" << std::endl;
             return;
           }
@@ -940,7 +822,8 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       if( checkInst ){
         Trace("datatypes-debug") << "  checking instantiate" << std::endl;
         instantiate( eqc1, t1 );
-        if( d_conflict ){
+        if (d_state.isInConflict())
+        {
           return;
         }
       }
@@ -979,6 +862,8 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
       return -1;
     }else{
       int tindex = utils::isTester(lbl);
+      Trace("datatypes-debug") << "Label of " << n << " is " << lbl
+                               << " with tindex " << tindex << std::endl;
       Assert(tindex != -1);
       return tindex;
     }
@@ -1033,9 +918,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
       d_term_sk[n] = k;
       Node eq = k.eqNode( n );
       Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
-      d_pending_lem.push_back( eq );
-      //doSendLemma( eq );
-      //d_pending_exp[ eq ] = d_true;
+      d_im.addPendingLemma(eq);
       return k;
     }else{
       return (*it).second;
@@ -1051,6 +934,7 @@ void TheoryDatatypes::addTester(
   Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
   Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
   bool tpolarity = t.getKind()!=NOT;
+  Assert((tpolarity ? t : t[0]).getKind() == APPLY_TESTER);
   Node j, jt;
   bool makeConflict = false;
   int prevTIndex = getLabelIndex(eqc, n);
@@ -1068,7 +952,7 @@ void TheoryDatatypes::addTester(
         d_conflictNode = mkAnd( assumptions );
         Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
         d_out->conflict( d_conflictNode );
-        d_conflict = true;
+        d_state.notifyInConflict();
         return;
       }else{
         makeConflict = true;
@@ -1122,16 +1006,8 @@ void TheoryDatatypes::addTester(
       Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
       if( tpolarity ){
         instantiate( eqc, n );
-        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
-        {
-          if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){
-            Assert(n.getKind() != APPLY_CONSTRUCTOR);
-            Node infer = utils::mkTester(n, i, dt).negate();
-            Trace("datatypes-infer") << "DtInfer : neg label : " << infer << " by " << t << std::endl;
-            d_infer.push_back( infer );
-            d_infer_exp.push_back( t );
-          }
-        }
+        // We could propagate is-C1(x) => not is-C2(x) here for all other
+        // constructors, but empirically this hurts performance.
       }else{
         //check if we have reached the maximum number of testers
         // in this case, add the positive tester
@@ -1167,18 +1043,15 @@ void TheoryDatatypes::addTester(
                              ? NodeManager::currentNM()->mkConst(false)
                              : utils::mkTester(t_arg, testerIndex, dt);
           Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
-          d_pending.push_back( t_concl );
-          d_pending_exp[ t_concl ] = t_concl_exp;
+          d_im.addPendingInference(t_concl, t_concl_exp);
           Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
-          d_infer.push_back( t_concl );
-          d_infer_exp.push_back( t_concl_exp );
           return;
         }
       }
     }
   }
   if( makeConflict ){
-    d_conflict = true;
+    d_state.notifyInConflict();
     Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
     std::vector< TNode > assumptions;
     explain( j, assumptions );
@@ -1245,7 +1118,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
           d_conflictNode = mkAnd( assumptions );
           Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
           d_out->conflict( d_conflictNode );
-          d_conflict = true;
+          d_state.notifyInConflict();
           return;
         }
       }
@@ -1332,10 +1205,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
       Trace("datatypes-infer") << "DtInfer : collapse sel";
       //Trace("datatypes-infer") << ( wrong ? " wrong" : "");
       Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl;
-      d_pending.push_back( eq );
-      d_pending_exp[eq] = peq;
-      d_infer.push_back( eq );
-      d_infer_exp.push_back(peq);
+      d_im.addPendingInference(eq, peq);
     }
   }
 }
@@ -1486,7 +1356,7 @@ void TheoryDatatypes::computeCareGraph(){
 bool TheoryDatatypes::collectModelValues(TheoryModel* m,
                                          const std::set<Node>& termSet)
 {
-  Trace("dt-cmi") << "Datatypes : Collect model info "
+  Trace("dt-cmi") << "Datatypes : Collect model values "
                   << d_equalityEngine->consistent() << std::endl;
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
@@ -1639,7 +1509,7 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
       Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
       a = v1.eqNode( v2 ).negate();
       //send out immediately as lemma
-      doSendLemma( a );
+      d_im.lemma(a);
       Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
     }
     d_singleton_lemma[index][tn] = a;
@@ -1697,7 +1567,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
     Node lem = nm->mkNode(LEQ, d_zero, n);
     Trace("datatypes-infer")
         << "DtInfer : size geq zero : " << lem << std::endl;
-    d_pending_lem.push_back(lem);
+    d_im.addPendingLemma(lem);
   }
   else if (nk == DT_HEIGHT_BOUND && n[1].getConst<Rational>().isZero())
   {
@@ -1722,7 +1592,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
                                           : nm->mkNode(OR, children));
     }
     Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
-    d_pending_lem.push_back(lem);
+    d_im.addPendingLemma(lem);
   }
 }
 
@@ -1751,6 +1621,7 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
 }
 
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
+  Trace("datatypes-debug") << "Instantiate: " << n << std::endl;
   //add constructor to equivalence class if not done so already
   int index = getLabelIndex( eqc, n );
   if (index == -1 || eqc->d_inst)
@@ -1781,13 +1652,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   eq = tt.eqNode(tt_cons);
   Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq
                           << std::endl;
-  d_pending.push_back(eq);
-  d_pending_exp[eq] = exp;
+  d_im.addPendingInference(eq, exp);
   Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
   Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
                            << std::endl;
-  d_infer.push_back(eq);
-  d_infer_exp.push_back(exp);
 }
 
 void TheoryDatatypes::checkCycles() {
@@ -1822,7 +1690,7 @@ void TheoryDatatypes::checkCycles() {
             d_conflictNode = mkAnd( expl );
             Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
-            d_conflict = true;
+            d_state.notifyInConflict();
             return;
           }
         }
@@ -1872,11 +1740,8 @@ void TheoryDatatypes::checkCycles() {
           Trace("dt-cdt") << std::endl;
           Node eq = part_out[i][0].eqNode( part_out[i][j] );
           Node eqExp = mkAnd( exp );
-          d_pending.push_back( eq );
-          d_pending_exp[ eq ] = eqExp;
+          d_im.addPendingInference(eq, eqExp);
           Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
-          d_infer.push_back( eq );
-          d_infer_exp.push_back( eqExp );
         }
       }
     }
@@ -2051,39 +1916,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
   }
 }
 
-bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
-  //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
-  //  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
-  //  (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
-  //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
-  //  (4) collapse selector : S( C( t1...tn ) ) = t'
-  //  (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn )
-  //  (6) non-negative size : 0 <= size( t )
-  //We may need to communicate outwards if the conclusions involve other theories.  Also communicate (6) and OR conclusions.
-  Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
-  bool addLemma = false;
-  if( options::dtInferAsLemmas() && exp!=d_true ){
-    addLemma = true;    
-  }else if( n.getKind()==EQUAL ){
-    TypeNode tn = n[0].getType();
-    if( !tn.isDatatype() ){
-      addLemma = true;
-    }else{
-      const DType& dt = tn.getDType();
-      addLemma = dt.involvesExternalType();
-    }
-  }else if( n.getKind()==LEQ || n.getKind()==OR ){
-    addLemma = true;
-  }
-  if( addLemma ){
-    Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
-    return true;
-  }else{
-    Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
-    return false;
-  }
-}
-
 bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); }
 
 bool TheoryDatatypes::areEqual( TNode a, TNode b ){
@@ -2250,8 +2082,6 @@ void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet)
     }
     ++eqcs_i;
   }
-  Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size()
-                  << " relevant terms..." << std::endl;
 }
 
 std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 211653125..37a4f81f7 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -26,6 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/inference_manager.h"
 #include "theory/datatypes/sygus_extension.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -43,9 +44,6 @@ class TheoryDatatypes : public Theory {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
-  /** inferences */
-  NodeList d_infer;
-  NodeList d_infer_exp;
   Node d_true;
   Node d_zero;
   /** mkAnd */
@@ -70,6 +68,7 @@ class TheoryDatatypes : public Theory {
                                      TNode t2,
                                      bool value) override
     {
+      AlwaysAssert(tag == THEORY_DATATYPES);
       Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_dt.propagateLit(t1.eqNode(t2));
@@ -169,20 +168,6 @@ private:
   /** selector apps for eqch equivalence class */
   NodeUIntMap d_selector_apps;
   std::map< Node, std::vector< Node > > d_selector_apps_data;
-  /** Are we in conflict */
-  context::CDO<bool> d_conflict;
-  /** added lemma
-   *
-   * This flag is set to true during a full effort check if this theory
-   * called d_out->lemma(...).
-   */
-  bool d_addedLemma;
-  /** 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;
   /** The conflict node */
   Node d_conflictNode;
   /**
@@ -195,10 +180,6 @@ private:
    * collectTerms(...) on.
    */
   BoolMap d_collectTermsCacheU;
-  /** pending assertions/merges */
-  std::vector< Node > d_pending_lem;
-  std::vector< Node > d_pending;
-  std::map< Node, Node > d_pending_exp;
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionTerms;
   /** counter for forcing assignments (ensures fairness) */
@@ -218,12 +199,6 @@ private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
 
-  /** flush pending facts */
-  void flushPendingFacts();
-
-  /** do send lemma */
-  bool doSendLemma( Node lem );
-  bool doSendLemmas( std::vector< Node >& lem );
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 
@@ -263,9 +238,10 @@ private:
   /** finish initialization */
   void finishInit() override;
   //--------------------------------- end initialization
-
   /** propagate */
   bool propagateLit(TNode literal);
+  /** Conflict when merging two constants */
+  void conflict(TNode a, TNode b);
   /** explain */
   void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
   void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
@@ -274,23 +250,25 @@ private:
   TrustNode explain(TNode literal) override;
   Node explainLit(TNode literal);
   Node explain( std::vector< Node >& lits );
-  /** Conflict when merging two constants */
-  void conflict(TNode a, TNode b);
   /** called when a new equivalance class is created */
   void eqNotifyNewClass(TNode t);
   /** called when two equivalance classes have merged */
   void eqNotifyMerge(TNode t1, TNode t2);
 
-  void check(Effort e) override;
+  //--------------------------------- standard check
+  /** Do we need a check call at last call effort? */
   bool needsCheckLastEffort() override;
+  /** Pre-check, called before the fact queue of the theory is processed. */
+  bool preCheck(Effort level) override;
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  /** Notify fact */
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  //--------------------------------- end standard check
   void preRegisterTerm(TNode n) override;
   TrustNode expandDefinition(Node n) override;
   TrustNode ppRewrite(TNode n) override;
-  void notifySharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-  bool collectModelValues(TheoryModel* m,
-                          const std::set<Node>& termSet) override;
-  void shutdown() override {}
   std::string identify() const override
   {
     return std::string("TheoryDatatypes");
@@ -337,8 +315,6 @@ private:
   Node getInstantiateCons(Node n, const DType& dt, int index);
   /** check instantiate */
   void instantiate( EqcInfo* eqc, Node n );
-  /** must communicate fact */
-  bool mustCommunicateFact( Node n, Node exp );
 private:
   //equality queries
   bool hasTerm( TNode a );
@@ -347,6 +323,9 @@ private:
   bool areCareDisequal( TNode x, TNode y );
   TNode getRepresentative( TNode a );
 
+  /** Collect model values in m based on the relevant terms given by termSet */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   /**
    * Compute relevant terms. This includes datatypes in non-singleton
    * equivalence classes.
@@ -360,6 +339,8 @@ private:
   DatatypesRewriter d_rewriter;
   /** A (default) theory state object */
   TheoryState d_state;
+  /** The inference manager */
+  InferenceManager d_im;
 };/* class TheoryDatatypes */
 
 }/* CVC4::theory::datatypes namespace */