diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-23 20:34:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-23 20:34:40 -0500 |
commit | 33fe4c274ca71237601e776c7be942bd2bfd02af (patch) | |
tree | 20d7ee1992d1c0f31e6b5a88d7d7bdc26c32884f /src/expr/expr_manager_template.cpp | |
parent | 907cc0aceb81b9282f63367652f1f68bae4fb40e (diff) |
Do not print internally generated datatypes in external outputs with sygus (#2234)
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 19 |
1 files changed, 13 insertions, 6 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; |