diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-11 11:23:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-11 18:15:18 -0400 |
commit | c3a959b3112af83492694b8f0919381b1c467fb8 (patch) | |
tree | 62ae7f49087bfb61a439161b5bc1cb5c8c691f21 /src/expr/node_manager.h | |
parent | f49c16dd1169d3de4bbfcdca22af1269bbd0a005 (diff) |
Theory of strings.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
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 a65655501..31f6d75d9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -683,6 +683,9 @@ public: /** Get the (singleton) type for strings. */ inline TypeNode stringType(); + /** Get the (singleton) type for RegExp. */ + inline TypeNode regexpType(); + /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -1030,6 +1033,11 @@ 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 bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); |