Fix declare-datatypes dumping bug (bug 385).

3 files changed, 22 insertions, 14 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a838d6d30..d87c498e6 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -718,9 +718,9 @@ TesterType ExprManager::mkTesterType(Type domain) const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
 }
 
-SortType ExprManager::mkSort(const std::string& name) const {
+SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const {
   NodeManagerScope nms(d_nodeManager);
-  return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))));
+  return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags))));
 }
 
 SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 58c0bbae3..3f0ec2f9c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -430,8 +430,14 @@ public:
   /** Make a type representing a tester with the given parameterization. */
   TesterType mkTesterType(Type domain) const;
 
+  /** Bits for use in mkSort() flags. */
+  enum {
+    SORT_FLAG_NONE = 0,
+    SORT_FLAG_PLACEHOLDER = 1
+  };/* enum */
+
   /** Make a new sort with the given name. */
-  SortType mkSort(const std::string& name) const;
+  SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
 
   /** Make a sort constructor from a name and arity. */
   SortConstructorType mkSortConstructor(const std::string& name,
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7c84f3f15..a65655501 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -75,9 +75,9 @@ typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordA
 class NodeManagerListener {
 public:
   virtual ~NodeManagerListener() { }
-  virtual void nmNotifyNewSort(TypeNode tn) { }
+  virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
   virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
-  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
+  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
   virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
   virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
   virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
@@ -778,14 +778,15 @@ public:
   inline TypeNode mkTesterType(TypeNode domain);
 
   /** Make a new (anonymous) sort of arity 0. */
-  inline TypeNode mkSort();
+  inline TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort with the given name of arity 0. */
-  inline TypeNode mkSort(const std::string& name);
+  inline TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort by parameterizing the given sort constructor. */
   inline TypeNode mkSort(TypeNode constructor,
-                         const std::vector<TypeNode>& children);
+                         const std::vector<TypeNode>& children,
+                         uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort with the given name and arity. */
   inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
@@ -1220,31 +1221,32 @@ inline bool NodeManager::hasOperator(Kind k) {
   }
 }
 
-inline TypeNode NodeManager::mkSort() {
+inline TypeNode NodeManager::mkSort(uint32_t flags) {
   NodeBuilder<1> nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn);
+    (*i)->nmNotifyNewSort(tn, flags);
   }
   return tn;
 }
 
-inline TypeNode NodeManager::mkSort(const std::string& name) {
+inline TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
   NodeBuilder<1> nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   setAttribute(tn, expr::VarNameAttr(), name);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn);
+    (*i)->nmNotifyNewSort(tn, flags);
   }
   return tn;
 }
 
 inline TypeNode NodeManager::mkSort(TypeNode constructor,
-                                    const std::vector<TypeNode>& children) {
+                                    const std::vector<TypeNode>& children,
+                                    uint32_t flags) {
   Assert(constructor.getKind() == kind::SORT_TYPE &&
          constructor.getNumChildren() == 0,
          "expected a sort constructor");
@@ -1262,7 +1264,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyInstantiateSortConstructor(constructor, type);
+    (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
   }
   return type;
 }