diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b7871c0e8..08ac1f175 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -719,8 +719,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 1); st = mk_str_stoi(args[0], result); break; - case OP_CHAR_LE: - case OP_CHAR_CONST: + case _OP_CHAR_LE: + case _OP_CHAR_CONST: break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 45c318f7d..1273dba85 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -617,9 +617,9 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_REPLACE_RE] = alloc(psig, m, "str.replace_re", 1, 3, seqAreAseqA, seqA); m_sigs[OP_SEQ_REPLACE_ALL] = alloc(psig, m, "str.replace_all", 1, 3, seqAseqAseqA, seqA); m_sigs[OP_STRING_CONST] = nullptr; - m_sigs[OP_CHAR_CONST] = nullptr; + m_sigs[_OP_CHAR_CONST] = nullptr; sort* charTcharT[2] = { m_char, m_char }; - m_sigs[OP_CHAR_LE] = unicode() ? alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT) : nullptr; + m_sigs[_OP_CHAR_LE] = unicode() ? alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT) : nullptr; m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[_OP_STRING_FROM_CHAR] = alloc(psig, m, "char", 1, 0, nullptr, strT); @@ -930,19 +930,19 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, m_has_re = true; return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE); - case OP_CHAR_LE: + case _OP_CHAR_LE: if (arity == 2 && domain[0] == m_char && domain[1] == m_char) { return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception("Incorrect parameters passed to character comparison"); - case OP_CHAR_CONST: + case _OP_CHAR_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_int() && 0 <= parameters[0].get_int() && parameters[0].get_int() < static_cast(max_char()))) { m.raise_exception("invalid character declaration"); } - return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters)); + return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, _OP_CHAR_CONST, num_parameters, parameters)); case OP_SEQ_IN_RE: m_has_re = true; @@ -1035,7 +1035,7 @@ app* seq_decl_plugin::mk_string(zstring const& s) { app* seq_decl_plugin::mk_char(unsigned u) { if (unicode()) { parameter param(u); - func_decl* f = m_manager->mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, 1, ¶m)); + func_decl* f = m_manager->mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, _OP_CHAR_CONST, 1, ¶m)); return m_manager->mk_const(f); } else { @@ -1051,7 +1051,7 @@ bool seq_decl_plugin::is_considered_uninterpreted(func_decl * f) { } bool seq_decl_plugin::is_unique_value(app* e) const { - if (is_app_of(e, m_family_id, OP_CHAR_CONST)) + if (is_app_of(e, m_family_id, _OP_CHAR_CONST)) return true; return false; } @@ -1062,7 +1062,7 @@ bool seq_decl_plugin::is_value(app* e) const { return true; if (is_app_of(e, m_family_id, OP_STRING_CONST)) return true; - if (is_app_of(e, m_family_id, OP_CHAR_CONST)) + if (is_app_of(e, m_family_id, _OP_CHAR_CONST)) return true; if (is_app_of(e, m_family_id, OP_SEQ_UNIT) && m_manager->is_value(e->get_arg(0))) @@ -1097,8 +1097,8 @@ bool seq_decl_plugin::are_distinct(app* a, app* b) const { if (is_app_of(a, m_family_id, OP_STRING_CONST) && is_app_of(b, m_family_id, OP_STRING_CONST)) return true; - if (is_app_of(a, m_family_id, OP_CHAR_CONST) && - is_app_of(b, m_family_id, OP_CHAR_CONST)) + if (is_app_of(a, m_family_id, _OP_CHAR_CONST) && + is_app_of(b, m_family_id, _OP_CHAR_CONST)) return true; if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) @@ -1176,7 +1176,7 @@ unsigned seq_util::max_mul(unsigned x, unsigned y) const { bool seq_util::is_const_char(expr* e, unsigned& c) const { if (seq.unicode()) { - return is_app_of(e, m_fid, OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); + return is_app_of(e, m_fid, _OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); } else { rational r; @@ -1187,7 +1187,7 @@ bool seq_util::is_const_char(expr* e, unsigned& c) const { bool seq_util::is_char_le(expr const* e) const { if (seq.unicode()) - return is_app_of(e, m_fid, OP_CHAR_LE); + return is_app_of(e, m_fid, _OP_CHAR_LE); else return bv().is_bv_ule(e) && is_char(to_app(e)->get_arg(0)); } @@ -1204,7 +1204,7 @@ app* seq_util::mk_le(expr* ch1, expr* ch2) const { if (seq.unicode()) { expr* es[2] = { ch1, ch2 }; - return m.mk_app(m_fid, OP_CHAR_LE, 2, es); + return m.mk_app(m_fid, _OP_CHAR_LE, 2, es); } else { rational r1, r2; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 5729b4ab9..4fdc8a065 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -27,7 +27,6 @@ Revision History: #include #include "util/lbool.h" - enum seq_sort_kind { SEQ_SORT, RE_SORT, @@ -87,8 +86,8 @@ enum seq_op_kind { OP_STRING_TO_CODE, OP_STRING_FROM_CODE, - OP_CHAR_CONST, // constant character - OP_CHAR_LE, // Unicode comparison + _OP_CHAR_CONST, // constant character + _OP_CHAR_LE, // Unicode comparison // internal only operators. Converted to SEQ variants. _OP_STRING_FROM_CHAR, _OP_STRING_STRREPL,