mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

handle undefined constant cases for int.to.str

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-13 17:13:10 -07:00
parent 893bcbb585
commit ead704f52f
2 changed files with 23 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1082,9 +1082,19 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
if (m_util.str.is_string(a, str)) {
std::string s = str.encode();
for (unsigned i = 0; i < s.length(); ++i) {
if (s[i] == '-') { if (i != 0) return BR_FAILED; }
else if ('0' <= s[i] && s[i] <= '9') continue;
return BR_FAILED;
if (s[i] == '-') {
if (i != 0) {
result = m_autil.mk_int(-1);
return BR_DONE;
}
}
else if ('0' <= s[i] && s[i] <= '9') {
continue;
}
else {
result = m_autil.mk_int(-1);
return BR_DONE;
}
}
rational r(s.c_str());
result = m_autil.mk_numeral(r, true);

12
src/smt/theory_seq.cpp
View file

@ -520,7 +520,7 @@ bool theory_seq::branch_variable_mb() {
break;
}
}
TRACE("seq", tout << "branch_variable_mb\n";);
CTRACE("seq", change, tout << "branch_variable_mb\n";);
return change;
}
@ -2348,7 +2348,14 @@ bool theory_seq::add_stoi_axiom(expr* e) {
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) {
if (!get_num_value(e, val)) {
literal l = mk_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
TRACE("seq", tout << l << " " << ctx.get_assignment(l) << "\n";
ctx.display(tout););
return true;
}
if (!m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
if (!val.is_minus_one()) {
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
@ -3467,6 +3474,7 @@ bool theory_seq::get_num_value(expr* e, rational& val) const {
next = next->get_next();
}
while (next != n);
TRACE("seq", tout << "no value for " << mk_pp(e, m) << "\n";);
return false;
}