mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

strengthening length properties for int.to.str. Issue #589

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-15 12:27:04 -07:00
parent 99314b7252
commit 10cdd527ca
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_seq.cpp
View file

@ -2823,6 +2823,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
- len(unit(u)) = 1 if x = unit(u) - len(unit(u)) = 1 if x = unit(u)
- len(str) = str.length() if x = str - len(str) = str.length() if x = str
- len(empty) = 0 if x = empty - len(empty) = 0 if x = empty
- len(int.to.str(i)) >= 1 if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
- len(x) >= 0 otherwise - len(x) >= 0 otherwise
*/ */
void theory_seq::add_length_axiom(expr* n) { void theory_seq::add_length_axiom(expr* n) {
@ -2837,16 +2838,17 @@ void theory_seq::add_length_axiom(expr* n) {
m_rewrite(len); m_rewrite(len);
SASSERT(n != len); SASSERT(n != len);
add_axiom(mk_eq(len, n, false)); add_axiom(mk_eq(len, n, false));
if (!ctx.at_base_level()) { }
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n))); else if (m_util.str.is_itos(x)) {
} add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(1))));
} }
else { else {
add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0)))); add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
}
} }
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
}
} }