From d55af419554ec7c36d1c9cf93d79cc3b6c2479ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Nov 2018 19:54:34 -0800 Subject: [PATCH] constrain lengths Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 194da2913..9b79786fd 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3514,13 +3514,15 @@ void theory_seq::add_itos_axiom(expr* e) { // n >= 0 & len(e) = k => 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 void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { context& ctx = get_context(); zstring s; expr_ref ith_char(m), num(m), coeff(m); expr_ref_vector nums(m), chars(m); - literal len_eq_k = mk_preferred_eq(m_util.str.mk_length(e), m_autil.mk_int(k)); + expr_ref len(m_util.str.mk_length(e), m); + literal len_eq_k = mk_preferred_eq(len, m_autil.mk_int(k)); literal ge0 = mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))); literal_vector digits; digits.push_back(~len_eq_k); @@ -3545,6 +3547,21 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { add_axiom(~len_eq_k, ~ge0, mk_preferred_eq(n, num)); add_axiom(~len_eq_k, ~ge0, mk_preferred_eq(e, m_util.str.mk_concat(chars))); + + SASSERT(k > 0); + rational lb = power(rational(10), k - 1); + rational ub = power(rational(10), k) - 1; + arith_util a (m); + 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); } @@ -3570,6 +3587,7 @@ bool theory_seq::add_itos_val_axiom(expr* e) { return true; } + return false; }