diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 59 |
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() ); |