From d3564f5b509910fae23df1aaa6b06c648871593e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2021 06:42:19 -0800 Subject: [PATCH] move unicode toggle to char-plugin Signed-off-by: Nikolaj Bjorner --- src/ast/char_decl_plugin.cpp | 7 ++++--- src/ast/char_decl_plugin.h | 7 +++++-- src/ast/seq_decl_plugin.cpp | 3 +-- src/ast/seq_decl_plugin.h | 10 +++++----- 4 files changed, 15 insertions(+), 12 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index efc40cf31..5b06bf619 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -17,12 +17,13 @@ Author: --*/ #pragma once -#include "util/zstring.h" +#include "util/gparams.h" #include "ast/char_decl_plugin.h" #include "ast/ast_pp.h" char_decl_plugin::char_decl_plugin(): m_charc_sym("Char") { + m_unicode = gparams::get_value("unicode") == "true"; } char_decl_plugin::~char_decl_plugin() { @@ -54,7 +55,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, msg << "integer parameter expected"; else if (parameters[0].get_int() < 0) msg << "non-negative parameter expected"; - else if (parameters[0].get_int() > static_cast(zstring::unicode_max_char())) + else if (parameters[0].get_int() > static_cast(max_char())) msg << "parameter expected within character range"; else return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters)); @@ -99,7 +100,7 @@ bool char_decl_plugin::are_distinct(app* a, app* b) const { } app* char_decl_plugin::mk_char(unsigned u) { - SASSERT(u <= zstring::unicode_max_char()); + SASSERT(u <= max_char()); 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); diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index 92e666721..48cd59aff 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -22,6 +22,7 @@ Revision History: --*/ #pragma once +#include "util/zstring.h" #include "ast/ast.h" #include @@ -37,6 +38,7 @@ enum char_op_kind { class char_decl_plugin : public decl_plugin { sort* m_char { nullptr }; symbol m_charc_sym; + bool m_unicode { true }; void set_manager(ast_manager * m, family_id id) override; @@ -80,7 +82,8 @@ public: return is_app_of(e, m_family_id, OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); } - - + bool unicode() const { return m_unicode; } + unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); } + unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); } }; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 63df850e0..6ad306d2d 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#include "util/gparams.h" #include "ast/seq_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" @@ -33,7 +32,6 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false), m_reglan(nullptr), m_has_re(false), m_has_seq(false) { - m_unicode = gparams::get_value("unicode") == "true"; } void seq_decl_plugin::finalize() { @@ -280,6 +278,7 @@ void seq_decl_plugin::init() { void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); bv_util bv(*m); + m_char_plugin = static_cast(m_manager->get_plugin(m_manager->mk_family_id("char"))); if (unicode()) m_char = get_char_plugin().char_sort(); else diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index cc31b54eb..ef5049476 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -134,7 +134,7 @@ class seq_decl_plugin : public decl_plugin { sort* m_reglan; bool m_has_re; bool m_has_seq; - bool m_unicode { false }; + char_decl_plugin* m_char_plugin { nullptr }; void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); @@ -163,7 +163,7 @@ public: ~seq_decl_plugin() override {} void finalize() override; - bool unicode() const { return m_unicode; } + bool unicode() const { return get_char_plugin().unicode(); } decl_plugin * mk_fresh() override { return alloc(seq_decl_plugin); } @@ -188,8 +188,8 @@ public: bool is_char(ast* a) const { return a == m_char; } - unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); } - unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); } + unsigned max_char() const { return get_char_plugin().max_char(); } + unsigned num_bits() const { return get_char_plugin().num_bits(); } app* mk_string(symbol const& s); app* mk_string(zstring const& s); @@ -203,7 +203,7 @@ public: sort* char_sort() const { return m_char; } sort* string_sort() const { return m_string; } - char_decl_plugin& get_char_plugin() { return *static_cast(m_manager->get_plugin(m_manager->mk_family_id("char"))); } + char_decl_plugin& get_char_plugin() const { return *m_char_plugin; } };