From e969bd1c9737759c1228aed3d40198ae32b9ad99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2021 06:26:44 -0800 Subject: [PATCH] fully remove seq-based characters Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 -- src/ast/seq_decl_plugin.cpp | 54 ------------------------------- src/ast/seq_decl_plugin.h | 3 -- 3 files changed, 60 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 08ac1f175..ebfb7e14c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -719,9 +719,6 @@ 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: - break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index dc472942b..63df850e0 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -24,8 +24,6 @@ Revision History: #include "ast/bv_decl_plugin.h" #include -#define _USE_CHAR_PLUGIN 1 - seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), @@ -256,12 +254,6 @@ 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_LE] = nullptr; - if (unicode() && !_USE_CHAR_PLUGIN) { - sort* charTcharT[2] = { m_char, m_char }; - m_sigs[_OP_CHAR_LE] = alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT); - } 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); @@ -289,11 +281,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); bv_util bv(*m); if (unicode()) -#if _USE_CHAR_PLUGIN m_char = get_char_plugin().char_sort(); -#else - m_char = m->mk_sort(symbol("Unicode"), sort_info(m_family_id, _CHAR_SORT, 0, nullptr)); -#endif else m_char = bv.mk_sort(8); m->inc_ref(m_char); @@ -329,8 +317,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter } return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); } - case _CHAR_SORT: - return m_char; case _STRING_SORT: return m_string; case _REGLAN_SORT: @@ -576,20 +562,6 @@ 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: - 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: - 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)); - case OP_SEQ_IN_RE: m_has_re = true; return mk_seq_fun(k, arity, domain, range, _OP_STRING_IN_REGEXP); @@ -677,13 +649,7 @@ app* seq_decl_plugin::mk_string(zstring const& s) { app* seq_decl_plugin::mk_char(unsigned u) { if (unicode()) { -#if _USE_CHAR_PLUGIN return get_char_plugin().mk_char(u); -#else - 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)); - return m_manager->mk_const(f); -#endif } else { bv_util bv(*m_manager); @@ -698,8 +664,6 @@ 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)) - return true; return false; } @@ -709,8 +673,6 @@ 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)) - return true; if (is_app_of(e, m_family_id, OP_SEQ_UNIT) && m_manager->is_value(e->get_arg(0))) return true; @@ -744,9 +706,6 @@ 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)) - return true; if (is_app_of(a, m_family_id, OP_SEQ_UNIT) && is_app_of(b, m_family_id, OP_SEQ_UNIT)) return m_manager->are_distinct(a->get_arg(0), b->get_arg(0)); @@ -823,11 +782,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()) { -#if _USE_CHAR_PLUGIN return ch.is_const_char(e, c); -#else - return is_app_of(e, m_fid, _OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); -#endif } else { rational r; @@ -838,11 +793,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()) -#if _USE_CHAR_PLUGIN return ch.is_le(e); -#else - return is_app_of(e, m_fid, _OP_CHAR_LE); -#endif else return bv().is_bv_ule(e) && is_char(to_app(e)->get_arg(0)); } @@ -858,12 +809,7 @@ app* seq_util::mk_le(expr* ch1, expr* ch2) const { expr_ref _ch1(ch1, m), _ch2(ch2, m); if (seq.unicode()) { -#if _USE_CHAR_PLUGIN return ch.mk_le(ch1, ch2); -#else - expr* es[2] = { ch1, ch2 }; - return m.mk_app(m_fid, _OP_CHAR_LE, 2, es); -#endif } else { rational r1, r2; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index f2b2b2973..cc31b54eb 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -31,7 +31,6 @@ Revision History: enum seq_sort_kind { SEQ_SORT, RE_SORT, - _CHAR_SORT, // internal only _STRING_SORT, _REGLAN_SORT }; @@ -87,8 +86,6 @@ enum seq_op_kind { OP_STRING_TO_CODE, OP_STRING_FROM_CODE, - _OP_CHAR_CONST, // constant character - _OP_CHAR_LE, // Unicode comparison // internal only operators. Converted to SEQ variants. _OP_STRING_FROM_CHAR, _OP_STRING_STRREPL,