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

z3str3: fixes to str.indexof when axiomatizing constant expressions

Browse source
This commit is contained in:
Murphy Berzish 2019-10-21 20:45:43 -04:00 committed by Nikolaj Bjorner
parent 0acbdffacf
commit 76b3198282
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_str.cpp
View file

@ -1335,6 +1335,23 @@ namespace smt {
return; return;
} }
SASSERT(ex->get_num_args() == 3); SASSERT(ex->get_num_args() == 3);
{
// Attempt to rewrite to an integer constant. If this succeeds,
// assert equality with that constant.
// The rewriter normally takes care of this for terms that are in scope
// at the beginning of the search.
// We perform the check here to catch terms that are added during the search.
expr_ref rwex(ex, m);
rw(rwex);
if (m_autil.is_numeral(rwex)) {
TRACE("str", tout << "constant expression " << mk_pp(ex, m) << " simplifies to " << mk_pp(rwex, m) << std::endl;);
assert_axiom(ctx.mk_eq_atom(ex, rwex));
axiomatized_terms.insert(ex);
return;
}
}
// if the third argument is exactly the integer 0, we can use this "simple" indexof; // if the third argument is exactly the integer 0, we can use this "simple" indexof;
// otherwise, we call the "extended" version // otherwise, we call the "extended" version
expr * startingPosition = ex->get_arg(2); expr * startingPosition = ex->get_arg(2);
@ -1516,6 +1533,7 @@ namespace smt {
{ {
expr_ref premise(m.mk_not(u.str.mk_contains(H, N)), m); expr_ref premise(m.mk_not(u.str.mk_contains(H, N)), m);
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
rw(premise);
assert_implication(premise, conclusion); assert_implication(premise, conclusion);
} }
// case 4: 0 < i < len(H), N non-empty, and H contains N // case 4: 0 < i < len(H), N non-empty, and H contains N