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.

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c7e2c7c1bcd19956f802dc5d8945a0e9d4d14d26..a98c77a5d14bd2692d6e3101713b3bbc6b02e27a 100644 (file)
--- 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 e9a0ba052cc8da120896ca2e7a80150ea3aac5b8..0d5df098dfc2eae1ecdb6d6ecf4cc6d23ccb1455 100644 (file)
--- 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 );