From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Jun 2018 02:46:56 +0000 (-0500)
Subject: Clear pending inferences during datatypes splitting (#2056)
X-Git-Tag: cvc5-1.0.0~4976
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2022ec61d569e6408a0eccbde4954ccb7cac61a7;p=cvc5.git

Clear pending inferences during datatypes splitting (#2056)
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4c79a31e9..7bc6eb3b0 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -188,7 +188,6 @@ void TheoryDatatypes::check(Effort e) {
     Trace("datatypes-debug") << "Check for splits " << e << endl;
     do {
       d_addedFact = false;
-      bool added_split = false;
       std::map< TypeNode, Node > rec_singletons;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
@@ -307,12 +306,11 @@ void TheoryDatatypes::check(Effort e) {
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                     Node lemma = DatatypesRewriter::mkSplit(n, dt);
                     Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                    //doSendLemma( lemma );
                     d_out->lemma( lemma, false, false, true );
+                    d_addedLemma = true;
                   }
-                  added_split = true;
                   if( !options::dtBlastSplits() ){
-                    return;
+                    break;
                   }
                 }
               }else{
@@ -325,11 +323,20 @@ void TheoryDatatypes::check(Effort e) {
         }
         ++eqcs_i;
       }
-      if( added_split ){
-        return;
+      if (d_addedLemma)
+      {
+        // clear pending facts: we added a lemma, so internal inferences are
+        // no longer necessary
+        d_pending.clear();
+        d_pending_exp.clear();
+      }
+      else
+      {
+        // we did not add a lemma, process internal inferences. This loop
+        // will repeat.
+        Trace("datatypes-debug") << "Flush pending facts..." << std::endl;
+        flushPendingFacts();
       }
-      Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
-      flushPendingFacts();
       /*
       if( !d_conflict ){
         if( options::dtRewriteErrorSel() ){