mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

fixing bugs reported in #4518

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-21 15:50:19 -07:00
parent b1824fea10
commit aab50ff3f5
5 changed files with 70 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/smt/seq_axioms.cpp
View file

@ -846,6 +846,13 @@ void seq_axioms::add_suffix_axiom(expr* e) {
m_rewrite(t);
literal lit = mk_literal(e);
literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
#if 0
expr_ref x = m_sk.mk_pre(t, mk_sub(mk_len(t), mk_len(s)));
expr_ref y = m_sk.mk_tail(t, mk_sub(mk_len(s), a.mk_int(1)));
add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
add_axiom(lit, s_gt_t, mk_eq(mk_len(y), mk_len(s)));
add_axiom(lit, s_gt_t, ~mk_eq(y, s));
#else
sort* char_sort = nullptr;
VERIFY(seq.is_seq(m.get_sort(s), char_sort));
expr_ref x = m_sk.mk("seq.suffix.x", s, t);
@ -856,6 +863,7 @@ void seq_axioms::add_suffix_axiom(expr* e) {
add_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(y, seq.str.mk_unit(c), x)));
add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(z, seq.str.mk_unit(d), x)));
add_axiom(lit, s_gt_t, ~mk_eq(c, d));
#endif
}
void seq_axioms::add_prefix_axiom(expr* e) {
@ -866,6 +874,14 @@ void seq_axioms::add_prefix_axiom(expr* e) {
m_rewrite(t);
literal lit = mk_literal(e);
literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
#if 0
expr_ref x = m_sk.mk_pre(t, mk_len(s));
expr_ref y = m_sk.mk_tail(t, mk_sub(mk_sub(mk_len(t), mk_len(s)), a.mk_int(1)));
add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
add_axiom(lit, s_gt_t, mk_eq(mk_len(x), mk_len(s)));
add_axiom(lit, s_gt_t, ~mk_eq(x, s));
#else
sort* char_sort = nullptr;
VERIFY(seq.is_seq(m.get_sort(s), char_sort));
expr_ref x = m_sk.mk("seq.prefix.x", s, t);
@ -876,6 +892,7 @@ void seq_axioms::add_prefix_axiom(expr* e) {
add_axiom(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y)));
add_axiom(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x));
add_axiom(lit, s_gt_t, ~mk_eq(c, d));
#endif
}
/***

16
src/smt/seq_eq_solver.cpp
View file

@ -758,10 +758,6 @@ bool theory_seq::branch_ternary_variable() {
}
bool theory_seq::eq_unit(expr* l, expr* r) const {
return l == r || is_unit_nth(l) || is_unit_nth(r);
}
// exists x, y, rs' != empty s.t. (ls = x ++ rs ++ y) || (ls = rs' ++ y && rs = x ++ rs')
bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs) {
SASSERT(!ls.empty() && !rs.empty());
@ -773,7 +769,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
return result;
}
for (unsigned i = 0; i < ls.size(); ++i) {
if (eq_unit(ls[i], rs.back())) {
if (!m.are_distinct(ls[i], rs.back())) {
bool same = true;
if (i == 0) {
m_overlap_lhs.insert(pair, true);
@ -783,7 +779,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
if (rs.size() > i) {
unsigned diff = rs.size() - (i + 1);
for (unsigned j = 0; same && j < i; ++j) {
same = eq_unit(ls[j], rs[diff + j]);
same = !m.are_distinct(ls[j], rs[diff + j]);
}
if (same) {
m_overlap_lhs.insert(pair, true);
@ -794,7 +790,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
else {
unsigned diff = (i + 1) - rs.size();
for (unsigned j = 0; same && j < rs.size()-1; ++j) {
same = eq_unit(ls[diff + j], rs[j]);
same = !m.are_distinct(ls[diff + j], rs[j]);
}
if (same) {
m_overlap_lhs.insert(pair, true);
@ -819,7 +815,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
}
for (unsigned i = 0; i < ls.size(); ++i) {
unsigned diff = ls.size()-1-i;
if (eq_unit(ls[diff], rs[0])) {
if (!m.are_distinct(ls[diff], rs[0])) {
bool same = true;
if (i == 0) {
m_overlap_rhs.insert(pair, true);
@ -828,7 +824,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
// ls = x ++ rs' && rs = rs' ++ y, diff = |x|
if (rs.size() > i) {
for (unsigned j = 1; same && j <= i; ++j) {
same = eq_unit(ls[diff+j], rs[j]);
same = !m.are_distinct(ls[diff+j], rs[j]);
}
if (same) {
m_overlap_rhs.insert(pair, true);
@ -838,7 +834,7 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
// ls = x ++ rs ++ y, diff = |x|
else {
for (unsigned j = 1; same && j < rs.size(); ++j) {
same = eq_unit(ls[diff + j], rs[j]);
same = !m.are_distinct(ls[diff + j], rs[j]);
}
if (same) {
m_overlap_rhs.insert(pair, true);

9
src/smt/seq_skolem.h
View file

@ -102,12 +102,21 @@ namespace smt {
bool is_skolem(symbol const& s, expr const* e) const;
bool is_skolem(expr const* e) const { return seq.is_skolem(e); }
bool is_first(expr* e, expr*& u) { return is_skolem(m_seq_first, e) && (u = to_app(e)->get_arg(0), true); }
bool is_last(expr* e, expr*& u) { return is_skolem(m_seq_last, e) && (u = to_app(e)->get_arg(0), true); }
bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); }
bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); }
bool is_tail(expr* e) const { return is_skolem(m_tail, e); }
bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); }
bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); }
bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); }
bool is_indexof_left(expr* e, expr*& x, expr*& y) const {
return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
}
bool is_indexof_right(expr* e, expr*& x, expr*& y) const {
return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
}
bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }

39
src/smt/theory_seq.cpp
View file

@ -2213,6 +2213,41 @@ expr_ref theory_seq::elim_skolem(expr* e) {
todo.pop_back();
continue;
}
if (m_sk.is_first(a, x) && cache.contains(x)) {
x = cache[x];
result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_autil.mk_sub(m_util.str.mk_length(x), m_autil.mk_int(1)));
trail.push_back(result);
cache.insert(a, result);
todo.pop_back();
continue;
}
if (m_sk.is_last(a, x) && cache.contains(x)) {
x = cache[x];
result = m_util.str.mk_nth(x, m_autil.mk_sub(m_util.str.mk_length(x), m_autil.mk_int(1)));
trail.push_back(result);
cache.insert(a, result);
todo.pop_back();
continue;
}
if (m_sk.is_indexof_left(a, x, y) && cache.contains(x) && cache.contains(y)) {
x = cache[x];
y = cache[y];
result = m_util.str.mk_substr(x, m_autil.mk_int(0), m_util.str.mk_index(x, y, m_autil.mk_int(0)));
trail.push_back(result);
cache.insert(a, result);
todo.pop_back();
continue;
}
if (m_sk.is_indexof_right(a, x, y) && cache.contains(x) && cache.contains(y)) {
x = cache[x];
y = cache[y];
expr_ref offset(m_autil.mk_add(m_util.str.mk_length(y), m_util.str.mk_index(x, y, m_autil.mk_int(0))), m);
result = m_util.str.mk_substr(x, offset, m_util.str.mk_length(x));
trail.push_back(result);
cache.insert(a, result);
todo.pop_back();
continue;
}
args.reset();
for (expr* arg : *to_app(a)) {
@ -2282,6 +2317,7 @@ void theory_seq::validate_assign_eq(enode* a, enode* b, enode_pair_vector const&
void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector const& lits, expr_ref_vector& fmls) {
smt_params fp;
fp.m_seq_validate = false;
fp.m_max_conflicts = 100;
expr_ref fml(m);
kernel k(m, fp);
for (literal lit : lits) {
@ -2292,6 +2328,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
fmls.push_back(m.mk_eq(p.first->get_owner(), p.second->get_owner()));
}
TRACE("seq", tout << fmls << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) {
fml = elim_skolem(fmls.get(i));
fmls[i] = fml;
@ -2301,7 +2338,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
k.assert_expr(f);
}
lbool r = k.check();
if (r != l_false && !m.limit().is_canceled()) {
if (r == l_true) {
model_ref mdl;
k.get_model(mdl);
IF_VERBOSE(0,

1
src/smt/theory_seq.h
View file

@ -451,7 +451,6 @@ namespace smt {
void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
bool branch_variable_eq(eq const& e);
bool branch_binary_variable(eq const& e);
bool eq_unit(expr* l, expr* r) const;
bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool branch_ternary_variable_rhs(eq const& e);