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

4 files changed, 46 insertions, 34 deletions

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;
 }