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 | |
parent | b44f183a75deea11fa379554b893b6656e1864b2 (diff) |
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 3 | ||||
-rw-r--r-- | src/expr/node_manager.h | 11 | ||||
-rw-r--r-- | src/expr/type_constant.h | 4 |
3 files changed, 17 insertions, 1 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 280c55254..9006bf4d9 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -228,6 +228,9 @@ TypeNode NodeManager::computeType(TNode n, bool check) // Infer the type switch(n.getKind()) { + case kind::BUILTIN: + typeNode = builtinOperatorType(); + break; case kind::SORT_TYPE: typeNode = kindType(); break; 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; diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index 3001d4513..23c23cc9f 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -36,7 +36,9 @@ enum TypeConstant { /** The real type */ REAL_TYPE, /** The kind type (type of types) */ - KIND_TYPE + KIND_TYPE, + /** The builtin operator type (type of non-PARAMETERIZED operators) */ + BUILTIN_OPERATOR_TYPE };/* enum TypeConstant */ /** |