Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer

5 files changed, 32 insertions, 37 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index cf21ca6eb..9131c220f 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -953,7 +953,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
           } else {
             Debug("parser") << "  " << *i << " not declared" << std::endl;
             if(topLevel) {
-              Expr func = PARSER_STATE->mkVar(*i, t, true);
+              Expr func = PARSER_STATE->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
               Command* decl = new DeclareFunctionCommand(*i, func, t);
               seq->addCommand(decl);
             } else {
@@ -968,13 +968,14 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
           // like e.g. FORALL(x:INT = 4): [...]
           PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
         }
-        Debug("parser") << "made " << idList.front() << " = " << f << std::endl;
+        assert(!idList.empty());
         for(std::vector<std::string>::const_iterator i = idList.begin(),
               i_end = idList.end();
             i != i_end;
             ++i) {
+          Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
-          Expr func = EXPR_MANAGER->mkVar(*i, t, true);
+          Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
           PARSER_STATE->defineFunction(*i, f);
           Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
@@ -1330,7 +1331,7 @@ prefixFormula[CVC4::Expr& f]
     { PARSER_STATE->popScope();
       Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
       std::string name = "lambda";
-      Expr func = PARSER_STATE->mkAnonymousFunction(name, t);
+      Expr func = PARSER_STATE->mkAnonymousFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
       Command* cmd = new DefineFunctionCommand(name, func, terms, f);
       PARSER_STATE->preemptCommand(cmd);
       f = func;
@@ -1341,7 +1342,7 @@ prefixFormula[CVC4::Expr& f]
     boundVarDecl[ids,t] RPAREN COLON formula[f]
     { PARSER_STATE->popScope();
       UNSUPPORTED("array literals not supported yet");
-      f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), true);
+      f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), ExprManager::VAR_FLAG_GLOBAL);
     }
   ;
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a7834a5aa..125861113 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -139,11 +139,10 @@ bool Parser::isPredicate(const std::string& name) {
 }
 
 Expr
-Parser::mkVar(const std::string& name, const Type& type,
-              bool levelZero) {
-  Debug("parser") << "mkVar(" << name << ", " << type << ", " << levelZero << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(name, type, levelZero);
-  defineVar(name, expr, levelZero);
+Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+  Expr expr = d_exprManager->mkVar(name, type, flags);
+  defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
   return expr;
 }
 
@@ -156,35 +155,31 @@ Parser::mkBoundVar(const std::string& name, const Type& type) {
 }
 
 Expr
-Parser::mkFunction(const std::string& name, const Type& type,
-                   bool levelZero) {
+Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(name, type, levelZero);
-  defineFunction(name, expr, levelZero);
+  Expr expr = d_exprManager->mkVar(name, type, flags);
+  defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
   return expr;
 }
 
 Expr
-Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
+Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
   stringstream name;
   name << prefix << "_anon_" << ++d_anonymousFunctionCount;
-  return mkFunction(name.str(), type);
+  return mkFunction(name.str(), type, flags);
 }
 
 std::vector<Expr>
-Parser::mkVars(const std::vector<std::string> names,
-               const Type& type,
-               bool levelZero) {
+Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type, levelZero));
+    vars.push_back(mkVar(names[i], type, flags));
   }
   return vars;
 }
 
 std::vector<Expr>
-Parser::mkBoundVars(const std::vector<std::string> names,
-                    const Type& type) {
+Parser::mkBoundVars(const std::vector<std::string> names, const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkBoundVar(names[i], type));
@@ -193,16 +188,14 @@ Parser::mkBoundVars(const std::vector<std::string> names,
 }
 
 void
-Parser::defineVar(const std::string& name, const Expr& val,
-                  bool levelZero) {
-  Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
+Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) {
+  Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;;
   d_symtab->bind(name, val, levelZero);
   assert( isDeclared(name) );
 }
 
 void
-Parser::defineFunction(const std::string& name, const Expr& val,
-                       bool levelZero) {
+Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) {
   d_symtab->bindDefinedFunction(name, val, levelZero);
   assert( isDeclared(name) );
 }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 91566f5f6..d07756cf4 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -359,14 +359,14 @@ public:
 
   /** Create a new CVC4 variable expression of the given type. */
   Expr mkVar(const std::string& name, const Type& type,
-             bool levelZero = false);
+             uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
   /**
    * 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,
-           bool levelZero = false);
+           uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
   /** Create a new CVC4 bound variable expression of the given type. */
   Expr mkBoundVar(const std::string& name, const Type& type);
@@ -378,18 +378,19 @@ public:
 
   /** Create a new CVC4 function expression of the given type. */
   Expr mkFunction(const std::string& name, const Type& type,
-                  bool levelZero = false);
+                  uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
   /**
    * Create a new CVC4 function expression of the given type,
    * appending a unique index to its name.  (That's the ONLY
    * difference between mkAnonymousFunction() and mkFunction()).
    */
-  Expr mkAnonymousFunction(const std::string& prefix, const Type& type);
+  Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
+                           uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val,
-                       bool levelZero = false);
+                 bool levelZero = false);
 
   /** Create a new function definition (e.g., from a define-fun). */
   void defineFunction(const std::string& name, const Expr& val,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c048feea7..f047bc88e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -329,7 +329,7 @@ command returns [CVC4::Command* cmd = NULL]
       // 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);
+      Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
   | /* value query */
@@ -526,7 +526,7 @@ extendedCommand[CVC4::Command*& cmd]
     ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
       { PARSER_STATE->checkUserSymbol(name); }
       term[e,e2]
-      { Expr func = PARSER_STATE->mkFunction(name, e.getType());
+      { Expr func = PARSER_STATE->mkFunction(name, e.getType(), ExprManager::VAR_FLAG_DEFINED);
         $cmd = new DefineFunctionCommand(name, func, e);
       }
     | LPAREN_TOK
@@ -560,7 +560,7 @@ extendedCommand[CVC4::Command*& cmd]
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
-        Expr func = PARSER_STATE->mkFunction(name, t);
+        Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
         $cmd = new DefineFunctionCommand(name, func, terms, e);
       }
     )
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 96c608f77..eb49d7dcc 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -177,7 +177,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name,
       expr = getVariable(name);
     } else {
       Type t = term ? d_unsorted : getExprManager()->booleanType();
-      expr = mkVar(name, t, true); // levelZero
+      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
       preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
   } else { // Its an application
@@ -187,7 +187,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name,
       std::vector<Type> sorts(args.size(), d_unsorted);
       Type t = term ? d_unsorted : getExprManager()->booleanType();
       t = getExprManager()->mkFunctionType(sorts, t);
-      expr = mkVar(name, t, true); // levelZero
+      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
       preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
     // args might be rationals, in which case we need to create