mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
streamline unicode/ascii toggling. Fix bit-width for unicode to 18
This commit is contained in:
parent
90eb4de526
commit
03fd251ccb
|
@ -1950,7 +1950,7 @@ br_status seq_rewriter::mk_str_lt(expr* a, expr* b, expr_ref& result) {
|
|||
br_status seq_rewriter::mk_str_from_code(expr* a, expr_ref& result) {
|
||||
rational r;
|
||||
if (m_autil.is_numeral(a, r)) {
|
||||
if (r.is_neg() || r > zstring::max_char()) {
|
||||
if (r.is_neg() || r > u().max_char()) {
|
||||
result = str().mk_string(symbol(""));
|
||||
}
|
||||
else {
|
||||
|
@ -3979,19 +3979,19 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
|
|||
if (u().is_char(elem)) {
|
||||
unsigned ch = 0;
|
||||
svector<std::pair<unsigned, unsigned>> ranges, ranges1;
|
||||
ranges.push_back(std::make_pair(0, zstring::max_char()));
|
||||
ranges.push_back(std::make_pair(0, u().max_char()));
|
||||
auto exclude_char = [&](unsigned ch) {
|
||||
if (ch == 0) {
|
||||
intersect(1, zstring::max_char(), ranges);
|
||||
intersect(1, u().max_char(), ranges);
|
||||
}
|
||||
else if (ch == zstring::max_char()) {
|
||||
else if (ch == u().max_char()) {
|
||||
intersect(0, ch-1, ranges);
|
||||
}
|
||||
else {
|
||||
ranges1.reset();
|
||||
ranges1.append(ranges);
|
||||
intersect(0, ch - 1, ranges);
|
||||
intersect(ch + 1, zstring::max_char(), ranges1);
|
||||
intersect(ch + 1, u().max_char(), ranges1);
|
||||
ranges.append(ranges1);
|
||||
}
|
||||
};
|
||||
|
@ -4007,7 +4007,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
|
|||
intersect(0, ch, ranges);
|
||||
}
|
||||
else if (u().is_char_le(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
|
||||
intersect(ch, zstring::max_char(), ranges);
|
||||
intersect(ch, u().max_char(), ranges);
|
||||
}
|
||||
else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
|
||||
exclude_char(ch);
|
||||
|
@ -4017,10 +4017,10 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
|
|||
}
|
||||
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) {
|
||||
// not (e <= ch)
|
||||
if (ch == zstring::max_char())
|
||||
if (ch == u().max_char())
|
||||
ranges.reset();
|
||||
else
|
||||
intersect(ch+1, zstring::max_char(), ranges);
|
||||
intersect(ch+1, u().max_char(), ranges);
|
||||
}
|
||||
else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) {
|
||||
// not (ch <= e)
|
||||
|
|
|
@ -180,7 +180,7 @@ bool zstring::uses_unicode() const {
|
|||
|
||||
bool zstring::well_formed() const {
|
||||
for (unsigned ch : m_buffer) {
|
||||
if (ch > max_char())
|
||||
if (ch > unicode_max_char())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
@ -398,9 +398,8 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false),
|
|||
}
|
||||
|
||||
void seq_decl_plugin::finalize() {
|
||||
for (psig* s : m_sigs) {
|
||||
for (psig* s : m_sigs)
|
||||
dealloc(s);
|
||||
}
|
||||
m_manager->dec_ref(m_string);
|
||||
m_manager->dec_ref(m_char);
|
||||
m_manager->dec_ref(m_reglan);
|
||||
|
@ -938,7 +937,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
if (!(num_parameters == 1 && arity == 0 &&
|
||||
parameters[0].is_int() &&
|
||||
0 <= parameters[0].get_int() &&
|
||||
parameters[0].get_int() < static_cast<int>(zstring::max_char()))) {
|
||||
parameters[0].get_int() < static_cast<int>(max_char()))) {
|
||||
m.raise_exception("invalid character declaration");
|
||||
}
|
||||
return m.mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, num_parameters, parameters));
|
||||
|
|
|
@ -118,8 +118,10 @@ private:
|
|||
bool uses_unicode() const;
|
||||
bool is_escape_char(char const *& s, unsigned& result);
|
||||
public:
|
||||
static unsigned max_char() { return 196607; }
|
||||
static unsigned num_bits() { return 16; }
|
||||
static unsigned unicode_max_char() { return 196607; }
|
||||
static unsigned unicode_num_bits() { return 18; }
|
||||
static unsigned ascii_max_char() { return 255; }
|
||||
static unsigned ascii_num_bits() { return 8; }
|
||||
zstring() {}
|
||||
zstring(char const* s);
|
||||
zstring(const std::string &str) : zstring(str.c_str()) {}
|
||||
|
@ -225,6 +227,9 @@ 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(); }
|
||||
|
||||
app* mk_string(symbol const& s);
|
||||
app* mk_string(zstring const& s);
|
||||
app* mk_char(unsigned ch);
|
||||
|
@ -266,6 +271,8 @@ public:
|
|||
app* mk_char(unsigned ch) const;
|
||||
app* mk_le(expr* ch1, expr* ch2) const;
|
||||
app* mk_lt(expr* ch1, expr* ch2) const;
|
||||
unsigned max_char() const { return seq.max_char(); }
|
||||
unsigned num_bits() const { return seq.num_bits(); }
|
||||
|
||||
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
|
||||
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
|
||||
|
|
|
@ -811,7 +811,7 @@ void seq_axioms::add_str_to_code_axiom(expr* n) {
|
|||
VERIFY(seq.str.is_to_code(n, e));
|
||||
literal len_is1 = mk_eq(mk_len(e), a.mk_int(1));
|
||||
add_axiom(~len_is1, mk_ge(n, 0));
|
||||
add_axiom(~len_is1, mk_le(n, zstring::max_char()));
|
||||
add_axiom(~len_is1, mk_le(n, seq.max_char()));
|
||||
add_axiom(len_is1, mk_eq(n, a.mk_int(-1)));
|
||||
}
|
||||
|
||||
|
@ -824,7 +824,7 @@ void seq_axioms::add_str_from_code_axiom(expr* n) {
|
|||
expr* e = nullptr;
|
||||
VERIFY(seq.str.is_from_code(n, e));
|
||||
literal ge = mk_ge(e, 0);
|
||||
literal le = mk_le(e, zstring::max_char());
|
||||
literal le = mk_le(e, seq.max_char());
|
||||
literal emp = mk_literal(seq.str.mk_is_empty(n));
|
||||
add_axiom(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1)));
|
||||
add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e));
|
||||
|
|
|
@ -81,7 +81,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < zstring::num_bits(); ++i)
|
||||
for (unsigned i = 0; i < seq.num_bits(); ++i)
|
||||
ebits.push_back(seq.mk_char_bit(e, i));
|
||||
ctx().internalize(ebits.c_ptr(), ebits.size(), true);
|
||||
for (expr* arg : ebits)
|
||||
|
@ -92,7 +92,9 @@ namespace smt {
|
|||
ctx().mark_as_relevant(bits2char);
|
||||
enode* n1 = th.ensure_enode(e);
|
||||
enode* n2 = th.ensure_enode(bits2char);
|
||||
justification* j = ctx().mk_justification(ext_theory_eq_propagation_justification(th.get_id(), ctx().get_region(), 0, nullptr, 0, nullptr, n1, n2));
|
||||
justification* j =
|
||||
ctx().mk_justification(
|
||||
ext_theory_eq_propagation_justification(th.get_id(), ctx().get_region(), n1, n2));
|
||||
ctx().assign_eq(n1, n2, eq_justification(j));
|
||||
}
|
||||
++m_stats.m_num_blast;
|
||||
|
@ -206,7 +208,7 @@ namespace smt {
|
|||
enforce_ackerman(u, v);
|
||||
return false;
|
||||
}
|
||||
if (c >= zstring::max_char()) {
|
||||
if (c >= seq.max_char()) {
|
||||
enforce_value_bound(v);
|
||||
return false;
|
||||
}
|
||||
|
@ -232,7 +234,7 @@ namespace smt {
|
|||
if (seq.is_char(e) && m_var2value[v] == UINT_MAX) {
|
||||
d = c;
|
||||
while (values.contains(c)) {
|
||||
c = (c + 1) % zstring::max_char();
|
||||
c = (c + 1) % seq.max_char();
|
||||
if (d == c) {
|
||||
enforce_bits();
|
||||
return false;
|
||||
|
@ -260,7 +262,7 @@ namespace smt {
|
|||
|
||||
void seq_unicode::enforce_value_bound(theory_var v) {
|
||||
TRACE("seq", tout << "enforce bound " << v << "\n";);
|
||||
enode* n = th.ensure_enode(seq.mk_char(zstring::max_char()));
|
||||
enode* n = th.ensure_enode(seq.mk_char(seq.max_char()));
|
||||
theory_var w = n->get_th_var(th.get_id());
|
||||
SASSERT(has_bits(w));
|
||||
init_bits(v);
|
||||
|
@ -317,7 +319,7 @@ namespace smt {
|
|||
void seq_unicode::collect_statistics(::statistics& st) const {
|
||||
st.update("seq char ackerman", m_stats.m_num_ackerman);
|
||||
st.update("seq char bounds", m_stats.m_num_bounds);
|
||||
st.update("seq char2bit", m_stats.m_num_blast);
|
||||
st.update("seq char2bit", m_stats.m_num_blast);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -373,6 +373,12 @@ namespace smt {
|
|||
unsigned num_params = 0, parameter* params = nullptr):
|
||||
ext_theory_simple_justification(fid, r, num_lits, lits, num_eqs, eqs, num_params, params), m_lhs(lhs), m_rhs(rhs) {}
|
||||
|
||||
ext_theory_eq_propagation_justification(
|
||||
family_id fid, region & r,
|
||||
enode * lhs, enode * rhs):
|
||||
ext_theory_simple_justification(fid, r, 0, nullptr, 0, nullptr, 0, nullptr), m_lhs(lhs), m_rhs(rhs) {}
|
||||
|
||||
|
||||
proof * mk_proof(conflict_resolution & cr) override;
|
||||
|
||||
char const * get_name() const override { return "ext-theory-eq-propagation"; }
|
||||
|
|
Loading…
Reference in a new issue