From d03fa5697e278bef5cbc385978634421cb5a050b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 28 Aug 2020 03:19:32 -0500
Subject: [PATCH] Do not delay processing equivalence class merges in datatypes
 (#4952)

Currently, the theory of datatypes buffers its processing of when equivalence class merges are processed. This was an earlier design to avoid using the equality engine while it was doing internal operations. Now, equivalence class merge callbacks are called at a time when it is safe to use the equality engine and thus this level of indirection is unnecessary.

This will simplify further work on datatypes towards having a standard inference manager.
---
 src/theory/datatypes/theory_datatypes.cpp | 40 +++--------------------
 src/theory/datatypes/theory_datatypes.h   |  3 --
 2 files changed, 5 insertions(+), 38 deletions(-)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c7e2c7c1b..a98c77a5d 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -160,7 +160,7 @@ void TheoryDatatypes::check(Effort e) {
   if (done() && e<EFFORT_FULL) {
     return;
   }
-  Assert(d_pending.empty() && d_pending_merge.empty());
+  Assert(d_pending.empty());
   d_addedLemma = false;
   
   if( e == EFFORT_LAST_CALL ){
@@ -198,7 +198,7 @@ void TheoryDatatypes::check(Effort e) {
 
   if( e == EFFORT_FULL && !d_conflict && !d_addedLemma && !d_valuation.needCheck() ) {
     //check for cycles
-    Assert(d_pending.empty() && d_pending_merge.empty());
+    Assert(d_pending.empty());
     do {
       d_addedFact = false;
       Trace("datatypes-proc") << "Check cycles..." << std::endl;
@@ -372,18 +372,6 @@ void TheoryDatatypes::check(Effort e) {
         Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
         flushPendingFacts();
       }
-      /*
-      if( !d_conflict ){
-        if( options::dtRewriteErrorSel() ){
-          bool innerAddedFact = false;
-          do {
-            collapseSelectors();
-            innerAddedFact = !d_pending.empty() || !d_pending_merge.empty();
-            flushPendingFacts();
-          }while( !d_conflict && innerAddedFact );
-        }
-      }
-      */
     }while( !d_conflict && !d_addedLemma && d_addedFact );
     Trace("datatypes-debug") << "Finished, conflict=" << d_conflict << ", lemmas=" << d_addedLemma << std::endl;
     if( !d_conflict ){
@@ -403,7 +391,6 @@ bool TheoryDatatypes::needsCheckLastEffort() {
 }
 
 void TheoryDatatypes::flushPendingFacts(){
-  doPendingMerges();
   //pending lemmas: used infrequently, only for definitional lemmas
   if( !d_pending_lem.empty() ){
     int i = 0;
@@ -412,7 +399,6 @@ void TheoryDatatypes::flushPendingFacts(){
       i++;
     }
     d_pending_lem.clear();
-    doPendingMerges();
   }
   int i = 0;
   while( !d_conflict && i<(int)d_pending.size() ){
@@ -458,19 +444,6 @@ void TheoryDatatypes::flushPendingFacts(){
   d_pending_exp.clear();
 }
 
-void TheoryDatatypes::doPendingMerges(){
-  if( !d_conflict ){
-    //do all pending merges
-    int i=0;
-    while( i<(int)d_pending_merge.size() ){
-      Assert(d_pending_merge[i].getKind() == EQUAL);
-      merge( d_pending_merge[i][0], d_pending_merge[i][1] );
-      i++;
-    }
-  }
-  d_pending_merge.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;
@@ -495,8 +468,8 @@ bool TheoryDatatypes::doSendLemmas( std::vector< Node >& lemmas ){
   return ret;
 }
         
-void TheoryDatatypes::assertFact( Node fact, Node exp ){
-  Assert(d_pending_merge.empty());
+void TheoryDatatypes::assertFact( Node fact, Node exp)
+{
   Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact << std::endl;
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
@@ -505,7 +478,6 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
   }else{
     d_equalityEngine->assertPredicate(atom, polarity, exp);
   }
-  doPendingMerges();
   // could be sygus-specific
   if (d_sygusExtension)
   {
@@ -523,8 +495,6 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
     addTester( tindex, fact, eqc, rep, t_arg );
     Trace("dt-tester") << "Done assert tester." << std::endl;
-    //do pending merges
-    doPendingMerges();
     Trace("dt-tester") << "Done pending merges." << std::endl;
     if( !d_conflict && polarity ){
       if (d_sygusExtension)
@@ -851,7 +821,7 @@ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
   if( t1.getType().isDatatype() ){
     Trace("datatypes-debug")
         << "NotifyMerge : " << t1 << " " << t2 << std::endl;
-    d_pending_merge.push_back( t1.eqNode( t2 ) );
+    merge(t1,t2);
   }
 }
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e9a0ba052..0d5df098d 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -199,7 +199,6 @@ private:
   std::vector< Node > d_pending_lem;
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
-  std::vector< Node > d_pending_merge;
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionTerms;
   /** counter for forcing assignments (ensures fairness) */
@@ -222,8 +221,6 @@ private:
   /** flush pending facts */
   void flushPendingFacts();
 
-  /** do pending merged */
-  void doPendingMerges();
   /** do send lemma */
   bool doSendLemma( Node lem );
   bool doSendLemmas( std::vector< Node >& lem );
-- 
2.30.2