Add support for quantifier-specific instantiation levels. Add option for setting inst-level 0 only for input terms.

16 files changed, 123 insertions, 43 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 16484a320..33be85d11 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -744,22 +744,22 @@ Command* DefineNamedFunctionCommand::clone() const {
 SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
   d_attr( attr ), d_expr( expr ){
 }
-/*
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr,
+
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
                                                   std::vector<Expr>& values ) throw() :
-  d_id( id ), d_expr( expr ){
+  d_attr( attr ), d_expr( expr ){
   d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() );
 }
 
-SetUserAttributeCommand::SetUserAttributeCommand( const std::string& id, Expr expr,
-                                                  std::string& value ) throw() :
-  d_id( id ), d_expr( expr ), d_str_value( value ){
+SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
+                                                  const std::string& value ) throw() :
+  d_attr( attr ), d_expr( expr ), d_str_value( value ){
 }
-*/
+
 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
   try {
     if(!d_expr.isNull()) {
-      smtEngine->setUserAttribute( d_attr, d_expr );
+      smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
     }
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
@@ -769,11 +769,15 @@ void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
 
 Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){
   Expr expr = d_expr.exportTo(exprManager, variableMap);
-  return new SetUserAttributeCommand( d_attr, expr );
+  SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value );
+  c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
+  return c;
 }
 
 Command* SetUserAttributeCommand::clone() const{
-  return new SetUserAttributeCommand( d_attr, d_expr );
+  SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value );
+  c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
+  return c;
 }
 
 std::string SetUserAttributeCommand::getCommandName() const throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 606618d21..c4e7fbf89 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -439,12 +439,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 protected:
   std::string d_attr;
   Expr d_expr;
-  //std::vector<Expr> d_expr_values;
-  //std::string d_str_value;
+  std::vector<Expr> d_expr_values;
+  std::string d_str_value;
 public:
   SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
-  //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) throw();
+  SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw();
+  SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw();
   ~SetUserAttributeCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d512437af..3f8e321dd 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1167,6 +1167,26 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       attr = std::string(":no-pattern");
       PARSER_STATE->attributeNotSupported(attr);
     }
+  | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL
+    {
+      Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) );
+      std::vector<Expr> values;
+      values.push_back( n );
+      std::string attr_name("inst-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 );
+      c->setMuted(true);
+      PARSER_STATE->preemptCommand(c);
+    }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
@@ -1690,6 +1710,8 @@ INCLUDE_TOK : 'include';
 ATTRIBUTE_PATTERN_TOK : ':pattern';
 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
+ATTRIBUTE_INST_LEVEL : ':inst-level';
+ATTRIBUTE_RR_PRIORITY : ':rr-priority';
 
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 20851ac94..77ee362c0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3174,6 +3174,14 @@ void SmtEnginePrivate::processAssertions() {
   // introducing new ones
 
   dumpAssertions("post-everything", d_assertionsToCheck);
+  
+  //set instantiation level of everything to zero
+  if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
+    for( unsigned i=0; i < d_assertionsToCheck.size(); i++ ) {
+      theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertionsToCheck[i], 0 );
+    }
+  }
+  
 
   // Push the formula to SAT
   {
@@ -4102,9 +4110,13 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
   return d_statisticsRegistry->getStatistic(name);
 }
 
-void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
+void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
   SmtScope smts(this);
-  d_theoryEngine->setUserAttribute(attr, expr.getNode());
+  std::vector<Node> node_values;
+  for( unsigned i=0; i<expr_values.size(); i++ ){
+    node_values.push_back( expr_values[i].getNode() );
+  }
+  d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
 }
 
 void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 71b42534a..1671654d1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -651,7 +651,7 @@ public:
    * This function is called when an attribute is set by a user.
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
-  void setUserAttribute(const std::string& attr, Expr expr);
+  void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value);
 
   /**
    * Set print function in model
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 71b05cec5..3260f7122 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -74,6 +74,8 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de
  when to apply instantiation
 option instMaxLevel --inst-max-level=N int :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 eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index a5de6ffa9..b41987923 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
@@ -22,7 +23,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
+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;
@@ -32,14 +34,22 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
       Trace("quant-attr") << "Set conjecture " << n << std::endl;
       ConjectureAttribute ca;
       n.setAttribute( ca, true );
-    }else if( attr=="rr_priority" ){
-      //Trace("quant-attr") << "Set rr priority " << n << std::endl;
-      //RrPriorityAttribute rra;
-
+    }else if( attr=="inst-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] );
+      setUserAttribute( attr, n[i], node_values, str_value );
     }
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index cf9620a07..34649ae05 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -44,7 +44,7 @@ struct QuantifiersAttributes
     *   This function will apply a custom set of attributes to all top-level universal
     *   quantifiers contained in n
     */
-  static void setUserAttribute( const std::string& attr, Node n );
+  static void setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value );
 };
 
 
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d6b336dfa..504ecd667 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -55,6 +55,13 @@ typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribu
 struct BoundIntLitAttributeId {};
 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
 
+//for quantifier instantiation level
+struct QuantInstLevelAttributeId {};
+typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
+
+//rewrite-rule priority
+struct RrPriorityAttributeId {};
+typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 
 class QuantifiersEngine;
 
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 4ba3c499d..4e8a0a411 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -42,6 +42,8 @@ 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( "rr-priority", this );
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
@@ -193,6 +195,6 @@ bool TheoryQuantifiers::restart(){
   }
 }
 
-void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){
-  QuantifiersAttributes::setUserAttribute( attr, n );
+void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
+  QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index ffd3c4c59..6febc8417 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -69,7 +69,7 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
-  void setUserAttribute( const std::string& attr, Node n );
+  void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
   bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
 private:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f80f65723..eb5dbaef0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -404,7 +404,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
           }
         }
       }
-      setInstantiationLevelAttr( body, f[1], maxInstLevel+1, terms );
+      setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
     }
     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
     ++(d_statistics.d_instantiations);
@@ -415,22 +415,31 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   }
 }
 
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms ){
+void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
+  Trace("inst-level-debug") << "IL : " << n << " " << qn << " " << level << std::endl;
   //if not from the vector of terms we instantiatied
-  if( std::find( inst_terms.begin(), inst_terms.end(), n )==inst_terms.end() ){
+  if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
     //if this is a new term, without an instantiation level
-    if( n!=qn && !n.hasAttribute(InstLevelAttribute()) ){
+    if( !n.hasAttribute(InstLevelAttribute()) ){
       InstLevelAttribute ila;
       n.setAttribute(ila,level);
+      Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
     }
-    Assert( qn.getKind()!=BOUND_VARIABLE );
     Assert( n.getNumChildren()==qn.getNumChildren() );
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      setInstantiationLevelAttr( n[i], qn[i], level, inst_terms );
+      setInstantiationLevelAttr( n[i], qn[i], level );
     }
   }
 }
 
+void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
+  InstLevelAttribute ila;
+  n.setAttribute(ila,level);
+  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    setInstantiationLevelAttr( n[i], level );
+  }
+}
+
 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
   if( n.getKind()==INST_CONSTANT ){
     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
@@ -579,11 +588,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
 
   if( options::instMaxLevel()!=-1 ){
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( terms[i].hasAttribute(InstLevelAttribute()) &&
-          (int)terms[i].getAttribute(InstLevelAttribute())>options::instMaxLevel() ){
-        Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute());
-        Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl;
-        return false;
+      if( terms[i].hasAttribute(InstLevelAttribute()) ){
+        unsigned ml = options::instMaxLevel();
+        if( f.hasAttribute(QuantInstLevelAttribute()) ){
+          ml = f.getAttribute(QuantInstLevelAttribute());
+        }
+        if( terms[i].getAttribute(InstLevelAttribute())>ml ){
+          Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute());
+          Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
+          return false;
+        }
+      }else{
+        if( options::instLevelInputOnly() ){
+          Trace("inst-add-debug") << "Term " << terms[i] << " does not have an instantiation level." << std::endl;
+          return false;
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f74c478ae..5315a1de8 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -205,7 +205,7 @@ private:
   /** instantiate f with arguments terms */
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
-  void setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms );
+  static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
   /** flush lemmas */
   void flushLemmas();
 public:
@@ -235,6 +235,8 @@ public:
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** get number of waiting lemmas */
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+  /** set instantiation level attr */
+  static void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
   /** get number of quantifiers */
   int getNumQuantifiers() { return (int)d_quants.size(); }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 7bfc7051f..ac3d018fb 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -678,7 +678,7 @@ public:
     * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
     *  via the syntax (! n :attr)
     */
-  virtual void setUserAttribute(const std::string& attr, Node n) {
+  virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
     Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface",
                   identify().c_str());
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index eb1da84b2..1b0270b94 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1668,11 +1668,11 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 }
 
 
-void TheoryEngine::setUserAttribute(const std::string& attr, Node n) {
+void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
   Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
   if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
     for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
-      d_attr_handle[attr][i]->setUserAttribute(attr, n);
+      d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
     }
   } else {
     //unhandled exception?
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e6684d56e..eec4f1168 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -820,7 +820,7 @@ public:
    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
    * via the syntax (! n :attr)
    */
-  void setUserAttribute(const std::string& attr, Node n);
+  void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
 
   /**
    * Handle user attribute.