diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-28 16:27:19 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-28 16:27:27 +0100 |
commit | 68f22235a62f5276b206e9a6692a85001beb8d42 (patch) | |
tree | f9700ab9aaacf866121c7e4f947dffd20710f628 /src/theory/quantifiers_engine.cpp | |
parent | 388a6acf4acd50a7611faae91b3489ac2209e584 (diff) |
Synchronize conjecture generation with E-matching. Minor fix to --full-saturate-quant.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4dc8df09d..d6c6f4667 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -171,8 +171,9 @@ d_lemmas_produced_c(u){ d_builder = NULL; } - //options d_total_inst_count_debug = 0; + d_ierCounter = 0; + d_ierCounter_lc = 0; } QuantifiersEngine::~QuantifiersEngine(){ @@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } + if( e==Theory::EFFORT_FULL ){ + d_ierCounter++; + }else if( e==Theory::EFFORT_LAST_CALL ){ + d_ierCounter_lc++; + } bool needsCheck = false; bool needsModel = false; bool needsFullModel = false; @@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { + //determine if we should perform check, based on instWhenMode + bool performCheck = false; + if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){ + performCheck = ( e >= Theory::EFFORT_FULL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){ + performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck(); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){ + performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){ + performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + }else{ + performCheck = true; + } + if( e==Theory::EFFORT_LAST_CALL ){ + //with bounded integers, skip every other last call, + // since matching loops may occur with infinite quantification + if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + performCheck = false; + } + } + return performCheck; +} + void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ //take default output channel if none is provided |