diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-06 21:46:56 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-06 21:46:56 -0500 |
commit | 2022ec61d569e6408a0eccbde4954ccb7cac61a7 (patch) | |
tree | 023662585fd71598407849205efc553e74324c47 /src | |
parent | af5832b414fbee30904014aaf68a7f3b277b693d (diff) |
Clear pending inferences during datatypes splitting (#2056)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 23 |
1 files changed, 15 insertions, 8 deletions
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() ){ |