Fix declare-datatypes dumping bug (bug 385).

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a838d6d30959817a69a922d265398916b4afe207..d87c498e64e46747b80495a78a80ffb536150428 100644 (file)
--- 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 58c0bbae38ce7bf58f9ba69d46b943fcf647c809..3f0ec2f9cca142f85fe333bd3cb09ec013358246 100644 (file)
--- 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 7c84f3f15e6bef583b9fc7895645d0524e3024ad..a656555016f716089905f94af26c8b508f9d22ae 100644 (file)
--- 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;
 }

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index cbdee9c74ad0a79d11b7b0238724b5eaa6b147e5..03d1e7a8a5d294124640e2460f0fb6a5987ece08 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1951,15 +1951,15 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
      * below. */
   : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
     ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2);
+        t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
         params.push_back( t );
       }
       ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2);
+        t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
         params.push_back( t ); }
       )* RBRACKET
     )?
-    { datatypes.push_back(Datatype(id,params));
+    { datatypes.push_back(Datatype(id, params));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 42ca27caf475392b6e4b21a6f3f0f174bc8b59d4..5d9b6c7ae0600f81d2ab8cdd7eb19d7d9b0a8735 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -231,9 +231,9 @@ Parser::defineParameterizedType(const std::string& name,
 }
 
 SortType
-Parser::mkSort(const std::string& name) {
+Parser::mkSort(const std::string& name, uint32_t flags) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Type type = d_exprManager->mkSort(name);
+  Type type = d_exprManager->mkSort(name, flags);
   defineType(name, type);
   return type;
 }
@@ -248,7 +248,7 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) {
 }
 
 SortType Parser::mkUnresolvedType(const std::string& name) {
-  SortType unresolved = mkSort(name);
+  SortType unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
   d_unresolved.insert(unresolved);
   return unresolved;
 }

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d07756cf4e880920a8f407e2ec7af608bbdf0e97..b6ba482b76d97faf0d5b9b5fe55318a81d220213 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -411,7 +411,8 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  SortType mkSort(const std::string& name);
+  SortType mkSort(const std::string& name,
+                  uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /**
    * Creates a new sort constructor with the given name and arity.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8107158853f2fbee806effdb132fe4257a7b5a17..987220cc7ed9956ae783b6950f7540089bcac6fe 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -419,11 +419,13 @@ public:
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
-  void nmNotifyNewSort(TypeNode tn) {
+  void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
                          0,
                          tn.toType());
-    d_smt.addToModelCommandAndDump(c);
+    if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) {
+      d_smt.addToModelCommandAndDump(c, flags);
+    }
   }
 
   void nmNotifyNewSortConstructor(TypeNode tn) {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1da8d26daf083f118707b5cfef6782b1d32b39e4..3531f92e79a1b8ed1ddf4bcd8717f230d13b2129 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -336,7 +336,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, uint32_t flags = ExprManager::VAR_FLAG_NONE, bool userVisible = true, const char* dumpTag = "declarations");
+  void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
 
   /**
    * Get the model (only if immediately preceded by a SAT