11 files changed, 153 insertions, 44 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index a32e7f6b0..5f949789a 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -122,10 +122,10 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
-  if( f.getNumChildren()==3 && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){
+  if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){
     return STATUS_UNKNOWN;
   }else{
-    int peffort = ( f.getNumChildren()==3 && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1;
+    int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1;
     //int peffort = 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
@@ -347,6 +347,27 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
   }
 }
 
+bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) {
+  if( f.getNumChildren()==3 ){
+    std::map< Node, bool >::iterator it = d_hasUserPatterns.find( f );
+    if( it==d_hasUserPatterns.end() ){
+      bool hasPat = false;
+      for( unsigned i=0; i<f[2].getNumChildren(); i++ ){
+        if( f[2][i].getKind()==INST_PATTERN ){
+          hasPat = true;
+          break;
+        }
+      }
+      d_hasUserPatterns[f] = hasPat;
+      return hasPat;
+    }else{
+      return it->second;
+    }
+  }else{
+    return false;
+  }
+}
+
 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() ){
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 53ca5bf78..c2b4f7533 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -88,6 +88,10 @@ private:
   int process( Node f, Theory::Effort effort, int e );
   /** generate triggers */
   void generateTriggers( Node f, Theory::Effort effort, int e, int & status );
+  /** has user patterns */
+  bool hasUserPatterns( Node f );
+  /** has user patterns */
+  std::map< Node, bool > d_hasUserPatterns;
 public:
   /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
       rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 1fda30301..a8774440e 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -34,6 +34,7 @@ sort INST_PATTERN_TYPE \
 # 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"
+operator INST_ATTRIBUTE 1 "instantiation attribute"
 
 sort INST_PATTERN_LIST_TYPE \
     Cardinality::INTEGERS \
@@ -48,6 +49,7 @@ 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_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
 
 # for rewrite rules
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 4179dcbf5..2c9a33388 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -383,7 +383,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
   return !TermDb::isRewriteRule( f ) &&
-         ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
+         ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 8d479c29e..f58e89c38 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -25,31 +25,25 @@ using namespace CVC4::theory::quantifiers;
 
 void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value ){
   Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
-  if( n.getKind()==FORALL ){
-    if( attr=="axiom" ){
-      Trace("quant-attr") << "Set axiom " << n << std::endl;
-      AxiomAttribute aa;
-      n.setAttribute( aa, true );
-    }else if( attr=="conjecture" ){
-      Trace("quant-attr") << "Set conjecture " << n << std::endl;
-      ConjectureAttribute ca;
-      n.setAttribute( ca, true );
-    }else if( attr=="quant-inst-max-level" ){
-      Assert( node_values.size()==1 );
-      uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
-      Trace("quant-attr") << "Set instantiation level " << n << " to " << lvl << std::endl;
-      QuantInstLevelAttribute qila;
-      n.setAttribute( qila, lvl );
-    }else if( attr=="rr-priority" ){
-      Assert( node_values.size()==1 );
-      uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
-      Trace("quant-attr") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
-      RrPriorityAttribute rrpa;
-      n.setAttribute( rrpa, lvl );
-    }
-  }else{
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      setUserAttribute( attr, n[i], node_values, str_value );
-    }
+  if( attr=="axiom" ){
+    Trace("quant-attr-debug") << "Set axiom " << n << std::endl;
+    AxiomAttribute aa;
+    n.setAttribute( aa, true );
+  }else if( attr=="conjecture" ){
+    Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
+    ConjectureAttribute ca;
+    n.setAttribute( ca, true );
+  }else if( attr=="quant-inst-max-level" ){
+    Assert( node_values.size()==1 );
+    uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
+    Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
+    QuantInstLevelAttribute qila;
+    n.setAttribute( qila, lvl );
+  }else if( attr=="rr-priority" ){
+    Assert( node_values.size()==1 );
+    uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
+    Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
+    RrPriorityAttribute rrpa;
+    n.setAttribute( rrpa, lvl );
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 34649ae05..bad58eef8 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -26,14 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** Attribute true for quantifiers that are axioms */
-struct AxiomAttributeId {};
-typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
-
-/** Attribute true for quantifiers that are conjecture */
-struct ConjectureAttributeId {};
-typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
-
 /** Attribute priority for rewrite rules */
 //struct RrPriorityAttributeId {};
 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0d85eae83..7ec503016 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -976,3 +976,66 @@ Node TermDb::getRewriteRule( Node q ) {
     return Node::null();
   }
 }
+
+
+void TermDb::computeAttributes( Node q ) {
+  if( q.getNumChildren()==3 ){
+    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+      if( q[2][i].getKind()==INST_ATTRIBUTE ){
+        Node avar = q[2][i][0];
+        if( avar.getAttribute(AxiomAttribute()) ){
+          Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
+          d_qattr_axiom[q] = true;
+        }
+        if( avar.getAttribute(ConjectureAttribute()) ){
+          Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
+          d_qattr_conjecture[q] = true;
+        }
+        if( avar.hasAttribute(QuantInstLevelAttribute()) ){
+          d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
+          Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
+        }
+        if( avar.hasAttribute(RrPriorityAttribute()) ){
+          d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
+          Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
+        }
+      }
+    }
+  }
+}
+
+bool TermDb::isQAttrConjecture( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_conjecture.find( q );
+  if( it==d_qattr_conjecture.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
+bool TermDb::isQAttrAxiom( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_axiom.find( q );
+  if( it==d_qattr_axiom.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
+int TermDb::getQAttrQuantInstLevel( Node q ) {
+  std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
+  if( it==d_qattr_qinstLevel.end() ){
+    return -1;
+  }else{
+    return it->second;
+  }
+}
+
+int TermDb::getQAttrRewriteRulePriority( Node q ) {
+  std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q );
+  if( it==d_qattr_rr_priority.end() ){
+    return -1;
+  }else{
+    return it->second;
+  }
+}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 91ad0135b..e9234bdfe 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -25,6 +25,14 @@
 namespace CVC4 {
 namespace theory {
 
+/** Attribute true for quantifiers that are axioms */
+struct AxiomAttributeId {};
+typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
+
+/** Attribute true for quantifiers that are conjecture */
+struct ConjectureAttributeId {};
+typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
+  
 /** Attribute true for nodes that should not be used for matching */
 struct NoMatchAttributeId {};
 /** use the special for boolean flag */
@@ -285,6 +293,24 @@ public: //general queries concerning quantified formulas wrt modules
   /** get the rewrite rule associated with the quanfied formula */
   static Node getRewriteRule( Node q );
   
+//attributes
+private:
+  std::map< Node, bool > d_qattr_conjecture;
+  std::map< Node, bool > d_qattr_axiom;
+  std::map< Node, int > d_qattr_rr_priority;
+  std::map< Node, int > d_qattr_qinstLevel;
+  //record attributes
+  void computeAttributes( Node q );
+public:
+  /** is conjecture */
+  bool isQAttrConjecture( Node q );
+  /** is axiom */
+  bool isQAttrAxiom( Node q );
+  /** get instantiation level */
+  int getQAttrQuantInstLevel( Node q );
+  /** get rewrite rule priority */
+  int getQAttrRewriteRulePriority( Node q );
+  
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 18546b09c..e71489fc5 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -42,7 +42,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
-  out.handleUserAttribute( "inst-level", this );
+  out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "rr-priority", this );
 }
 
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 7fc69c539..5d86c29c0 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -96,13 +96,21 @@ struct QuantifierInstNoPatternTypeRule {
   }
 };/* struct QuantifierInstNoPatternTypeRule */
 
+struct QuantifierInstAttributeTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::INST_ATTRIBUTE );
+    return nodeManager->instPatternType();
+  }
+};/* struct QuantifierInstAttributeTypeRule */
+
 struct QuantifierInstPatternListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
     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 && n[i].getKind()!=kind::INST_NO_PATTERN ){
+        if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){
           throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern");
         }
       }
@@ -148,7 +156,6 @@ public:
   }
 };/* class RewriteRuleTypeRule */
 
-
 class RRRewriteTypeRule {
 public:
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5bf285ae2..d81db8b8d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -286,6 +286,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){
     Assert( f.getKind()==FORALL );
     //make instantiation constants for f
     d_term_db->makeInstantiationConstantsFor( f );
+    d_term_db->computeAttributes( f );
     //register with quantifier relevance
     if( d_quant_rel ){
       d_quant_rel->registerQuantifier( f );
@@ -464,10 +465,9 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 
 bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) {
   if( n.hasAttribute(InstLevelAttribute()) ){
-    unsigned ml = options::instMaxLevel();
-    if( f.hasAttribute(QuantInstLevelAttribute()) ){
-      ml = f.getAttribute(QuantInstLevelAttribute());
-    }
+    int fml = d_term_db->getQAttrQuantInstLevel( f );
+    unsigned ml = fml>=0 ? fml : options::instMaxLevel();
+
     if( n.getAttribute(InstLevelAttribute())>ml ){
       Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
       Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;