From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 23 Aug 2013 20:01:13 +0000 (-0400)
Subject: Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault... 
X-Git-Tag: cvc5-1.0.0~7287^2~31
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3a4670710d3ffdc99879a1d27f37cf775af18eb;p=cvc5.git

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

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 3a2feb624..424ebab11 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -805,20 +805,20 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) {
+Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal);
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
   INC_STAT_VAR(type, false);
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(Type type, bool isGlobal) {
+Expr ExprManager::mkVar(Type type, uint32_t flags) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal));
+  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
 }
 
 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 15278dfb6..58c0bbae3 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -468,6 +468,13 @@ public:
   Type getType(Expr e, bool check = false)
     throw(TypeCheckingException);
 
+  /** Bits for use in mkVar() flags. */
+  enum {
+    VAR_FLAG_NONE = 0,
+    VAR_FLAG_GLOBAL = 1,
+    VAR_FLAG_DEFINED = 2
+  };/* enum */
+
   /**
    * Create a new, fresh variable.  This variable is guaranteed to be
    * distinct from every variable thus far in the ExprManager, even
@@ -477,28 +484,33 @@ public:
    *
    * @param name a name to associate to the fresh new variable
    * @param type the type for the new variable
-   * @param isGlobal whether this variable is to be considered "global"
-   * or not.  Note that this information isn't used by the ExprManager,
-   * but is passed on to the ExprManager's event subscribers like the
-   * model-building service; if isGlobal is true, this newly-created
-   * variable will still available in models generated after an
-   * intervening pop.
+   * @param flags - VAR_FLAG_NONE - no flags;
+   * VAR_FLAG_GLOBAL - whether this variable is to be
+   * considered "global" or not.  Note that this information isn't
+   * used by the ExprManager, but is passed on to the ExprManager's
+   * event subscribers like the model-building service; if isGlobal
+   * is true, this newly-created variable will still available in
+   * models generated after an intervening pop.
+   * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
+   * use with SmtEngine::defineFunction().  This keeps a declaration
+   * from being emitted in API dumps (since a subsequent definition is
+   * expected to be dumped instead).
    */
-  Expr mkVar(const std::string& name, Type type, bool isGlobal = false);
+  Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
 
   /**
    * Create a (nameless) new, fresh variable.  This variable is guaranteed
    * to be distinct from every variable thus far in the ExprManager.
    *
    * @param type the type for the new variable
-   * @param isGlobal whether this variable is to be considered "global"
+   * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
    * or not.  Note that this information isn't used by the ExprManager,
    * but is passed on to the ExprManager's event subscribers like the
    * model-building service; if isGlobal is true, this newly-created
    * variable will still available in models generated after an
    * intervening pop.
    */
-  Expr mkVar(Type type, bool isGlobal = false);
+  Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
 
   /**
    * Create a new, fresh variable for use in a binder expression
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 7e809ed62..1b1bc7535 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -146,7 +146,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
           bool isGlobal;
           Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
           NodeManagerScope nullScope(NULL);
-          to_e = to->mkVar(name, type, isGlobal);// FIXME thread safety
+          to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : ExprManager::VAR_FLAG_NONE);// FIXME thread safety
         } else if(n.getKind() == kind::SKOLEM) {
           // skolems are only available at the Node level (not the Expr level)
           TypeNode typeNode = TypeNode::fromType(type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 913b8befb..f44c7e78b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -79,8 +79,8 @@ public:
   virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
   virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
   virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
-  virtual void nmNotifyNewVar(TNode n, bool isGlobal) { }
-  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { }
+  virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
+  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
 };/* class NodeManagerListener */
 
 class NodeManager {
@@ -90,8 +90,8 @@ class NodeManager {
   friend class expr::TypeChecker;
 
   // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal);
-  friend Expr ExprManager::mkVar(Type, bool isGlobal);
+  friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
+  friend Expr ExprManager::mkVar(Type, uint32_t flags);
 
   // friend so it can access NodeManager's d_listeners and notify clients
   friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
@@ -309,12 +309,12 @@ class NodeManager {
    * version of this is private to avoid internal uses of mkVar() from
    * within CVC4.  Such uses should employ mkSkolem() instead.
    */
-  Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false);
+  Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+  Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
   /** Create a variable with the given type. */
-  Node mkVar(const TypeNode& type, bool isGlobal = false);
-  Node* mkVarPtr(const TypeNode& type, bool isGlobal = false);
+  Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+  Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
 public:
 
@@ -1532,27 +1532,27 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 }
 
 
-inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) {
+inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
-  setAttribute(n, expr::GlobalVarAttr(), isGlobal);
+  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, isGlobal);
+    (*i)->nmNotifyNewVar(n, flags);
   }
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const std::string& name,
-                                   const TypeNode& type, bool isGlobal) {
+                                   const TypeNode& type, uint32_t flags) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
-  setAttribute(*n, expr::GlobalVarAttr(), isGlobal);
+  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, isGlobal);
+    (*i)->nmNotifyNewVar(*n, flags);
   }
   return n;
 }
@@ -1570,24 +1570,24 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name,
   return n;
 }
 
-inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) {
+inline Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
-  setAttribute(n, expr::GlobalVarAttr(), isGlobal);
+  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, isGlobal);
+    (*i)->nmNotifyNewVar(n, flags);
   }
   return n;
 }
 
-inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) {
+inline Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
-  setAttribute(*n, expr::GlobalVarAttr(), isGlobal);
+  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, isGlobal);
+    (*i)->nmNotifyNewVar(*n, flags);
   }
   return n;
 }
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
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 76856532f..7b25c6fd9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -556,6 +556,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
+     tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
      tryToStream<DeclareFunctionCommand>(out, c) ||
      tryToStream<DeclareTypeCommand>(out, c) ||
@@ -770,15 +771,26 @@ static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw()
 
 static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
   Expr func = c->getFunction();
-  const vector<Expr>& formals = c->getFormals();
+  const vector<Expr>* formals = &c->getFormals();
   out << "(define-fun " << func << " (";
   Type type = func.getType();
+  Expr formula = c->getFormula();
   if(type.isFunction()) {
-    vector<Expr>::const_iterator i = formals.begin();
+    vector<Expr> f;
+    if(formals->empty()) {
+      const vector<Type>& params = FunctionType(type).getArgTypes();
+      for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
+        f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
+                                                       NodeManager::SKOLEM_NO_NOTIFY).toExpr());
+      }
+      formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
+      formals = &f;
+    }
+    vector<Expr>::const_iterator i = formals->begin();
     for(;;) {
       out << "(" << (*i) << " " << (*i).getType() << ")";
       ++i;
-      if(i != formals.end()) {
+      if(i != formals->end()) {
         out << " ";
       } else {
         break;
@@ -786,7 +798,6 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
     }
     type = FunctionType(type).getRangeType();
   }
-  Expr formula = c->getFormula();
   out << ") " << type << " " << formula << ")";
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index df253bef5..603e82c3e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -438,17 +438,19 @@ public:
     d_smt.addToModelCommandAndDump(c);
   }
 
-  void nmNotifyNewVar(TNode n, bool isGlobal) {
+  void nmNotifyNewVar(TNode n, uint32_t flags) {
     DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
                              n.toExpr(),
                              n.getType().toType());
-    d_smt.addToModelCommandAndDump(c, isGlobal);
+    if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
+      d_smt.addToModelCommandAndDump(c, flags);
+    }
     if(n.getType().isBoolean() && !options::incrementalSolving()) {
       d_boolVars.push_back(n);
     }
   }
 
-  void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) {
+  void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) {
     string id = n.getAttribute(expr::VarNameAttr());
     DeclareFunctionCommand c(id,
                              n.toExpr(),
@@ -456,7 +458,9 @@ public:
     if(Dump.isOn("skolems") && comment != "") {
       Dump("skolems") << CommentCommand(id + " is " + comment);
     }
-    d_smt.addToModelCommandAndDump(c, isGlobal, false, "skolems");
+    if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
+      d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
+    }
     if(n.getType().isBoolean() && !options::incrementalSolving()) {
       d_boolVars.push_back(n);
     }
@@ -1218,13 +1222,13 @@ void SmtEngine::defineFunction(Expr func,
       throw TypeCheckingException(func, ss.str());
     }
   }
-  if(Dump.isOn("declarations")) {
-    stringstream ss;
-    ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
-       << func;
-    DefineFunctionCommand c(ss.str(), func, formals, formula);
-    addToModelCommandAndDump(c, false, true, "declarations");
-  }
+
+  stringstream ss;
+  ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
+     << func;
+  DefineFunctionCommand c(ss.str(), func, formals, formula);
+  addToModelCommandAndDump(c, ExprManager::VAR_FLAG_NONE, true, "declarations");
+
   SmtScope smts(this);
 
   // Substitute out any abstract values in formula
@@ -3412,7 +3416,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   return SExpr(sexprs);
 }
 
-void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool userVisible, const char* dumpTag) {
+void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) {
   Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
   SmtScope smts(this);
   // If we aren't yet fully inited, the user might still turn on
@@ -3425,7 +3429,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool u
   // and expects to find their cardinalities in the model.
   if(/* userVisible && */ (!d_fullyInited || options::produceModels())) {
     doPendingPops();
-    if(isGlobal) {
+    if(flags & ExprManager::VAR_FLAG_GLOBAL) {
       d_modelGlobalCommands.push_back(c.clone());
     } else {
       d_modelCommands->push_back(c.clone());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 552f5cd67..9f00fad6b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -331,7 +331,7 @@ class CVC4_PUBLIC SmtEngine {
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
-  void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations");
+  void addToModelCommandAndDump(const Command& c, uint32_t flags = ExprManager::VAR_FLAG_NONE, bool userVisible = true, const char* dumpTag = "declarations");
 
   /**
    * Get the model (only if immediately preceded by a SAT