Support :no-pattern.

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; i<f2.getNumChildren(); i++ ){
-            patexprs.push_back( f2[i] );
+            if( f2[i].getKind()==kind::INST_PATTERN ){
+              patexprs.push_back( f2[i] );
+            }else{
+              std::stringstream ss;
+              ss << "warning: rewrite rules do not support " << f2[i] << " within instantiation pattern list";
+              PARSER_STATE->warning(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 );