mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

#4153

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 22:03:11 -07:00
parent e67112f289
commit 4d54b4109f
2 changed files with 90 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/smt/seq_axioms.cpp
View file

@ -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));
}
}