Do not print internally generated datatypes in external outputs with sygus (#2234)

3 files changed, 38 insertions, 12 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 425f78555..5d5c1ef68 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -640,22 +640,29 @@ SetType ExprManager::mkSetType(Type elementType) const {
   return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
 }
 
-DatatypeType ExprManager::mkDatatypeType(Datatype& datatype) {
+DatatypeType ExprManager::mkDatatypeType(Datatype& datatype, uint32_t flags)
+{
   // Not worth a special implementation; this doesn't need to be fast
   // code anyway.
   vector<Datatype> datatypes;
   datatypes.push_back(datatype);
-  std::vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+  std::vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes, flags);
   Assert(result.size() == 1);
   return result.front();
 }
 
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
+    std::vector<Datatype>& datatypes, uint32_t flags)
+{
   std::set<Type> unresolvedTypes;
-  return mkMutualDatatypeTypes(datatypes, unresolvedTypes);
+  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags);
 }
 
-std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes) {
+std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
+    std::vector<Datatype>& datatypes,
+    std::set<Type>& unresolvedTypes,
+    uint32_t flags)
+{
   NodeManagerScope nms(d_nodeManager);
   std::map<std::string, DatatypeType> nameResolutions;
   std::vector<DatatypeType> dtts;
@@ -764,7 +771,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(std::vector<Datatyp
   }
 
   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewDatatypes(dtts);
+    (*i)->nmNotifyNewDatatypes(dtts, flags);
   }
   
   return dtts;
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index bce1c8940..dce1a57a5 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -372,14 +372,27 @@ public:
   /** Make the type of set with the given parameterization. */
   SetType mkSetType(Type elementType) const;
 
+  /** Bits for use in mkDatatypeType() flags.
+   *
+   * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
+   * out as a definition, for example, in models or during dumping.
+   */
+  enum
+  {
+    DATATYPE_FLAG_NONE = 0,
+    DATATYPE_FLAG_PLACEHOLDER = 1
+  }; /* enum */
+
   /** Make a type representing the given datatype. */
-  DatatypeType mkDatatypeType(Datatype& datatype);
+  DatatypeType mkDatatypeType(Datatype& datatype,
+                              uint32_t flags = DATATYPE_FLAG_NONE);
 
   /**
    * Make a set of types representing the given datatypes, which may be
    * mutually recursive.
    */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes);
+  std::vector<DatatypeType> mkMutualDatatypeTypes(
+      std::vector<Datatype>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
 
   /**
    * Make a set of types representing the given datatypes, which may
@@ -410,7 +423,10 @@ public:
    * then no complicated Type needs to be created, and the above,
    * simpler form of mkMutualDatatypeTypes() is enough.
    */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, std::set<Type>& unresolvedTypes);
+  std::vector<DatatypeType> mkMutualDatatypeTypes(
+      std::vector<Datatype>& datatypes,
+      std::set<Type>& unresolvedTypes,
+      uint32_t flags = DATATYPE_FLAG_NONE);
 
   /**
    * Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7d1259fcc..61aaa8721 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -62,8 +62,10 @@ class NodeManagerListener {
   virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
   virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
                                                   uint32_t flags) {}
-  virtual void nmNotifyNewDatatypes(
-      const std::vector<DatatypeType>& datatypes) {}
+  virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes,
+                                    uint32_t flags)
+  {
+  }
   virtual void nmNotifyNewVar(TNode n, uint32_t flags) {}
   virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
                                  uint32_t flags) {}
@@ -86,7 +88,8 @@ class NodeManager {
   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(std::vector<Datatype>&, std::set<Type>&);
+  friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
+      std::vector<Datatype>&, std::set<Type>&, uint32_t);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {