Add --inst-max-level=N option for Kshitij. Support define-const command in Smt2.

3 files changed, 48 insertions, 14 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2118a240d..8dcebc5ee 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -344,6 +344,28 @@ command returns [CVC4::Command* cmd = NULL]
       Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
+  | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { /* add variables to parser state before parsing term */
+      Debug("parser") << "define const: '" << name << "'" << std::endl;
+      PARSER_STATE->pushScope(true);
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end();
+          i != iend;
+          ++i) {
+        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
+      }
+    }
+    term[expr, expr2]
+    { PARSER_STATE->popScope();
+      // declare the name down here (while parsing term, signature
+      // must not be extended with the name itself; no recursion
+      // permitted)
+      Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
+      $cmd = new DefineFunctionCommand(name, func, terms, expr);
+    }
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -487,7 +509,7 @@ extendedCommand[CVC4::Command*& cmd]
     sortSymbol[t,CHECK_DECLARED]
     { Expr c = PARSER_STATE->mkVar(name, t);
       $cmd = new DeclareFunctionCommand(name, c, t); }
-
+      
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
@@ -1645,6 +1667,7 @@ DECLARE_FUNS_TOK : 'declare-funs';
 DECLARE_PREDS_TOK : 'declare-preds';
 DEFINE_TOK : 'define';
 DECLARE_CONST_TOK : 'declare-const';
+DEFINE_CONST_TOK : 'define-const';
 SIMPLIFY_TOK : 'simplify';
 INCLUDE_TOK : 'include';
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 32e65438e..e733764f0 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -67,6 +67,8 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false
 
 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  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 eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index eaf5e8228..63697f5e7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -319,7 +319,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
       Trace("inst") << "   " << terms[i];
       Trace("inst") << std::endl;
     }
-    //uint64_t maxInstLevel = 0;
     if( options::cbqi() ){
       for( int i=0; i<(int)terms.size(); i++ ){
         if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
@@ -328,22 +327,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
             Debug("inst") << "   " << terms[i] << std::endl;
           }
           Unreachable("Bad instantiation");
-        }else{
-          Trace("inst") << "   " << terms[i];
-          //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
-          Trace("inst") << std::endl;
-          //if( terms[i].hasAttribute(InstLevelAttribute()) ){
-            //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            //  maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
-            //}
-          //}else{
-            //setInstantiationLevelAttr( terms[i], 0 );
-          //}
         }
       }
     }
+    if( options::instMaxLevel()!=-1 ){
+      uint64_t maxInstLevel = 0;
+      for( int i=0; i<(int)terms.size(); i++ ){
+        if( terms[i].hasAttribute(InstLevelAttribute()) ){
+          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+          }
+        }
+      }
+      setInstantiationLevelAttr( body, maxInstLevel+1 );
+    }
     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
-    //setInstantiationLevelAttr( body, maxInstLevel+1 );
     ++(d_statistics.d_instantiations);
     return true;
   }else{
@@ -504,6 +502,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   }
   Trace("inst-add-debug") << std::endl;
 
+  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;
+      }
+    }
+  }
+
   //check for duplication
   ///*
   bool alreadyExists = false;