mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fix #2257, remove unsound length constraints for str.to.int because leading digits can be 0

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-27 15:51:23 -07:00
parent 9cb1a0f094
commit bd46c52f95
1 changed files with 1 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_seq.cpp
View file

@ -3576,7 +3576,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
// n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
// 10^k <= n < 10^{k+1}-1 => len(e) = k
// 10^k <= n < 10^{k+1}-1 => len(e) => k
void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
context& ctx = get_context();
@ -3618,15 +3618,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
rational ub = power(rational(10), k) - 1;
arith_util& a = m_autil;
literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb)));
literal ubl = mk_literal(a.mk_le(n, a.mk_int(ub)));
literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k)));
literal le_k = mk_literal(a.mk_le(len, a.mk_int(k)));
// n >= lb => len(s) >= k
// n >= 0 & len(s) >= k => n >= lb
// 0 <= n <= ub => len(s) <= k
add_axiom(~lbl, ge_k);
add_axiom(~ge0, lbl, ~ge_k);
add_axiom(~ge0, ~ubl, le_k);
}