From: ajreynol Date: Mon, 13 Oct 2014 13:53:48 +0000 (+0200) Subject: Model building into quantifiers engine. Simplify axiom-inst mode. X-Git-Tag: cvc5-1.0.0~6566 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3da09bb56cf9fb3a74c9baef55209bc943aa435b;p=cvc5.git Model building into quantifiers engine. Simplify axiom-inst mode. --- diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index d6dac6f14..353b6d1c4 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -740,7 +740,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //debug the model debugModel( fm ); }else{ - fm->initialize( d_considerAxioms ); + fm->initialize(); //process representatives fm->d_rep_id.clear(); fm->d_domain.clear(); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 0a0d4eba8..07fea3cca 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -74,7 +74,7 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { } } -void FirstOrderModel::initialize( bool considerAxioms ) { +void FirstOrderModel::initialize() { processInitialize( true ); //this is called after representatives have been chosen and the equality engine has been built //for each quantifier, collect all operators we care about @@ -86,10 +86,8 @@ void FirstOrderModel::initialize( bool considerAxioms ) { } } processInitializeQuantifier( f ); - if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){ - //initialize relevant models within bodies of all quantifiers - initializeModelForTerm( f[1] ); - } + //initialize relevant models within bodies of all quantifiers + initializeModelForTerm( f[1] ); } processInitialize( false ); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 6ad04a1e6..0b282d5a5 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -78,7 +78,7 @@ public: virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; } // initialize the model - void initialize( bool considerAxioms = true ); + void initialize(); virtual void processInitialize( bool ispre ) = 0; /** mark model set */ void markModelSet() { d_isModelSet = true; } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 64ebb6cda..3148901da 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -335,7 +335,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( fullModel==optBuildAtFullModel() ){ Trace("fmc") << "---Full Model Check reset() " << std::endl; - fm->initialize( d_considerAxioms ); + fm->initialize(); d_quant_models.clear(); d_rep_ids.clear(); d_star_insts.clear(); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index cbff2b581..f6392a0b2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -36,7 +36,7 @@ using namespace CVC4::theory::quantifiers; QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) : TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){ - d_considerAxioms = true; + } bool QModelBuilder::isQuantifierActive( Node f ) { @@ -161,7 +161,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; }else{ //initialize model - fm->initialize( d_considerAxioms ); + fm->initialize(); //analyze the functions Trace("model-engine-debug") << "Analyzing model..." << std::endl; analyzeModel( fm ); @@ -382,7 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){ } bool QModelBuilderIG::isQuantifierActive( Node f ){ - return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end(); + return d_qe->hasOwnership( f ) && d_quant_sat.find( f )==d_quant_sat.end(); } bool QModelBuilderIG::isTermActive( Node n ){ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 4b0046089..3e4471fa4 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -44,8 +44,6 @@ public: virtual bool optUseModel(); //whether to construct model at fullModel = true virtual bool optBuildAtFullModel() { return false; } - //consider axioms - bool d_considerAxioms; /** number of lemmas generated while building model */ //is the exhaustive instantiation incomplete? bool d_incomplete_check; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 92361f68a..eede5c3a8 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -52,86 +52,50 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_LAST_CALL; } +bool ModelEngine::needsModel( Theory::Effort e ) { + return true; +} + void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ int addedLemmas = 0; - bool needsBuild = true; FirstOrderModel* fm = d_quantEngine->getModel(); - quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); - if( fm->getNumAssertedQuantifiers()>0 ){ - //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - } - ++(d_statistics.d_inst_rounds); - Assert( mb!=NULL ); - bool buildAtFullModel = mb->optBuildAtFullModel(); - needsBuild = !buildAtFullModel; - //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 ){ - Trace("model-engine") << "---Model Engine Round---" << std::endl; - //initialize the model - Trace("model-engine-debug") << "Build model..." << std::endl; - mb->d_considerAxioms = effort>=1; - mb->d_addedLemmas = 0; - mb->buildModel( fm, buildAtFullModel ); - addedLemmas += (int)mb->d_addedLemmas; - //if builder has lemmas, add and return - if( addedLemmas==0 ){ - Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - //let the strong solver verify that the model is minimal - //for debugging, this will if there are terms in the model that the strong solver was not notified of - uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); - if( !ufss || ufss->debugModel( fm ) ){ - Trace("model-engine-debug") << "Check model..." << std::endl; - d_incomplete_check = false; - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //successfully built an acceptable model, now check it - addedLemmas += checkModel(); - }else{ - addedLemmas++; - } - } - } - 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; - } - } - } - if( Trace.isOn("model-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; - } + + //the following will test that the model satisfies all asserted universal quantifiers by + // (model-based) exhaustive instantiation. + double clSet = 0; + if( Trace.isOn("model-engine") ){ + Trace("model-engine") << "---Model Engine Round---" << std::endl; + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + ++(d_statistics.d_inst_rounds); + + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + //for debugging, this will if there are terms in the model that the strong solver was not notified of + uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + if( !ufss || ufss->debugModel( fm ) ){ + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + addedLemmas += checkModel(); }else{ - Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl; + addedLemmas++; + } + + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } + if( addedLemmas==0 ){ 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"); - if( options::produceModels() && needsBuild ){ - // finish building the model - mb->buildModel( fm, 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 } @@ -173,6 +137,7 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); + Assert( mb!=NULL ); //flatten the representatives //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; @@ -216,32 +181,46 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); - for( int e=0; egetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - //determine if we should check this quantifier - if( mb->isQuantifierActive( f ) ){ - exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + //default : 1 : conj,axiom + //priority : 0 : conj, 1 : axiom + //trust : 0 : conj + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // FMC uses two sub-effort levels + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); + for( int e=0; egetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + bool isAx = getTermDatabase()->isQAttrAxiom( f ); + //determine if we should check this quantifier + if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } } + if( optOneQuantPerRound() && d_addedLemmas>0 ){ + break; + } + }else{ + Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; } - if( optOneQuantPerRound() && d_addedLemmas>0 ){ - break; - } - }else{ - Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; } } } + if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //set incomplete + if( effort==0 ){ + d_quantEngine->getOutputChannel().setIncomplete(); + } + break; + } } //print debug information - Trace("model-engine-debug") << "Instantiate axioms : " << ( mb->d_considerAxioms ? "yes" : "no" ) << std::endl; Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 6929188bc..8c53084f0 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -48,6 +48,7 @@ public: virtual ~ModelEngine(); public: bool needsCheck( Theory::Effort e ); + bool needsModel( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node f ); diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp index fd3a76a52..5dd6316b3 100644 --- a/src/theory/quantifiers/qinterval_builder.cpp +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -943,7 +943,7 @@ void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //debug the model debugModel( fm ); }else{ - fm->initialize( d_considerAxioms ); + fm->initialize(); //process representatives fm->d_rep_id.clear(); fm->d_max.clear(); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 09cae8eca..135f3547a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -256,7 +256,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = false; - bool needsBuildModel = false; + bool needsModel = false; std::vector< QuantifiersModule* > qm; if( d_model->getNumAssertedQuantifiers()>0 ){ needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call @@ -264,9 +264,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_modules[i]->needsCheck( e ) ){ qm.push_back( d_modules[i] ); needsCheck = true; + if( d_modules[i]->needsModel( e ) ){ + needsModel = true; + } } } } + bool defaultBuildModel = false; if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; Trace("quant-engine-debug") << " modules to check : "; @@ -319,15 +323,34 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){ - for( int i=0; i<(int)qm.size(); i++ ){ - Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl; - qm[i]->check( e, quant_e ); + bool success = true; + //build the model if any module requested it + if( quant_e==QEFFORT_MODEL && needsModel ){ + Assert( d_builder!=NULL ); + Trace("quant-engine-debug") << "Build model, fullModel = " << d_builder->optBuildAtFullModel() << "..." << std::endl; + d_builder->d_addedLemmas = 0; + d_builder->buildModel( d_model, d_builder->optBuildAtFullModel() ); + //we are done if model building was unsuccessful + if( d_builder->d_addedLemmas>0 ){ + success = false; + } + } + if( success ){ + //check each module + for( int i=0; i<(int)qm.size(); i++ ){ + Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl; + qm[i]->check( e, quant_e ); + } } //flush all current lemmas flushLemmas(); //if we have added one, stop if( d_hasAddedLemma ){ break; + //otherwise, complete the model generation if necessary + }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !d_builder->optBuildAtFullModel() ){ + Trace("quant-engine-debug") << "Build completed model..." << std::endl; + d_builder->buildModel( d_model, true ); } } Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; @@ -336,7 +359,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ // this happens if no quantifiers are currently asserted and no model-building module is enabled if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ if( options::produceModels() && !d_model->isModelSet() ){ - needsBuildModel = true; + defaultBuildModel = true; } if( Trace.isOn("inst-per-quant") ){ for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ @@ -354,11 +377,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; }else{ if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){ - needsBuildModel = true; + defaultBuildModel = true; } } - if( needsBuildModel ){ + if( defaultBuildModel ){ Trace("quant-engine-debug") << "Build the model..." << std::endl; d_te->getModelBuilder()->buildModel( d_model, true ); Trace("quant-engine-debug") << "Done building the model." << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index ee905ad09..75b55ca4a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -53,6 +53,8 @@ public: virtual void finishInit() {} /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } + /* whether this module needs a model built */ + virtual bool needsModel( Theory::Effort e ) { return false; } /* reset at a round */ virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */