From 3d83a435f3d9108c6457d4058ba5262d0d72634e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 Apr 2021 13:22:29 -0500 Subject: Use exceptions when constructing malformed datatypes (#6303) Fixes #5150. --- src/expr/node_manager.cpp | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4b95e08df..dd372a81d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -599,9 +599,11 @@ std::vector NodeManager::mkMutualDatatypeTypes( typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params); } - AlwaysAssert(nameResolutions.find(dtp->getName()) == nameResolutions.end()) - << "cannot construct two datatypes at the same time " - "with the same name"; + if (nameResolutions.find(dtp->getName()) != nameResolutions.end()) + { + throw Exception( + "cannot construct two datatypes at the same time with the same name"); + } nameResolutions.insert(std::make_pair(dtp->getName(), typeNode)); dtts.push_back(typeNode); } @@ -624,9 +626,11 @@ std::vector NodeManager::mkMutualDatatypeTypes( std::string name = ut.getAttribute(expr::VarNameAttr()); std::map::const_iterator resolver = nameResolutions.find(name); - AlwaysAssert(resolver != nameResolutions.end()) - << "cannot resolve type " + name - + "; it's not among the datatypes being defined"; + if (resolver == nameResolutions.end()) + { + throw Exception("cannot resolve type " + name + + "; it's not among the datatypes being defined"); + } // We will instruct the Datatype to substitute "ut" (the // unresolved SortType used as a placeholder in complex types) // with "(*resolver).second" (the TypeNode we created in the @@ -679,8 +683,10 @@ std::vector NodeManager::mkMutualDatatypeTypes( // This next one's a "hard" check, performed in non-debug builds // as well; the other ones should all be guaranteed by the // cvc5::DType class, but this actually needs to be checked. - AlwaysAssert(!selectorType.getRangeType().isFunctionLike()) - << "cannot put function-like things in datatypes"; + if (selectorType.getRangeType().isFunctionLike()) + { + throw Exception("cannot put function-like things in datatypes"); + } } } } -- cgit v1.2.3