mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #5096 fix #5099

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-15 09:43:34 -07:00
parent 18143d8932
commit d62f6c62b5
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/seq_axioms.cpp
View file

@ -693,7 +693,8 @@ namespace seq {
/** /**
stoi(s) >= -1 stoi(s) >= -1
stoi("") = -1 stoi("") = -1
stoi(s) >= 0 => is_digit(nth(s,0)) stoi(s) >= 0 => is_digit(nth(s,0))
stoi(s) >= 0 => len(s) >= 1
*/ */
void axioms::stoi_axiom(expr* e) { void axioms::stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";); TRACE("seq", tout << mk_pp(e, m) << "\n";);
@ -701,8 +702,10 @@ namespace seq {
expr* s = nullptr; expr* s = nullptr;
VERIFY (seq.str.is_stoi(e, s)); VERIFY (seq.str.is_stoi(e, s));
add_clause(mk_ge(e, -1)); // stoi(s) >= -1 add_clause(mk_ge(e, -1)); // stoi(s) >= -1
add_clause(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1 add_clause(mk_eq(seq.str.mk_stoi(seq.str.mk_empty(s->get_sort())), a.mk_int(-1)));
// add_clause(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1))); // s = "" => stoi(s) = -1
add_clause(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0)) add_clause(~ge0, is_digit(mk_nth(s, 0))); // stoi(s) >= 0 => is_digit(nth(s,0))
add_clause(~ge0, mk_ge(mk_len(s), 1)); // stoi(s) >= 0 => len(s) >= 1
} }