mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

fix is_string_term()

Browse source
This commit is contained in:
Murphy Berzish 2017-04-27 13:58:36 -04:00
parent d16b20d62b
commit 334677a7eb
1 changed files with 2 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/seq_decl_plugin.h
View file

@ -275,18 +275,12 @@ public:
bool is_string_term(expr const * n) const { bool is_string_term(expr const * n) const {
sort * s = get_sort(n); sort * s = get_sort(n);
return is_sort_of(s, m_fid, _STRING_SORT); return (u.is_seq(s) && u.is_string(s));
} }
bool is_non_string_sequence(expr const * n) const { bool is_non_string_sequence(expr const * n) const {
if (is_string_term(n))
return false;
sort * s = get_sort(n); sort * s = get_sort(n);
if (u.is_seq(s) && !u.is_string(s)) { return (u.is_seq(s) && !u.is_string(s));
return true;
}
return false;
} }
MATCH_BINARY(is_concat); MATCH_BINARY(is_concat);