From 7811a91bad1d1f4586f82d221049de956567368a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 13:59:02 -0400 Subject: [PATCH] fix is_string_term() --- src/ast/seq_decl_plugin.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 2882e905d..833455ff4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -273,6 +273,15 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } + bool is_string_term(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && u.is_string(s)); + } + + bool is_non_string_sequence(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && !u.is_string(s)); + } MATCH_BINARY(is_concat); MATCH_UNARY(is_length);