From 548582b252170f35a602705a109d88a608611cca Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 16 Sep 2015 11:07:36 +0200 Subject: [PATCH] Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. --- src/smt/smt_engine.cpp | 7 +- src/theory/quantifiers/first_order_model.cpp | 5 +- src/theory/quantifiers/first_order_model.h | 4 - src/theory/quantifiers/fun_def_process.cpp | 2 + src/theory/quantifiers/model_engine.cpp | 83 +++++++++++--------- src/theory/quantifiers/model_engine.h | 2 + src/theory/quantifiers/modes.cpp | 18 ----- src/theory/quantifiers/modes.h | 9 --- src/theory/quantifiers/options | 9 +-- src/theory/quantifiers/options_handlers.h | 34 -------- src/theory/quantifiers/term_database.h | 4 + src/theory/rep_set.cpp | 14 +++- src/theory/rep_set.h | 3 + src/theory/theory_model.cpp | 3 + 14 files changed, 81 insertions(+), 116 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4874b076e..0af5c7fc1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -739,7 +739,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_context->push(); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); - if( options::fmfFunWellDefined() ){ + if( options::fmfFunWellDefined() || options::fmfFunWellDefinedRelevant() ){ d_fmfRecFunctionsAbs = new(true) TypeNodeMap(d_userContext); d_fmfRecFunctionsConcrete = new(true) NodeListMap(d_userContext); } @@ -1364,6 +1364,11 @@ void SmtEngine::setDefaults() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } + if( options::fmfFunWellDefinedRelevant() ){ + if( !options::fmfFunWellDefined.wasSetByUser() ){ + options::fmfFunWellDefined.set( true ); + } + } if( options::fmfFunWellDefined() ){ if( !options::finiteModelFind.wasSetByUser() ){ options::finiteModelFind.set( true ); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 346631889..36d055b69 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -32,7 +32,7 @@ using namespace CVC4::theory::quantifiers::fmcheck; FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : TheoryModel( c, name, true ), -d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ +d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){ } @@ -40,9 +40,6 @@ void FirstOrderModel::assertQuantifier( Node n, bool reduced ){ if( !reduced ){ if( n.getKind()==FORALL ){ d_forall_asserts.push_back( n ); - if( n.getAttribute(AxiomAttribute()) ){ - d_axiom_asserted = true; - } }else if( n.getKind()==NOT ){ Assert( n[0].getKind()==FORALL ); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 25d71984d..a31e85d7e 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -47,8 +47,6 @@ class FirstOrderModel : public TheoryModel protected: /** quant engine */ QuantifiersEngine * d_qe; - /** whether an axiom is asserted */ - context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; /** list of quantifiers that have been marked to reduce */ @@ -68,8 +66,6 @@ public: //for Theory Quantifiers: Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } /** get number to reduce quantifiers */ unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); } - /** bool axiom asserted */ - bool isAxiomAsserted() { return d_axiom_asserted; } /** initialize model for term */ void initializeModelForTerm( Node n ); virtual void processInitializeModelForTerm( Node n ) = 0; diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 0197bda6b..632e19a18 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -55,6 +55,8 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { std::stringstream ss; ss << "I_" << f; TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() ); + AbsTypeFunDefAttribute atfda; + iType.setAttribute(atfda,true); d_sorts[f] = iType; //create functions f1...fn mapping from this sort to concrete elements diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 2ad8be3a1..752e88c5a 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -52,7 +52,7 @@ bool ModelEngine::needsCheck( Theory::Effort e ) { } unsigned ModelEngine::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_MODEL; + return QuantifiersEngine::QEFFORT_MODEL; } void ModelEngine::reset_round( Theory::Effort e ) { @@ -64,7 +64,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); - //the following will test that the model satisfies all asserted universal quantifiers by + //the following will test that the model satisfies all asserted universal quantifiers by // (model-based) exhaustive instantiation. double clSet = 0; if( Trace.isOn("model-engine") ){ @@ -88,7 +88,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ }else{ addedLemmas++; } - + if( Trace.isOn("model-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; @@ -143,8 +143,6 @@ bool ModelEngine::optOneQuantPerRound(){ int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); - quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); - Assert( mb!=NULL ); //flatten the representatives //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; @@ -192,52 +190,59 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - //default : 1 : conj,axiom - //priority : 0 : conj, 1 : axiom - //trust : 0 : conj - int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; - for( int effort=startEffort; effort<2; effort++ ){ - // FMC uses two sub-effort levels - int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); - for( int e=0; egetNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - bool isAx = getTermDatabase()->isQAttrAxiom( f ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; - //determine if we should check this quantifier - if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ - exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); - } + // FMC uses two sub-effort levels + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); + for( int e=0; egetNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + //determine if we should check this quantifier + if( considerQuantifiedFormula( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); } - if( optOneQuantPerRound() && d_addedLemmas>0 ){ - break; - } - }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } + if( optOneQuantPerRound() && d_addedLemmas>0 ){ + break; + } + }else{ + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } } - if( d_addedLemmas==0 && options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ - //set incomplete - if( effort==0 ){ - d_incomplete_check = true; - } - break; - } } + //print debug information Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; } +bool ModelEngine::considerQuantifiedFormula( Node q ) { + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q ); + 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 quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index c357c2876..1fb4255b2 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -34,6 +34,8 @@ 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/modes.cpp b/src/theory/quantifiers/modes.cpp index ebc1088a8..253f23561 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -59,24 +59,6 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod return out; } -std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode mode) { - switch(mode) { - case theory::quantifiers::AXIOM_INST_MODE_DEFAULT: - out << "AXIOM_INST_MODE_DEFAULT"; - break; - case theory::quantifiers::AXIOM_INST_MODE_TRUST: - out << "AXIOM_INST_MODE_TRUST"; - break; - case theory::quantifiers::AXIOM_INST_MODE_PRIORITY: - out << "AXIOM_INST_MODE_PRIORITY"; - break; - default: - out << "AxiomInstMode!UNKNOWN"; - } - - return out; -} - std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { case theory::quantifiers::MBQI_GEN_EVAL: diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 94ba7daaf..9502fd362 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -48,15 +48,6 @@ typedef enum { LITERAL_MATCH_EQUALITY, } LiteralMatchMode; -typedef enum { - /** default, use all methods for axioms */ - AXIOM_INST_MODE_DEFAULT, - /** only use heuristic methods for axioms, return unknown in the case no instantiations are produced */ - AXIOM_INST_MODE_TRUST, - /** only use heuristic methods for axioms, resort to all methods when no instantiations are produced */ - AXIOM_INST_MODE_PRIORITY, -} AxiomInstMode; - typedef enum { /** mbqi from CADE 24 paper */ MBQI_GEN_EVAL, diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 74ce3cc6c..a31fbe6e7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -110,9 +110,6 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode -option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" - policy for instantiating axioms - ### finite model finding options option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write @@ -120,8 +117,10 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option quantFunWellDefined --quant-fun-wd bool :default false assume that function defined by quantifiers are well defined -option fmfFunWellDefined --fmf-fun bool :default false - find models for finite runs of defined functions, assumes functions are well-defined +option fmfFunWellDefined --fmf-fun bool :default false :read-write + find models for recursively defined functions, assumes functions are admissible +option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false + find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e5e484625..f27b98a3d 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -60,24 +60,6 @@ predicate\n\ Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ \n\ "; - -static const std::string axiomInstModeHelp = "\ -Axiom instantiation modes currently supported by the --axiom-inst option:\n\ -\n\ -default \n\ -+ Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\ - instantiating axioms.\n\ -\n\ -trust \n\ -+ Treat axioms only using heuristic instantiation. Return unknown if in the case\n\ - that no instantiations are produced.\n\ -\n\ -priority \n\ -+ Treat axioms only using heuristic instantiation. Resort to using all methods\n\ - in the case that no instantiations are produced.\n\ -\n\ -"; - static const std::string mbqiModeHelp = "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ @@ -292,22 +274,6 @@ inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, Smt } } -inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return AXIOM_INST_MODE_DEFAULT; - } else if(optarg == "trust") { - return AXIOM_INST_MODE_TRUST; - } else if(optarg == "priority") { - return AXIOM_INST_MODE_PRIORITY; - } else if(optarg == "help") { - puts(axiomInstModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --axiom-inst: `") + - optarg + "'. Try --axiom-inst help."); - } -} - inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "gen-ev") { return MBQI_GEN_EVAL; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7c136a186..477b964ee 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -92,6 +92,10 @@ typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribu struct SygusProxyAttributeId {}; typedef expr::Attribute SygusProxyAttribute; +//attribute for fun-def abstraction type +struct AbsTypeFunDefAttributeId {}; +typedef expr::Attribute AbsTypeFunDefAttribute; + class QuantifiersEngine; namespace inst{ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 6a64f762e..a90a4cf17 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -29,6 +29,7 @@ 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 ) { @@ -91,7 +92,7 @@ int RepSet::getIndexFor( Node n ) const { bool RepSet::complete( TypeNode t ){ std::map< TypeNode, bool >::iterator it = d_type_complete.find( t ); if( it==d_type_complete.end() ){ - //remove all previous + //remove all previous for( unsigned i=0; i::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){ #if 0 for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ @@ -193,7 +203,7 @@ bool RepSetIterator::initialize(){ //FIXME: // terms in rep_set are now constants which mapped to terms through TheoryModel // thus, should introduce a constant and a term. for now, just a term. - + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index f1114edcf..2df824b5d 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -33,6 +33,7 @@ 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 */ @@ -49,6 +50,8 @@ 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 c4bc94bd2..92f834bff 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -824,6 +824,9 @@ 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 -- 2.30.2