diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-14 19:06:49 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-14 19:06:49 -0600 |
commit | 85df7998e4362e0a9c796146d07d7b9e91045a31 (patch) | |
tree | 0ab2e33e807651386cd041257c1abff2bb769057 /src/theory/quantifiers_engine.cpp | |
parent | 748e20967ae7698f6b545a5128633865701aeb2d (diff) |
Make QEffort an enum (#1366)
* Make QEffort an enum.
* Format
* Minor
* Fix
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f6b920cda..bc2b533be 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -120,7 +120,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } d_tr_trie = new inst::TriggerTrie; - d_curr_effort_level = QEFFORT_NONE; + d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; d_useModelEe = false; @@ -444,7 +444,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ return; } bool needsCheck = !d_lemmas_waiting.empty(); - unsigned needsModelE = QEFFORT_NONE; + QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE; std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -454,7 +454,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ needsCheck = true; //can only request model at last call since theory combination can find inconsistencies if( e>=Theory::EFFORT_LAST_CALL ){ - unsigned me = d_modules[i]->needsModel( e ); + QuantifiersModule::QEffort me = d_modules[i]->needsModel(e); needsModelE = me<needsModelE ? me : needsModelE; } } @@ -559,7 +559,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ ++(d_statistics.d_instantiation_rounds); } Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; - for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ + for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT; + qef <= QuantifiersModule::QEFFORT_LAST_CALL; + ++qef) + { + QuantifiersModule::QEffort quant_e = + static_cast<QuantifiersModule::QEffort>(qef); d_curr_effort_level = quant_e; //build the model if any module requested it if( needsModelE==quant_e && !d_model->isBuilt() ){ @@ -590,7 +595,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ break; }else{ Assert( !d_conflict ); - if( quant_e==QEFFORT_CONFLICT ){ + if (quant_e == QuantifiersModule::QEFFORT_CONFLICT) + { if( e==Theory::EFFORT_FULL ){ //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){ @@ -601,7 +607,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_LAST_CALL ){ d_ierCounter_lc = d_ierCounter_lc + 1; } - }else if( quant_e==QEFFORT_MODEL ){ + } + else if (quant_e == QuantifiersModule::QEFFORT_MODEL) + { if( e==Theory::EFFORT_LAST_CALL ){ //sources of incompleteness if( !d_recorded_inst.empty() ){ @@ -655,7 +663,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } - d_curr_effort_level = QEFFORT_NONE; + d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; if( d_hasAddedLemma ){ //debug information @@ -1293,7 +1301,9 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 ); } } - if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){ + if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT + && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE) + { //notify listeners for( unsigned j=0; j<d_inst_notify.size(); j++ ){ if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ |