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.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 014255a7c04048bbab834fbf63990be633991fad..ccd0e685348e428b64f16b5196cc778e08039ad4 100644 (file)
--- 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 d951f94a7de4713d33b3f523d430c629370833aa..50c955d48c58168c390f0422c25ca114128aa3fc 100644 (file)
--- 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] ) ){