From ff216dc63edd0e9dc50bc38010ea50fa565e7e97 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 23 Sep 2014 15:34:03 +0200 Subject: [PATCH] Support :no-pattern. --- src/parser/smt2/Smt2.g | 14 ++++++++---- .../quantifiers/inst_strategy_e_matching.cpp | 14 ++++++++++-- .../quantifiers/inst_strategy_e_matching.h | 4 ++++ .../quantifiers/instantiation_engine.cpp | 12 +++++++++- src/theory/quantifiers/instantiation_engine.h | 1 + src/theory/quantifiers/kinds | 2 ++ .../theory_quantifiers_type_rules.h | 9 +++++++- src/theory/quantifiers/trigger.cpp | 22 ++++++++++++------- src/theory/quantifiers/trigger.h | 4 ++-- 9 files changed, 64 insertions(+), 18 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2efa7b55c..61b898806 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1050,7 +1050,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr, attr] - { if(attr == ":pattern" && ! attexpr.isNull()) { + { if( ( attr == ":pattern" || attr == ":no-pattern" ) && ! attexpr.isNull()) { patexprs.push_back( attexpr ); } } @@ -1084,7 +1084,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else if(! patexprs.empty()) { if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ for( size_t i=0; iwarning(ss.str()); + } } } expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); @@ -1176,10 +1182,10 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":pattern"); retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); } - | ATTRIBUTE_NO_PATTERN_TOK LPAREN_TOK term[patexpr, e2]+ RPAREN_TOK + | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2] { attr = std::string(":no-pattern"); - PARSER_STATE->attributeNotSupported(attr); + retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr); } | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index ef1997d4c..a32e7f6b0 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -88,6 +88,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ } void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ + Assert( pat.getKind()==INST_PATTERN ); //add to generators bool usable = true; std::vector< Node > nodes; @@ -100,6 +101,7 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ } } if( usable ){ + Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl; //extend to literal matching d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option @@ -196,8 +198,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; - Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true ); - Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; + Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true ); + Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen.size() << std::endl; Trace("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ Trace("auto-gen-trigger") << patTermsF[i] << " "; @@ -345,6 +347,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor } } +void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) { + Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 ); + if( std::find( d_user_no_gen[f].begin(), d_user_no_gen[f].end(), pat[0] )==d_user_no_gen[f].end() ){ + Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << f << std::endl; + d_user_no_gen[f].push_back( pat[0] ); + } +} + void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 968194e49..53ca5bf78 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -80,6 +80,8 @@ private: std::map< Node, bool > d_made_multi_trigger; //processed trigger this round std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger; + //instantiation no patterns + std::map< Node, std::vector< Node > > d_user_no_gen; private: /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); @@ -111,6 +113,8 @@ public: } /** set generate additional */ void setGenerateAdditional( bool val ) { d_generate_additional = val; } + /** add pattern */ + void addUserNoPattern( Node f, Node pat ); };/* class InstStrategyAutoGenTriggers */ class InstStrategyFreeVariable : public InstStrategy{ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 684831773..7207ceefb 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -315,7 +315,11 @@ void InstantiationEngine::registerQuantifier( Node f ){ //add patterns for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; - addUserPattern( f, subsPat[i] ); + if( subsPat[i].getKind()==INST_PATTERN ){ + addUserPattern( f, subsPat[i] ); + }else if( subsPat[i].getKind()==INST_NO_PATTERN ){ + addUserNoPattern( f, subsPat[i] ); + } } } } @@ -432,6 +436,12 @@ void InstantiationEngine::addUserPattern( Node f, Node pat ){ } } +void InstantiationEngine::addUserNoPattern( Node f, Node pat ){ + if( d_i_ag ){ + d_i_ag->addUserNoPattern( f, pat ); + } +} + InstantiationEngine::Statistics::Statistics(): d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0), d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0), diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 393f53897..bf0bb03e1 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -137,6 +137,7 @@ public: Node getNextDecisionRequest(); /** add user pattern */ void addUserPattern( Node f, Node pat ); + void addUserNoPattern( Node f, Node pat ); public: /** statistics class */ class Statistics { diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 6fb480c3d..1fda30301 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -33,6 +33,7 @@ sort INST_PATTERN_TYPE \ # This node is used for specifying hints for quantifier instantiation. # An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger. operator INST_PATTERN 1: "instantiation pattern" +operator INST_NO_PATTERN 1 "instantiation no-pattern" sort INST_PATTERN_LIST_TYPE \ Cardinality::INTEGERS \ @@ -46,6 +47,7 @@ typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule +typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule # for rewrite rules diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index e4b1732dd..7fc69c539 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -88,6 +88,13 @@ struct QuantifierInstPatternTypeRule { } };/* struct QuantifierInstPatternTypeRule */ +struct QuantifierInstNoPatternTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::INST_NO_PATTERN ); + return nodeManager->instPatternType(); + } +};/* struct QuantifierInstNoPatternTypeRule */ struct QuantifierInstPatternListTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -95,7 +102,7 @@ struct QuantifierInstPatternListTypeRule { Assert(n.getKind() == kind::INST_PATTERN_LIST ); if( check ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=kind::INST_PATTERN ){ + if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN ){ throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern"); } } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 11ec0210d..b2b8e7197 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -325,7 +325,7 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; bool newHasPol = n.getKind()==IFF ? false : hasPol; @@ -337,14 +337,17 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; }else{ - Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + Node nu; + if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ + nu = getIsUsableTrigger( n, f, pol, hasPol ); + } if( !nu.isNull() ){ patMap[ nu ] = true; return true; @@ -355,7 +358,10 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } }else{ bool retVal = false; - Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + Node nu; + if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ + nu = getIsUsableTrigger( n, f, pol, hasPol ); + } if( !nu.isNull() ){ patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ @@ -367,7 +373,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } @@ -408,12 +414,12 @@ bool Trigger::isPureTheoryTrigger( Node n ) { } } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); + collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); @@ -441,7 +447,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); + collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 74a87591f..75ada4f83 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -94,7 +94,7 @@ private: static bool isUsable( Node n, Node f ); static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ); + static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { @@ -102,7 +102,7 @@ public: TS_MIN_TRIGGER, TS_ALL, }; - static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false ); + static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false ); public: /** is usable trigger */ static bool isUsableTrigger( Node n, Node f ); -- 2.30.2