diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-13 10:13:16 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-13 10:13:30 +0200 |
commit | e7439fc0daf1049f59540b9aeb890a52d86a77bd (patch) | |
tree | 823cfdcb1ddedcfc2e787893ffc688c090c10a07 /src/theory/quantifiers/model_engine.cpp | |
parent | dcb85a122a2dc9c80c2626ba6ab83f97d7e983ad (diff) |
Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 1d6676464..ce780a29b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -35,7 +35,7 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), -d_incomplete_check(false), +d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), d_totalLemmas(0) @@ -55,6 +55,10 @@ unsigned ModelEngine::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_MODEL; } +void ModelEngine::reset_round( Theory::Effort e ) { + d_incomplete_check = true; +} + void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ int addedLemmas = 0; @@ -95,16 +99,16 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - //if the check was incomplete, we must set incomplete flag - if( d_incomplete_check ){ - d_quantEngine->getOutputChannel().setIncomplete(); - } }else{ //otherwise, the search will continue } } } +bool ModelEngine::checkComplete() { + return !d_incomplete_check; +} + void ModelEngine::registerQuantifier( Node f ){ if( Trace.isOn("fmf-warn") ){ bool canHandle = true; @@ -218,7 +222,7 @@ int ModelEngine::checkModel(){ if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ //set incomplete if( effort==0 ){ - d_quantEngine->getOutputChannel().setIncomplete(); + d_incomplete_check = true; } break; } |