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

z3str3: construct correct counterexamples for string-integer in model construction (#4562)

Browse source
This commit is contained in:
Murphy Berzish 2020-07-27 14:15:41 -05:00 committed by GitHub
parent d591bf62c1
commit 2fb914d2a2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_str_mc.cpp
View file

@ -1135,10 +1135,18 @@ namespace smt {
precondition.push_back(m.mk_eq(e, mk_int(ival))); precondition.push_back(m.mk_eq(e, mk_int(ival)));
// Assert (arg == arg_chars) in the subsolver. // Assert (arg == arg_chars) in the subsolver.
if (!fixed_length_reduce_eq(subsolver, arg, arg_char_expr, stoi_cex)) { if (!fixed_length_reduce_eq(subsolver, arg, arg_char_expr, stoi_cex)) {
// Counterexample: (str.to_int S) == ival AND len(S) == slen cannot both be true.
stoi_cex = expr_ref(m.mk_not(m.mk_and(
m.mk_eq(e, mk_int(ival)),
m.mk_eq(mk_strlen(arg), mk_int(slen))
)), m);
assert_axiom(stoi_cex); assert_axiom(stoi_cex);
add_persisted_axiom(stoi_cex); add_persisted_axiom(stoi_cex);
return l_undef; return l_undef;
} }
fixed_length_reduced_boolean_formulas.push_back(m.mk_eq(e, mk_int(ival)));
} }
} else { } else {
TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(e, get_manager()) << std::endl;); TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(e, get_manager()) << std::endl;);
@ -1172,10 +1180,16 @@ namespace smt {
expr_ref _e(e, m); expr_ref _e(e, m);
expr_ref arg_char_expr(mk_string(ival_str), m); expr_ref arg_char_expr(mk_string(ival_str), m);
if (!fixed_length_reduce_eq(subsolver, _e, arg_char_expr, itos_cex)) { if (!fixed_length_reduce_eq(subsolver, _e, arg_char_expr, itos_cex)) {
// Counterexample: N in (str.from_int N) == ival AND len(str.from_int N) == slen cannot both be true.
itos_cex = expr_ref(m.mk_not(m.mk_and(
m.mk_eq(arg, mk_int(ival)),
m.mk_eq(mk_strlen(e), mk_int(slen))
)), m);
assert_axiom(itos_cex); assert_axiom(itos_cex);
add_persisted_axiom(itos_cex); add_persisted_axiom(itos_cex);
return l_undef; return l_undef;
} }
fixed_length_reduced_boolean_formulas.push_back(m.mk_eq(arg, mk_int(ival)));
} else { } else {
TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(arg, get_manager()) << std::endl;); TRACE("str_fl", tout << "integer theory has no assignment for " << mk_pp(arg, get_manager()) << std::endl;);
// consistency needs to be checked after the string is assigned // consistency needs to be checked after the string is assigned