diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 788 |
1 files changed, 554 insertions, 234 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 66b92e1de..6fa02a8d3 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -24,8 +24,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/quantifiers_attributes.h" - -#define RECONSIDER_FUNC_CONSTANT +#include "theory/quantifiers/inst_gen.h" using namespace std; using namespace CVC4; @@ -58,43 +57,98 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { d_addedLemmas = 0; //only construct first order model if optUseModel() is true if( optUseModel() ){ - //initialize model - fm->initialize( d_considerAxioms ); - //analyze the functions - Trace("model-engine-debug") << "Analyzing model..." << std::endl; - analyzeModel( fm ); - //analyze the quantifiers - Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; - analyzeQuantifiers( fm ); - //if applicable, find exceptions - if( optInstGen() ){ - //now, see if we know that any exceptions via InstGen exist - Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; + if( optUseModel() ){ + //check if any quantifiers are un-initialized for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - if( isQuantifierActive( f ) ){ - d_addedLemmas += doInstGen( fm, f ); - if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ - break; + d_addedLemmas += initializeQuantifier( f ); + } + } + if( d_addedLemmas>0 ){ + Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; + }else{ + //initialize model + fm->initialize( d_considerAxioms ); + //analyze the functions + Trace("model-engine-debug") << "Analyzing model..." << std::endl; + analyzeModel( fm ); + //analyze the quantifiers + Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; + d_quant_sat.clear(); + d_uf_prefs.clear(); + analyzeQuantifiers( fm ); + //if applicable, find exceptions + if( optInstGen() ){ + //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++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + d_addedLemmas += doInstGen( fm, f ); + if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ + break; + } } } - } - if( Trace.isOn("model-engine") ){ - if( d_addedLemmas>0 ){ - Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Trace("model-engine") << "No InstGen lemmas..." << std::endl; + if( Trace.isOn("model-engine") ){ + if( d_addedLemmas>0 ){ + Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + }else{ + Trace("model-engine") << "No InstGen lemmas..." << std::endl; + } } } + if( d_addedLemmas==0 ){ + //if no immediate exceptions, build the model + // this model will be an approximation that will need to be tested via exhaustive instantiation + Trace("model-engine-debug") << "Building model..." << std::endl; + constructModel( fm ); + } } - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Trace("model-engine-debug") << "Building model..." << std::endl; - constructModel( fm ); + } + } +} + +int ModelEngineBuilder::initializeQuantifier( Node f ){ + if( d_quant_init.find( f )==d_quant_init.end() ){ + d_quant_init[f] = true; + Debug("inst-fmf-init") << "Initialize " << f << std::endl; + //add the model basis instantiation + // This will help produce the necessary information for model completion. + // We do this by extending distinguish ground assertions (those + // containing terms with "model basis" attribute) to hold for all cases. + + ////first, check if any variables are required to be equal + //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); + // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ + // Node n = it->first; + // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){ + // Notice() << "Unhandled phase req: " << n << std::endl; + // } + //} + std::vector< Node > vars; + std::vector< Node > terms; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, j ); + Node t = d_qe->getTermDatabase()->getModelBasisTerm( ic.getType() ); + vars.push_back( f[0][j] ); + terms.push_back( t ); + //calculate the basis match for f + d_quant_basis_match[f].set( ic, t); + } + ++(d_statistics.d_num_quants_init); + if( optInstGen() ){ + //add model basis instantiation + if( d_qe->addInstantiation( f, vars, terms ) ){ + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + ++(d_statistics.d_num_quants_init_fail); } } } + return 0; } void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ @@ -127,197 +181,6 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } -void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ - d_quant_sat.clear(); - d_quant_selection_lit.clear(); - d_quant_selection_lit_candidates.clear(); - d_quant_selection_lit_terms.clear(); - d_term_selection_lit.clear(); - d_op_selection_terms.clear(); - d_uf_prefs.clear(); - int quantSatInit = 0; - int nquantSatInit = 0; - //analyze the preferences of each quantifier - for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( isQuantifierActive( f ) ){ - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - //the pro/con preferences for this quantifier - std::vector< Node > pro_con[2]; - //the terms in the selection literal we choose - std::vector< Node > selectionLitTerms; - //for each asserted quantifier f, - // - determine selection literals - // - check which function/predicates have good and bad definitions for satisfying f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ - //the literal n is phase-required for quantifier f - Node n = it->first; - Node gn = d_qe->getTermDatabase()->getModelBasis( n ); - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - bool value; - //if the corresponding ground abstraction literal has a SAT value - if( d_qe->getValuation().hasSatValue( gn, value ) ){ - //collect the non-ground uf terms that this literal contains - // and compute if all of the symbols in this literal have - // constant definitions. - bool isConst = true; - std::vector< Node > uf_terms; - if( n.hasAttribute(InstConstantAttribute()) ){ - isConst = false; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ - if( n[j].getKind()==APPLY_UF && - fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull(); - }else{ - isConst = false; - } - } - } - } - } - //check if the value in the SAT solver matches the preference according to the quantifier - int pref = 0; - if( value!=it->second ){ - //we have a possible selection literal - bool selectLit = d_quant_selection_lit[f].isNull(); - bool selectLitConstraints = true; - //it is a constantly defined selection literal : the quantifier is sat - if( isConst ){ - selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end(); - d_quant_sat[f] = true; - //check if choosing this literal would add any additional constraints to default definitions - selectLitConstraints = false; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - if( d_uf_prefs[op].d_reconsiderModel ){ - selectLitConstraints = true; - } - } - if( !selectLitConstraints ){ - selectLit = true; - } - } - //see if we wish to choose this as a selection literal - d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); - if( selectLit ){ - Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; - d_quant_selection_lit[f] = value ? n : n.notNode(); - selectionLitTerms.clear(); - selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); - if( !selectLitConstraints ){ - break; - } - } - pref = 1; - }else{ - pref = -1; - } - //if we are not yet SAT, so we will add to preferences - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] ); - } - } - } - } - //process information about selection literal for f - if( !d_quant_selection_lit[f].isNull() ){ - d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() ); - for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ - d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f]; - d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] ); - } - }else{ - Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl; - } - //process information about requirements and preferences of quantifier f - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; - for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ - Debug("fmf-model-prefs") << selectionLitTerms[i] << " "; - d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false; - } - Debug("fmf-model-prefs") << std::endl; - quantSatInit++; - ++(d_statistics.d_pre_sat_quant); - }else{ - nquantSatInit++; - ++(d_statistics.d_pre_nsat_quant); - //note quantifier's value preferences to models - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); - } - } - } - } - } - Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; -} - -int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ - int addedLemmas = 0; - //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. - //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, - // effectively acting as partial instantiations instead of pointwise instantiations. - if( !d_quant_selection_lit[f].isNull() ){ - Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; - for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){ - bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; - Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); - std::vector< Node > tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ - if( lit[j].getKind()==APPLY_UF ){ - tr_terms.push_back( lit[j] ); - }else{ - tr_terms.clear(); - break; - } - } - } - if( tr_terms.size()==1 && !phase ){ - //equality between a function and a ground term, use literal matching - tr_terms.clear(); - tr_terms.push_back( lit ); - } - } - //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 ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); - } - } - } - return addedLemmas; -} - void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){ //build model for UF for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ @@ -337,20 +200,21 @@ void ModelEngineBuilder::constructModel( FirstOrderModel* fm ){ } void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ -#ifdef RECONSIDER_FUNC_CONSTANT - if( d_uf_model_constructed[op] ){ - if( d_uf_prefs[op].d_reconsiderModel ){ - //if we are allowed to reconsider default value, then see if the default value can be improved - Node v = d_uf_prefs[op].d_const_val; - if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ - Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; - fm->d_uf_model_tree[op].clear(); - fm->d_uf_model_gen[op].clear(); - d_uf_model_constructed[op] = false; + if( optReconsiderFuncConstants() ){ + //reconsider constant functions that weren't necessary + if( d_uf_model_constructed[op] ){ + if( d_uf_prefs[op].d_reconsiderModel ){ + //if we are allowed to reconsider default value, then see if the default value can be improved + Node v = d_uf_prefs[op].d_const_val; + if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ + Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; + fm->d_uf_model_tree[op].clear(); + fm->d_uf_model_gen[op].clear(); + d_uf_model_constructed[op] = false; + } } } } -#endif if( !d_uf_model_constructed[op] ){ //construct the model for the uninterpretted function/predicate bool setDefaultVal = true; @@ -359,7 +223,6 @@ void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ //set the values in the model for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ Node n = fm->d_uf_terms[op][i]; - d_qe->getTermDatabase()->computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ Node v = fm->getRepresentative( n ); //if this assertion did not help the model, just consider it ground @@ -372,7 +235,7 @@ void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ //also set as default value if necessary //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){ - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( shouldSetDefaultValue( n ) ){ fm->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ //incidentally already set, we will not need to find a default value @@ -415,23 +278,480 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ return options::fmfInstGenOneQuantPerRound(); } +bool ModelEngineBuilder::optReconsiderFuncConstants(){ + return false; +} + void ModelEngineBuilder::setEffort( int effort ){ d_considerAxioms = effort>=1; } ModelEngineBuilder::Statistics::Statistics(): d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), - d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0) + d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0), + d_num_quants_init("ModelEngine::Num_Quants", 0 ), + d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 ) { StatisticsRegistry::registerStat(&d_pre_sat_quant); StatisticsRegistry::registerStat(&d_pre_nsat_quant); + StatisticsRegistry::registerStat(&d_num_quants_init); + StatisticsRegistry::registerStat(&d_num_quants_init_fail); } ModelEngineBuilder::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_pre_sat_quant); StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); + StatisticsRegistry::unregisterStat(&d_num_quants_init); + StatisticsRegistry::unregisterStat(&d_num_quants_init_fail); } bool ModelEngineBuilder::isQuantifierActive( Node f ){ return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } + + + + + +void ModelEngineBuilderDefault::analyzeQuantifiers( FirstOrderModel* fm ){ + d_quant_selection_lit.clear(); + d_quant_selection_lit_candidates.clear(); + d_quant_selection_lit_terms.clear(); + d_term_selection_lit.clear(); + d_op_selection_terms.clear(); + //analyze each quantifier + for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + analyzeQuantifier( fm, f ); + } + } +} + + +void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; + //the pro/con preferences for this quantifier + std::vector< Node > pro_con[2]; + //the terms in the selection literal we choose + std::vector< Node > selectionLitTerms; + //for each asserted quantifier f, + // - determine selection literals + // - check which function/predicates have good and bad definitions for satisfying f + for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); + it != d_qe->d_phase_reqs[f].end(); ++it ){ + //the literal n is phase-required for quantifier f + Node n = it->first; + Node gn = d_qe->getTermDatabase()->getModelBasis( f, n ); + Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; + bool value; + //if the corresponding ground abstraction literal has a SAT value + if( d_qe->getValuation().hasSatValue( gn, value ) ){ + //collect the non-ground uf terms that this literal contains + // and compute if all of the symbols in this literal have + // constant definitions. + bool isConst = true; + std::vector< Node > uf_terms; + if( n.hasAttribute(InstConstantAttribute()) ){ + isConst = false; + if( gn.getKind()==APPLY_UF ){ + uf_terms.push_back( gn ); + isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull(); + }else if( gn.getKind()==EQUAL ){ + isConst = true; + for( int j=0; j<2; j++ ){ + if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( n[j].getKind()==APPLY_UF && + fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ + uf_terms.push_back( gn[j] ); + isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull(); + }else{ + isConst = false; + } + } + } + } + } + //check if the value in the SAT solver matches the preference according to the quantifier + int pref = 0; + if( value!=it->second ){ + //we have a possible selection literal + bool selectLit = d_quant_selection_lit[f].isNull(); + bool selectLitConstraints = true; + //it is a constantly defined selection literal : the quantifier is sat + if( isConst ){ + selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end(); + d_quant_sat[f] = true; + //check if choosing this literal would add any additional constraints to default definitions + selectLitConstraints = false; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + Node op = uf_terms[j].getOperator(); + if( d_uf_prefs[op].d_reconsiderModel ){ + selectLitConstraints = true; + } + } + if( !selectLitConstraints ){ + selectLit = true; + } + } + //see if we wish to choose this as a selection literal + d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); + if( selectLit ){ + Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; + d_quant_selection_lit[f] = value ? n : n.notNode(); + selectionLitTerms.clear(); + selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); + if( !selectLitConstraints ){ + break; + } + } + pref = 1; + }else{ + pref = -1; + } + //if we are not yet SAT, so we will add to preferences + if( d_quant_sat.find( f )==d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); + Debug("fmf-model-prefs") << " the definition of " << n << std::endl; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] ); + } + } + } + } + //process information about selection literal for f + if( !d_quant_selection_lit[f].isNull() ){ + d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() ); + for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ + d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f]; + d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] ); + } + }else{ + Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl; + } + //process information about requirements and preferences of quantifier f + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; + for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ + Debug("fmf-model-prefs") << selectionLitTerms[i] << " "; + d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false; + } + Debug("fmf-model-prefs") << std::endl; + ++(d_statistics.d_pre_sat_quant); + }else{ + ++(d_statistics.d_pre_nsat_quant); + //note quantifier's value preferences to models + for( int k=0; k<2; k++ ){ + for( int j=0; j<(int)pro_con[k].size(); j++ ){ + Node op = pro_con[k][j].getOperator(); + Node r = fm->getRepresentative( pro_con[k][j] ); + d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + } + } + } +} + +int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ + int addedLemmas = 0; + //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. + //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, + // effectively acting as partial instantiations instead of pointwise instantiations. + if( !d_quant_selection_lit[f].isNull() ){ + Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; + for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){ + bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; + Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; + Assert( lit.hasAttribute(InstConstantAttribute()) ); + std::vector< Node > tr_terms; + if( lit.getKind()==APPLY_UF ){ + //only match predicates that are contrary to this one, use literal matching + Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + tr_terms.push_back( eq ); + }else if( lit.getKind()==EQUAL ){ + //collect trigger terms + for( int j=0; j<2; j++ ){ + if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( lit[j].getKind()==APPLY_UF ){ + tr_terms.push_back( lit[j] ); + }else{ + tr_terms.clear(); + break; + } + } + } + if( tr_terms.size()==1 && !phase ){ + //equality between a function and a ground term, use literal matching + tr_terms.clear(); + tr_terms.push_back( lit ); + } + } + //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 ); + //Notice() << "Trigger = " << (*tr) << std::endl; + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + //d_qe->d_optInstMakeRepresentative = false; + //d_qe->d_optMatchIgnoreModelBasis = true; + addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); + } + } + } + return addedLemmas; +} + +bool ModelEngineBuilderDefault::shouldSetDefaultValue( Node n ){ + return n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1; +} + + + + + +void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){ + //for new inst gen + d_quant_selection_formula.clear(); + d_term_selected.clear(); + //analyze each quantifier + for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + analyzeQuantifier( fm, f ); + } + } + //analyze each partially instantiated quantifier + for( std::map< Node, Node >::iterator it = d_sub_quant_parent.begin(); it != d_sub_quant_parent.end(); ++it ){ + Node fp = getParentQuantifier( it->first ); + if( isQuantifierActive( fp ) ){ + analyzeQuantifier( fm, it->first ); + } + } +} + +void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + //determine selection formula, set terms in selection formula as being selected + Node s = getSelectionFormula( d_qe->getTermDatabase()->getCounterexampleBody( f ), + d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); + Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl; + if( !s.isNull() ){ + d_quant_selection_formula[f] = s; + Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); + setSelectedTerms( gs ); + } +} + + +int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ + int addedLemmas = 0; + //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. + //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, + // effectively acting as partial instantiations instead of pointwise instantiations. + if( !d_quant_selection_formula[f].isNull() ){ + //first, try on sub quantifiers + for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ + addedLemmas += doInstGen( fm, d_sub_quants[f][i] ); + } + if( addedLemmas>0 ){ + return addedLemmas; + }else{ + Node fp = getParentQuantifier( f ); + Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; + Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl; + //get all possible values of selection formula + InstGenProcess igp( d_quant_selection_formula[f] ); + igp.calculateMatches( d_qe, f ); + Trace("inst-gen-debug") << "Add inst-gen instantiations..." << std::endl; + for( int i=0; i<igp.getNumMatches(); i++ ){ + //if the match is not already true in the model + if( igp.getMatchValue( i )!=fm->d_true ){ + InstMatch m; + igp.getMatch( d_qe->getEqualityQuery(), i, m ); + //we only consider matches that are non-empty + // matches that are empty should trigger other instances that are non-empty + if( !m.empty() ){ + bool addInst = false; + //translate to be in terms match in terms of fp + InstMatch mp; + getParentQuantifierMatch( mp, fp, m, f ); + + //if this is a partial instantion + if( !m.isComplete( f ) ){ + Trace("inst-gen-debug") << "- partial inst" << std::endl; + //if the instantiation does not yet exist + if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true, NULL ) ){ + //get the partial instantiation pf + Node pf = d_qe->getInstantiation( fp, mp ); + Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; + Trace("inst-gen-pi") << " " << pf << std::endl; + d_sub_quants[ f ].push_back( pf ); + d_sub_quant_inst[ pf ] = InstMatch( &mp ); + d_sub_quant_parent[ pf ] = fp; + mp.add( d_quant_basis_match[ fp ] ); + addInst = true; + } + }else{ + addInst = true; + } + if( addInst ){ + Trace("inst-gen-debug") << "- complete inst" << std::endl; + //otherwise, get instantiation and add ground instantiation in terms of root parent + if( d_qe->addInstantiation( fp, mp ) ){ + addedLemmas++; + } + } + } + } + } + if( addedLemmas==0 ){ + //all sub quantifiers must be satisfied as well + bool subQuantSat = true; + for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ + if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){ + subQuantSat = false; + break; + } + } + if( subQuantSat ){ + d_quant_sat[ f ] = true; + } + } + Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl; + } + } + return addedLemmas; +} + +bool ModelEngineBuilderInstGen::shouldSetDefaultValue( Node n ){ + return d_term_selected.find( n )!=d_term_selected.end(); +} + +//if possible, returns a formula n' such that ( n' <=> polarity ) => ( n <=> polarity ), and ( n' <=> polarity ) is true in the current context, +// and NULL otherwise +Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ + if( n.getKind()==NOT ){ + Node nn = getSelectionFormula( fn[0], n[0], !polarity, useOption ); + if( !nn.isNull() ){ + return nn.negate(); + } + }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){ + //whether we only need to find one or all + bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity ); + std::vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i]; + Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i]; + Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); + if( nn.isNull()!=posPol ){ //TODO: may want to weaken selection formula + return nn; + } + children.push_back( nn ); + } + if( !posPol ){ + return NodeManager::currentNM()->mkNode( n.getKind()==AND ? AND : OR, children ); + } + }else if( n.getKind()==ITE ){ + Node nn; + Node nc[2]; + //get selection formula for the + for( int i=0; i<2; i++ ){ + nn = getSelectionFormula( i==0 ? fn[0] : fn[0].negate(), i==0 ? n[0] : n[0].negate(), true, useOption ); + nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption ); + if( !nn.isNull() && !nc[i].isNull() ){ + return NodeManager::currentNM()->mkNode( AND, nn, nc[i] ); + } + } + if( !nc[0].isNull() && !nc[1].isNull() ){ + return NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] ); + } + }else if( n.getKind()==IFF || n.getKind()==XOR ){ + bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF; + for( int p=0; p<2; p++ ){ + Node nn[2]; + for( int i=0; i<2; i++ ){ + bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 ); + nn[i] = getSelectionFormula( pol ? fn[i] : fn[i].negate(), pol ? n[i] : n[i].negate(), true, useOption ); + if( nn[i].isNull() ){ + break; + } + } + if( !nn[0].isNull() && !nn[1].isNull() ){ + return NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] ); + } + } + }else{ + //literal case + //first, check if it is a usable selection literal + if( isUsableSelectionLiteral( n, useOption ) ){ + bool value; + if( d_qe->getValuation().hasSatValue( n, value ) ){ + if( value==polarity ){ + return fn; + } + } + } + } + return Node::null(); +} + +void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ + + //if it is apply uf and has model basis arguments, then mark term as being "selected" + if( s.getKind()==APPLY_UF ){ + Assert( s.hasAttribute(ModelBasisArgAttribute()) ); + if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; + if( s.getAttribute(ModelBasisArgAttribute())==1 ){ + d_term_selected[ s ] = true; + Trace("sel-form") << " " << s << " is a selected term." << std::endl; + } + } + for( int i=0; i<(int)s.getNumChildren(); i++ ){ + setSelectedTerms( s[i] ); + } +} + +bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ + if( n.getKind()==FORALL ){ + return false; + }else if( n.getKind()!=APPLY_UF ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + //if it is a variable, then return false + if( n[i].getAttribute(ModelBasisAttribute()) ){ + return false; + } + } + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( !isUsableSelectionLiteral( n[i], useOption ) ){ + return false; + } + } + return true; +} + +Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){ + std::map< Node, Node >::iterator it = d_sub_quant_parent.find( f ); + if( it==d_sub_quant_parent.end() ){ + return f; + }else{ + return getParentQuantifier( it->second ); + } +} + +void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ + int counter = 0; + for( size_t i=0; i<fp[0].getNumChildren(); i++ ){ + Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i ); + if( fp[0][i]==f[0][counter] ){ + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter ); + Node n = m.getValue( ic ); + if( !n.isNull() ){ + mp.setMatch( d_qe->getEqualityQuery(), icp, n ); + } + counter++; + } + } + mp.add( d_sub_quant_inst[f] ); +} + |