diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 10:43:28 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-15 10:43:28 -0500 |
commit | dd963729849ca7f1001373c56e800bd62781fe98 (patch) | |
tree | 34ed8121a5d17a92f1e59fd6055f40feeb932db0 /src/theory/quantifiers_engine.cpp | |
parent | d43e5fb294d89ba69f7d2607a12c8700b7ec9345 (diff) |
Refactor setIncomplete in quantifiers.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 43 |
1 files changed, 32 insertions, 11 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e48c6eafe..fbfdb856e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -219,7 +219,6 @@ void QuantifiersEngine::finishInit(){ d_sg_gen = new quantifiers::ConjectureGenerator( this, c ); d_modules.push_back( d_sg_gen ); } - //maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules if( !options::finiteModelFind() || options::fmfInstEngine() ){ d_inst_engine = new quantifiers::InstantiationEngine( this ); d_modules.push_back( d_inst_engine ); @@ -395,13 +394,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_conflict = false; d_hasAddedLemma = false; bool setIncomplete = false; - if( e==Theory::EFFORT_LAST_CALL ){ - //sources of incompleteness - if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ - Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl; - setIncomplete = true; - } - } bool usedModelBuilder = false; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; @@ -544,20 +536,49 @@ void QuantifiersEngine::check( Theory::Effort e ){ } }else if( quant_e==QEFFORT_MODEL ){ if( e==Theory::EFFORT_LAST_CALL ){ + //sources of incompleteness if( !d_recorded_inst.empty() ){ + Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; setIncomplete = true; } //if we have a chance not to set incomplete if( !setIncomplete ){ setIncomplete = false; //check if we should set the incomplete flag - for( unsigned i=0; i<qm.size(); i++ ){ - if( !qm[i]->checkComplete() ){ - Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl; + for( unsigned i=0; i<d_modules.size(); i++ ){ + if( !d_modules[i]->checkComplete() ){ + Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl; setIncomplete = true; break; } } + if( !setIncomplete ){ + //look at individual quantified formulas, one module must claim completeness for each one + for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){ + bool hasCompleteM = false; + Node q = d_model->getAssertedQuantifier( i ); + QuantifiersModule * qmd = getOwner( q ); + if( qmd!=NULL ){ + hasCompleteM = qmd->checkCompleteFor( q ); + }else{ + for( unsigned j=0; j<d_modules.size(); j++ ){ + if( d_modules[j]->checkCompleteFor( q ) ){ + qmd = d_modules[j]; + hasCompleteM = true; + break; + } + } + } + if( !hasCompleteM ){ + Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl; + setIncomplete = true; + break; + }else{ + Assert( qmd!=NULL ); + Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl; + } + } + } } //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL if( !setIncomplete ){ |