From 74acadc8e7aebd9cd7d41bed64d67e42f45de640 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 25 Jul 2021 11:04:00 -0500
Subject: [PATCH] Changes to datatypes in preparation for central equality
 engine (#6901)

This adds changes from the centralEeDev branch for datatypes.

The changes in behavior are that the inference manager clears its pending inferences when the state is in conflict, and preCheck processes pending facts immediately (which may have been enqueued prior to the call to check via ee merges). These are required to make datatypes robust to the order in which check / merge / backtracks can occur.
---
 src/theory/datatypes/inference_manager.cpp |  7 +++++++
 src/theory/datatypes/theory_datatypes.cpp  | 15 ++++++++++-----
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 014255a7c..ccd0e6853 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -69,6 +69,13 @@ void InferenceManager::addPendingInference(Node conc,
 
 void InferenceManager::process()
 {
+  // if we are in conflict, immediately reset and clear pending
+  if (d_theoryState.isInConflict())
+  {
+    reset();
+    clearPending();
+    return;
+  }
   // process pending lemmas, used infrequently, only for definitional lemmas
   doPendingLemmas();
   // now process the pending facts
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d951f94a7..50c955d48 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -168,13 +168,17 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
 
 bool TheoryDatatypes::preCheck(Effort level)
 {
+  Trace("datatypes-check") << "TheoryDatatypes::preCheck: " << level
+                           << std::endl;
+  d_im.process();
   d_im.reset();
-  d_im.clearPending();
   return false;
 }
 
 void TheoryDatatypes::postCheck(Effort level)
 {
+  Trace("datatypes-check") << "TheoryDatatypes::postCheck: " << level
+                           << std::endl;
   // Apply any last pending inferences, which may occur if the last processed
   // fact was an internal one and triggered further internal inferences.
   d_im.process();
@@ -182,7 +186,6 @@ void TheoryDatatypes::postCheck(Effort level)
   {
     Assert(d_sygusExtension != nullptr);
     d_sygusExtension->check();
-    return;
   }
   else if (level == EFFORT_FULL && !d_state.isInConflict()
            && !d_im.hasSentLemma() && !d_valuation.needCheck())
@@ -532,18 +535,19 @@ void TheoryDatatypes::eqNotifyNewClass(TNode t){
 void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
 {
   if( t1.getType().isDatatype() ){
-    Trace("datatypes-debug")
+    Trace("datatypes-merge")
         << "NotifyMerge : " << t1 << " " << t2 << std::endl;
-    merge(t1,t2);
+    merge(t1, t2);
   }
 }
 
 void TheoryDatatypes::merge( Node t1, Node t2 ){
   if (!d_state.isInConflict())
   {
+    Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl;
+    Assert(areEqual(t1, t2));
     TNode trep1 = t1;
     TNode trep2 = t2;
-    Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
     EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
     if( eqc2 ){
       bool checkInst = false;
@@ -575,6 +579,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           }
           else
           {
+            Assert(areEqual(cons1, cons2));
             //do unification
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( !areEqual( cons1[i], cons2[i] ) ){
-- 
2.30.2