From a1135ca591276f6d02b3632bc77a3934ded2d2af Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 25 Feb 2016 10:10:47 -0600 Subject: [PATCH] Minor improvement to partial qe. Add options for representative selection in FMF. --- src/options/options_handler.cpp | 34 ++++++- src/options/options_handler.h | 2 + src/options/quantifiers_modes.h | 8 ++ src/options/quantifiers_options | 4 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 42 ++++---- src/theory/quantifiers/inst_strategy_cbqi.h | 2 +- src/theory/quantifiers/term_database.cpp | 15 +++ src/theory/quantifiers/term_database.h | 5 + src/theory/quantifiers_engine.cpp | 98 +++++++++---------- src/theory/quantifiers_engine.h | 4 + src/theory/strings/theory_strings.cpp | 1 + 11 files changed, 137 insertions(+), 78 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index f214b032c..152e22f14 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -428,7 +428,7 @@ post \n\ "; const std::string OptionsHandler::s_macrosQuantHelp = "\ -Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ +Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ \n\ all \n\ + Infer definitions for functions, including those containing quantified formulas.\n\ @@ -442,7 +442,7 @@ ground-uf \n\ "; const std::string OptionsHandler::s_quantDSplitHelp = "\ -Template modes for quantifiers splitting, supported by --quant-split:\n\ +Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\ \n\ none \n\ + Never split quantified formulas.\n\ @@ -455,6 +455,20 @@ agg \n\ \n\ "; +const std::string OptionsHandler::s_quantRepHelp = "\ +Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\ +\n\ +ee \n\ ++ Let equality engine choose representatives.\n\ +\n\ +first (default) \n\ ++ Choose terms that appear first.\n\ +\n\ +depth \n\ ++ Choose terms that are of minimal depth.\n\ +\n\ +"; + theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "pre-full") { return theory::quantifiers::INST_WHEN_PRE_FULL; @@ -716,6 +730,22 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std } } +theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::QUANT_REP_MODE_EE; + } else if(optarg == "first" || optarg == "default") { + return theory::quantifiers::QUANT_REP_MODE_FIRST; + } else if(optarg == "depth") { + return theory::quantifiers::QUANT_REP_MODE_DEPTH; + } else if(optarg == "help") { + puts(s_quantRepHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-rep-mode: `") + + optarg + "'. Try --quant-rep-mode help."); + } +} + // theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { #ifndef CVC4_USE_ABC diff --git a/src/options/options_handler.h b/src/options/options_handler.h index a2d67be60..720889ca2 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -101,6 +101,7 @@ public: theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException); // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); @@ -201,6 +202,7 @@ public: static const std::string s_literalMatchHelp; static const std::string s_macrosQuantHelp; static const std::string s_quantDSplitHelp; + static const std::string s_quantRepHelp; static const std::string s_mbqiModeHelp; static const std::string s_modelFormatHelp; static const std::string s_prenexQuantModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 7395a9a30..8aa3756cc 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -172,6 +172,14 @@ enum QuantDSplitMode { QUANT_DSPLIT_MODE_AGG, }; +enum QuantRepMode { + /** let equality engine choose representatives */ + QUANT_REP_MODE_EE, + /** default, choose representatives that appear first */ + QUANT_REP_MODE_FIRST, + /** choose representatives that have minimal depth */ + QUANT_REP_MODE_DEPTH, +}; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index cba1423a0..58367f2e2 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -100,8 +100,8 @@ option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option instLevelInputOnly --inst-level-input-only bool :default true only input terms are assigned instantiation level zero -option internalReps --quant-internal-reps bool :default true - instantiate with representatives chosen by quantifiers engine +option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode + selection mode for representatives in quantifiers engine option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index e6c9b9e6b..faad18c28 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,7 +34,9 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) { + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ) +//, d_added_inst( qe->getUserContext() ) +{ } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -97,14 +99,6 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { }else{ Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; } - //if doing partial quantifier elimination, do not process this if already processed once - if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){ - if( d_added_inst.find( q )!=d_added_inst.end() ){ - d_quantEngine->getModel()->setQuantifierActive( q, false ); - d_cbqi_set_quant_inactive = true; - d_incomplete_check = true; - } - } } } } @@ -597,21 +591,23 @@ InstStrategyCegqi::~InstStrategyCegqi() throw () { } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { - d_check_vts_lemma_lc = true; + d_check_vts_lemma_lc = false; } -void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { +void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( e==0 ){ - CegInstantiator * cinst = getInstantiator( f ); - Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; - d_curr_quant = f; + CegInstantiator * cinst = getInstantiator( q ); + Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; + d_curr_quant = q; if( !cinst->check() ){ d_incomplete_check = true; + d_check_vts_lemma_lc = true; } d_curr_quant = Node::null(); }else if( e==1 ){ //minimize the free delta heuristically on demand if( d_check_vts_lemma_lc ){ + Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; d_check_vts_lemma_lc = false; d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); d_small_const = Rewriter::rewrite( d_small_const ); @@ -635,13 +631,21 @@ void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); - //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); - if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ - d_added_inst.insert( d_curr_quant ); + //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma + if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){ + d_cbqi_set_quant_inactive = true; + d_incomplete_check = true; + d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); return true; }else{ - return false; + //check if we need virtual term substitution (if used delta or infinity) + bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); + if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ + //d_added_inst.insert( d_curr_quant ); + return true; + }else{ + return false; + } } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8de844eb8..fd8afb149 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -40,7 +40,7 @@ protected: /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; /** whether we have instantiated quantified formulas */ - NodeSet d_added_inst; + //NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cb23b8bb7..be0f60654 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1680,6 +1680,21 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) { } } +int TermDb::getTermDepth( Node n ) { + if (!n.hasAttribute(TermDepthAttribute()) ){ + int maxDepth = -1; + for( unsigned i=0; imaxDepth ){ + maxDepth = depth; + } + } + TermDepthAttribute tda; + n.setAttribute(tda,1+maxDepth); + } + return n.getAttribute(TermDepthAttribute()); +} + bool TermDb::containsUninterpretedConstant( Node n ) { std::map< Node, bool > visited; return containsUninterpretedConstant2( n, visited ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5560098c9..b1cfcf2ae 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -68,6 +68,9 @@ typedef expr::Attribute InstLevelAttribute; struct InstVarNumAttributeId {}; typedef expr::Attribute InstVarNumAttribute; +struct TermDepthAttributeId {}; +typedef expr::Attribute TermDepthAttribute; + struct ModelBasisAttributeId {}; typedef expr::Attribute ModelBasisAttribute; //for APPLY_UF terms, 1 : term has direct child with model basis attribute, @@ -436,6 +439,8 @@ public: static bool containsTerms( Node n, std::vector< Node >& t ); /** contains uninterpreted constant */ static bool containsUninterpretedConstant( Node n ); + /** get the term depth of n */ + static int getTermDepth( Node n ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bbc41278e..9568966d6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -741,6 +741,24 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v } } +bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) { + if( options::incrementalSolving() ){ + Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; + inst::CDInstMatchTrie* imt; + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); + if( it!=d_c_inst_match_trie.end() ){ + imt = it->second; + }else{ + imt = new CDInstMatchTrie( getUserContext() ); + d_c_inst_match_trie[q] = imt; + } + return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst ); + }else{ + Trace("inst-add-debug") << "Adding into inst trie" << std::endl; + return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst ); + } +} + void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){ Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl; //if not from the vector of terms we instantiatied @@ -956,22 +974,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } //check for duplication - bool alreadyExists = false; - if( options::incrementalSolving() ){ - Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; - inst::CDInstMatchTrie* imt; - std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); - if( it!=d_c_inst_match_trie.end() ){ - imt = it->second; - }else{ - imt = new CDInstMatchTrie( getUserContext() ); - d_c_inst_match_trie[q] = imt; - } - alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst ); - }else{ - Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst ); - } + bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst ); if( alreadyExists ){ Trace("inst-add-debug") << " -> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate_eq); @@ -1260,27 +1263,27 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ Assert( f.isNull() || f.getKind()==FORALL ); Node r = getRepresentative( a ); - if( !options::internalReps() ){ - return r; - }else{ - if( options::finiteModelFind() ){ - if( r.isConst() ){ - //map back from values assigned by model, if any - if( d_qe->getModel() ){ - std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); - if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ - r = it->second; - r = getRepresentative( r ); - }else{ - if( r.getType().isSort() ){ - Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; - //should never happen : UF constants should never escape model - Assert( false ); - } + if( options::finiteModelFind() ){ + if( r.isConst() ){ + //map back from values assigned by model, if any + if( d_qe->getModel() ){ + std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); + if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ + r = it->second; + r = getRepresentative( r ); + }else{ + if( r.getType().isSort() ){ + Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + //should never happen : UF constants should never escape model + Assert( false ); } } } } + } + if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ + return r; + }else{ TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); if( itir==d_int_rep[v_tn].end() ){ @@ -1320,7 +1323,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } - Trace("internal-rep-select") << "...Choose " << r_best << std::endl; + Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; Assert( r_best.getType().isSubtypeOf( v_tn ) ); d_int_rep[v_tn][r] = r_best; if( r_best!=a ){ @@ -1446,23 +1449,6 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } } -/* -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; - } -} -*/ - //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){ if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject @@ -1479,8 +1465,12 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type return options::instLevelInputOnly() ? -1 : 0; } }else{ - //score prefers earliest use of this term as a representative - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){ + //score prefers earliest use of this term as a representative + return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; + }else{ + Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); + return quantifiers::TermDb::getTermDepth( n ); + } } - //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c5c88487b..b9ce2063a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -99,6 +99,7 @@ namespace quantifiers { class QuantEqualityEngine; class FullSaturation; class InstStrategyCbqi; + class InstStrategyCegqi; class QuantDSplit; }/* CVC4::theory::quantifiers */ @@ -111,6 +112,7 @@ class EqualityQueryQuantifiersEngine; class QuantifiersEngine { friend class quantifiers::InstantiationEngine; + friend class quantifiers::InstStrategyCegqi; friend class quantifiers::ModelEngine; friend class quantifiers::RewriteEngine; friend class quantifiers::QuantConflictFind; @@ -292,6 +294,8 @@ private: void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); + /** record instantiation, return true if it was non-duplicate */ + bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a4ebe5e97..175bd2c2a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2027,6 +2027,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form Trace("strings-entail") << " explanation was : " << et.second << std::endl; conc = e==0 ? eq1 : eq2; antec_new_lits.push_back( et.second ); + break; } } } -- 2.30.2