diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-11-04 16:52:06 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-11-04 16:52:06 +0000 |
commit | 37812f8ad9743b372608e871efe3e336c4ebd631 (patch) | |
tree | 704591a3151169ed998956cbe4b85be8725941c2 /src/expr/node_manager.h | |
parent | b5fd5b61a9f0f993703497fb1c8d678cf2d8bb01 (diff) |
STRING_TYPE and CONST_STRING and associate type infrastructure implemented.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 84ed78662..adba8087c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -515,6 +515,9 @@ public: /** Get the (singleton) type for pseudobooleans. */ inline TypeNode pseudobooleanType(); + /** Get the (singleton) type for strings. */ + inline TypeNode stringType(); + /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); @@ -780,6 +783,11 @@ inline TypeNode NodeManager::pseudobooleanType() { return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE)); } +/** Get the (singleton) type for strings. */ +inline TypeNode NodeManager::stringType() { + return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE)); +} + /** Get the (singleton) type for sorts. */ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); |