Parser: add the possibility to bind at level 0.

5 files changed, 67 insertions, 30 deletions

diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index 777bbc94b..bf1f7d097 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -68,6 +68,10 @@ public:
     return super::insert(v, v);
   }
 
+  void insertAtContextLevelZero(const V& v) {
+    return super::insertAtContextLevelZero(v, v);
+  }
+
   bool contains(const V& v) {
     return find(v) != end();
   }
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 22187ad06..6038fadab 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -49,17 +49,25 @@ DeclarationScope::~DeclarationScope() {
   delete d_context;
 }
 
-void DeclarationScope::bind(const std::string& name, Expr obj) throw(AssertionException) {
+void DeclarationScope::bind(const std::string& name, Expr obj,
+                            bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
-  d_exprMap->insert(name, obj);
+  if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
+  else d_exprMap->insert(name, obj);
 }
 
-void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException) {
+void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj,
+                            bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
-  d_exprMap->insert(name, obj);
-  d_functions->insert(obj);
+  if(levelZero){
+    d_exprMap->insertAtContextLevelZero(name, obj);
+    d_functions->insertAtContextLevelZero(obj);
+  } else {
+    d_exprMap->insert(name, obj);
+    d_functions->insert(obj);
+  }
 }
 
 bool DeclarationScope::isBound(const std::string& name) const throw() {
@@ -80,13 +88,19 @@ Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionExce
   return (*d_exprMap->find(name)).second;
 }
 
-void DeclarationScope::bindType(const std::string& name, Type t) throw() {
-  d_typeMap->insert(name, make_pair(vector<Type>(), t));
+void DeclarationScope::bindType(const std::string& name, Type t,
+                                bool levelZero) throw() {
+  if(levelZero){
+    d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
+  }else{
+    d_typeMap->insert(name, make_pair(vector<Type>(), t));
+  }
 }
 
 void DeclarationScope::bindType(const std::string& name,
                                 const std::vector<Type>& params,
-                                Type t) throw() {
+                                Type t,
+                                bool levelZero) throw() {
   if(Debug.isOn("sort")) {
     Debug("sort") << "bindType(" << name << ", [";
     if(params.size() > 0) {
@@ -96,7 +110,11 @@ void DeclarationScope::bindType(const std::string& name,
     }
     Debug("sort") << "], " << t << ")" << endl;
   }
-  d_typeMap->insert(name, make_pair(params, t));
+  if(levelZero){
+    d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
+  } else {
+    d_typeMap->insert(name, make_pair(params, t));
+  }
 }
 
 bool DeclarationScope::isBoundType(const std::string& name) const throw() {
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 27533cca8..8695d9287 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -72,12 +72,14 @@ public:
    * <code>name</code> is already bound to an expression in the current
    * level, then the binding is replaced. If <code>name</code> is bound
    * in a previous level, then the binding is "covered" by this one
-   * until the current scope is popped.
+   * until the current scope is popped. If levelZero is true the name
+   * shouldn't be already bound.
    *
    * @param name an identifier
    * @param obj the expression to bind to <code>name</code>
+   * @param levelZero set if the binding must be done at level 0
    */
-  void bind(const std::string& name, Expr obj) throw(AssertionException);
+  void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
 
   /**
    * Bind a function body to a name in the current scope.  If
@@ -89,8 +91,9 @@ public:
    *
    * @param name an identifier
    * @param obj the expression to bind to <code>name</code>
+   * @param levelZero set if the binding must be done at level 0
    */
-  void bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException);
+  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -101,8 +104,9 @@ public:
    *
    * @param name an identifier
    * @param t the type to bind to <code>name</code>
+   * @param levelZero set if the binding must be done at level 0
    */
-  void bindType(const std::string& name, Type t) throw();
+  void bindType(const std::string& name, Type t, bool levelZero = false) throw();
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -117,7 +121,7 @@ public:
    */
   void bindType(const std::string& name,
                 const std::vector<Type>& params,
-                Type t) throw();
+                Type t, bool levelZero = false) throw();
 
   /**
    * Check whether a name is bound to an expression with either bind()
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 3efc315cc..2265355f0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -141,18 +141,20 @@ bool Parser::isPredicate(const std::string& name) {
 }
 
 Expr
-Parser::mkVar(const std::string& name, const Type& type) {
+Parser::mkVar(const std::string& name, const Type& type,
+              bool levelZero) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
-  defineVar(name, expr);
+  defineVar(name, expr, levelZero);
   return expr;
 }
 
 Expr
-Parser::mkFunction(const std::string& name, const Type& type) {
+Parser::mkFunction(const std::string& name, const Type& type,
+                            bool levelZero) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
-  defineFunction(name, expr);
+  defineFunction(name, expr, levelZero);
   return expr;
 }
 
@@ -165,23 +167,26 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
 
 std::vector<Expr>
 Parser::mkVars(const std::vector<std::string> names,
-               const Type& type) {
+               const Type& type,
+               bool levelZero) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type));
+    vars.push_back(mkVar(names[i], type, levelZero));
   }
   return vars;
 }
 
 void
-Parser::defineVar(const std::string& name, const Expr& val) {
-  d_declScope->bind(name, val);
+Parser::defineVar(const std::string& name, const Expr& val,
+                       bool levelZero) {
+  d_declScope->bind(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
 void
-Parser::defineFunction(const std::string& name, const Expr& val) {
-  d_declScope->bindDefinedFunction(name, val);
+Parser::defineFunction(const std::string& name, const Expr& val,
+                       bool levelZero) {
+  d_declScope->bindDefinedFunction(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index a3ddba013..635dd6b6c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -337,16 +337,19 @@ public:
   Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 
   /** Create a new CVC4 variable expression of the given type. */
-  Expr mkVar(const std::string& name, const Type& type);
+  Expr mkVar(const std::string& name, const Type& type,
+             bool levelZero = false);
 
   /**
    * Create a set of new CVC4 variable expressions of the given type.
    */
   std::vector<Expr>
-  mkVars(const std::vector<std::string> names, const Type& type);
+    mkVars(const std::vector<std::string> names, const Type& type,
+           bool levelZero = false);
 
   /** Create a new CVC4 function expression of the given type. */
-  Expr mkFunction(const std::string& name, const Type& type);
+  Expr mkFunction(const std::string& name, const Type& type,
+                  bool levelZero = false);
 
   /**
    * Create a new CVC4 function expression of the given type,
@@ -356,10 +359,12 @@ public:
   Expr mkAnonymousFunction(const std::string& prefix, const Type& type);
 
   /** Create a new variable definition (e.g., from a let binding). */
-  void defineVar(const std::string& name, const Expr& val);
+  void defineVar(const std::string& name, const Expr& val,
+                       bool levelZero = false);
 
   /** Create a new function definition (e.g., from a define-fun). */
-  void defineFunction(const std::string& name, const Expr& val);
+  void defineFunction(const std::string& name, const Expr& val,
+                      bool levelZero = false);
 
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
@@ -432,7 +437,8 @@ public:
   /**
    * Preempt the next returned command with other ones; used to
    * support the :named attribute in SMT-LIBv2, which implicitly
-   * inserts a new command before the current one.
+   * inserts a new command before the current one. Also used in TPTP
+   * because function and predicate symbols are implicitly declared.
    */
   void preemptCommand(Command* cmd);