Skip to content

Commit

Permalink
#4153
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Apr 29, 2020
1 parent e67112f commit 4d54b41
Show file tree
Hide file tree
Showing 2 changed files with 90 additions and 11 deletions.
55 changes: 55 additions & 0 deletions src/ast/rewriter/seq_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -882,6 +882,17 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
if (offset == 0 && _pos > 0) {
return BR_FAILED;
}
std::function<bool(expr*)> is_unit = [&](expr *e) { return m_util.str.is_unit(e); };

if (_pos == 0 && as.forall(is_unit)) {
result = m_util.str.mk_empty(m().get_sort(a));
for (unsigned i = 1; i <= as.size(); ++i) {
result = m().mk_ite(m_autil.mk_ge(c, m_autil.mk_int(i)),
m_util.str.mk_concat(i, as.c_ptr(), m().get_sort(a)),
result);
}
return BR_REWRITE_FULL;
}
if (_pos == 0 && !constantLen) {
return BR_FAILED;
}
Expand Down Expand Up @@ -1736,6 +1747,50 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
return BR_DONE;
}
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (m().is_ite(a, c, t, e)) {
result = m().mk_ite(c, m_util.str.mk_stoi(t), m_util.str.mk_stoi(e));
return BR_REWRITE_FULL;
}

expr* u = nullptr;
unsigned ch = 0;
if (m_util.str.is_unit(a, u) && m_util.is_const_char(u, ch)) {
if ('0' <= ch && ch <= '9') {
result = m_autil.mk_int(ch - '0');
}
else {
result = m_autil.mk_int(-1);
}
return BR_DONE;
}

expr_ref_vector as(m());
m_util.str.get_concat_units(a, as);
if (as.empty()) {
result = m_autil.mk_int(-1);
return BR_DONE;
}
if (m_util.str.is_unit(as.back())) {
// if head = "" then tail else
// if tail < 0 then tail else
// if stoi(head) >= 0 and then stoi(head)*10+tail else -1
expr_ref tail(m_util.str.mk_stoi(as.back()), m());
expr_ref head(m_util.str.mk_concat(as.size() - 1, as.c_ptr(), m().get_sort(a)), m());
expr_ref stoi_head(m_util.str.mk_stoi(head), m());
result = m().mk_ite(m_autil.mk_ge(stoi_head, m_autil.mk_int(0)),
m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), stoi_head), tail),
m_autil.mk_int(-1));

result = m().mk_ite(m_autil.mk_ge(tail, m_autil.mk_int(0)),
result,
tail);
result = m().mk_ite(m_util.str.mk_is_empty(head),
tail,
result);
return BR_REWRITE_FULL;
}

return BR_FAILED;
}

Expand Down
46 changes: 35 additions & 11 deletions src/smt/seq_axioms.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -563,21 +563,32 @@ void seq_axioms::add_itos_axiom(expr* e) {
/**
stoi(s) >= -1
stoi("") = -1
stoi(s) >= 0 => len(s) > 0
stoi(s) >= 0 => is_digit(nth(s,0))
*/
void seq_axioms::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
expr* s = nullptr;
VERIFY (seq.str.is_stoi(e, s));
add_axiom(mk_ge(e, -1));
add_axiom(~mk_literal(seq.str.mk_is_empty(s)), mk_eq(seq.str.mk_stoi(s), a.mk_int(-1)));
add_axiom(mk_ge(e, -1)); // stoi(s) >= -1
add_axiom(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1
literal ge0 = mk_ge(e, 0);
add_axiom(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0))

}

/**
stoi(s) >= 0, len(s) <= k => stoi(s) = stoi(s, k)
len(s) > 0 => stoi(s, 0) = digit(nth_i(s, 0))
len(s) <= k => stoi(s) = stoi(s, k)
len(s) > 0, is_digit(nth(s,0)) => stoi(s, 0) = digit(nth_i(s, 0))
len(s) > 0, ~is_digit(nth(s,0)) => stoi(s, 0) = -1
0 < i, len(s) <= i => stoi(s, i) = stoi(s, i - 1)
0 < i, len(s) > i => stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1))
0 < i, len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i - 1)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1))
0 < i, len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1
0 < i, len(s) > i, ~is_digit(nth(s, i - 1)) => stoi(s, i) = -1
Define auxiliary function with the property:
for 0 <= i < k
Expand All @@ -599,17 +610,30 @@ void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
m_rewrite(s);
auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); };
auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, j)); };
auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); };
expr_ref len = mk_len(s);
literal ge0 = mk_ge(e, 0);
literal lek = mk_le(len, k);
add_axiom(~ge0, ~mk_eq(len, a.mk_int(0)));
add_axiom(~ge0, ~lek, mk_eq(e, stoi2(k-1)));
add_axiom(mk_le(len, 0), mk_eq(stoi2(0), digit(0)));
add_axiom(~ge0, is_digit(mk_nth(s, 0)));
add_axiom(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1)
add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
add_axiom(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
for (unsigned i = 1; i < k; ++i) {
add_axiom(mk_le(len, i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));

// len(s) <= i => stoi(s, i) = stoi(s, i - 1)

add_axiom(~mk_le(len, i), mk_eq(stoi2(i), stoi2(i-1)));
add_axiom(~ge0, mk_le(len, i), is_digit(mk_nth(s, i)));

// len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(i)
// len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1
// len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1

add_axiom(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));
add_axiom(mk_le(len, i), is_digit_(i), mk_eq(stoi2(i), a.mk_int(-1)));
add_axiom(mk_le(len, i), mk_ge(stoi2(i-1), 0), mk_eq(stoi2(i), a.mk_int(-1)));

// stoi(s) >= 0, i < len(s) => is_digit(nth(s, i))

add_axiom(~ge0, mk_le(len, i), is_digit_(i));
}
}

Expand Down

0 comments on commit 4d54b41

Please sign in to comment.