diff options
author | Guy <katz911@gmail.com> | 2016-06-20 10:17:04 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-20 10:17:04 -0700 |
commit | 4b8972fec229012812bb7edc9e315c2e54f7c059 (patch) | |
tree | 930d63632dc3eb3e945967dee4e442b76c26ee3a /src/theory/theory_engine.cpp | |
parent | 150863561376c8cb7b170793f693352eab582ba9 (diff) | |
parent | dc27675a9b9aa0346122390afdb28280f4495e9c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 33 |
1 files changed, 22 insertions, 11 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 34eff5a47..881acdddd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -518,18 +518,29 @@ 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() ) { - //d_theoryTable[THEORY_STRINGS]->check(Theory::EFFORT_LAST_CALL); - if(d_logicInfo.isQuantified()) { - // quantifiers engine must pass effort last call check - d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built - } else if(options::produceModels()) { - // must build model at this point - d_curr_model_builder->buildModel(d_curr_model, true); + //calls to theories requiring the model go here + //FIXME: this should not be theory-specific + if(d_logicInfo.isTheoryEnabled(THEORY_SEP)) { + Assert( d_theoryTable[THEORY_SEP]!=NULL ); + if( d_theoryTable[THEORY_SEP]->hasFacts() ){ + // must build model at this point + d_curr_model_builder->buildModel(getModel(), false); + d_theoryTable[THEORY_SEP]->check(Theory::EFFORT_LAST_CALL); + } } - Trace("theory::assertions-model") << endl; - if (Trace.isOn("theory::assertions-model")) { - printAssertions("theory::assertions-model"); + if( ! d_inConflict && ! needCheck() ){ + if(d_logicInfo.isQuantified()) { + // quantifiers engine must pass effort last call check + d_quantEngine->check(Theory::EFFORT_LAST_CALL); + // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built + } else if(options::produceModels()) { + // must build model at this point + d_curr_model_builder->buildModel(getModel(), true); + } + Trace("theory::assertions-model") << endl; + if (Trace.isOn("theory::assertions-model")) { + printAssertions("theory::assertions-model"); + } } } |