summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r--src/theory/quantifiers/model_engine.cpp258
1 files changed, 146 insertions, 112 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a69b278c0..90b8c62ba 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -36,7 +36,8 @@ using namespace CVC4::theory::inst;
//Model Engine constructor
ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ){
+d_rel_domain( qe, qe->getModel() ),
+d_fmc( qe ){
if( options::fmfNewInstGen() ){
d_builder = new ModelEngineBuilderInstGen( c, qe );
@@ -75,6 +76,11 @@ void ModelEngine::check( Theory::Effort e ){
//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::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
+ //for full model checking
+ if( d_fmc.isActive() ){
+ Trace("model-engine-debug") << "Reset full model checker..." << std::endl;
+ d_fmc.reset( fm );
+ }
Trace("model-engine-debug") << "Check model..." << std::endl;
d_incomplete_check = false;
//print debug
@@ -161,15 +167,23 @@ int ModelEngine::checkModel( int checkOption ){
if( it->first.isSort() ){
Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Trace("model-engine-debug") << " ";
+ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
for( size_t i=0; i<it->second.size(); i++ ){
//Trace("model-engine-debug") << it->second[i] << " ";
Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
+ Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl;
}
}
}
+ //full model checking: construct models for all functions
+ if( d_fmc.isActive() ){
+ for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
+ d_fmc.getModel(fm, it->first);
+ }
+ }
//compute the relevant domain if necessary
if( optUseRelevantDomain() ){
d_rel_domain.compute();
@@ -179,36 +193,41 @@ int ModelEngine::checkModel( int checkOption ){
d_relevantLemmas = 0;
d_totalLemmas = 0;
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- //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( fm->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
- }
- }
- d_totalLemmas += totalInst;
- //determine if we should check this quantifiers
- bool checkQuant = false;
- if( checkOption==check_model_full ){
- checkQuant = d_builder->isQuantifierActive( f );
- }else if( checkOption==check_model_no_inst_gen ){
- checkQuant = !d_builder->hasInstGen( f );
- }
- //if we need to consider this quantifier on this iteration
- if( checkQuant ){
- addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
- if( Trace.isOn("model-engine-warn") ){
- if( addedLemmas>10000 ){
- Debug("fmf-exit") << std::endl;
- debugPrint("fmf-exit");
- exit( 0 );
+ int e_max = d_fmc.isActive() ? 2 : 1;
+ for( int e=0; e<e_max; e++) {
+ if (addedLemmas==0) {
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ //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( fm->d_rep_set.hasType( tn ) ){
+ totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ }
+ }
+ d_totalLemmas += totalInst;
+ //determine if we should check this quantifiers
+ bool checkQuant = false;
+ if( checkOption==check_model_full ){
+ checkQuant = d_builder->isQuantifierActive( f );
+ }else if( checkOption==check_model_no_inst_gen ){
+ checkQuant = !d_builder->hasInstGen( f );
+ }
+ //if we need to consider this quantifier on this iteration
+ if( checkQuant ){
+ addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e );
+ if( Trace.isOn("model-engine-warn") ){
+ if( addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
+ }
+ }
+ if( optOneQuantPerRound() && addedLemmas>0 ){
+ break;
+ }
}
- }
- if( optOneQuantPerRound() && addedLemmas>0 ){
- break;
}
}
}
@@ -222,100 +241,115 @@ int ModelEngine::checkModel( int checkOption ){
return addedLemmas;
}
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){
int addedLemmas = 0;
- Trace("inst-fmf-ei") << "Exhaustive instantiate " << 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;
- //create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- if( riter.setQuantifier( f ) ){
- //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] );
+ bool useModel = d_builder->optUseModel();
+ if (d_fmc.isActive() && effort==0) {
+ addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+ }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) {
+ if(d_fmc.isActive()){
+ useModel = false;
+ int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+ if( lem!=-1 ){
+ return lem;
+ }
}
- d_quantEngine->getModel()->resetEvaluate();
- int tests = 0;
- int triedLemmas = 0;
- 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()->getInstConstantBody( 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;
- }
+ Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << 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;
+ //create a rep set iterator and iterate over the (relevant) domain of the quantifier
+ RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+ if( riter.setQuantifier( f ) ){
+ Debug("inst-fmf-ei") << "Set domain..." << std::endl;
+ //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] );
}
- if( eval==1 ){
- //instantiation is already true -> skip
- riter.increment2( depIndex );
- }else{
- //instantiation was not shown to be true, construct the match
- InstMatch 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("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+ d_quantEngine->getModel()->resetEvaluate();
+ Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+ int tests = 0;
+ int triedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ d_testLemmas++;
+ int eval = 0;
+ int depIndex;
+ if( useModel ){
+ //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()->getInstConstantBody( 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;
+ }
}
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- d_triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 && optExhInstEvalSkipMultiple() ){
- riter.increment2( depIndex );
+ if( eval==1 ){
+ //instantiation is already true -> skip
+ riter.increment2( depIndex );
+ }else{
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine, 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++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 && optExhInstEvalSkipMultiple() ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
+ }
}else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
riter.increment();
}
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
- riter.increment();
}
}
+ //print debugging information
+ 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;
+ Trace("inst-fmf-ei") << "Finished: " << std::endl;
+ //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
+ Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl;
+ if( addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
+ Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
+ Trace("model-engine-warn") << std::endl;
+ }
}
- //print debugging information
- 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;
- Trace("inst-fmf-ei") << "Finished: " << std::endl;
- //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl;
- if( addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
- Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
- Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
+ //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;
}
- //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;
return addedLemmas;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback