diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-08 10:14:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-08 10:14:31 -0600 |
commit | 564234963dd7e76c8d9b88ef941a6683694e5b53 (patch) | |
tree | 313e46520c07d1536fffbad4b7080937cfc09aae /src/theory/theory_engine.cpp | |
parent | 805d4b7483e51a9b4d24058d493f85700a87f099 (diff) |
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 43 |
1 files changed, 30 insertions, 13 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 944185b31..4e2062c43 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -605,8 +605,6 @@ void TheoryEngine::check(Theory::Effort effort) { if( theory->needsCheckLastEffort() ){ if( !d_curr_model->isBuilt() ){ if( !d_curr_model_builder->buildModel(d_curr_model) ){ - //model building should fail only if the model builder adds lemmas - Assert( needCheck() ); break; } } @@ -617,10 +615,14 @@ void TheoryEngine::check(Theory::Effort effort) { } if( ! d_inConflict && ! needCheck() ){ if(d_logicInfo.isQuantified()) { - // quantifiers engine must pass effort last call check + // quantifiers engine must check at last call effort d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that d_curr_model has been built - } else if(options::produceModels() && !d_curr_model->isBuilt()) { + } + } + if (!d_inConflict && !needCheck()) + { + if (options::produceModels() && !d_curr_model->isBuilt()) + { // must build model at this point d_curr_model_builder->buildModel(d_curr_model); } @@ -631,14 +633,21 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl; if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { - //we will answer SAT + // case where we are about to answer SAT if( d_masterEqualityEngine != NULL ){ AlwaysAssert(d_masterEqualityEngine->consistent()); } - if( options::produceModels() ){ - d_curr_model_builder->debugCheckModel(d_curr_model); - // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model) - postProcessModel(d_curr_model); + if (d_curr_model->isBuilt()) + { + // model construction should always succeed unless lemmas were added + AlwaysAssert(d_curr_model->isBuiltSuccess()); + if (options::produceModels()) + { + d_curr_model_builder->debugCheckModel(d_curr_model); + // Do post-processing of model from the theories (used for THEORY_SEP + // to construct heap model) + postProcessModel(d_curr_model); + } } } } catch(const theory::Interrupted&) { @@ -846,7 +855,8 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const { return true; } -void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ +bool TheoryEngine::collectModelInfo(theory::TheoryModel* m) +{ //have shared term engine collectModelInfo // d_sharedTerms.collectModelInfo( m ); // Consult each active theory to get all relevant information @@ -854,7 +864,10 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { if(d_logicInfo.isTheoryEnabled(theoryId)) { Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl; - d_theoryTable[theoryId]->collectModelInfo( m ); + if (!d_theoryTable[theoryId]->collectModelInfo(m)) + { + return false; + } } } // Get the Boolean variables @@ -870,8 +883,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ value = false; } Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl; - m->assertPredicate(var, value); + if (!m->assertPredicate(var, value)) + { + return false; + } } + return true; } void TheoryEngine::postProcessModel( theory::TheoryModel* m ){ |