From 8d8fe872ad59d23e95e403bdeed18b2ded7f4002 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2021 06:22:25 -0800 Subject: [PATCH] remove plugin status to theory_seq Signed-off-by: Nikolaj Bjorner --- src/ast/char_decl_plugin.cpp | 3 ++- src/smt/smt_setup.cpp | 2 +- src/smt/theory_char.cpp | 40 +++++++++++++++--------------------- src/smt/theory_char.h | 21 ++++++++----------- src/smt/theory_seq.cpp | 34 +----------------------------- src/smt/theory_seq.h | 2 -- 6 files changed, 29 insertions(+), 73 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index ca25d04d5..ee7652eda 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -76,7 +76,7 @@ void char_decl_plugin::get_op_names(svector& op_names, symbol cons } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { - sort_names.push_back(builtin_name("Unicode", CHAR_SORT)); + sort_names.push_back(builtin_name("Unicode", CHAR_SORT)); } bool char_decl_plugin::is_value(app* e) const { @@ -99,6 +99,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()); 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/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index b503a35c4..bccc840fc 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -940,7 +940,7 @@ namespace smt { 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, nullptr)); + m_context.register_plugin(alloc(smt::theory_char, m_context, ch_fid)); } diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index 82432fe00..715cb90c6 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -22,18 +22,12 @@ Author: namespace smt { - theory_char::theory_char(context& ctx, family_id fid, theory* th): + theory_char::theory_char(context& ctx, family_id fid): theory(ctx, fid), seq(m), - m_bb(m, ctx.get_fparams()), - m_th(th) + m_bb(m, ctx.get_fparams()) { - bv_util bv(m); - sort_ref b8(bv.mk_sort(8), m); - m_enabled = !seq.is_char(b8); m_bits2char = symbol("bits2char"); - if (!m_th) - m_th = this; } struct theory_char::reset_bits : public trail { @@ -102,7 +96,7 @@ namespace smt { if (has_bits(v)) return; - expr* e = m_th->get_expr(v); + expr* e = get_expr(v); m_bits.reserve(v + 1); auto& bits = m_bits[v]; while ((unsigned) v >= m_ebits.size()) @@ -142,8 +136,8 @@ namespace smt { void theory_char::internalize_le(literal lit, app* term) { expr* x = nullptr, *y = nullptr; VERIFY(seq.is_char_le(term, x, y)); - theory_var v1 = ctx.get_enode(x)->get_th_var(m_th->get_id()); - theory_var v2 = ctx.get_enode(y)->get_th_var(m_th->get_id()); + theory_var v1 = ctx.get_enode(x)->get_th_var(get_id()); + theory_var v2 = ctx.get_enode(y)->get_th_var(get_id()); init_bits(v1); init_bits(v2); auto const& b1 = get_ebits(v1); @@ -229,22 +223,22 @@ namespace smt { * 2. Assign values to characters that haven't been assigned. */ bool theory_char::final_check() { - TRACE("seq", tout << "final check " << m_th->get_num_vars() << "\n";); + TRACE("seq", tout << "final check " << get_num_vars() << "\n";); m_var2value.reset(); - m_var2value.resize(m_th->get_num_vars(), UINT_MAX); + m_var2value.resize(get_num_vars(), UINT_MAX); m_value2var.reset(); // extract the initial set of constants. uint_set values; unsigned c = 0, d = 0; - for (unsigned v = m_th->get_num_vars(); v-- > 0; ) { - expr* e = m_th->get_expr(v); + for (unsigned v = get_num_vars(); v-- > 0; ) { + expr* e = get_expr(v); if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) { - CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << m_th->get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";); - enode* r = m_th->get_enode(v)->get_root(); + CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";); + enode* r = get_enode(v)->get_root(); m_value2var.reserve(c + 1, null_theory_var); theory_var u = m_value2var[c]; - if (u != null_theory_var && r != m_th->get_enode(u)->get_root()) { + if (u != null_theory_var && r != get_enode(u)->get_root()) { enforce_ackerman(u, v); return false; } @@ -269,8 +263,8 @@ namespace smt { // assign values to other unassigned nodes c = 'A'; - for (unsigned v = m_th->get_num_vars(); v-- > 0; ) { - expr* e = m_th->get_expr(v); + for (unsigned v = get_num_vars(); v-- > 0; ) { + expr* e = get_expr(v); if (seq.is_char(e) && m_var2value[v] == UINT_MAX) { d = c; while (values.contains(c)) { @@ -281,7 +275,7 @@ namespace smt { } } TRACE("seq", tout << "fresh: " << mk_pp(e, m) << " := " << c << "\n";); - for (enode* n : *m_th->get_enode(v)) + for (enode* n : *get_enode(v)) m_var2value[n->get_th_var(get_id())] = c; m_value2var.reserve(c + 1, null_theory_var); m_value2var[c] = v; @@ -293,9 +287,9 @@ namespace smt { void theory_char::enforce_bits() { TRACE("seq", tout << "enforce bits\n";); - for (unsigned v = m_th->get_num_vars(); v-- > 0; ) { + for (unsigned v = get_num_vars(); v-- > 0; ) { expr* e = get_expr(v); - if (seq.is_char(e) && m_th->get_enode(v)->is_root() && !has_bits(v)) + if (seq.is_char(e) && get_enode(v)->is_root() && !has_bits(v)) init_bits(v); } } diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index d236f7320..90a403829 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -16,8 +16,7 @@ Author: --*/ #pragma once -#include "ast/seq_decl_plugin.h" -#include "ast/bv_decl_plugin.h" +#include "ast/char_decl_plugin.h" #include "ast/rewriter/bit_blaster/bit_blaster.h" #include "model/char_factory.h" #include "smt/smt_theory.h" @@ -44,7 +43,6 @@ namespace smt { stats m_stats; symbol m_bits2char; char_factory* m_factory { nullptr }; - theory* m_th; struct reset_bits; @@ -57,15 +55,20 @@ namespace smt { void enforce_value_bound(theory_var v); void enforce_bits(); + bool final_check(); + void new_const_char(theory_var v, unsigned c); + unsigned get_char_value(theory_var v); + void internalize_le(literal lit, app* term); + theory_var mk_var(enode* n) override; public: - theory_char(context& ctx, family_id fid, theory * th); + theory_char(context& ctx, family_id fid); void new_eq_eh(theory_var v1, theory_var v2) override; void new_diseq_eh(theory_var v1, theory_var v2) override; - theory * mk_fresh(context * new_ctx) override { return alloc(theory_char, *new_ctx, get_family_id(), nullptr); } + theory * mk_fresh(context * new_ctx) override { return alloc(theory_char, *new_ctx, get_family_id()); } bool internalize_atom(app * atom, bool gate_ctx) override; bool internalize_term(app * term) override; void display(std::ostream& out) const override {} @@ -74,14 +77,6 @@ namespace smt { model_value_proc * mk_value(enode * n, model_generator & mg) override; void collect_statistics(::statistics& st) const override; - // Methods exposed when theory_char is a sub-theory of seq and not a stand-alone theory - // ensure coherence for character codes and equalities of shared symbols. - bool enabled() const { return m_enabled; } - bool final_check(); - void new_const_char(theory_var v, unsigned c); - unsigned get_char_value(theory_var v); - - void internalize_le(literal lit, app* term); }; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 037f0f344..ad632143b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -108,8 +108,6 @@ Outline: #include "smt/theory_lra.h" #include "smt/smt_kernel.h" -#define _USE_CHAR (false && m_char.enabled()) - using namespace smt; void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) { @@ -274,7 +272,6 @@ theory_seq::theory_seq(context& ctx): m_autil(m), m_sk(m, m_rewrite), m_ax(*this, m_rewrite), - m_char(ctx, get_family_id(), this), m_regex(*this), m_arith_value(m), m_trail_stack(*this), @@ -356,9 +353,6 @@ final_check_status theory_seq::final_check_eh() { TRACEFIN("zero_length"); return FC_CONTINUE; } - if (_USE_CHAR && !m_char.final_check()) { - return FC_CONTINUE; - } if (get_fparams().m_split_w_len && len_based_split()) { ++m_stats.m_branch_variable; TRACEFIN("split_based_on_length"); @@ -1491,11 +1485,6 @@ bool theory_seq::internalize_term(app* term) { bool_var bv = ctx.mk_bool_var(term); ctx.set_var_theory(bv, get_id()); ctx.mark_as_relevant(bv); - if (m_util.is_char_le(term) && _USE_CHAR) { - mk_var(ensure_enode(term->get_arg(0))); - mk_var(ensure_enode(term->get_arg(1))); - m_char.internalize_le(literal(bv, false), term); - } } enode* e = nullptr; @@ -1510,9 +1499,6 @@ bool theory_seq::internalize_term(app* term) { relevant_eh(term); } - unsigned c = 0; - if (_USE_CHAR && m_util.is_const_char(term, c)) - m_char.new_const_char(v, c); return true; } @@ -1771,7 +1757,6 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq extensionality", m_stats.m_extensionality); st.update("seq fixed length", m_stats.m_fixed_length); st.update("seq int.to.str", m_stats.m_int_string); - m_char.collect_statistics(st); } void theory_seq::init_search_eh() { @@ -1994,12 +1979,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { m_concat.shrink(start); return sv; } - else if (_USE_CHAR && m_util.is_char(e)) { - unsigned ch = m_char.get_char_value(n->get_th_var(get_id())); - app* val = m_util.str.mk_char(ch); - m_factory->add_trail(val); - return alloc(expr_wrapper_proc, val); - } else { return alloc(expr_wrapper_proc, mk_value(e)); } @@ -2304,7 +2283,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons theory_var theory_seq::mk_var(enode* n) { expr* o = n->get_owner(); - if (!m_util.is_seq(o) && !m_util.is_re(o) && (!_USE_CHAR || !m_util.is_char(o))) + if (!m_util.is_seq(o) && !m_util.is_re(o)) return null_theory_var; if (is_attached_to_var(n)) @@ -2963,9 +2942,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) { // no-op } - else if (_USE_CHAR && m_util.is_char_le(e)) { - // no-op - } else if (m_util.is_skolem(e)) { // no-op @@ -2984,10 +2960,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { enode* n2 = get_enode(v2); expr* o1 = n1->get_owner(); expr* o2 = n2->get_owner(); - if (_USE_CHAR && m_util.is_char(o1)) { - m_char.new_eq_eh(v1, v2); - return; - } if (!m_util.is_seq(o1) && !m_util.is_re(o1)) return; if (m_util.is_re(o1)) { @@ -3035,10 +3007,6 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { m_regex.propagate_ne(e1, e2); return; } - if (_USE_CHAR && m_util.is_char(n1->get_owner())) { - m_char.new_diseq_eh(v1, v2); - return; - } if (!m_util.is_seq(e1)) return; m_exclude.update(e1, e2); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 7c77d32f5..71a728a38 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -28,7 +28,6 @@ Revision History: #include "util/obj_ref_hashtable.h" #include "smt/smt_theory.h" #include "smt/smt_arith_value.h" -#include "smt/theory_char.h" #include "smt/theory_seq_empty.h" #include "smt/seq_skolem.h" #include "smt/seq_axioms.h" @@ -356,7 +355,6 @@ namespace smt { arith_util m_autil; seq_skolem m_sk; seq_axioms m_ax; - theory_char m_char; seq_regex m_regex; arith_value m_arith_value; th_trail_stack m_trail_stack;