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

fix #2920

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-04 08:55:55 -08:00
parent d4d3971ecd
commit 3ab7477663
2 changed files with 39 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
src/smt/theory_seq.cpp
View file

@ -2054,8 +2054,12 @@ bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
}
bool theory_seq::is_post(expr* e, expr*& s, expr*& l) {
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), l = to_app(e)->get_arg(1), true);
bool theory_seq::is_post(expr* e, expr*& s, expr*& start) {
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), start = to_app(e)->get_arg(1), true);
}
expr_ref theory_seq::mk_post(expr* s, expr* i) {
return mk_skolem(m_post, s, i);
}
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
@ -2556,23 +2560,24 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs
return false;
}
/**
nth(x,idx) = rhs =>
x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
NB: need 0 <= idx < len(rhs)
*/
bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
expr* s = nullptr, *idx = nullptr;
if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
rational r;
bool idx_is_zero = m_autil.is_numeral(idx, r) && r.is_zero();
expr_ref_vector ls1(m), rs1(m);
expr_ref idx1(m_autil.mk_add(m_autil.mk_int(1), idx), m);
expr_ref lent(m_autil.mk_sub(mk_len(ls[0]), idx1), m);
m_rewrite(lent);
expr_ref hd = mk_skolem(m_pre, s, idx);
expr_ref tl = mk_skolem(m_post, s, lent);
expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
m_rewrite(idx1);
expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
rhs = m_util.str.mk_unit(rhs);
if (!idx_is_zero) rs1.push_back(hd);
rs1.push_back(rhs);
rs1.push_back(tl);
ls1.push_back(s);
if (!idx_is_zero) rs1.push_back(mk_skolem(m_pre, s, idx));
rs1.push_back(m_util.str.mk_unit(rhs));
rs1.push_back(mk_post(s, idx1));
m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));
return true;
}
@ -3184,14 +3189,14 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
return true;
}
}
else if (is_post(e, s, l)) {
else if (is_post(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
literal l_ge_0 = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(s), l), zero));
literal _lits[2] = { l_ge_0, l_le_len_s };
if (ctx.get_assignment(l_ge_0) == l_true &&
ctx.get_assignment(l_le_len_s) == l_true) {
len = l;
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal len_s_ge_i = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(s), i), zero));
literal _lits[2] = { i_ge_0, len_s_ge_i };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(len_s_ge_i) == l_true) {
len = mk_sub(mk_len(s), i);
lits.append(2, _lits);
TRACE("seq", ctx.display_literals_verbose(tout << "post length " << len << "\n", 2, _lits) << "\n";);
return true;
@ -4458,7 +4463,7 @@ expr_ref theory_seq::elim_skolem(expr* e) {
x = cache[x];
y = cache[y];
result = m_util.str.mk_length(x);
result = m_util.str.mk_substr(x, m_autil.mk_sub(result, y), y);
result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y));
trail.push_back(result);
cache.insert(a, result);
todo.pop_back();
@ -4516,16 +4521,16 @@ void theory_seq::validate_axiom(literal_vector const& lits) {
}
void theory_seq::validate_conflict(enode_pair_vector const& eqs, literal_vector const& lits) {
IF_VERBOSE(10, display_deps(verbose_stream() << "; conflict\n", lits, eqs));
if (get_context().get_fparams().m_seq_validate) {
IF_VERBOSE(1, display_deps(verbose_stream() << "; conflict\n", lits, eqs));
expr_ref_vector fmls(m);
validate_fmls(eqs, lits, fmls);
}
}
void theory_seq::validate_assign(literal lit, enode_pair_vector const& eqs, literal_vector const& lits) {
IF_VERBOSE(10, display_deps(verbose_stream() << "; assign\n", lits, eqs); display_lit(verbose_stream(), ~lit));
if (get_context().get_fparams().m_seq_validate) {
IF_VERBOSE(1, display_deps(verbose_stream() << "; assign\n", lits, eqs); display_lit(verbose_stream(), ~lit));
literal_vector _lits(lits);
_lits.push_back(~lit);
expr_ref_vector fmls(m);
@ -4534,10 +4539,10 @@ void theory_seq::validate_assign(literal lit, enode_pair_vector const& eqs, lite
}
void theory_seq::validate_assign_eq(enode* a, enode* b, enode_pair_vector const& eqs, literal_vector const& lits) {
IF_VERBOSE(10, display_deps(verbose_stream() << "; assign-eq\n", lits, eqs);
verbose_stream() << "(not (= " << mk_bounded_pp(a->get_owner(), m)
<< " " << mk_bounded_pp(b->get_owner(), m) << "))\n");
if (get_context().get_fparams().m_seq_validate) {
IF_VERBOSE(1, display_deps(verbose_stream() << "; assign-eq\n", lits, eqs);
verbose_stream() << "(not (= " << mk_bounded_pp(a->get_owner(), m)
<< " " << mk_bounded_pp(b->get_owner(), m) << "))\n");
expr_ref_vector fmls(m);
fmls.push_back(m.mk_not(m.mk_eq(a->get_owner(), b->get_owner())));
validate_fmls(eqs, lits, fmls);
@ -4900,7 +4905,7 @@ void theory_seq::deque_axiom(expr* n) {
/*
encode that s is not contained in of xs1
where s1 is all of s, except the last element.
s = "" or s = s1*(unit c)
s = "" or !contains(x*s1, s)
*/
@ -4969,7 +4974,6 @@ void theory_seq::add_indexof_axiom(expr* i) {
// ~contains(t,s) <=> indexof(t,s,offset) = -1
add_axiom(cnt, i_eq_m1);
// add_axiom(~cnt, ~i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
@ -5005,8 +5009,8 @@ void theory_seq::add_indexof_axiom(expr* i) {
// 0 <= offset & offset < len(t) => t = xy
// 0 <= offset & offset < len(t) => len(x) = offset
// 0 <= offset & offset < len(t) & -1 = indexof(y,s,0) = -1 => -1 = i
// 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 = -1 =>
// 0 <= offset & offset < len(t) & indexof(y,s,0) = -1 => -1 = i
// 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 =>
// -1 = indexof(y,s,0) + offset = indexof(t, s, offset)
add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
@ -5044,10 +5048,10 @@ void theory_seq::add_last_indexof_axiom(expr* i) {
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal cnt2 = mk_literal(m_util.str.mk_contains(mk_concat(s_tail, y), s));
literal i_eq_m1 = mk_eq(i, minus_one, false);
literal i_eq_0 = mk_eq(i, zero, false);
literal i_eq_0 = mk_eq(i, zero, false);
literal s_eq_empty = mk_eq_empty(s);
literal t_eq_empty = mk_eq_empty(t);
expr_ref xsy = mk_concat(x, s, y);
expr_ref xsy = mk_concat(x, s, y);
add_axiom(cnt, i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
@ -5360,7 +5364,6 @@ static T* get_th_arith(context& ctx, theory_id afid, expr* e) {
}
}
bool theory_seq::get_num_value(expr* e, rational& val) const {
return m_arith_value.get_value_equiv(e, val) && val.is_int();
}
@ -5378,8 +5381,6 @@ bool theory_seq::upper_bound(expr* e, rational& hi) const {
return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int();
}
// The difference with lower_bound function is that since in some cases,
// the lower bound is not updated for all the enodes in the same eqc,
// we have to traverse the eqc to query for the better lower bound.
@ -5419,7 +5420,6 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
return true;
}
bool theory_seq::get_length(expr* e, rational& val) {
rational val1;
expr_ref len(m), len_val(m);
@ -5515,7 +5515,7 @@ void theory_seq::add_extract_axiom(expr* e) {
expr_ref lx = mk_len(x);
expr_ref le = mk_len(e);
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m);
expr_ref y(mk_skolem(m_post, s, ls_minus_i_l), m);
expr_ref y = mk_post(s, mk_add(i, l));
expr_ref xe = mk_concat(x, e);
expr_ref xey = mk_concat(x, e, y);
expr_ref zero(m_autil.mk_int(0), m);
@ -5530,7 +5530,7 @@ void theory_seq::add_extract_axiom(expr* e) {
literal le_is_0 = mk_eq(le, zero, false);
// 0 <= i & i <= |s| => xey = s
// 0 <= i & i <= |s| & 0 <= l => xey = s
// 0 <= i & i <= |s| => |x| = i
// 0 <= i & i <= |s| & l >= 0 & |s| >= l + i => |e| = l
// 0 <= i & i <= |s| & |s| < l + i => |e| = |s| - i
@ -5539,7 +5539,7 @@ void theory_seq::add_extract_axiom(expr* e) {
// |s| <= 0 => |e| = 0
// l <= 0 => |e| = 0
// |e| = 0 & i >= 0 & |s| > i & |s| > 0 => l <= 0
add_axiom(~i_ge_0, ~i_le_ls, mk_seq_eq(xey, s));
add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, mk_seq_eq(xey, s));
add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false));
add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, ~ls_ge_li, mk_eq(le, l, false));
add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, ls_ge_li, mk_eq(le, mk_sub(ls, i), false));
@ -5613,7 +5613,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
expr_ref ls = mk_len(s);
expr_ref ls_minus_l(mk_sub(ls, l), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref y(mk_skolem(m_post, s, ls_minus_l), m);
expr_ref y = mk_post(s, l);
expr_ref ey = mk_concat(e, y);
literal l_ge_0 = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal l_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(l, ls), zero));
@ -5974,8 +5974,6 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
return true;
}
void theory_seq::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
expr* e = ctx.bool_var2expr(v);

1
src/smt/theory_seq.h
View file

@ -591,6 +591,7 @@ namespace smt {
bool is_eq(expr* e, expr*& a, expr*& b) const;
bool is_pre(expr* e, expr*& s, expr*& i);
bool is_post(expr* e, expr*& s, expr*& i);
expr_ref mk_post(expr* s, expr* i);
expr_ref mk_sk_ite(expr* c, expr* t, expr* f);
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);