From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 28 Aug 2020 08:19:32 +0000 (-0500)
Subject: Do not delay processing equivalence class merges in datatypes (#4952)
X-Git-Tag: cvc5-1.0.0~2946
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d03fa5697e278bef5cbc385978634421cb5a050b;p=cvc5.git

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 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 );