diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 538cd38c8..dd4bfbd78 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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 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; } @@ -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; } diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index a6f8f6ab2..a751df7aa 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -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 @@ -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)); } }