From 1c779966545190efa59b019572237562eea66dbf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Nov 2012 20:54:11 +0000 Subject: [PATCH] more minor updates to inst gen and representative selection, clean up of equality query --- src/theory/quantifiers/inst_gen.cpp | 152 ++++++++++++++--------- src/theory/quantifiers/inst_match.cpp | 37 +++--- src/theory/quantifiers/inst_match.h | 8 +- src/theory/quantifiers/model_builder.cpp | 123 ++++++++++-------- src/theory/quantifiers/model_builder.h | 12 +- src/theory/quantifiers/model_engine.cpp | 34 ++--- src/theory/quantifiers/model_engine.h | 1 + src/theory/quantifiers/term_database.cpp | 55 +++++--- src/theory/quantifiers/term_database.h | 4 +- src/theory/quantifiers/trigger.cpp | 5 - src/theory/quantifiers_engine.cpp | 18 ++- src/theory/uf/inst_strategy.cpp | 28 ----- src/theory/uf/inst_strategy.h | 19 --- 13 files changed, 256 insertions(+), 240 deletions(-) diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 428a224ee..932a00185 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -19,7 +19,7 @@ #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/first_order_model.h" -#define RECONSIDER_FUNC_CONSTANT +//#define CHILD_USE_CONSIDER using namespace std; using namespace CVC4; @@ -55,6 +55,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins } void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){ + Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl; //whether we are doing a product or sum or matches bool doProduct = true; //get the model @@ -64,32 +65,25 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto std::vector< Node > considerTerms; std::vector< std::vector< Node > > newConsiderVal; std::vector< bool > newUseConsider; + std::map< Node, InstMatch > considerTermsMatch[2]; + std::map< Node, bool > considerTermsSuccess[2]; newConsiderVal.resize( d_children.size() ); - newUseConsider.resize( d_children.size(), false ); + newUseConsider.resize( d_children.size(), useConsider ); if( d_node.getKind()==APPLY_UF ){ Node op = d_node.getOperator(); if( useConsider ){ +#ifndef CHILD_USE_CONSIDER + for( size_t i=0; igetEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ), qe->getEqualityQuery()->getEngine() ); while( !eqc.isFinished() ){ Node en = (*eqc); if( en.getKind()==APPLY_UF && en.getOperator()==op ){ - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( en ); - bool isActive = !en.getAttribute(NoMatchAttribute()); - //check if we need to consider it - if( isSelected || isActive ){ considerTerms.push_back( en ); -#if 0 - for( int i=0; i<(int)d_children.size(); i++ ){ - int childIndex = d_children_index[i]; - Node n = qe->getModel()->getRepresentative( n ); - if( std::find( newConsiderVal[i].begin(), newConsiderVal[i].end(), n )==newConsiderVal[i].end() ){ - newConsiderVal[i].push_back( n ); - } - } -#endif - } } ++eqc; } @@ -97,23 +91,92 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto }else{ considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() ); } - }else if( d_node.getType().isBoolean() ){ - if( useConsider ){ - Assert( considerVal.size()==1 ); - bool reqPol = considerVal[0]==fm->d_true; - if( d_node.getKind()==NOT ){ - if( !newConsiderVal.empty() ){ - newConsiderVal[0].push_back( reqPol ? fm->d_false : fm->d_true ); - newUseConsider[0] = true; + //for each term we consider, calculate a current match + for( size_t i=0; igetModelEngine()->getModelBuilder()->isTermSelected( n ); + bool hadSuccess = false; + for( int t=(isSelected ? 0 : 1); t<2; t++ ){ + if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ + considerTermsMatch[t][n] = InstMatch(); + considerTermsSuccess[t][n] = true; + for( size_t j=0; jgetEqualityQuery(), d_node[j], n[j] ) ){ + Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to "; + Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl; + considerTermsSuccess[t][n] = false; + break; + } + }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){ + Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; + considerTermsSuccess[t][n] = false; + break; + } + } + } + } + //if successful, store it + if( considerTermsSuccess[t][n] ){ +#ifdef CHILD_USE_CONSIDER + if( !hadSuccess ){ + hadSuccess = true; + for( size_t k=0; kgetModel()->getRepresentative( n[childIndex] ); + if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){ + newConsiderVal[k].push_back( r ); + //check if we now need to consider the entire domain + TypeNode tn = r.getType(); + if( qe->getModel()->d_rep_set.hasType( tn ) ){ + if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){ + newConsiderVal[k].clear(); + newUseConsider[k] = false; + } + } + } + }else{ + //matching against selected term, will need to consider all values + newConsiderVal[k].clear(); + newUseConsider[k] = false; + } + } + } + } +#endif + } } - }else if( d_node.getKind()==AND || d_node.getKind()==OR ){ - for( size_t i=0; igetEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl; - success = false; - break; - } - }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){ - Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; - success = false; - break; - } - } - } - } - if( success ){ + if( considerTermsSuccess[t][n] ){ //try to find unifier for d_node = n - calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 ); + calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 ); } } } } - }else{ //if this is an interpreted function if( doProduct ){ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 4a89a4dd3..16f06017e 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -54,9 +54,11 @@ bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ bool InstMatch::add( InstMatch& m ){ for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[it->first] = it->second; + if( !it->second.isNull() ){ + std::map< Node, Node >::iterator itf = d_map.find( it->first ); + if( itf==d_map.end() || itf->second.isNull() ){ + d_map[it->first] = it->second; + } } } return true; @@ -91,7 +93,7 @@ void InstMatch::debugPrint( const char* c ){ // Debug( c ) << std::endl; //} } -/* + void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); @@ -101,27 +103,18 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } } -void InstMatch::makeInternal( QuantifiersEngine* qe ){ - if( options::cbqi() ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); - } - } - } +void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ + EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); + for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ + d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); } } -*/ + void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){ d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); } - //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){ - // d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); - //} } } @@ -132,8 +125,8 @@ void InstMatch::applyRewrite(){ } /** get value */ -Node InstMatch::getValue( Node var ){ - std::map< Node, Node >::iterator it = d_map.find( var ); +Node InstMatch::getValue( Node var ) const{ + std::map< Node, Node >::const_iterator it = d_map.find( var ); if( it!=d_map.end() ){ return it->second; }else{ @@ -145,7 +138,7 @@ Node InstMatch::getValue( Node var ){ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ if( long(index)d_order.size()) ) ){ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); d_data[n].addInstMatch2( qe, f, m, index+1, imtio ); } } @@ -156,7 +149,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& return true; }else{ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 43c0d26c7..41ebb63d2 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -55,13 +55,13 @@ public: /** is complete? */ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } /** make complete */ - //void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal: ensure that no term in d_map contains instantiation constants */ - //void makeInternal( QuantifiersEngine* qe ); + void makeComplete( Node f, QuantifiersEngine* qe ); + /** make internal representative */ + void makeInternalRepresentative( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** get value */ - Node getValue( Node var ); + Node getValue( Node var ) const; /** clear */ void clear(){ d_map.clear(); } /** is_empty */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 8b34a3a12..c7e68acb1 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -59,6 +59,35 @@ d_qe( qe ), d_curr_model( c, NULL ){ d_considerAxioms = true; } +void ModelEngineBuilder::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") ){ + 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(); + } + } + } +} + void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* fm = (FirstOrderModel*)m; if( fullModel ){ @@ -73,33 +102,8 @@ 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(); - } - } - } - //END FOR DEBUGGING + //debug the model + debugModel( fm ); }else{ d_curr_model = fm; d_addedLemmas = 0; @@ -113,7 +117,9 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { for( int i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ - d_addedLemmas += initializeQuantifier( f, f ); + int lems = initializeQuantifier( f, f ); + d_statistics.d_init_inst_gen_lemmas += lems; + d_addedLemmas += lems; } } if( d_addedLemmas>0 ){ @@ -128,14 +134,14 @@ void ModelEngineBuilder::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; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ analyzeQuantifier( fm, f ); } } - //if applicable, find exceptions + + //if applicable, find exceptions to model via inst-gen if( optInstGen() ){ d_didInstGen = true; d_instGenMatches = 0; @@ -148,10 +154,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { for( int i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ - int addedLemmas = doInstGen( fm, f ); - d_addedLemmas += addedLemmas; + int lems = doInstGen( fm, f ); + d_statistics.d_inst_gen_lemmas += lems; + d_addedLemmas += lems; //temporary - if( addedLemmas>0 ){ + if( lems>0 ){ d_numQuantInstGen++; }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ d_numQuantSat++; @@ -160,7 +167,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){ + if( optOneQuantPerRoundInstGen() && lems>0 ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -208,7 +215,7 @@ 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; + Trace("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 @@ -236,7 +243,6 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ //add model basis instantiation 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. @@ -322,22 +328,22 @@ void ModelEngineBuilder::setEffort( int effort ){ } 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_success("ModelEngine::Num_Quants_Inst_Gen_Success", 0 ) + d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0), + d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0), + d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ), + d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 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_success); + StatisticsRegistry::registerStat(&d_num_partial_quants_init); + StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); + StatisticsRegistry::registerStat(&d_inst_gen_lemmas); } 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_success); + StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); + StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); + StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); } bool ModelEngineBuilder::isQuantifierActive( Node f ){ @@ -470,9 +476,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) 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++ ){ @@ -604,12 +608,14 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) - +////////////////////// Inst-Gen style Model Builder /////////// void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ //for new inst gen d_quant_selection_formula.clear(); d_term_selected.clear(); + + //d_sub_quant_inst_trie.clear();//* } int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ @@ -621,6 +627,9 @@ int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ } void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + //Node fp = getParentQuantifier( f );//* + //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ); + //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//* Trace("sel-form-debug") << "* Analyze " << f << std::endl; //determine selection formula, set terms in selection formula as being selected Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ), @@ -659,9 +668,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; if( fp!=f ) Trace("inst-gen") << " "; Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula[f] << std::endl; - //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. + //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model. if( !d_quant_selection_formula[f].isNull() ){ //first, try on sub quantifiers bool subQuantSat = true; @@ -688,6 +695,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ if( igp.getMatchValue( i )!=fm->d_true ){ InstMatch m; igp.getMatch( d_qe->getEqualityQuery(), i, m ); + //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl; //we only consider matches that are non-empty // matches that are empty should trigger other instances that are non-empty if( !m.empty() ){ @@ -695,9 +703,12 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ //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 ) ){ + //need to make it internal here + //Trace("mkInternal") << "Make internal representative " << mp << std::endl; + //mp.makeInternalRepresentative( d_qe ); + //Trace("mkInternal") << "Got " << mp << std::endl; //if the instantiation does not yet exist if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ //also add it to children @@ -709,9 +720,11 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ d_sub_quants[ f ].push_back( pf ); d_sub_quant_inst[ pf ] = InstMatch( &mp ); d_sub_quant_parent[ pf ] = fp; - //now make the match mp complete + //now make mp a complete match mp.add( d_quant_basis_match[ fp ] ); d_quant_basis_match[ pf ] = InstMatch( &mp ); + ++(d_statistics.d_num_quants_init); + ++(d_statistics.d_num_partial_quants_init); addedLemmas += initializeQuantifier( pf, fp ); Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; subQuantSat = false; @@ -979,5 +992,5 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ) } bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ - return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, modInst ); + return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); } \ No newline at end of file diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 7331daf8e..908cfca2b 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -69,7 +69,7 @@ protected: protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; - //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + //initialize quantifiers, return number of lemmas produced virtual int initializeQuantifier( Node f, Node fp ); //analyze model virtual void analyzeModel( FirstOrderModel* fm ); @@ -98,6 +98,8 @@ public: bool d_considerAxioms; // set effort void setEffort( int effort ); + //debug model + void debugModel( FirstOrderModel* fm ); public: //whether to construct model virtual bool optUseModel(); @@ -110,10 +112,10 @@ public: /** 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_success; + IntStat d_num_partial_quants_init; + IntStat d_init_inst_gen_lemmas; + IntStat d_inst_gen_lemmas; Statistics(); ~Statistics(); }; @@ -180,7 +182,7 @@ private: ///information for (new) InstGen std::map< Node, bool > d_term_selected; //a collection of (complete) InstMatch structures produced for each root quantifier std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie; - //a collection of InstMatch structures, representing the children for each quantifier + //for each quantifier, a collection of InstMatch structures, representing the children std::map< Node, inst::InstMatchTrie > d_child_sub_quant_inst_trie; //children quantifiers for each quantifier, each is an instance std::map< Node, std::vector< Node > > d_sub_quants; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 87f842862..defb58bf2 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,19 +153,6 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #endif } -bool containsNN( Node n, Node nc ){ - if( n==nc ){ - return true; - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( containsNN( n[i], nc ) ){ - return true; - } - } - return false; - } -} - int ModelEngine::checkModel( int checkOption ){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -177,20 +164,11 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; for( size_t i=0; isecond.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; + //Trace("model-engine-debug") << it->second[i] << " "; + Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] ); + Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - for( size_t i=0; isecond.size(); i++ ){ - std::vector< Node > eqc; - d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc ); - Trace("model-engine-debug-eqc") << " " << it->second[i] << " : { "; - for( size_t j=0; jsecond[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){ - Trace("model-engine-debug-eqc") << eqc[j] << " "; - } - } - Trace("model-engine-debug-eqc") << "}" << std::endl; - } } } } @@ -242,6 +220,7 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; } + d_statistics.d_exh_inst_lemmas += addedLemmas; return addedLemmas; } @@ -361,13 +340,15 @@ ModelEngine::Statistics::Statistics(): d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), d_eval_lits("ModelEngine::Eval_Lits", 0 ), - d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ) + d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ), + d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_eval_formulas); StatisticsRegistry::registerStat(&d_eval_uf_terms); StatisticsRegistry::registerStat(&d_eval_lits); StatisticsRegistry::registerStat(&d_eval_lits_unknown); + StatisticsRegistry::registerStat(&d_exh_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ @@ -376,6 +357,7 @@ ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_eval_uf_terms); StatisticsRegistry::unregisterStat(&d_eval_lits); StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 2560cf50e..394ceaf42 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -78,6 +78,7 @@ public: IntStat d_eval_uf_terms; IntStat d_eval_lits; IntStat d_eval_lits_unknown; + IntStat d_exh_inst_lemmas; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d637fa25f..591270ab0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -161,27 +161,29 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } for( int i=0; i<2; i++ ){ Node n = NodeManager::currentNM()->mkConst( i==1 ); - eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ), - d_quantEngine->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - computeModelBasisArgAttribute( en ); - if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ - if( !en.getAttribute(NoMatchAttribute()) ){ - Node op = en.getOperator(); - if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - NoMatchAttribute nma; - en.setAttribute(nma,true); - congruentCount++; + if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ), + d_quantEngine->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + computeModelBasisArgAttribute( en ); + if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( !en.getAttribute(NoMatchAttribute()) ){ + Node op = en.getOperator(); + if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ + NoMatchAttribute nma; + en.setAttribute(nma,true); + congruentCount++; + }else{ + nonCongruentCount++; + d_op_count[ op ]++; + } }else{ - nonCongruentCount++; - d_op_count[ op ]++; + alreadyCongruentCount++; } - }else{ - alreadyCongruentCount++; } + ++eqc; } - ++eqc; } } Debug("term-db-cong") << "TermDb: Reset" << std::endl; @@ -300,6 +302,25 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){ } } +/** get the i^th instantiation constant of f */ +Node TermDb::getInstantiationConstant( Node f, int i ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return it->second[i]; + }else{ + return Node::null(); + } +} + +/** get number of instantiation constants for f */ +int TermDb::getNumInstantiationConstants( Node f ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return (int)it->second.size(); + }else{ + return 0; + } +} Node TermDb::getInstConstantBody( Node f ){ std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e1786d44c..5060ac1a7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -154,9 +154,9 @@ private: void makeInstantiationConstantsFor( Node f ); public: /** get the i^th instantiation constant of f */ - Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } + Node getInstantiationConstant( Node f, int i ) const; /** get number of instantiation constants for f */ - int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } + int getNumInstantiationConstants( Node f ) const; /** get the ce body f[e/x] */ Node getInstConstantBody( Node f ); /** get counterexample literal (for cbqi) */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c64a75ec4..553189d13 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -85,7 +85,6 @@ void Trigger::reset( Node eqc ){ bool Trigger::getNextMatch( InstMatch& m ){ bool retVal = d_mg->getNextMatch( m, d_quantEngine ); - //m.makeInternal( d_quantEngine->getEqualityQuery() ); return retVal; } @@ -98,10 +97,6 @@ int Trigger::addTerm( Node t ){ return d_mg->addTerm( d_f, t, d_quantEngine ); } -//bool Trigger::nonunifiable( TNode t, const std::vector & vars){ -// return d_mg->nonunifiable(t,vars); -//} - int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine ); if( addedLemmas>0 ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ebd6d32ea..3f6ba8a0f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -719,6 +719,22 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& e } } +int getDepth( Node n ){ + if( n.getNumChildren()==0 ){ + return 0; + }else{ + int maxDepth = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + int depth = getDepth( n[i] ); + if( depth>maxDepth ){ + maxDepth = depth; + } + } + return maxDepth; + } +} + int EqualityQueryQuantifiersEngine::getRepScore( Node n ){ - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; //initial + //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 4fe5772de..433ceee85 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -322,34 +322,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } -#if 0 - -void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){ -} - -int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e ){ - if( e<4 ){ - return STATUS_UNFINISHED; - }else{ - for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin(); - it != InstMatchGenerator::d_match_fails.end(); ++it ){ - for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( !it2->second.empty() ){ - Node n1 = it->first; - Node n2 = it2->first; - if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){ - d_quantEngine->addSplitEquality( n1, n2, true ); - } - it2->second.clear(); - } - } - } - return STATUS_UNKNOWN; - } -} - -#endif /* 0 */ - void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ } diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 5a3b9cc3d..aaa5f27a1 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -116,25 +116,6 @@ public: void setGenerateAdditional( bool val ) { d_generate_additional = val; } };/* class InstStrategyAutoGenTriggers */ -#if 0 - -class InstStrategyAddFailSplits : public InstStrategy{ -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryUf* d_th; - /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); -public: - InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ){} - ~InstStrategyAddFailSplits(){} - /** identify */ - std::string identify() const { return std::string("AddFailSplits"); } -};/* class InstStrategyAddFailSplits */ - -#endif /* 0 */ - class InstStrategyFreeVariable : public InstStrategy{ private: /** InstantiatorTheoryUf class */ -- 2.30.2