From 33fe4c274ca71237601e776c7be942bd2bfd02af Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 23 Aug 2018 20:34:40 -0500 Subject: [PATCH] Do not print internally generated datatypes in external outputs with sygus (#2234) --- src/expr/expr_manager_template.cpp | 19 +++++++++++----- src/expr/expr_manager_template.h | 22 ++++++++++++++++--- src/expr/node_manager.h | 9 +++++--- src/smt/smt_engine.cpp | 10 ++++++--- .../quantifiers/sygus/sygus_grammar_cons.cpp | 8 +++++-- .../quantifiers/sygus/sygus_grammar_norm.cpp | 2 +- 6 files changed, 52 insertions(+), 18 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 datatypes; datatypes.push_back(datatype); - std::vector result = mkMutualDatatypeTypes(datatypes); + std::vector result = mkMutualDatatypeTypes(datatypes, flags); Assert(result.size() == 1); return result.front(); } -std::vector ExprManager::mkMutualDatatypeTypes(std::vector& datatypes) { +std::vector ExprManager::mkMutualDatatypeTypes( + std::vector& datatypes, uint32_t flags) +{ std::set unresolvedTypes; - return mkMutualDatatypeTypes(datatypes, unresolvedTypes); + return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags); } -std::vector ExprManager::mkMutualDatatypeTypes(std::vector& datatypes, std::set& unresolvedTypes) { +std::vector ExprManager::mkMutualDatatypeTypes( + std::vector& datatypes, + std::set& unresolvedTypes, + uint32_t flags) +{ NodeManagerScope nms(d_nodeManager); std::map nameResolutions; std::vector dtts; @@ -764,7 +771,7 @@ std::vector ExprManager::mkMutualDatatypeTypes(std::vector::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 mkMutualDatatypeTypes(std::vector& datatypes); + std::vector mkMutualDatatypeTypes( + std::vector& 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 mkMutualDatatypeTypes(std::vector& datatypes, std::set& unresolvedTypes); + std::vector mkMutualDatatypeTypes( + std::vector& datatypes, + std::set& 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& datatypes) {} + virtual void nmNotifyNewDatatypes(const std::vector& 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 ExprManager::mkMutualDatatypeTypes(std::vector&, std::set&); + friend std::vector ExprManager::mkMutualDatatypeTypes( + std::vector&, std::set&, uint32_t); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d7c1ece96..c4492d3a1 100644 --- 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& dtts) override + void nmNotifyNewDatatypes(const std::vector& 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 index fbbfdec09..e05df8581 100644 --- 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 types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); + std::vector 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 types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); + std::vector 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 index 5a87c8ebd..868e69b21 100644 --- 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 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(); -- 2.30.2