mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

add missing digit axioms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 11:12:37 -07:00
parent 99c90d2419
commit b92b6c0fc6
3 changed files with 38 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/smt/seq_axioms.cpp
View file

@ -461,7 +461,7 @@ void seq_axioms::add_at_axiom(expr* e) {
expr_ref nth(m);
unsigned k = iv.get_unsigned();
for (unsigned j = 0; j <= k; ++j) {
es.push_back(seq.str.mk_unit(mk_nth(s, a.mk_int(j))));
es.push_back(seq.str.mk_unit(mk_nth(s, j)));
}
nth = es.back();
es.push_back(m_sk.mk_tail(s, i));
@ -562,29 +562,34 @@ void seq_axioms::add_stoi_axiom(expr* e) {
0 < i, len(s) > i => stoi(s, i) = 10*stoi(s, i - 1) + digit(nth_i(s, i - 1))
Define auxiliary function with the property:
for 0 <= i < len(s)
for 0 <= i < k
stoi(s, i) := stoi(extract(s, 0, i+1))
for 0 < i < len(s):
for 0 < i < k:
len(s) > i => stoi(s, i) := stoi(extract(s, 0, i))*10 + stoi(extract(s, i, 1))
len(s) <= i => stoi(s, i) := stoi(extract(s, 0, i-1), i-1)
for i <= i < k:
stoi(s) > = 0, len(s) > i => is_digit(nth(s, i))
*/
void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
SASSERT(k > 0);
expr* s = nullptr;
VERIFY (seq.str.is_stoi(e, 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, a.mk_int(j))); };
auto digit = [&](unsigned j) { return m_sk.mk_digit2int(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_eq(len, a.mk_int(0)), mk_eq(stoi2(0), digit(0)));
add_axiom(mk_le(len, 0), mk_eq(stoi2(0), digit(0)));
add_axiom(~ge0, is_digit(mk_nth(s, 0)));
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))));
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)));
}
}
@ -619,6 +624,32 @@ void seq_axioms::add_itos_axiom(expr* s, unsigned k) {
}
}
literal seq_axioms::is_digit(expr* ch) {
ensure_digit_axiom();
literal isd = mk_literal(m_sk.mk_is_digit(ch));
expr_ref d2i = m_sk.mk_digit2int(ch);
expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m);
expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m);
literal lo = mk_literal(_lo);
literal hi = mk_literal(_hi);
add_axiom(~lo, ~hi, isd);
add_axiom(~isd, lo);
add_axiom(~isd, hi);
return isd;
}
void seq_axioms::ensure_digit_axiom() {
if (!m_digits_initialized) {
for (unsigned i = 0; i < 10; ++i) {
expr_ref cnst(seq.mk_char('0'+i), m);
add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
}
ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
m_digits_initialized = true;
}
}
/**
e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or
c < d e1 < e2 => prefix(e1, e2) or e2 = xdz e1 < e2 => e1 != e2
@ -711,30 +742,6 @@ void seq_axioms::add_prefix_axiom(expr* e) {
add_axiom(lit, e1_gt_e2, ~mk_eq(c, d));
}
literal seq_axioms::is_digit(expr* ch) {
literal isd = mk_literal(m_sk.mk_is_digit(ch));
expr_ref d2i = m_sk.mk_digit2int(ch);
expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m);
expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m);
literal lo = mk_literal(_lo);
literal hi = mk_literal(_hi);
add_axiom(~lo, ~hi, isd);
add_axiom(~isd, lo);
add_axiom(~isd, hi);
return isd;
}
void seq_axioms::ensure_digit_axiom() {
if (!m_digits_initialized) {
for (unsigned i = 0; i < 10; ++i) {
expr_ref cnst(seq.mk_char('0'+i), m);
add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
}
ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
m_digits_initialized = true;
}
}
expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
expr_ref bound_tracker = m_sk.mk_length_limit(s, k);

2
src/smt/seq_axioms.h
View file

@ -46,7 +46,7 @@ namespace smt {
expr_ref mk_sub(expr* x, expr* y);
expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(seq.str.mk_concat(e1, e2, e3), m); }
expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); }
expr_ref mk_nth(expr* e, expr* i) { return expr_ref(seq.str.mk_nth_i(e, i), m); }
expr_ref mk_nth(expr* e, unsigned i) { return expr_ref(seq.str.mk_nth_i(e, a.mk_int(i)), m); }
literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); }
literal mk_le(expr* e, int k) { return mk_le_e(e, a.mk_int(k)); }
literal mk_ge(expr* e, rational const& k) { return mk_ge_e(e, a.mk_int(k)); }

1
src/smt/smt_internalizer.cpp
View file

@ -197,6 +197,7 @@ namespace smt {
for (auto & kv : sorted_exprs) {
expr* e = kv.first;
if (!is_app(e) ||
!m.is_bool(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m.get_basic_family_id())
internalize_rec(e, kv.second);