Do not print internally generated datatypes in external outputs with…

… sygus (cvc5#2234)
timothy-king · Aug 24, 2018 · 33fe4c2 · 33fe4c2
1 parent 907cc0a
commit 33fe4c2
Show file tree

Hide file tree

Showing 6 changed files with 52 additions and 18 deletions.
diff --git 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
@@ -372,14 +372,27 @@ class CVC4_PUBLIC ExprManager {
   /** 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 @@ class CVC4_PUBLIC ExprManager {
    * 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
@@ -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 {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
@@ -734,10 +734,14 @@ class SmtEnginePrivate : public NodeManagerListener {
     }
   }
 
-  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override
+  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
+                            uint32_t flags) override
   {
-    DatatypeDeclarationCommand c(dtts);
-    d_smt.addToModelCommandAndDump(c);
+    if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+    {
+      DatatypeDeclarationCommand c(dtts);
+      d_smt.addToModelCommandAndDump(c);
+    }
   }
 
   void nmNotifyNewVar(TNode n, uint32_t flags) override

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -843,7 +843,9 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
                         unres);
   Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
   Assert( !datatypes.empty() );
-  std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
+  std::vector<DatatypeType> types =
+      NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
+          datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
   Assert( types.size()==datatypes.size() );
   return TypeNode::fromType( types[0] );
 }
@@ -882,7 +884,9 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
     // we have a single sygus constructor that encodes the template
     datatypes.back().addSygusConstructor( op.toExpr(), cname, argTypes );
     datatypes.back().setSygus( templ.getType().toType(), bvl.toExpr(), true, true );
-    std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
+    std::vector<DatatypeType> types =
+        NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
+            datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     Assert( types.size()==1 );
     return TypeNode::fromType( types[0] );
   }

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -551,7 +551,7 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
   Assert(d_dt_all.size() == d_unres_t_all.size());
   std::vector<DatatypeType> types =
       NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
-          d_dt_all, d_unres_t_all);
+          d_dt_all, d_unres_t_all, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
   Assert(types.size() == d_dt_all.size());
   /* Clear accumulators */
   d_dt_all.clear();