From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Oct 2020 03:22:16 +0000 (-0500)
Subject: Process pending inferences at the beginning of datatypes post check (#5213)
X-Git-Tag: cvc5-1.0.0~2744
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c540b4b96a100ba1d280c700c6c360efeb24fc2;p=cvc5.git

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 f056b9c5d..fc7c93900 100644
--- 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 376dbb1db..c7ba82024 100644
--- 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 5699e75ad..7985f7de0 100644
--- 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 74bbcc375..6edc0298f 100644
--- 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 */