diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
commit | 96ce991a4b8593f7ec831c3a9b40b214d2ac3761 (patch) | |
tree | bf804dcc18a20394a6fba8ac4bed6932ca4c7c02 /src/expr/node_manager.h | |
parent | b44f183a75deea11fa379554b893b6656e1864b2 (diff) |
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
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; |