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.cpp59
1 files changed, 33 insertions, 26 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 95b674cca..3ae36b1d4 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file model_builder.cpp
** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Implementation of model builder class
**/
@@ -50,14 +50,14 @@ bool QModelBuilder::optUseModel() {
void QModelBuilder::debugModel( FirstOrderModel* fm ){
//debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
- if( Trace.isOn("quant-model-warn") ){
- Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl;
+ if( Trace.isOn("quant-check-model") ){
+ Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
int tests = 0;
int bad = 0;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
std::vector< Node > vars;
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
RepSetIterator riter( d_qe, &(fm->d_rep_set) );
@@ -65,26 +65,26 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
while( !riter.isFinished() ){
tests++;
std::vector< Node > terms;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- terms.push_back( riter.getTerm( i ) );
+ for( int k=0; k<riter.getNumTerms(); k++ ){
+ terms.push_back( riter.getTerm( k ) );
}
Node n = d_qe->getInstantiation( f, vars, terms );
Node val = fm->getValue( n );
if( val!=fm->d_true ){
- Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl;
- Trace("quant-model-warn") << " " << f << std::endl;
- Trace("quant-model-warn") << " Evaluates to " << val << std::endl;
+ Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl;
+ Trace("quant-check-model") << " " << f << std::endl;
+ Trace("quant-check-model") << " Evaluates to " << val << std::endl;
bad++;
}
riter.increment();
}
- Trace("quant-model-warn") << "Tested " << tests << " instantiations";
+ Trace("quant-check-model") << "Tested " << tests << " instantiations";
if( bad>0 ){
- Trace("quant-model-warn") << ", " << bad << " failed" << std::endl;
+ Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
}
- Trace("quant-model-warn") << "." << std::endl;
+ Trace("quant-check-model") << "." << std::endl;
}else{
- Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl;
+ Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
}
}
}
@@ -149,17 +149,21 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
if( optUseModel() ){
Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
//check if any quantifiers are un-initialized
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
int lems = initializeQuantifier( f, f );
d_statistics.d_init_inst_gen_lemmas += lems;
d_addedLemmas += lems;
+ if( d_qe->inConflict() ){
+ break;
+ }
}
}
if( d_addedLemmas>0 ){
Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
}else{
+ Assert( !d_qe->inConflict() );
//initialize model
fm->initialize();
//analyze the functions
@@ -169,7 +173,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
d_quant_sat.clear();
d_uf_prefs.clear();
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
analyzeQuantifier( fm, f );
@@ -186,7 +190,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
d_numQuantNoSelForm = 0;
//now, see if we know that any exceptions via InstGen exist
Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
int lems = doInstGen( fm, f );
@@ -202,7 +206,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
}else{
d_numQuantNoSelForm++;
}
- if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
+ if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
break;
}
}else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
@@ -276,7 +280,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
//try to add it
Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
//add model basis instantiation
- if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){
+ if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){
d_quant_basis_match_added[f] = true;
return 1;
}else{
@@ -426,8 +430,11 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
//add as instantiation
- if( d_qe->addInstantiation( f, m ) ){
+ if( d_qe->addInstantiation( f, m, true ) ){
d_addedLemmas++;
+ if( d_qe->inConflict() ){
+ break;
+ }
//if the instantiation is show to be false, and we wish to skip multiple instantiations at once
if( eval==-1 ){
riter.increment2( depIndex );
@@ -660,7 +667,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
//if applicable, try to add exceptions here
if( !tr_terms.empty() ){
//make a trigger for these terms, add instantiations
- inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW, options::smartTriggers() );
+ inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW );
//Notice() << "Trigger = " << (*tr) << std::endl;
tr->resetInstantiationRound();
tr->reset( Node::null() );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback