Process pending inferences at the beginning of datatypes post check (#5213)

This fixes a potential crash in datatypes where a pending inference is not processed on a call to Theory::check. This ensures the pending set of inferences in datatypes is empty after each check. This also ensures the pending vectors are cleared before each check in datatypes.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index f056b9c5d98bfde6cb7bc78ba2b86367bc2b8669..fc7c939008395ab6262f4d85e02337a988a34a3f 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -76,6 +76,8 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma)
     {
       exp.push_back(d_exp);
     }
+    Trace("dt-lemma-debug")
+        << "DatatypesInference : " << d_conc << " via " << exp << std::endl;
     return im->lemmaExp(d_conc, exp, {});
   }
   // assert the internal fact

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 376dbb1dbd0749161bbf80275234f5c4160572a6..c7ba820246affc7e2d1102178929bd85b46de140 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -156,11 +156,15 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
 bool TheoryDatatypes::preCheck(Effort level)
 {
   d_im.reset();
+  d_im.clearPending();
   return false;
 }
 
 void TheoryDatatypes::postCheck(Effort level)
 {
+  // 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();
   if (level == EFFORT_LAST_CALL)
   {
     Assert(d_sygusExtension != nullptr);
@@ -369,6 +373,8 @@ void TheoryDatatypes::notifyFact(TNode atom,
                                  TNode fact,
                                  bool isInternal)
 {
+  Trace("datatypes-debug") << "TheoryDatatypes::assertFact : " << fact
+                           << ", isInternal = " << isInternal << std::endl;
   // could be sygus-specific
   if (d_sygusExtension)
   {

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 5699e75ad5d65e9c89f29e2f3b17341b4aba25db..7985f7de05625b40952a3d90dda691b6325ea97a 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -118,6 +118,12 @@ void InferenceManagerBuffered::doPendingPhaseRequirements()
   }
   d_pendingReqPhase.clear();
 }
+void InferenceManagerBuffered::clearPending()
+{
+  d_pendingFact.clear();
+  d_pendingLem.clear();
+  d_pendingReqPhase.clear();
+}
 void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
 void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
 void InferenceManagerBuffered::clearPendingPhaseRequirements()

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 74bbcc3754f35f7944c15a697ef3a646ca1f0fc7..6edc0298f615f565b2e6605a9a4c0dc9e880db0b 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -115,6 +115,8 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    * phase requirements and clears d_pendingReqPhase.
    */
   void doPendingPhaseRequirements();
+  /** Clear pending facts, lemmas, and phase requirements without processing */
+  void clearPending();
   /** Clear pending facts, without processing */
   void clearPendingFacts();
   /** Clear pending lemmas, without processing */