diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-03 17:47:15 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-03 17:47:15 -0600 |
commit | 7029e89bc6ada688da48dc54362aef180b7c20ef (patch) | |
tree | bb41df6904c57d63c10129d05948eb57fe8e34cf /src/expr | |
parent | 81ac7cd609ef011b615dccefde702fd5b3a5c39f (diff) |
Add scope methods constructing types in API (#5393)
This addresses the nightly failures. It ensures a node manager is in scope when constructing type nodes.
It also simplifies the construction of atomic type nodes to avoid an extra TypeNode(...) constructor.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 65 | ||||
-rw-r--r-- | src/expr/node_manager.h | 88 |
2 files changed, 78 insertions, 75 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e9f121047..7c847d8ce 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -105,6 +105,71 @@ NodeManager::NodeManager(ExprManager* exprManager) init(); } +TypeNode NodeManager::booleanType() +{ + return mkTypeConst<TypeConstant>(BOOLEAN_TYPE); +} + +TypeNode NodeManager::integerType() +{ + return mkTypeConst<TypeConstant>(INTEGER_TYPE); +} + +TypeNode NodeManager::realType() +{ + return mkTypeConst<TypeConstant>(REAL_TYPE); +} + +TypeNode NodeManager::stringType() +{ + return mkTypeConst<TypeConstant>(STRING_TYPE); +} + +TypeNode NodeManager::regExpType() +{ + return mkTypeConst<TypeConstant>(REGEXP_TYPE); +} + +TypeNode NodeManager::roundingModeType() +{ + return mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE); +} + +TypeNode NodeManager::boundVarListType() +{ + return mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE); +} + +TypeNode NodeManager::instPatternType() +{ + return mkTypeConst<TypeConstant>(INST_PATTERN_TYPE); +} + +TypeNode NodeManager::instPatternListType() +{ + return mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE); +} + +TypeNode NodeManager::builtinOperatorType() +{ + return mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE); +} + +TypeNode NodeManager::mkBitVectorType(unsigned size) +{ + return mkTypeConst<BitVectorSize>(BitVectorSize(size)); +} + +TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) +{ + return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig)); +} + +TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) +{ + return mkTypeConst<FloatingPointSize>(fs); +} + void NodeManager::init() { // `mkConst()` indirectly needs the correct NodeManager in scope because we // call `NodeValue::inc()` which uses `NodeManager::curentNM()` diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cf19aab9..99db9feb2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -808,37 +808,37 @@ class NodeManager { const typename AttrKind::value_type& value); /** Get the (singleton) type for Booleans. */ - inline TypeNode booleanType(); + TypeNode booleanType(); /** Get the (singleton) type for integers. */ - inline TypeNode integerType(); + TypeNode integerType(); /** Get the (singleton) type for reals. */ - inline TypeNode realType(); + TypeNode realType(); /** Get the (singleton) type for strings. */ - inline TypeNode stringType(); + TypeNode stringType(); /** Get the (singleton) type for RegExp. */ - inline TypeNode regExpType(); + TypeNode regExpType(); /** Get the (singleton) type for rounding modes. */ - inline TypeNode roundingModeType(); + TypeNode roundingModeType(); /** Get the bound var list type. */ - inline TypeNode boundVarListType(); + TypeNode boundVarListType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternType(); + TypeNode instPatternType(); /** Get the instantiation pattern type. */ - inline TypeNode instPatternListType(); + TypeNode instPatternListType(); /** * Get the (singleton) type for builtin operators (that is, the type * of the Node returned from Node::getOperator() when the operator * is built-in, like EQUAL). */ - inline TypeNode builtinOperatorType(); + TypeNode builtinOperatorType(); /** * Make a function type from domain to range. @@ -906,11 +906,11 @@ class NodeManager { /** Make the type of floating-point with <code>exp</code> bit exponent and <code>sig</code> bit significand */ - inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); - inline TypeNode mkFloatingPointType(FloatingPointSize fs); + TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + TypeNode mkFloatingPointType(FloatingPointSize fs); /** Make the type of bitvectors of size <code>size</code> */ - inline TypeNode mkBitVectorType(unsigned size); + TypeNode mkBitVectorType(unsigned size); /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); @@ -1129,56 +1129,6 @@ public: } };/* class NodeManagerScope */ -/** Get the (singleton) type for booleans. */ -inline TypeNode NodeManager::booleanType() { - return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE)); -} - -/** Get the (singleton) type for integers. */ -inline TypeNode NodeManager::integerType() { - return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE)); -} - -/** Get the (singleton) type for reals. */ -inline TypeNode NodeManager::realType() { - return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE)); -} - -/** Get the (singleton) type for strings. */ -inline TypeNode NodeManager::stringType() { - return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE)); -} - -/** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regExpType() { - return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE)); -} - -/** Get the (singleton) type for rounding modes. */ -inline TypeNode NodeManager::roundingModeType() { - return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE)); -} - -/** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType() { - return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType() { - return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType() { - return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE)); -} - -/** Get the (singleton) type for builtin operators. */ -inline TypeNode NodeManager::builtinOperatorType() { - return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); -} - inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { @@ -1187,18 +1137,6 @@ inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { return mkTypeNode(kind::SEXPR_TYPE, typeNodes); } -inline TypeNode NodeManager::mkBitVectorType(unsigned size) { - return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); -} - -inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { - return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig))); -} - -inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { - return TypeNode(mkTypeConst<FloatingPointSize>(fs)); -} - inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, |