From 623e701247ed08e3f59d57b18ebe42f4d4db221e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 2 Dec 2016 08:51:29 -0600 Subject: [PATCH] Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723. --- src/theory/quantifiers/full_model_check.cpp | 4 +- src/theory/quantifiers/model_builder.cpp | 316 ++++++++++-------- src/theory/quantifiers/model_builder.h | 6 +- src/theory/quantifiers/model_engine.cpp | 63 +--- src/theory/quantifiers/model_engine.h | 2 - src/theory/quantifiers_engine.cpp | 2 +- src/theory/rep_set.cpp | 10 - src/theory/rep_set.h | 3 - src/theory/theory_model.cpp | 4 - test/regress/regress0/fmf/Makefile.am | 3 +- .../regress0/fmf/bug723-irrelevant-funs.smt2 | 52 +++ 11 files changed, 250 insertions(+), 215 deletions(-) create mode 100644 test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 72057e734..6b756428b 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -326,13 +326,15 @@ QModelBuilder( c, qe ){ } void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) { + //standard pre-process + preProcessBuildModelStd( m, fullModel ); + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( !fullModel ){ Trace("fmc") << "---Full Model Check preprocess() " << std::endl; d_preinitialized_types.clear(); //traverse equality engine eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); - std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ TypeNode tr = (*eqcs_i).getType(); d_preinitialized_types[tr] = true; diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index b30c2addb..a5ec16e3a 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -39,13 +39,57 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe } -bool QModelBuilder::isQuantifierActive( Node f ) { - return d_qe->hasOwnership( f ); +bool QModelBuilder::optUseModel() { + return options::mbqiMode()!=MBQI_NONE || options::fmfBound(); } +void QModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) { + preProcessBuildModelStd( m, fullModel ); +} -bool QModelBuilder::optUseModel() { - return options::mbqiMode()!=MBQI_NONE || options::fmfBound(); +void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) { + if( !fullModel ){ + if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){ + FirstOrderModel * fm = (FirstOrderModel*)m; + //traverse equality engine + std::map< TypeNode, bool > eqc_usort; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + TypeNode tr = (*eqcs_i).getType(); + eqc_usort[tr] = true; + ++eqcs_i; + } + //look at quantified formulas + for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i, true ); + if( fm->isQuantifierActive( q ) ){ + //check if any of these quantified formulas can be set inactive + if( options::fmfEmptySorts() ){ + for( unsigned i=0; isetQuantifierActive( q, false ); + } + } + }else if( options::fmfFunWellDefinedRelevant() ){ + if( q[0].getNumChildren()==1 ){ + TypeNode tn = q[0][0].getType(); + if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ + //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl; + //we are allowed to assume the introduced type is empty + if( eqc_usort.find( tn )==eqc_usort.end() ){ + Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; + fm->setQuantifierActive( q, false ); + } + } + } + } + } + } + } + } } void QModelBuilder::debugModel( FirstOrderModel* fm ){ @@ -152,9 +196,9 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; //check if any quantifiers are un-initialized for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( isQuantifierActive( f ) ){ - int lems = initializeQuantifier( f, f ); + Node q = fm->getAssertedQuantifier( i ); + if( d_qe->getModel()->isQuantifierActive( q ) ){ + int lems = initializeQuantifier( q, q ); d_statistics.d_init_inst_gen_lemmas += lems; d_addedLemmas += lems; if( d_qe->inConflict() ){ @@ -173,13 +217,10 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { analyzeModel( fm ); //analyze the quantifiers Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; - d_quant_sat.clear(); d_uf_prefs.clear(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( isQuantifierActive( f ) ){ - analyzeQuantifier( fm, f ); - } + Node q = fm->getAssertedQuantifier( i ); + analyzeQuantifier( fm, q ); } //if applicable, find exceptions to model via inst-gen @@ -194,15 +235,13 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - if( isQuantifierActive( f ) ){ + if( d_qe->getModel()->isQuantifierActive( f ) ){ int lems = doInstGen( fm, f ); d_statistics.d_inst_gen_lemmas += lems; d_addedLemmas += lems; //temporary if( lems>0 ){ d_numQuantInstGen++; - }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - d_numQuantSat++; }else if( hasInstGen( f ) ){ d_numQuantNoInstGen++; }else{ @@ -211,7 +250,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ break; } - }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + }else{ d_numQuantSat++; } } @@ -236,16 +275,6 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; 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; } } @@ -378,10 +407,6 @@ QModelBuilderIG::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } -bool QModelBuilderIG::isQuantifierActive( Node f ){ - return d_qe->hasOwnership( f ) && d_quant_sat.find( f )==d_quant_sat.end(); -} - bool QModelBuilderIG::isTermActive( Node n ){ return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments @@ -389,7 +414,6 @@ bool QModelBuilderIG::isTermActive( Node n ){ //to another active term } - //do exhaustive instantiation int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ @@ -502,133 +526,135 @@ int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { } void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - 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; - Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl; - //for each asserted quantifier f, - // - determine selection literals - // - check which function/predicates have good and bad definitions for satisfying f - if( d_phase_reqs.find( f )==d_phase_reqs.end() ){ - d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true ); - } - int selectLitScore = -1; - for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.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( TermDb::hasInstConstAttr(n) ){ - isConst = false; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = hasConstantDefinition( gn ); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( TermDb::hasInstConstAttr(n[j]) ){ - if( n[j].getKind()==APPLY_UF && - fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && hasConstantDefinition( gn[j] ); - }else{ - isConst = false; + if( d_qe->getModel()->isQuantifierActive( f ) ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); + 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; + Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl; + //for each asserted quantifier f, + // - determine selection literals + // - check which function/predicates have good and bad definitions for satisfying f + if( d_phase_reqs.find( f )==d_phase_reqs.end() ){ + d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true ); + } + int selectLitScore = -1; + for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.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( TermDb::hasInstConstAttr(n) ){ + isConst = false; + if( gn.getKind()==APPLY_UF ){ + uf_terms.push_back( gn ); + isConst = hasConstantDefinition( gn ); + }else if( gn.getKind()==EQUAL ){ + isConst = true; + for( int j=0; j<2; j++ ){ + if( TermDb::hasInstConstAttr(n[j]) ){ + if( n[j].getKind()==APPLY_UF && + fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ + uf_terms.push_back( gn[j] ); + isConst = isConst && hasConstantDefinition( gn[j] ); + }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; + //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_qe->getModel()->isQuantifierActive( f ); + d_qe->getModel()->setQuantifierActive( f, false ); + //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; } } - if( !selectLitConstraints ){ - selectLit = true; + //also check if it is naturally a better literal + if( !selectLit ){ + int score = getSelectionScore( uf_terms ); + //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl; + selectLit = scoregetModel()->isQuantifierActive( f ) ){ + 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" << 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; + //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" << std::endl; } - Debug("fmf-model-prefs") << std::endl; - }else{ - //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 = fmig->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + //process information about requirements and preferences of quantifier f + if( !d_qe->getModel()->isQuantifierActive( f ) ){ + 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; + }else{ + //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 = fmig->getRepresentative( pro_con[k][j] ); + d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + } } } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 9b89e5ef6..e1f586585 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -33,11 +33,11 @@ protected: context::CDO< FirstOrderModel* > d_curr_model; //quantifiers engine QuantifiersEngine* d_qe; + void preProcessBuildModel(TheoryModel* m, bool fullModel); + void preProcessBuildModelStd(TheoryModel* m, bool fullModel); public: QModelBuilder( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilder() throw() {} - // is quantifier active? - virtual bool isQuantifierActive( Node f ); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work // >0 : success @@ -105,7 +105,7 @@ protected: virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; protected: //map from quantifiers to if are SAT - std::map< Node, bool > d_quant_sat; + //std::map< Node, bool > d_quant_sat; //which quantifiers have been initialized std::map< Node, bool > d_quant_basis_match_added; //map from quantifiers to model basis match diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 20f5eae7b..9496f630d 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -183,14 +183,16 @@ int ModelEngine::checkModel(){ if( Trace.isOn("model-engine") ){ for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - int totalInst = 1; - for( unsigned j=0; jd_rep_set.hasType( tn ) ){ - totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){ + int totalInst = 1; + for( unsigned j=0; jd_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + } } + d_totalLemmas += totalInst; } - d_totalLemmas += totalInst; } } @@ -203,7 +205,7 @@ int ModelEngine::checkModel(){ Node q = fm->getAssertedQuantifier( i, true ); Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( considerQuantifiedFormula( q ) ){ + if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ exhaustiveInstantiate( q, e ); if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ break; @@ -230,38 +232,7 @@ int ModelEngine::checkModel(){ return d_addedLemmas; } -bool ModelEngine::considerQuantifiedFormula( Node q ) { - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ - Trace("model-engine-debug") << "Model builder inactive : " << q << std::endl; - return false; - }else if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ - Trace("model-engine-debug") << "Model inactive : " << q << std::endl; - return false; - }else{ - if( options::fmfEmptySorts() ){ - for( unsigned i=0; igetModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){ - Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; - return false; - } - } - }else if( options::fmfFunWellDefinedRelevant() ){ - if( q[0].getNumChildren()==1 ){ - TypeNode tn = q[0][0].getType(); - if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ - //we are allowed to assume the introduced type is empty - if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){ - Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; - return false; - } - } - } - } - return true; - } -} + void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //first check if the builder can do the exhaustive instantiation @@ -331,13 +302,15 @@ void ModelEngine::debugPrint( const char* c ){ Trace( c ) << "Quantifiers: " << std::endl; for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Trace( c ) << " "; - if( !considerQuantifiedFormula( q ) ){ - Trace( c ) << "*Inactive* "; - }else{ - Trace( c ) << " "; + if( d_quantEngine->hasOwnership( q, this ) ){ + Trace( c ) << " "; + if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Trace( c ) << "*Inactive* "; + }else{ + Trace( c ) << " "; + } + Trace( c ) << q << std::endl; } - Trace( c ) << q << std::endl; } //d_quantEngine->getModel()->debugPrint( c ); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index e89be8d2b..728539e91 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -34,8 +34,6 @@ private: private: //check model int checkModel(); - //consider quantified formula - bool considerQuantifiedFormula( Node q ); //exhaustively instantiate quantifier (possibly using mbqi) void exhaustiveInstantiate( Node f, int effort = 0 ); private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3168a78e2..a3b6293fb 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -766,7 +766,7 @@ void QuantifiersEngine::propagate( Theory::Effort level ){ } Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ - unsigned min_priority; + unsigned min_priority = 0; Node dec; for( unsigned i=0; igetNextDecisionRequest( priority ); diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 86bcb2cac..a2797dd8d 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -29,7 +29,6 @@ void RepSet::clear(){ d_type_complete.clear(); d_tmap.clear(); d_values_to_terms.clear(); - d_type_rlv_rep.clear(); } bool RepSet::hasRep( TypeNode tn, Node n ) { @@ -117,15 +116,6 @@ bool RepSet::complete( TypeNode t ){ } } -int RepSet::getNumRelevantGroundReps( TypeNode t ) { - std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t ); - if( it==d_type_rlv_rep.end() ){ - return 0; - }else{ - return it->second; - } -} - void RepSet::toStream(std::ostream& out){ for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ if( !it->first.isFunction() && !it->first.isPredicate() ){ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index ee927de86..a56fba39b 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -33,7 +33,6 @@ public: std::map< TypeNode, std::vector< Node > > d_type_reps; std::map< TypeNode, bool > d_type_complete; std::map< Node, int > d_tmap; - std::map< TypeNode, int > d_type_rlv_rep; // map from values to terms they were assigned for std::map< Node, Node > d_values_to_terms; /** clear the set */ @@ -50,8 +49,6 @@ public: int getIndexFor( Node n ) const; /** complete all values */ bool complete( TypeNode t ); - /** get number of relevant ground representatives for type */ - int getNumRelevantGroundReps( TypeNode t ); /** debug print */ void toStream(std::ostream& out); };/* class RepSet */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 3cdaeb106..71d82d5e4 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -602,7 +602,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // model-builder specific initialization preProcessBuildModel(tm, fullModel); - // Loop through all terms and make sure that assignable sub-terms are in the equality engine // Also, record #eqc per type (for finite model finding) std::map< TypeNode, unsigned > eqc_usort_count; @@ -960,9 +959,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) tm->d_rep_set.add((*i).getType(), *i); } } - for( std::map< TypeNode, std::vector< Node > >::iterator it = tm->d_rep_set.d_type_reps.begin(); it != tm->d_rep_set.d_type_reps.end(); ++it ){ - tm->d_rep_set.d_type_rlv_rep[it->first] = (int)it->second.size(); - } } //modelBuilder-specific initialization diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index cea0d7686..31fdb0a40 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ agree466.smt2 \ LeftistHeap.scala-8-ncm.smt2 \ sc-crash-052316.smt2 \ - bound-int-alt.smt2 + bound-int-alt.smt2 \ + bug723-irrelevant-funs.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 new file mode 100644 index 000000000..1a27bf170 --- /dev/null +++ b/test/regress/regress0/fmf/bug723-irrelevant-funs.smt2 @@ -0,0 +1,52 @@ +; COMMAND-LINE: --fmf-fun-rlv --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(define-fun $$isTrue$$ ((b Bool)) Bool b) +(define-fun $$isFalse$$ ((b Bool)) Bool (not b)) +(define-fun $$toString$$ ((b Bool)) String (ite b "true" "false") ) +(define-fun $$fromString$$ ((s String)) Bool (= s "true") ) +(define-fun $$inttostr$$ ((i Int)) String (ite (< i 0) (str.++ "-" (int.to.str (- i))) (int.to.str i))) +(declare-fun $$takeWhile$$ (String String) String) +(declare-fun $$takeWhileNot$$ (String String) String) +(declare-fun $$dropWhile$$ (String String) String) +(declare-fun $$dropWhileNot$$ (String String) String) +(declare-datatypes () ( + (AddressType (AddressType$C_AddressType (AddressType$C_AddressType$address String) (AddressType$C_AddressType$city String) (AddressType$C_AddressType$region String) (AddressType$C_AddressType$postalCode String) (AddressType$C_AddressType$country String))) + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_dateTime (Conditional_dateTime$CAbsent_dateTime) (Conditional_dateTime$CPresent_dateTime (Conditional_dateTime$CPresent_dateTime$value Int))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (CustomerType (CustomerType$C_CustomerType (CustomerType$C_CustomerType$companyName String) (CustomerType$C_CustomerType$contactName String) (CustomerType$C_CustomerType$contactTitle String) (CustomerType$C_CustomerType$phone String) (CustomerType$C_CustomerType$fax Conditional_string) (CustomerType$C_CustomerType$fullAddress AddressType) (CustomerType$C_CustomerType$customerID Int))) + (List_CustomerType (List_CustomerType$CNil_CustomerType) (List_CustomerType$Cstr_CustomerType (List_CustomerType$Cstr_CustomerType$head CustomerType) (List_CustomerType$Cstr_CustomerType$tail List_CustomerType))) + (List_OrderType (List_OrderType$CNil_OrderType) (List_OrderType$Cstr_OrderType (List_OrderType$Cstr_OrderType$head OrderType) (List_OrderType$Cstr_OrderType$tail List_OrderType))) + (OrderType (OrderType$C_OrderType (OrderType$C_OrderType$customerID Int) (OrderType$C_OrderType$employeeID Int) (OrderType$C_OrderType$orderDate Int) (OrderType$C_OrderType$requiredDate Int) (OrderType$C_OrderType$shipInfo ShipInfoType))) + (RootType (RootType$C_RootType (RootType$C_RootType$customers List_CustomerType) (RootType$C_RootType$orders List_OrderType))) + (ShipInfoType (ShipInfoType$C_ShipInfoType (ShipInfoType$C_ShipInfoType$shipVia Int) (ShipInfoType$C_ShipInfoType$freight Int) (ShipInfoType$C_ShipInfoType$shipName String) (ShipInfoType$C_ShipInfoType$shipAddress String) (ShipInfoType$C_ShipInfoType$shipCity String) (ShipInfoType$C_ShipInfoType$shipRegion String) (ShipInfoType$C_ShipInfoType$shipPostalCode String) (ShipInfoType$C_ShipInfoType$shipCountry String) (ShipInfoType$C_ShipInfoType$shippedDate Conditional_dateTime))) +) ) + +(define-fun f2866$toXml((a$$2869 AddressType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "
") (AddressType$C_AddressType$address a$$2869)) "
") "") (AddressType$C_AddressType$city a$$2869)) "") "") (AddressType$C_AddressType$region a$$2869)) "") "") (AddressType$C_AddressType$postalCode a$$2869)) "") "") (AddressType$C_AddressType$country a$$2869)) "") "")) +(define-fun f2656$toXml((c$$2659 CustomerType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "") "") (CustomerType$C_CustomerType$companyName c$$2659)) "") "") (CustomerType$C_CustomerType$contactName c$$2659)) "") "") (CustomerType$C_CustomerType$contactTitle c$$2659)) "") "") (CustomerType$C_CustomerType$phone c$$2659)) "") (ite (is-Conditional_string$CPresent_string (CustomerType$C_CustomerType$fax c$$2659)) (str.++ (str.++ "" (Conditional_string$CPresent_string$value (CustomerType$C_CustomerType$fax c$$2659))) "") "")) (f2866$toXml (CustomerType$C_CustomerType$fullAddress c$$2659))) "")) +(define-funs-rec + ( + (f2574$toXml((lc$$2577 List_CustomerType)) String) + ) + ( + (ite (is-List_CustomerType$CNil_CustomerType lc$$2577) "" (str.++ (f2656$toXml (List_CustomerType$Cstr_CustomerType$head lc$$2577)) (f2574$toXml (List_CustomerType$Cstr_CustomerType$tail lc$$2577)))) + ) +) +(define-fun f2942$toXml((s$$2945 ShipInfoType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "") ">")) "") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$shipVia s$$2945))) "") "") ($$inttostr$$ (ShipInfoType$C_ShipInfoType$freight s$$2945))) "") "") (ShipInfoType$C_ShipInfoType$shipName s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipAddress s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipCity s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipRegion s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipPostalCode s$$2945)) "") "") (ShipInfoType$C_ShipInfoType$shipCountry s$$2945)) "") "")) +(define-fun f2776$toXml((o$$2779 OrderType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "") ($$inttostr$$ (OrderType$C_OrderType$customerID o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$employeeID o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$orderDate o$$2779))) "") "") ($$inttostr$$ (OrderType$C_OrderType$requiredDate o$$2779))) "") (f2942$toXml (OrderType$C_OrderType$shipInfo o$$2779))) "")) +(define-funs-rec + ( + (f2615$toXml((lo$$2618 List_OrderType)) String) + ) + ( + (ite (is-List_OrderType$CNil_OrderType lo$$2618) "" (str.++ (f2776$toXml (List_OrderType$Cstr_OrderType$head lo$$2618)) (f2615$toXml (List_OrderType$Cstr_OrderType$tail lo$$2618)))) + ) +) +(define-fun f2526$toXml((r$$2529 RootType)) String (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ (str.++ "" "") (f2574$toXml (RootType$C_RootType$customers r$$2529))) "") "") (f2615$toXml (RootType$C_RootType$orders r$$2529))) "") "")) + +(declare-fun $Report$3105$0$1$() String) +(assert (= $Report$3105$0$1$ "")) +; should be fast since functions introduced by define-fun-rec do not appear in the ground assertion +(check-sat) + -- 2.30.2