diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 19 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 22 | ||||
-rw-r--r-- | src/expr/node_manager.h | 9 |
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 { |