diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 206cf35d5..04de81b1c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -472,6 +472,12 @@ public: inline TypeNode kindType(); /** + * 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(); + + /** * Make a function type from domain to range. * * @param domain the domain type @@ -680,6 +686,11 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); } +/** Get the (singleton) type for builtin operators. */ +inline TypeNode NodeManager::builtinOperatorType() { + return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); +} + /** Make a function type from domain to range. */ inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { std::vector<TypeNode> sorts; |