Refactor quantifiers attributes.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e7d614b8512acddee11ca5e5ca30c3cae120df17..366c76194f1ade306ac89472dcb4972633a085a8 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1079,7 +1079,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
     /* attributed expressions */
   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
     ( attribute[expr, attexpr, attr]
-      { if( ( attr == ":pattern" || attr == ":no-pattern" ) && ! attexpr.isNull()) {
+      { if( ! attexpr.isNull()) {
           patexprs.push_back( attexpr );
         }
       }
@@ -1199,7 +1199,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       }
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
-      Command* c = new SetUserAttributeCommand( attr_name, expr );
+      //will set the attribute on auxiliary var (preserves attribute on formula through rewriting)
+      Type t = EXPR_MANAGER->booleanType();
+      Expr avar = PARSER_STATE->mkVar(attr_name, t);
+      retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
+      Command* c = new SetUserAttributeCommand( attr_name, avar );
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     } else {
@@ -1216,23 +1220,17 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       attr = std::string(":no-pattern");
       retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr);
     }
-  | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL
+  | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL
     {
       Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
       std::vector<Expr> values;
       values.push_back( n );
-      std::string attr_name("quant-inst-max-level");
-      Command* c = new SetUserAttributeCommand( attr_name, expr, values );
-      c->setMuted(true);
-      PARSER_STATE->preemptCommand(c);
-    }
-  | ATTRIBUTE_RR_PRIORITY_LEVEL INTEGER_LITERAL
-    {
-      Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
-      std::vector<Expr> values;
-      values.push_back( n );
-      std::string attr_name("rr-priority");
-      Command* c = new SetUserAttributeCommand( attr_name, expr, values );
+      std::string attr_name(AntlrInput::tokenText($tok));
+      attr_name.erase( attr_name.begin() );
+      Type t = EXPR_MANAGER->booleanType();
+      Expr avar = PARSER_STATE->mkVar(attr_name, t);
+      retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
+      Command* c = new SetUserAttributeCommand( attr_name, avar, values );
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 89f35bf05384c4bb75eddc6bbdf1e15333dd06e7..6ce8efef913198ba3e458c31cdb56ede74fda5da 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -724,6 +724,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
       switch(k) {
+      case kind::INST_ATTRIBUTE:
       case kind::BOUND_VAR_LIST:
         result.top() << top;
         worklist.pop();

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index a32e7f6b0fb5f06c9d7b05cdbcddc3d4010eddbf..5f949789a3ad83586b37657aa45e4a09fdc96af7 100644 (file)
--- 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 53ca5bf78300785dae8f22775b417de4884289a4..c2b4f7533136ef38ab7b0063c032593855cba257 100644 (file)
--- 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 1fda30301376829f8e8558f83fb20b6617c93a23..a8774440eb256b87de43c9de556e77a106a4eb79 100644 (file)
--- 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 4179dcbf530394638960fca383438c8f2b6e90a5..2c9a33388e9efc3e360c43db050cca7d0ec9b780 100644 (file)
--- 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 8d479c29ebbb7532bb089bf802a18b37c6b20675..f58e89c38261457de38be1b3d6abd67e8087766c 100644 (file)
--- 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 34649ae0504fa767b6dc2cc13e479554e0cde6de..bad58eef850f49b319f79c643616d0bd7fe8b4f7 100644 (file)
--- 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 0d85eae8331a5231f04bf47c6a4be2046c01fc4a..7ec5030166d71daf010c72426d2283ac19edd152 100644 (file)
--- 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 91ad0135be8d6034d7eaf7a974186012c77f0cd9..e9234bdfeafbf04d363870456e5e1bfdf908cf35 100644 (file)
--- 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 18546b09cbf8a6fe6931ec5a0539ad1b075fc858..e71489fc52303ffbfbc18428069726bf7a9aefec 100644 (file)
--- 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 7fc69c539c0fd15173faf09adefa59426c1a4ced..5d86c29c042aaac10163dc45b78963897ef3c4fc 100644 (file)
--- 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 5bf285ae2f3ec392969e5ae0351a1b4f978e45ea..d81db8b8dfab3f7a668264adebc8adbcf64a63ce 100644 (file)
--- 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;