mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix #5715

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-16 09:35:54 -08:00
parent 2caa7e6e45
commit dd6a11b526
2 changed files with 24 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_seq.cpp
View file

@ -349,7 +349,7 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("propagate_contains");
return FC_CONTINUE;
}
if (fixed_length(true)) {
if (check_fixed_length(true, false)) {
++m_stats.m_fixed_length;
TRACEFIN("zero_length");
return FC_CONTINUE;
@ -359,7 +359,7 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("split_based_on_length");
return FC_CONTINUE;
}
if (fixed_length()) {
if (check_fixed_length(false, false)) {
++m_stats.m_fixed_length;
TRACEFIN("fixed_length");
return FC_CONTINUE;
@ -413,6 +413,11 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("branch_itos");
return FC_CONTINUE;
}
if (check_fixed_length(false, true)) {
++m_stats.m_fixed_length;
TRACEFIN("fixed_length");
return FC_CONTINUE;
}
if (m_unhandled_expr) {
TRACEFIN("give_up");
TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
@ -461,18 +466,18 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
}
bool theory_seq::fixed_length(bool is_zero) {
bool theory_seq::check_fixed_length(bool is_zero, bool check_long_strings) {
bool found = false;
for (unsigned i = 0; i < m_length.size(); ++i) {
expr* e = m_length.get(i);
if (fixed_length(e, is_zero)) {
if (fixed_length(e, is_zero, check_long_strings)) {
found = true;
}
}
return found;
}
bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings) {
rational lo, hi;
expr* e = nullptr;
VERIFY(m_util.str.is_length(len_e, e));
@ -493,12 +498,21 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
expr_ref seq(e, m), head(m), tail(m);
TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
if (ctx.get_assignment(a) == l_false)
return false;
if (!check_long_strings && lo > 20 && !is_zero)
return false;
if (lo.is_zero()) {
seq = m_util.str.mk_empty(e->get_sort());
}
else if (!is_zero) {
unsigned _lo = lo.get_unsigned();
expr_ref_vector elems(m);
expr_ref_vector elems(m);
for (unsigned j = 0; j < _lo; ++j) {
m_sk.decompose(seq, head, tail);
elems.push_back(head);
@ -506,10 +520,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
}
seq = mk_concat(elems.size(), elems.data());
}
TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
if (ctx.get_assignment(a) == l_false)
return false;
literal b = mk_seq_eq(seq, e);
if (ctx.get_assignment(b) == l_true)
return false;
@ -2873,7 +2883,7 @@ void theory_seq::add_axiom(literal_vector & lits) {
for (literal lit : lits)
ctx.mark_as_relevant(lit);
IF_VERBOSE(10, verbose_stream() << "ax ";
IF_VERBOSE(10, verbose_stream() << "ax";
for (literal l : lits) ctx.display_literal_smt2(verbose_stream() << " ", l);
verbose_stream() << "\n");
m_new_propagation = true;

6
src/smt/theory_seq.h
View file

@ -243,7 +243,7 @@ namespace smt {
replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_fixed_length() override {}
void operator()(theory_seq& th) override {
th.fixed_length(m_e);
th.fixed_length(m_e, false, false);
m_e.reset();
}
};
@ -436,8 +436,8 @@ namespace smt {
bool check_length_coherence();
bool check_length_coherence0(expr* e);
bool check_length_coherence(expr* e);
bool fixed_length(bool is_zero = false);
bool fixed_length(expr* e, bool is_zero);
bool check_fixed_length(bool is_zero, bool check_long_strings);
bool fixed_length(expr* e, bool is_zero, bool check_long_strings);
bool branch_variable_eq(depeq const& e);
bool branch_binary_variable(depeq const& e);
bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);