diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 386 |
1 files changed, 216 insertions, 170 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index cbeeed8d0..b5a9ee74c 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -15,7 +15,6 @@ **/ #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/rep_set_iterator.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" @@ -25,11 +24,11 @@ #include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" //#define ME_PRINT_WARNINGS #define EVAL_FAIL_SKIP_MULTIPLE -//#define ONE_QUANT_PER_ROUND using namespace std; using namespace CVC4; @@ -40,96 +39,97 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; //Model Engine constructor -ModelEngine::ModelEngine( QuantifiersEngine* qe ) : +ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), -d_builder( qe ), -d_rel_domain( qe->getModel() ){ +d_builder( c, qe ), +d_rel_domain( qe, qe->getModel() ){ } void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ - //first, check if we can minimize the model further - if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; - } + FirstOrderModel* fm = d_quantEngine->getModel(); //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; + Trace("model-engine") << "---Model Engine Round---" << std::endl; if( d_builder.optUseModel() ){ //check if any quantifiers are un-initialized - for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); addedLemmas += initializeQuantifier( f ); } } - if( addedLemmas==0 ){ - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "---Model Engine Round---" << std::endl; - } - Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl; - ++(d_statistics.d_inst_rounds); - //reset the quantifiers engine - d_quantEngine->resetInstantiationRound( e ); - //initialize the model - Debug("fmf-model-debug") << "Build model..." << std::endl; - d_builder.buildModel( d_quantEngine->getModel() ); - d_quantEngine->d_model_set = true; - //if builder has lemmas, add and return - if( d_builder.d_addedLemmas>0 ){ - addedLemmas += (int)d_builder.d_addedLemmas; - }else{ - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //verify we are SAT by trying exhaustive instantiation - if( optUseRelevantDomain() ){ - d_rel_domain.compute(); + if( addedLemmas>0 ){ + Trace("model-engine") << "Initialize, Added Lemmas = " << addedLemmas << std::endl; + } + //two effort levels: first try exhaustive instantiation without axioms, then with. + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // for effort = 0, we only instantiate non-axioms + // for effort = 1, we instantiate everything + if( addedLemmas==0 ){ + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); } - d_triedLemmas = 0; - d_testLemmas = 0; - d_relevantLemmas = 0; - d_totalLemmas = 0; - Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; - for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){ - addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); - if( optOneQuantPerRound() && addedLemmas>0 ){ - break; - } - } -#ifdef ME_PRINT_WARNINGS - if( addedLemmas>10000 ){ - break; + ++(d_statistics.d_inst_rounds); + //reset the quantifiers engine + d_quantEngine->resetInstantiationRound( e ); + //initialize the model + Trace("model-engine-debug") << "Build model..." << std::endl; + d_builder.setEffort( effort ); + d_builder.buildModel( fm, false ); + //if builder has lemmas, add and return + if( d_builder.d_addedLemmas>0 ){ + addedLemmas += (int)d_builder.d_addedLemmas; + }else{ + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + //for debugging, this will if there are terms in the model that the strong solver was not notified of + uf_ss->debugModel( fm ); + Trace("model-engine-debug") << "Check model..." << std::endl; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + checkModel( addedLemmas ); + //print debug information + if( Trace.isOn("model-engine") ){ + Trace("model-engine") << "Instantiate axioms : " << ( d_builder.d_considerAxioms ? "yes" : "no" ) << std::endl; + Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } -#endif - } - Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; - if( Trace.isOn("model-engine") ){ - Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } -#ifdef ME_PRINT_WARNINGS - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + } + if( addedLemmas==0 ){ + //if we have not added lemmas yet and axiomInstMode=trust, then we are done + if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //we must return unknown if an axiom is asserted + if( effort==0 ){ + d_incomplete_check = true; + } + break; } -#endif } } if( addedLemmas==0 ){ - //CVC4 will answer SAT - Debug("fmf-consistent") << std::endl; + Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; + //CVC4 will answer SAT or unknown + Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - // finish building the model in the standard way - d_builder.finishProcessBuildModel( d_quantEngine->getModel() ); + if( options::produceModels() ){ + // finish building the model in the standard way + d_builder.buildModel( fm, true ); + d_quantEngine->d_model_set = true; + } + //if the check was incomplete, we must set incomplete flag + if( d_incomplete_check ){ + d_quantEngine->getOutputChannel().setIncomplete(); + } }else{ //otherwise, the search will continue d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); @@ -154,11 +154,7 @@ bool ModelEngine::optUseRelevantDomain(){ } bool ModelEngine::optOneQuantPerRound(){ -#ifdef ONE_QUANT_PER_ROUND - return true; -#else - return false; -#endif + return options::fmfOneQuantPerRound(); } int ModelEngine::initializeQuantifier( Node f ){ @@ -178,11 +174,13 @@ int ModelEngine::initializeQuantifier( Node f ){ // Notice() << "Unhandled phase req: " << n << std::endl; // } //} + std::vector< Node > vars; std::vector< Node > ics; std::vector< Node > terms; for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() ); + vars.push_back( f[0][j] ); ics.push_back( ic ); terms.push_back( t ); //calculate the basis match for f @@ -193,67 +191,137 @@ int ModelEngine::initializeQuantifier( Node f ){ Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() ); d_quantEngine->getTermDatabase()->registerModelBasis( n, gn ); - //add model basis instantiation - if( d_quantEngine->addInstantiation( f, terms ) ){ - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - ++(d_statistics.d_num_quants_init_fail); + if( d_builder.optInstGen() ){ + //add model basis instantiation + if( d_quantEngine->addInstantiation( f, vars, terms ) ){ + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + ++(d_statistics.d_num_quants_init_fail); + } } } return 0; } -int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ - int tests = 0; - int addedLemmas = 0; - int triedLemmas = 0; - Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; +void ModelEngine::checkModel( int& addedLemmas ){ + FirstOrderModel* fm = d_quantEngine->getModel(); + //for debugging + if( Trace.isOn("model-engine") ){ + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + } + } + } + //verify we are SAT by trying exhaustive instantiation + d_incomplete_check = false; + if( optUseRelevantDomain() ){ + d_rel_domain.compute(); } - Debug("inst-fmf-ei") << std::endl; - if( d_builder.d_quant_selection_lits[f].empty() ){ - Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; + d_triedLemmas = 0; + d_testLemmas = 0; + d_relevantLemmas = 0; + d_totalLemmas = 0; + Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); #ifdef ME_PRINT_WARNINGS - Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } #endif - }else{ - Debug("inst-fmf-ei") << " Model literal definitions:" << std::endl; - for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ - Debug("inst-fmf-ei") << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; + if( optOneQuantPerRound() && addedLemmas>0 ){ + break; } } - RepSetIterator riter( f, d_quantEngine->getModel() ); - //set the domain for the iterator (the sufficient set of instantiations to try) - if( useRelInstDomain ){ - riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; +} + +int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ + int addedLemmas = 0; + //keep track of total instantiations for statistics + int totalInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( d_quantEngine->getModel()->d_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ tn ].size(); + } } - RepSetEvaluator reval( d_quantEngine->getModel(), &riter ); - while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ - d_testLemmas++; - if( d_builder.optUseModel() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - tests++; - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - int depIndex = riter.getNumTerms()-1; - int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex ); + d_totalLemmas += totalInst; + //if we need to consider this quantifier on this iteration + if( d_builder.isQuantifierActive( f ) ){ + Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl; + if( useRelInstDomain ){ + Trace("rel-dom") << "Relevant domain : " << std::endl; + for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){ + Trace("rel-dom") << " " << i << " : "; + for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){ + Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " "; + } + Trace("rel-dom") << std::endl; + } + } + int tests = 0; + int triedLemmas = 0; + Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl; + Debug("inst-fmf-ei") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + } + Debug("inst-fmf-ei") << std::endl; + RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); + riter.setQuantifier( f ); + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = d_incomplete_check || riter.d_incomplete; + //set the domain for the iterator (the sufficient set of instantiations to try) + if( useRelInstDomain ){ + riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + } + d_quantEngine->getModel()->resetEvaluate(); + while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ + d_testLemmas++; + int eval = 0; + int depIndex; + if( d_builder.optUseModel() ){ + //see if instantiation is already true in current model + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + tests++; + //if evaluate(...)==1, then the instantiation is already true in the model + // depIndex is the index of the least significant variable that this evaluation relies upon + depIndex = riter.getNumTerms()-1; + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + } + } if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + //instantiation is already true -> skip riter.increment2( depIndex ); }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + //instantiation was not shown to be true, construct the match InstMatch m; - riter.getMatch( d_quantEngine, m ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) ); + } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; d_triedLemmas++; + //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; #ifdef EVAL_FAIL_SKIP_MULTIPLE @@ -270,70 +338,48 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ riter.increment(); } } - }else{ - InstMatch m; - riter.getMatch( d_quantEngine, m ); - Debug("fmf-model-eval") << "* Add instantiation " << std::endl; - triedLemmas++; - d_triedLemmas++; - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - } - riter.increment(); } - } - d_statistics.d_eval_formulas += reval.d_eval_formulas; - d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms; - d_statistics.d_eval_lits += reval.d_eval_lits; - d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown; - int totalInst = 1; - int relevantInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size(); - relevantInst = relevantInst * (int)riter.d_domain[i].size(); - } - d_totalLemmas += totalInst; - d_relevantLemmas += relevantInst; - Debug("inst-fmf-ei") << "Finished: " << std::endl; - Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; -///----------- + d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; + d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; + d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; + d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; + int relevantInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + relevantInst = relevantInst * (int)riter.d_domain[i].size(); + } + d_relevantLemmas += relevantInst; + Debug("inst-fmf-ei") << "Finished: " << std::endl; + Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; + Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; #ifdef ME_PRINT_WARNINGS - if( addedLemmas>1000 ){ - Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl; - Notice() << " Inst Total: " << totalInst << std::endl; - Notice() << " Inst Relevant: " << totalRelevant << std::endl; - Notice() << " Inst Tried: " << triedLemmas << std::endl; - Notice() << " Inst Added: " << addedLemmas << std::endl; - Notice() << " # Tests: " << tests << std::endl; - Notice() << std::endl; - if( !d_builder.d_quant_selection_lits[f].empty() ){ - Notice() << " Model literal definitions:" << std::endl; - for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ - Notice() << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; - } + if( addedLemmas>1000 ){ + Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl; + Notice() << " Inst Total: " << totalInst << std::endl; + Notice() << " Inst Relevant: " << totalRelevant << std::endl; + Notice() << " Inst Tried: " << triedLemmas << std::endl; + Notice() << " Inst Added: " << addedLemmas << std::endl; + Notice() << " # Tests: " << tests << std::endl; Notice() << std::endl; } - } #endif -///----------- + } return addedLemmas; } void ModelEngine::debugPrint( const char* c ){ - Debug( c ) << "Quantifiers: " << std::endl; + Trace( c ) << "Quantifiers: " << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Debug( c ) << " "; - if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){ - Debug( c ) << "*SAT* "; + Trace( c ) << " "; + if( !d_builder.isQuantifierActive( f ) ){ + Trace( c ) << "*Inactive* "; }else{ - Debug( c ) << " "; + Trace( c ) << " "; } - Debug( c ) << f << std::endl; + Trace( c ) << f << std::endl; } //d_quantEngine->getModel()->debugPrint( c ); } |