diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 339 |
1 files changed, 12 insertions, 327 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 663f270eb..ddaaa5b6f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -21,16 +21,13 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" //#define ME_PRINT_WARNINGS -//#define DISABLE_EVAL_SKIP_MULTIPLE - -#define RECONSIDER_FUNC_CONSTANT #define EVAL_FAIL_SKIP_MULTIPLE -//#define ONE_QUANT_PER_ROUND_INST_GEN //#define ONE_QUANT_PER_ROUND using namespace std; @@ -41,324 +38,6 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; -ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : -TheoryEngineModelBuilder( qe->getTheoryEngine() ), -d_qe( qe ){ - -} - -Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){ - return eqc; -} - -void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { - d_addedLemmas = 0; - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - FirstOrderModel* fm = (FirstOrderModel*)m; - //initialize model - fm->initialize(); - //analyze the quantifiers - Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; - analyzeQuantifiers( fm ); - //if applicable, find exceptions - if( optInstGen() ){ - //now, see if we know that any exceptions via InstGen exist - Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - d_addedLemmas += doInstGen( fm, f ); - if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ - break; - } - } - } - if( Options::current()->printModelEngine ){ - if( d_addedLemmas>0 ){ - Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Message() << "No InstGen lemmas..." << std::endl; - } - } - Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; - } - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Debug("fmf-model-debug") << "Building model..." << std::endl; - finishBuildModel( fm ); - } - } -} - -void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ - d_quant_selection_lits.clear(); - d_quant_sat.clear(); - d_uf_prefs.clear(); - int quantSatInit = 0; - int nquantSatInit = 0; - //analyze the preferences of each quantifier - for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - std::vector< Node > pro_con[2]; - std::vector< Node > constantSatOps; - bool constantSatReconsider; - //for each asserted quantifier f, - // - determine which literals form model basis for each quantifier - // - check which function/predicates have good and bad definitions according to f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ - Node n = it->first; - Node gn = d_qe->getTermDatabase()->getModelBasis( n ); - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - //calculate preference - int pref = 0; - bool value; - if( d_qe->getValuation().hasSatValue( gn, value ) ){ - if( value!=it->second ){ - //store this literal as a model basis literal - // this literal will force a default values in model that (modulo exceptions) shows - // that f is satisfied by the model - d_quant_selection_lits[f].push_back( value ? n : n.notNode() ); - pref = 1; - }else{ - pref = -1; - } - } - if( pref!=0 ){ - //Store preferences for UF - bool isConst = !n.hasAttribute(InstConstantAttribute()); - std::vector< Node > uf_terms; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = fm->d_uf_model[gn.getOperator()].isConstant(); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ - if( n[j].getKind()==APPLY_UF ){ - Node op = gn[j].getOperator(); - if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && fm->d_uf_model[op].isConstant(); - }else{ - isConst = false; - } - }else{ - isConst = false; - } - } - } - } - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - if( pref==1 && isConst ){ - d_quant_sat[f] = true; - //instead, just note to the model for each uf term that f is pro its definition - constantSatReconsider = false; - constantSatOps.clear(); - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - constantSatOps.push_back( op ); - if( d_uf_prefs[op].d_reconsiderModel ){ - constantSatReconsider = true; - } - } - if( !constantSatReconsider ){ - break; - } - }else{ - int pcIndex = pref==1 ? 0 : 1; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[pcIndex].push_back( uf_terms[j] ); - } - } - } - } - 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)constantSatOps.size(); i++ ){ - Debug("fmf-model-prefs") << constantSatOps[i] << " "; - d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false; - } - Debug("fmf-model-prefs") << std::endl; - quantSatInit++; - d_statistics.d_pre_sat_quant += quantSatInit; - }else{ - nquantSatInit++; - d_statistics.d_pre_nsat_quant += quantSatInit; - //note quantifier's value preferences to models - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); - } - } - } - } - Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; -} - -int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ - //we wish to add all known exceptions to our model basis literal(s) - // 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. - int addedLemmas = 0; - for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){ - bool phase = d_quant_selection_lits[f][i].getKind()!=NOT; - Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); - std::vector< Node > tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - fm->getTermDatabase()->setInstantiationConstantAttr( eq, f ); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ - if( lit[j].getKind()==APPLY_UF ){ - tr_terms.push_back( lit[j] ); - }else{ - tr_terms.clear(); - break; - } - } - } - if( tr_terms.size()==1 && !phase ){ - //equality between a function and a ground term, use literal matching - tr_terms.clear(); - tr_terms.push_back( lit ); - } - } - //if applicable, try to add exceptions here - if( !tr_terms.empty() ){ - //make a trigger for these terms, add instantiations - Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); - } - } - return addedLemmas; -} - -void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ - //build model for UF - for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){ - finishBuildModelUf( fm, it->second ); - } - //build model for arrays - for( std::map< Node, Node >::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 = fm->getRepresentative( selModelBasis ); - } - Debug("fmf-model-debug") << "Done building models." << std::endl; -} - -void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){ - Node op = model.getOperator(); -#ifdef RECONSIDER_FUNC_CONSTANT - if( model.isModelConstructed() && model.isConstant() ){ - 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 t = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - Node v = model.getConstantValue( t ); - 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; - model.clearModel(); - } - } - } -#endif - if( !model.isModelConstructed() ){ - //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; i<model.d_ground_asserts.size(); i++ ){ - Node n = model.d_ground_asserts[i]; - Node v = model.d_ground_asserts_reps[i]; - //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 - model.setValue( n, v ); - if( model.optUsePartialDefaults() ){ - //also set as default value if necessary - //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){ - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ - model.setValue( n, v, false ); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - }else{ - if( n==defaultTerm ){ - model.setValue( 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() ); - model.setValue( defaultTerm, defaultVal, false ); - } - Debug("fmf-model-cons") << " Making model..."; - model.setModel(); - Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; - } -} - -bool ModelEngineBuilder::optUseModel() { - return Options::current()->fmfModelBasedInst; -} - -bool ModelEngineBuilder::optInstGen(){ - return Options::current()->fmfInstGen; -} - -bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ -#ifdef ONE_QUANT_PER_ROUND_INST_GEN - return true; -#else - return false; -#endif -} - -ModelEngineBuilder::Statistics::Statistics(): - d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), - d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0) -{ - StatisticsRegistry::registerStat(&d_pre_sat_quant); - StatisticsRegistry::registerStat(&d_pre_nsat_quant); -} - -ModelEngineBuilder::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_pre_sat_quant); - StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); -} - //Model Engine constructor ModelEngine::ModelEngine( QuantifiersEngine* qe ) : QuantifiersModule( qe ), @@ -448,6 +127,8 @@ void ModelEngine::check( Theory::Effort e ){ //CVC4 will answer SAT Debug("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); + // finish building the model in the standard way + d_builder.finishProcessBuildModel( d_quantEngine->getModel() ); }else{ //otherwise, the search will continue d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); @@ -601,12 +282,13 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ } } d_statistics.d_eval_formulas += reval.d_eval_formulas; - d_statistics.d_eval_eqs += reval.d_eval_eqs; d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms; + d_statistics.d_eval_lits += reval.d_eval_lits; + d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown; int totalInst = 1; int relevantInst = 1; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size(); + totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size(); relevantInst = relevantInst * (int)riter.d_domain[i].size(); } d_totalLemmas += totalInst; @@ -658,15 +340,17 @@ void ModelEngine::debugPrint( const char* c ){ ModelEngine::Statistics::Statistics(): d_inst_rounds("ModelEngine::Inst_Rounds", 0), d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), - d_eval_eqs("ModelEngine::Eval_Equalities", 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_num_quants_init("ModelEngine::Num_Quants", 0 ), d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_eqs); StatisticsRegistry::registerStat(&d_eval_uf_terms); + StatisticsRegistry::registerStat(&d_eval_lits); + StatisticsRegistry::registerStat(&d_eval_lits_unknown); StatisticsRegistry::registerStat(&d_num_quants_init); StatisticsRegistry::registerStat(&d_num_quants_init_fail); } @@ -674,8 +358,9 @@ ModelEngine::Statistics::Statistics(): ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_eqs); StatisticsRegistry::unregisterStat(&d_eval_uf_terms); + StatisticsRegistry::unregisterStat(&d_eval_lits); + StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); StatisticsRegistry::unregisterStat(&d_num_quants_init); StatisticsRegistry::unregisterStat(&d_num_quants_init_fail); } |