mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

remove plugin status to theory_seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-27 06:22:25 -08:00
parent 696b3c79b9
commit 8d8fe872ad
6 changed files with 29 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/char_decl_plugin.cpp
View file

@ -76,7 +76,7 @@ void char_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol cons
} }
void char_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const& logic) { void char_decl_plugin::get_sort_names(svector<builtin_name>& 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 { 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) { app* char_decl_plugin::mk_char(unsigned u) {
SASSERT(u <= zstring::unicode_max_char());
parameter param(u); 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)); 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); return m_manager->mk_const(f);

2
src/smt/smt_setup.cpp
View file

@ -940,7 +940,7 @@ namespace smt {
sort* s = seq.mk_string_sort(); sort* s = seq.mk_string_sort();
family_id ch_fid = ch->get_family_id(); family_id ch_fid = ch->get_family_id();
if (s->get_family_id() != ch_fid) 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));
} }

40
src/smt/theory_char.cpp
View file

@ -22,18 +22,12 @@ Author:
namespace smt { 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), theory(ctx, fid),
seq(m), seq(m),
m_bb(m, ctx.get_fparams()), m_bb(m, ctx.get_fparams())
m_th(th)
{ {
bv_util bv(m);
sort_ref b8(bv.mk_sort(8), m);
m_enabled = !seq.is_char(b8);
m_bits2char = symbol("bits2char"); m_bits2char = symbol("bits2char");
if (!m_th)
m_th = this;
} }
struct theory_char::reset_bits : public trail<context> { struct theory_char::reset_bits : public trail<context> {
@ -102,7 +96,7 @@ namespace smt {
if (has_bits(v)) if (has_bits(v))
return; return;
expr* e = m_th->get_expr(v); expr* e = get_expr(v);
m_bits.reserve(v + 1); m_bits.reserve(v + 1);
auto& bits = m_bits[v]; auto& bits = m_bits[v];
while ((unsigned) v >= m_ebits.size()) while ((unsigned) v >= m_ebits.size())
@ -142,8 +136,8 @@ namespace smt {
void theory_char::internalize_le(literal lit, app* term) { void theory_char::internalize_le(literal lit, app* term) {
expr* x = nullptr, *y = nullptr; expr* x = nullptr, *y = nullptr;
VERIFY(seq.is_char_le(term, x, y)); VERIFY(seq.is_char_le(term, x, y));
theory_var v1 = ctx.get_enode(x)->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(m_th->get_id()); theory_var v2 = ctx.get_enode(y)->get_th_var(get_id());
init_bits(v1); init_bits(v1);
init_bits(v2); init_bits(v2);
auto const& b1 = get_ebits(v1); auto const& b1 = get_ebits(v1);
@ -229,22 +223,22 @@ namespace smt {
* 2. Assign values to characters that haven't been assigned. * 2. Assign values to characters that haven't been assigned.
*/ */
bool theory_char::final_check() { 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.reset();
m_var2value.resize(m_th->get_num_vars(), UINT_MAX); m_var2value.resize(get_num_vars(), UINT_MAX);
m_value2var.reset(); m_value2var.reset();
// extract the initial set of constants. // extract the initial set of constants.
uint_set values; uint_set values;
unsigned c = 0, d = 0; unsigned c = 0, d = 0;
for (unsigned v = m_th->get_num_vars(); v-- > 0; ) { for (unsigned v = get_num_vars(); v-- > 0; ) {
expr* e = m_th->get_expr(v); expr* e = get_expr(v);
if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) { 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";); 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 = m_th->get_enode(v)->get_root(); enode* r = get_enode(v)->get_root();
m_value2var.reserve(c + 1, null_theory_var); m_value2var.reserve(c + 1, null_theory_var);
theory_var u = m_value2var[c]; 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); enforce_ackerman(u, v);
return false; return false;
} }
@ -269,8 +263,8 @@ namespace smt {
// assign values to other unassigned nodes // assign values to other unassigned nodes
c = 'A'; c = 'A';
for (unsigned v = m_th->get_num_vars(); v-- > 0; ) { for (unsigned v = get_num_vars(); v-- > 0; ) {
expr* e = m_th->get_expr(v); expr* e = get_expr(v);
if (seq.is_char(e) && m_var2value[v] == UINT_MAX) { if (seq.is_char(e) && m_var2value[v] == UINT_MAX) {
d = c; d = c;
while (values.contains(c)) { while (values.contains(c)) {
@ -281,7 +275,7 @@ namespace smt {
} }
} }
TRACE("seq", tout << "fresh: " << mk_pp(e, m) << " := " << c << "\n";); 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_var2value[n->get_th_var(get_id())] = c;
m_value2var.reserve(c + 1, null_theory_var); m_value2var.reserve(c + 1, null_theory_var);
m_value2var[c] = v; m_value2var[c] = v;
@ -293,9 +287,9 @@ namespace smt {
void theory_char::enforce_bits() { void theory_char::enforce_bits() {
TRACE("seq", tout << "enforce bits\n";); 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); 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); init_bits(v);
} }
} }

21
src/smt/theory_char.h
View file

@ -16,8 +16,7 @@ Author:
--*/ --*/
#pragma once #pragma once
#include "ast/seq_decl_plugin.h" #include "ast/char_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/bit_blaster/bit_blaster.h" #include "ast/rewriter/bit_blaster/bit_blaster.h"
#include "model/char_factory.h" #include "model/char_factory.h"
#include "smt/smt_theory.h" #include "smt/smt_theory.h"
@ -44,7 +43,6 @@ namespace smt {
stats m_stats; stats m_stats;
symbol m_bits2char; symbol m_bits2char;
char_factory* m_factory { nullptr }; char_factory* m_factory { nullptr };
theory* m_th;
struct reset_bits; struct reset_bits;
@ -57,15 +55,20 @@ namespace smt {
void enforce_value_bound(theory_var v); void enforce_value_bound(theory_var v);
void enforce_bits(); 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; theory_var mk_var(enode* n) override;
public: 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_eq_eh(theory_var v1, theory_var v2) override;
void new_diseq_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_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app * term) override; bool internalize_term(app * term) override;
void display(std::ostream& out) const 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; model_value_proc * mk_value(enode * n, model_generator & mg) override;
void collect_statistics(::statistics& st) const 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);
}; };
} }

34
src/smt/theory_seq.cpp
View file

@ -108,8 +108,6 @@ Outline:
#include "smt/theory_lra.h" #include "smt/theory_lra.h"
#include "smt/smt_kernel.h" #include "smt/smt_kernel.h"
#define _USE_CHAR (false && m_char.enabled())
using namespace smt; using namespace smt;
void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) { 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_autil(m),
m_sk(m, m_rewrite), m_sk(m, m_rewrite),
m_ax(*this, m_rewrite), m_ax(*this, m_rewrite),
m_char(ctx, get_family_id(), this),
m_regex(*this), m_regex(*this),
m_arith_value(m), m_arith_value(m),
m_trail_stack(*this), m_trail_stack(*this),
@ -356,9 +353,6 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("zero_length"); TRACEFIN("zero_length");
return FC_CONTINUE; return FC_CONTINUE;
} }
if (_USE_CHAR && !m_char.final_check()) {
return FC_CONTINUE;
}
if (get_fparams().m_split_w_len && len_based_split()) { if (get_fparams().m_split_w_len && len_based_split()) {
++m_stats.m_branch_variable; ++m_stats.m_branch_variable;
TRACEFIN("split_based_on_length"); TRACEFIN("split_based_on_length");
@ -1491,11 +1485,6 @@ bool theory_seq::internalize_term(app* term) {
bool_var bv = ctx.mk_bool_var(term); bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
ctx.mark_as_relevant(bv); 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; enode* e = nullptr;
@ -1510,9 +1499,6 @@ bool theory_seq::internalize_term(app* term) {
relevant_eh(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; 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 extensionality", m_stats.m_extensionality);
st.update("seq fixed length", m_stats.m_fixed_length); st.update("seq fixed length", m_stats.m_fixed_length);
st.update("seq int.to.str", m_stats.m_int_string); st.update("seq int.to.str", m_stats.m_int_string);
m_char.collect_statistics(st);
} }
void theory_seq::init_search_eh() { 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); m_concat.shrink(start);
return sv; 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 { else {
return alloc(expr_wrapper_proc, mk_value(e)); 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) { theory_var theory_seq::mk_var(enode* n) {
expr* o = n->get_owner(); 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; return null_theory_var;
if (is_attached_to_var(n)) 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)) { else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
// no-op // no-op
} }
else if (_USE_CHAR && m_util.is_char_le(e)) {
// no-op
}
else if (m_util.is_skolem(e)) { else if (m_util.is_skolem(e)) {
// no-op // no-op
@ -2984,10 +2960,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
enode* n2 = get_enode(v2); enode* n2 = get_enode(v2);
expr* o1 = n1->get_owner(); expr* o1 = n1->get_owner();
expr* o2 = n2->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)) if (!m_util.is_seq(o1) && !m_util.is_re(o1))
return; return;
if (m_util.is_re(o1)) { 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); m_regex.propagate_ne(e1, e2);
return; 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)) if (!m_util.is_seq(e1))
return; return;
m_exclude.update(e1, e2); m_exclude.update(e1, e2);

2
src/smt/theory_seq.h
View file

@ -28,7 +28,6 @@ Revision History:
#include "util/obj_ref_hashtable.h" #include "util/obj_ref_hashtable.h"
#include "smt/smt_theory.h" #include "smt/smt_theory.h"
#include "smt/smt_arith_value.h" #include "smt/smt_arith_value.h"
#include "smt/theory_char.h"
#include "smt/theory_seq_empty.h" #include "smt/theory_seq_empty.h"
#include "smt/seq_skolem.h" #include "smt/seq_skolem.h"
#include "smt/seq_axioms.h" #include "smt/seq_axioms.h"
@ -356,7 +355,6 @@ namespace smt {
arith_util m_autil; arith_util m_autil;
seq_skolem m_sk; seq_skolem m_sk;
seq_axioms m_ax; seq_axioms m_ax;
theory_char m_char;
seq_regex m_regex; seq_regex m_regex;
arith_value m_arith_value; arith_value m_arith_value;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;