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

constrain lengths

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-23 19:54:34 -08:00
parent 88fb826a03
commit d55af41955
1 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/smt/theory_seq.cpp
View file

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