diff options
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 2b79cd8b9..fb3e6fb36 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -18,6 +18,7 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" @@ -65,7 +66,7 @@ void InstantiationEngine::addCbqiLemma( Node f ){ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //if counterexample-based quantifier instantiation is active - if( Options::current()->cbqi ){ + if( options::cbqi() ){ //check if any cbqi lemma has not been added yet bool addedLemma = false; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ @@ -136,9 +137,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ return false; }else{ Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - if( Options::current()->printInstEngine ){ - Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - } + Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; //flush lemmas to output channel d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); return true; @@ -153,11 +152,11 @@ void InstantiationEngine::check( Theory::Effort e ){ } //determine if we should perform check, based on instWhenMode bool performCheck = false; - if( Options::current()->instWhenMode==Options::INST_WHEN_FULL ){ + if( options::instWhenMode()==INST_WHEN_FULL ){ performCheck = ( e >= Theory::EFFORT_FULL ); - }else if( Options::current()->instWhenMode==Options::INST_WHEN_FULL_LAST_CALL ){ + }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ performCheck = ( ( e==Theory::EFFORT_FULL && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); - }else if( Options::current()->instWhenMode==Options::INST_WHEN_LAST_CALL ){ + }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ performCheck = true; @@ -165,9 +164,9 @@ void InstantiationEngine::check( Theory::Effort e ){ if( performCheck ){ Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl; double clSet = 0; - if( Options::current()->printInstEngine ){ + if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); - Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; + Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } bool quantActive = false; //for each quantifier currently asserted, @@ -178,7 +177,7 @@ void InstantiationEngine::check( Theory::Effort e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){ + if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_ce_lit[ n ]; bool active, value; bool ceValue = false; @@ -232,21 +231,21 @@ void InstantiationEngine::check( Theory::Effort e ){ Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl; d_quantEngine->getOutputChannel().setIncomplete(); }else{ - Assert( Options::current()->finiteModelFind ); + Assert( options::finiteModelFind() ); Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl; } } } }else{ if( e==Theory::EFFORT_LAST_CALL ){ - if( Options::current()->cbqi ){ + if( options::cbqi() ){ debugSat( SAT_CBQI ); } } } - if( Options::current()->printInstEngine ){ + if( Trace.isOn("inst-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; + Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; } } } @@ -302,9 +301,9 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){ } bool InstantiationEngine::doCbqi( Node f ){ - if( Options::current()->cbqiSetByUser ){ - return Options::current()->cbqi; - }else if( Options::current()->cbqi ){ + if( options::cbqi.wasSetByUser() ){ + return options::cbqi(); + }else if( options::cbqi() ){ //if quantifier has a non-arithmetic variable, then do not use cbqi //if quantifier has an APPLY_UF term, then do not use cbqi return !hasNonArithmeticVariable( f ) && !hasApplyUf( f[1] ); |