diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-13 21:16:26 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-13 21:16:26 +0000 |
commit | 795e5ba8a1138a371409ac9c8e9da78ce652bb94 (patch) | |
tree | 5cc0d5bebbccf87b122b9e1690f27e398b4e8cc0 /src/theory/theory_engine.cpp | |
parent | 740df5937639738a0238312dfb061643e62ba605 (diff) |
refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a4b918984..9d93c6cc0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -321,13 +321,14 @@ void TheoryEngine::check(Theory::Effort effort) { // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) { if(d_logicInfo.isQuantified()) { + bool prevIncomplete = d_incomplete; // quantifiers engine must pass effort last call check d_quantEngine->check(Theory::EFFORT_LAST_CALL); // if we have given up, then possibly flip decision if(options::flipDecision()) { if(d_incomplete && !d_inConflict && !needCheck()) { if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) { - d_incomplete = false; + d_incomplete = prevIncomplete; } } } |