mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix is_string_term()

Browse source
This commit is contained in:
Murphy Berzish 2017-04-27 13:59:02 -04:00
parent 46ac718790
commit 7811a91bad
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/seq_decl_plugin.h
View file

@ -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);