diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 316 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 63 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 2 |
5 files changed, 195 insertions, 196 deletions
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; i<fm->getNumAssertedQuantifiers(); 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; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + //we are allowed to assume the type is empty + if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ + Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; + fm->setQuantifierActive( 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; i<fm->getNumAssertedQuantifiers(); 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; i<fm->getNumAssertedQuantifiers(); 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; i<fm->getNumAssertedQuantifiers(); 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 = score<selectLitScore; } - } - //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 = score<selectLitScore; - } - //see if we wish to choose this as a selection literal - d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); - if( selectLit ){ - selectLitScore = getSelectionScore( uf_terms ); - Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; - Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl; - d_quant_selection_lit[f] = value ? n : n.notNode(); - selectionLitTerms.clear(); - selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); - if( !selectLitConstraints ){ - break; + //see if we wish to choose this as a selection literal + d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); + if( selectLit ){ + selectLitScore = getSelectionScore( uf_terms ); + Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; + Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl; + d_quant_selection_lit[f] = value ? n : n.notNode(); + selectionLitTerms.clear(); + selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); + if( !selectLitConstraints ){ + break; + } } + pref = 1; + }else{ + pref = -1; } - pref = 1; - }else{ - pref = -1; - } - //if we are not yet SAT, so we will add to preferences - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] ); + //if we are not yet SAT, so we will add to preferences + if( d_qe->getModel()->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; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - int totalInst = 1; - for( unsigned j=0; j<f[0].getNumChildren(); j++ ){ - TypeNode tn = f[0][j].getType(); - if( fm->d_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; j<f[0].getNumChildren(); j++ ){ + TypeNode tn = f[0][j].getType(); + if( fm->d_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; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); - //we are allowed to assume the type is empty - if( tn.isSort() && d_quantEngine->getModel()->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; i<d_quantEngine->getModel()->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: |