diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 15:53:48 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-13 15:53:48 +0200 |
commit | 3da09bb56cf9fb3a74c9baef55209bc943aa435b (patch) | |
tree | 5053a353ad0cd21b63f09dbdfd142f4bed837878 /src/theory/quantifiers | |
parent | c3992de261f0fa968f50349de1bdc3f9bef6ce6b (diff) |
Model building into quantifiers engine. Simplify axiom-inst mode.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 155 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/qinterval_builder.cpp | 2 |
9 files changed, 78 insertions, 102 deletions
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; e<e_max; e++) { - if (d_addedLemmas==0) { - for( int i=0; i<fm->getNumAssertedQuantifiers(); 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; e<e_max; e++) { + if (d_addedLemmas==0) { + for( int i=0; i<fm->getNumAssertedQuantifiers(); 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(); |