move unicode toggle to char-plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<int>(zstring::unicode_max_char()))
+        else if (parameters[0].get_int() > static_cast<int>(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, &param));
     return m_manager->mk_const(f);

src/ast/char_decl_plugin.h

@@ -22,6 +22,7 @@ Revision History:
 --*/
 #pragma once
 
+#include "util/zstring.h"
 #include "ast/ast.h"
 #include <string>
 
@@ -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(); }
 
 };

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<char_decl_plugin*>(m_manager->get_plugin(m_manager->mk_family_id("char")));
     if (unicode())
         m_char = get_char_plugin().char_sort();
     else

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<char_decl_plugin*>(m_manager->get_plugin(m_manager->mk_family_id("char"))); }
+    char_decl_plugin& get_char_plugin() const { return *m_char_plugin; }
 
 };