summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_builder.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r--src/theory/quantifiers/model_builder.cpp102
1 files changed, 96 insertions, 6 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index fbf3ce59c..b1851cfa4 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -36,7 +36,6 @@ 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;
- d_addedLemmas = 0;
}
bool QModelBuilder::isQuantifierActive( Node f ) {
@@ -128,7 +127,6 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
debugModel( fm );
}else{
d_curr_model = fm;
- d_addedLemmas = 0;
d_didInstGen = false;
//reset the internal information
reset( fm );
@@ -340,15 +338,23 @@ bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
}
QModelBuilderIG::Statistics::Statistics():
- d_num_quants_init("QModelBuilder::Number_Quantifiers", 0),
- d_num_partial_quants_init("QModelBuilder::Number_Partial_Quantifiers", 0),
- d_init_inst_gen_lemmas("QModelBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
- d_inst_gen_lemmas("QModelBuilder::Inst_Gen_Lemmas", 0 )
+ d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+ d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
+ d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
+ d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
+ d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
+ d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
+ d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
+ d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
{
StatisticsRegistry::registerStat(&d_num_quants_init);
StatisticsRegistry::registerStat(&d_num_partial_quants_init);
StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas);
StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
+ StatisticsRegistry::registerStat(&d_eval_formulas);
+ StatisticsRegistry::registerStat(&d_eval_uf_terms);
+ StatisticsRegistry::registerStat(&d_eval_lits);
+ StatisticsRegistry::registerStat(&d_eval_lits_unknown);
}
QModelBuilderIG::Statistics::~Statistics(){
@@ -356,6 +362,10 @@ QModelBuilderIG::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
+ StatisticsRegistry::unregisterStat(&d_eval_formulas);
+ StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
+ StatisticsRegistry::unregisterStat(&d_eval_lits);
+ StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
}
bool QModelBuilderIG::isQuantifierActive( Node f ){
@@ -371,6 +381,86 @@ bool QModelBuilderIG::isTermActive( Node n ){
}
+//do exhaustive instantiation
+bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+ if( optUseModel() ){
+
+ RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
+ if( riter.setQuantifier( f ) ){
+ FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
+ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+ fmig->resetEvaluate();
+ Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+ while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+ d_triedLemmas++;
+ for( int i=0; i<(int)riter.d_index.size(); i++ ){
+ Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+ }
+ int eval = 0;
+ int depIndex;
+ //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;
+ //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 = fmig->evaluate( d_qe->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;
+ }
+ 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_qe, f, riter.d_index_order[i], riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ //add as instantiation
+ if( d_qe->addInstantiation( f, m ) ){
+ d_addedLemmas++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
+ }
+ }else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+ riter.increment();
+ }
+ }
+ }
+ //print debugging information
+ if( fmig ){
+ d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+ d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+ d_statistics.d_eval_lits += fmig->d_eval_lits;
+ d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
+ }
+ Trace("inst-fmf-ei") << "Finished: " << std::endl;
+ Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl;
+ if( d_addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << 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 = riter.d_incomplete;
+ return true;
+ }else{
+ return false;
+ }
+}
+
void QModelBuilderDefault::reset( FirstOrderModel* fm ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback