diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 318b45d4f..5453fd369 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -20,7 +20,12 @@ Author: #include "util/zstring.h" #include "ast/char_decl_plugin.h" -char_decl_plugin::char_decl_plugin() : m_charc_sym("Char") { +char_decl_plugin::char_decl_plugin(): + m_charc_sym("Char") { +} + +char_decl_plugin::~char_decl_plugin() { + m_manager->dec_ref(m_char); } func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, @@ -52,7 +57,8 @@ void char_decl_plugin::set_manager(ast_manager * m, family_id id) { } void char_decl_plugin::get_op_names(svector& op_names, symbol const& logic) { - op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); + // TODO: enable when character theory is turned on: + // op_names.push_back(builtin_name("char.<=", OP_CHAR_LE)); } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index ff26bc1e8..7f891b7d4 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -44,7 +44,7 @@ class char_decl_plugin : public decl_plugin { public: char_decl_plugin(); - ~char_decl_plugin() override {} + ~char_decl_plugin() override; void finalize() override {} diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 395104a0d..7781bf829 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -24,6 +24,7 @@ Revision History: #include "ast/datatype_decl_plugin.h" #include "ast/recfun_decl_plugin.h" #include "ast/dl_decl_plugin.h" +#include "ast/char_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" @@ -51,6 +52,9 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("seq")))) { m.register_plugin(symbol("seq"), alloc(seq_decl_plugin)); } + if (!m.get_plugin(m.mk_family_id(symbol("char")))) { + m.register_plugin(symbol("char"), alloc(char_decl_plugin)); + } if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) { m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin)); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 634208e12..65470bd23 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -27,6 +27,7 @@ Notes: #include "ast/bv_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "ast/char_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" @@ -701,6 +702,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("recfun"), alloc(recfun::decl::plugin), logic_has_recfun()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); + register_plugin(symbol("char"), alloc(char_decl_plugin), logic_has_seq()); register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb()); register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); @@ -717,6 +719,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("array"), logic_has_array(), fids); load_plugin(symbol("datatype"), logic_has_datatype(), fids); load_plugin(symbol("recfun"), logic_has_recfun(), fids); + load_plugin(symbol("char"), logic_has_seq(), fids); load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index c4fe9b05b..8e757ed59 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -33,6 +33,7 @@ Revision History: #include "smt/theory_dl.h" #include "smt/theory_seq_empty.h" #include "smt/theory_seq.h" +#include "smt/theory_char.h" #include "smt/theory_special_relations.h" #include "smt/theory_pb.h" #include "smt/theory_fpa.h" @@ -227,7 +228,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - m_context.register_plugin(alloc(theory_seq, m_context)); + setup_seq(); } void setup::setup_QF_UF(static_features const & st) { @@ -725,7 +726,7 @@ namespace smt { } else if (m_params.m_string_solver == "empty") { - m_context.register_plugin(alloc(smt::theory_seq_empty, m_context)); + setup_seq(); } else if (m_params.m_string_solver == "none") { // don't register any solver. @@ -895,7 +896,7 @@ namespace smt { setup_seq(); } else if (m_params.m_string_solver == "empty") { - m_context.register_plugin(alloc(smt::theory_seq_empty, m_context)); + setup_seq(); } else if (m_params.m_string_solver == "none") { // don't register any solver. @@ -929,6 +930,18 @@ namespace smt { void setup::setup_seq() { m_context.register_plugin(alloc(smt::theory_seq, m_context)); + setup_char(); + } + + void setup::setup_char() { + // temporary: enable only char theory if it is used in seq + seq_util seq(m_manager); + sort* ch = seq.mk_char_sort(); + sort* s = seq.mk_string_sort(); + family_id ch_fid = ch->get_family_id(); + if (s->get_family_id() != ch_fid) + m_context.register_plugin(alloc(smt::theory_char, m_context, ch_fid)); + } void setup::setup_special_relations() { diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index fad499bec..2daa67085 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -100,6 +100,7 @@ namespace smt { void setup_dl(); void setup_seq_str(static_features const & st); void setup_seq(); + void setup_char(); void setup_card(); void setup_i_arith(); void setup_mi_arith();