From b11f6d3a27d33b9075e57b37f77ad9d11732fce5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Oct 2012 15:28:24 +0000 Subject: [PATCH] more updates to inst gen: fixed partial instantiations, recognize duplicate defaults for uf --- src/theory/model.cpp | 8 +- src/theory/quantifiers/first_order_model.cpp | 4 +- src/theory/quantifiers/inst_gen.cpp | 28 +- src/theory/quantifiers/model_builder.cpp | 429 +++++++++++-------- src/theory/quantifiers/model_builder.h | 77 ++-- src/theory/quantifiers_engine.cpp | 14 +- src/theory/quantifiers_engine.h | 6 +- src/theory/uf/theory_uf_model.cpp | 16 +- 8 files changed, 343 insertions(+), 239 deletions(-) diff --git a/src/theory/model.cpp b/src/theory/model.cpp index dad1b5fe6..3a3f706ac 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -317,15 +317,15 @@ bool TheoryModel::areDisequal( Node a, Node b ){ //for debugging void TheoryModel::printRepresentativeDebug( const char* c, Node r ){ if( r.isNull() ){ - Debug( c ) << "null"; + Trace( c ) << "null"; }else if( r.getType().isBoolean() ){ if( areEqual( r, d_true ) ){ - Debug( c ) << "true"; + Trace( c ) << "true"; }else{ - Debug( c ) << "false"; + Trace( c ) << "false"; } }else{ - Debug( c ) << getRepresentative( r ); + Trace( c ) << getRepresentative( r ); } } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 28eeca624..3d98674a8 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -338,9 +338,9 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ //val = getRepresentative( val ); } } - Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; + Trace("fmf-eval-debug") << "Evaluate term " << n << " = "; printRepresentativeDebug( "fmf-eval-debug", val ); - Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; + Trace("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; } } return val; diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 099e3aa29..b4aed6021 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -61,7 +61,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ return; } } - Trace("cm") << "calculate matches " << d_node << std::endl; + Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl; //get the model FirstOrderModel* fm = qe->getModel(); if( d_node.getKind()==APPLY_UF ){ @@ -74,7 +74,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ for( int t=(isSelected ? 0 : 1); t<2; t++ ){ //do not consider ground case if it is already congruent to another ground term if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ - Trace("cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl; + Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl; bool success = true; InstMatch curr; for( size_t j=0; jgetEqualityQuery(), d_node[j], n[j] ) ){ - Trace("cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl; - Trace("cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl; + Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl; + Trace("inst-gen-cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl; success = false; break; } }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){ - Trace("cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; + Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; success = false; break; } @@ -110,7 +110,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ std::vector< Node > terms; calculateMatchesInterpreted( qe, f, curr, terms, 0 ); } - Trace("cm") << "done calculate matches" << std::endl; + Trace("inst-gen-cm") << "done calculate matches" << std::endl; //can clear information used for finding duplicates d_inst_trie.clear(); } @@ -123,11 +123,11 @@ bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){ void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){ if( childIndex==(int)d_children.size() ){ Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct? - Trace("cm") << " - u-match : " << val << std::endl; - Trace("cm") << " : " << curr << std::endl; + Trace("inst-gen-cm") << " - u-match : " << val << std::endl; + Trace("inst-gen-cm") << " : " << curr << std::endl; addMatchValue( qe, f, val, curr ); }else{ - Trace("cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl; + Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl; bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) ); for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){ //FIXME: is this correct? @@ -136,11 +136,11 @@ void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){ calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected ); }else{ - Trace("cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl; - Trace("cm") << childIndex << " match " << i << " not equal subs." << std::endl; + Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl; + Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl; } }else{ - Trace("cm") << childIndex << " match " << i << " not equal value." << std::endl; + Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl; } } } @@ -158,8 +158,8 @@ void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms ); val = Rewriter::rewrite( val ); } - Trace("cm") << " - i-match : " << val << std::endl; - Trace("cm") << " : " << curr << std::endl; + Trace("inst-gen-cm") << " - i-match : " << val << std::endl; + Trace("inst-gen-cm") << " : " << curr << std::endl; addMatchValue( qe, f, val, curr ); }else{ if( d_children_map.find( argIndex )==d_children_map.end() ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 4c30f6841..f61083029 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -33,6 +33,26 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ + if( argIndex<(int)n.getNumChildren() ){ + Node r; + if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ + r = n[ argIndex ]; + }else{ + r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); + } + std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); + if( it==d_data.end() ){ + d_data[r].addTerm2( qe, n, argIndex+1 ); + return true; + }else{ + return it->second.addTerm2( qe, n, argIndex+1 ); + } + }else{ + return false; + } +} + ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) : TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ), d_curr_model( c, NULL ){ @@ -53,17 +73,46 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { TheoryEngineModelBuilder::processBuildModel( m, fullModel ); //mark that the model has been set fm->markModelSet(); + //FOR DEBUGGING + if( Trace.isOn("quant-model-warn") ){ + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + std::vector< Node > vars; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + vars.push_back( f[0][j] ); + } + RepSetIterator riter( &(fm->d_rep_set) ); + riter.setQuantifier( f ); + while( !riter.isFinished() ){ + std::vector< Node > terms; + for( int i=0; igetInstantiation( 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; + } + riter.increment(); + } + } + } }else{ d_curr_model = fm; //build model for relevant symbols contained in quantified formulas d_addedLemmas = 0; + //reset the internal information + reset( fm ); //only construct first order model if optUseModel() is true if( optUseModel() ){ - if( optUseModel() ){ - //check if any quantifiers are un-initialized - for( int i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - d_addedLemmas += initializeQuantifier( f ); + Trace("model-engine") << "Initializing quantifiers..." << std::endl; + //check if any quantifiers are un-initialized + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + d_addedLemmas += initializeQuantifier( f, f ); } } if( d_addedLemmas>0 ){ @@ -78,7 +127,12 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; d_quant_sat.clear(); d_uf_prefs.clear(); - analyzeQuantifiers( fm ); + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( isQuantifierActive( f ) ){ + analyzeQuantifier( fm, f ); + } + } //if applicable, find exceptions if( optInstGen() ){ //now, see if we know that any exceptions via InstGen exist @@ -104,49 +158,65 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { //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 ); + //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 ){ + constructModelUf( fm, it->first ); + } + /* + //build model for arrays + for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){ + //consult the model basis select term + // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term + TypeNode tn = it->first.getType(); + Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) ); + it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) ); + } + */ + Trace("model-engine-debug") << "Done building models." << std::endl; } } } } } -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); +int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ + if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ + //create the basis match if necessary + if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ + Trace("inst-fmf-init") << "Initialize " << f << ", parent = " << fp << 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; + // } + //} + 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() ); + //calculate the basis match for f + d_quant_basis_match[f].set( ic, t); + } + ++(d_statistics.d_num_quants_init); } - ++(d_statistics.d_num_quants_init); + //try to add it if( optInstGen() ){ + Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; //add model basis instantiation - if( d_qe->addInstantiation( f, vars, terms ) ){ + if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ + d_quant_basis_match_added[f] = true; + ++(d_statistics.d_num_quants_init_success); 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); + d_quant_basis_match_added[f] = false; } } } @@ -158,8 +228,10 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ //determine if any functions are constant for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ Node op = it->first; + TermArgBasisTrie tabt; for( size_t i=0; id_uf_terms[op].size(); i++ ){ Node n = fm->d_uf_terms[op][i]; + //for calculating if op is constant if( !n.getAttribute(NoMatchAttribute()) ){ Node v = fm->getRepresentative( n ); if( i==0 ){ @@ -169,6 +241,14 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ break; } } + //for calculating terms that we don't need to consider + if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + //need to consider if it is not congruent modulo model basis + if( !tabt.addTerm( d_qe, n ) ){ + BasisNoMatchAttribute bnma; + n.setAttribute(bnma,true); + } + } } if( !d_uf_prefs[op].d_const_val.isNull() ){ fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); @@ -183,91 +263,6 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } -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 ){ - constructModelUf( fm, it->first ); - } - /* - //build model for arrays - for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){ - //consult the model basis select term - // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term - TypeNode tn = it->first.getType(); - Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) ); - it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) ); - } - */ - Trace("model-engine-debug") << "Done building models." << std::endl; -} - -void ModelEngineBuilder::constructModelUf( FirstOrderModel* fm, Node op ){ - 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; - } - } - } - } - if( !d_uf_model_constructed[op] ){ - //construct the model for the uninterpretted function/predicate - bool setDefaultVal = true; - Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; - //set the values in the model - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; - 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 - //set n = v in the model tree - Debug("fmf-model-cons") << " Set " << n << " = "; - fm->printRepresentativeDebug( "fmf-model-cons", v ); - Debug("fmf-model-cons") << std::endl; - //set it as ground value - fm->d_uf_model_gen[op].setValue( fm, n, v ); - 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( 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 - setDefaultVal = false; - } - } - }else{ - if( n==defaultTerm ){ - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - } - } - //set the overall default value if not set already (is this necessary??) - if( setDefaultVal ){ - Debug("fmf-model-cons") << " Choose default value..." << std::endl; - //chose defaultVal based on heuristic, currently the best ratio of "pro" responses - Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - Assert( !defaultVal.isNull() ); - fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); - } - Debug("fmf-model-cons") << " Making model..."; - fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); - d_uf_model_constructed[op] = true; - Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; - } -} - bool ModelEngineBuilder::optUseModel() { return options::fmfModelBasedInst(); } @@ -280,10 +275,6 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ return options::fmfInstGenOneQuantPerRound(); } -bool ModelEngineBuilder::optReconsiderFuncConstants(){ - return false; -} - void ModelEngineBuilder::setEffort( int effort ){ d_considerAxioms = effort>=1; } @@ -292,45 +283,43 @@ 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_num_quants_init("ModelEngine::Num_Quants", 0 ), - d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 ) + d_num_quants_init_success("ModelEngine::Num_Quants_Inst_Gen_Success", 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); + StatisticsRegistry::registerStat(&d_num_quants_init_success); } 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); + StatisticsRegistry::unregisterStat(&d_num_quants_init_success); } bool ModelEngineBuilder::isQuantifierActive( Node f ){ return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } +bool ModelEngineBuilder::isTermActive( Node n ){ + return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term + ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments + //and is not congruent to another + //active term +} -void ModelEngineBuilderDefault::analyzeQuantifiers( FirstOrderModel* fm ){ +void ModelEngineBuilderDefault::reset( 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 @@ -506,35 +495,93 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ return addedLemmas; } -bool ModelEngineBuilderDefault::shouldSetDefaultValue( Node n ){ - return n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1; +void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ + 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; + } + } + } + } + if( !d_uf_model_constructed[op] ){ + //construct the model for the uninterpretted function/predicate + bool setDefaultVal = true; + Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; + //set the values in the model + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + if( isTermActive( n ) ){ + Node v = fm->getRepresentative( n ); + Trace("fmf-model-cons") << "Set term " << n << " : " << fm->d_rep_set.getIndexFor( v ) << " " << v << std::endl; + //if this assertion did not help the model, just consider it ground + //set n = v in the model tree + //set it as ground value + fm->d_uf_model_gen[op].setValue( fm, n, v ); + if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ + //also set as default value if necessary + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + Trace("fmf-model-cons") << " Set as default." << std::endl; + 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 + setDefaultVal = false; + } + } + }else{ + if( n==defaultTerm ){ + fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } + } + } + } + //set the overall default value if not set already (is this necessary??) + if( setDefaultVal ){ + Trace("fmf-model-cons") << " Choose default value..." << std::endl; + //chose defaultVal based on heuristic, currently the best ratio of "pro" responses + Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + Assert( !defaultVal.isNull() ); + Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl; + fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + } + Debug("fmf-model-cons") << " Making model..."; + fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + d_uf_model_constructed[op] = true; + Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; + } } -void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){ + +void ModelEngineBuilderInstGen::reset( 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 ); - } +} + +int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ + int addedLemmas = ModelEngineBuilder::initializeQuantifier( f, fp ); + for( size_t i=0; igetTermDatabase()->getInstConstantBody( f ), d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); @@ -542,17 +589,26 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) // s = Rewriter::rewrite( s ); //} d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f ); - Trace("sel-form") << "Selection formula " << f << std::endl; - Trace("sel-form") << " " << s << std::endl; + Trace("sel-form-debug") << "Selection formula " << f << std::endl; + Trace("sel-form-debug") << " " << s << std::endl; if( !s.isNull() ){ d_quant_selection_formula[f] = s; Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); setSelectedTerms( gs ); } + //analyze sub quantifiers + for( size_t i=0; i0 ){ + Trace("inst-gen") << " -> children added lemmas" << std::endl; 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] ); @@ -580,7 +635,6 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ //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; Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; //translate to be in terms match in terms of fp InstMatch mp; @@ -598,13 +652,11 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ d_sub_quant_inst[ pf ] = InstMatch( &mp ); d_sub_quant_parent[ pf ] = fp; mp.add( d_quant_basis_match[ fp ] ); - addInst = true; + d_quant_basis_match[ pf ] = InstMatch( &mp ); + addedLemmas += initializeQuantifier( pf, fp ); + Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; } }else{ - addInst = true; - } - if( addInst ){ - //otherwise, get instantiation and add ground instantiation in terms of root parent if( d_qe->addInstantiation( fp, mp ) ){ addedLemmas++; } @@ -625,16 +677,17 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ d_quant_sat[ f ] = true; } } + if( fp!=f ) Trace("inst-gen") << " "; Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl; + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + if( fp!=f ) Trace("inst-gen") << " "; + Trace("inst-gen") << " -> *** it is satisfied" << 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' => ( n <=> polarity ), and n' is true in the current context, // and NULL otherwise Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ @@ -704,8 +757,14 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar if( !polarity ){ ret = ret.negate(); } + }else{ + Trace("sel-form-debug") << " (wrong polarity)" << std::endl; } + }else{ + Trace("sel-form-debug") << " (does not have sat value)" << std::endl; } + }else{ + Trace("sel-form-debug") << " (is not usable literal)" << std::endl; } } Trace("sel-form-debug") << " return " << ret << std::endl; @@ -747,15 +806,6 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption 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() || it->second.isNull() ){ - return f; - }else{ - return it->second; - } -} - void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ if( f!=fp ){ //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl; @@ -780,3 +830,30 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp } } +void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ + bool setDefaultVal = true; + Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + //set the values in the model + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + Node n = fm->d_uf_terms[op][i]; + if( isTermActive( n ) ){ + Node v = fm->getRepresentative( n ); + fm->d_uf_model_gen[op].setValue( fm, n, v ); + } + //also possible set as default + if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){ + Node v = fm->getRepresentative( n ); + fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + if( n==defaultTerm ){ + setDefaultVal = false; + } + } + } + //set the overall default value if not set already (is this necessary??) + if( setDefaultVal ){ + Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + } + fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + d_uf_model_constructed[op] = true; +} \ No newline at end of file diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index a4c38d608..e2f422a0a 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -23,6 +23,27 @@ namespace CVC4 { namespace theory { + +/** Attribute true for nodes that should not be used when considered for inst-gen basis */ +struct BasisNoMatchAttributeId {}; +/** use the special for boolean flag */ +typedef expr::Attribute< BasisNoMatchAttributeId, + bool, + expr::attr::NullCleanupStrategy, + true // context dependent + > BasisNoMatchAttribute; + +class TermArgBasisTrie { +private: + bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); +public: + /** the data */ + std::map< Node, TermArgBasisTrie > d_data; +public: + bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } +};/* class TermArgBasisTrie */ + + namespace quantifiers { /** model builder class @@ -44,27 +65,25 @@ protected: //built model uf std::map< Node, bool > d_uf_model_constructed; /** process build model */ - void processBuildModel( TheoryModel* m, bool fullModel ); + virtual void processBuildModel( TheoryModel* m, bool fullModel ); protected: - //initialize quantifiers, return number of lemmas produced - int initializeQuantifier( Node f ); + //reset + virtual void reset( FirstOrderModel* fm ) = 0; + //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + virtual int initializeQuantifier( Node f, Node fp ); //analyze model - void analyzeModel( FirstOrderModel* fm ); + virtual void analyzeModel( FirstOrderModel* fm ); //analyze quantifiers - virtual void analyzeQuantifiers( FirstOrderModel* fm ) = 0; - //build model - void constructModel( FirstOrderModel* fm ); - //theory-specific build models - void constructModelUf( FirstOrderModel* fm, Node op ); - /** set default value */ - virtual bool shouldSetDefaultValue( Node n ) = 0; + virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0; //do InstGen techniques for quantifier, return number of lemmas produced virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; + //theory-specific build models + virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; protected: //map from quantifiers to if are SAT std::map< Node, bool > d_quant_sat; //which quantifiers have been initialized - std::map< Node, bool > d_quant_init; + std::map< Node, bool > d_quant_basis_match_added; //map from quantifiers to model basis match std::map< Node, InstMatch > d_quant_basis_match; public: @@ -81,20 +100,21 @@ public: virtual bool optUseModel(); virtual bool optInstGen(); virtual bool optOneQuantPerRoundInstGen(); - virtual bool optReconsiderFuncConstants(); /** statistics class */ class Statistics { public: IntStat d_pre_sat_quant; IntStat d_pre_nsat_quant; IntStat d_num_quants_init; - IntStat d_num_quants_init_fail; + IntStat d_num_quants_init_success; Statistics(); ~Statistics(); }; Statistics d_statistics; // is quantifier active? bool isQuantifierActive( Node f ); + // is term active + bool isTermActive( Node n ); // is term selected virtual bool isTermSelected( Node n ) { return false; } };/* class ModelEngineBuilder */ @@ -113,15 +133,14 @@ private: ///information for (old) InstGen //map from operators to terms that appear in selection literals std::map< Node, std::vector< Node > > d_op_selection_terms; protected: - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); - /** set default value */ - bool shouldSetDefaultValue( Node n ); -private: + //reset + void reset( FirstOrderModel* fm ); //analyze quantifier void analyzeQuantifier( FirstOrderModel* fm, Node f ); + //do InstGen techniques for quantifier, return number of lemmas produced + int doInstGen( FirstOrderModel* fm, Node f ); + //theory-specific build models + void constructModelUf( FirstOrderModel* fm, Node op ); public: ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} ~ModelEngineBuilderDefault(){} @@ -145,23 +164,23 @@ private: ///information for (new) InstGen //*root* parent of each partial instantiation std::map< Node, Node > d_sub_quant_parent; protected: - //analyze quantifiers - void analyzeQuantifiers( FirstOrderModel* fm ); + //reset + void reset( FirstOrderModel* fm ); + //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + int initializeQuantifier( Node f, Node fp ); + //analyze quantifier + void analyzeQuantifier( FirstOrderModel* fm, Node f ); //do InstGen techniques for quantifier, return number of lemmas produced int doInstGen( FirstOrderModel* fm, Node f ); - /** set default value */ - bool shouldSetDefaultValue( Node n ); + //theory-specific build models + void constructModelUf( FirstOrderModel* fm, Node op ); private: - //analyze quantifier - void analyzeQuantifier( FirstOrderModel* fm, Node f ); //get selection formula for quantifier body Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption ); //set selected terms in term void setSelectedTerms( Node s ); //is usable selection literal bool isUsableSelectionLiteral( Node n, int useOption ); - // get parent quantifier - Node getParentQuantifier( Node f ); //get parent quantifier match void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ); public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4ba5c39e6..4e933a511 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -94,6 +94,9 @@ Valuation& QuantifiersEngine::getValuation(){ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); + if( e>=Theory::EFFORT_FULL ){ + Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; + } d_hasAddedLemma = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -116,6 +119,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ d_te->getModelBuilder()->buildModel( d_model, true ); } + if( e>=Theory::EFFORT_FULL ){ + Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; + } } std::vector QuantifiersEngine::createInstVariable( std::vector & vars ){ @@ -311,14 +317,16 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m ){ +bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ //make sure there are values for each variable we are instantiating m.makeComplete( f, this ); //make it representative, this is helpful for recognizing duplication - m.makeRepresentative( this ); + if( mkRep ){ + m.makeRepresentative( this ); + } Trace("inst-add") << "Add instantiation: " << m << std::endl; //check for duplication modulo equality - if( !d_inst_match_trie[f].addInstMatch( this, f, m, true ) ){ + if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){ Trace("inst-add") << " -> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 62e5d983e..be8830710 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -157,6 +157,8 @@ public: private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); + /** instantiate f with arguments terms */ + bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -166,10 +168,8 @@ public: bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ bool addLemma( Node lem ); - /** instantiate f with arguments terms */ - bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** do instantiation specified by m */ - bool addInstantiation( Node f, InstMatch& m ); + bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index f7272f7ba..02e2412a4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -386,9 +386,9 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* for( size_t i=0; iprintRepresentativeDebug( "fmf-model-cons", v ); - Debug("fmf-model-cons") << " ) = " << score << std::endl; + Debug("fmf-model-cons-debug") << " - score( "; + m->printRepresentativeDebug( "fmf-model-cons-debug", v ); + Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; if( score>maxScore ){ defaultVal = v; maxScore = score; @@ -416,10 +416,10 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* } #endif //get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons") << " Choose "; - m->printRepresentativeDebug("fmf-model-cons", defaultVal ); - Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; - Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; + Debug("fmf-model-cons-debug") << " Choose "; + m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal ); + Debug("fmf-model-cons-debug") << " as default value (" << defaultTerm << ")" << std::endl; + Debug("fmf-model-cons-debug") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; + Debug("fmf-model-cons-debug") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; return defaultVal; } -- 2.30.2