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

z3str3: fix contains-indexof precondition

Browse source
This commit is contained in:
Murphy Berzish 2018-08-07 15:12:37 -04:00
parent 7a84486df2
commit c65dbaea90
1 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_str.cpp
View file

@ -1388,7 +1388,7 @@ namespace smt {
// (but don't introduce it if it isn't already in the instance) // (but don't introduce it if it isn't already in the instance)
expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m); expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m);
expr_ref zeroAst(mk_int(0), m); expr_ref zeroAst(mk_int(0), m);
// (H contains N) <==> (H indexof N, i) >= 0 // (H contains N) <==> (H indexof N, 0) >= 0
expr_ref premise(u.str.mk_contains(haystack, needle), m); expr_ref premise(u.str.mk_contains(haystack, needle), m);
ctx.internalize(premise, false); ctx.internalize(premise, false);
expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m); expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
@ -1482,14 +1482,23 @@ namespace smt {
{ {
// heuristic: integrate with str.contains information // heuristic: integrate with str.contains information
// (but don't introduce it if it isn't already in the instance) // (but don't introduce it if it isn't already in the instance)
// (H contains N) <==> (H indexof N, i) >= 0 // (0 <= i < len(H)) ==> (H contains N) <==> (H indexof N, i) >= 0
expr_ref precondition1(m_autil.mk_gt(i, minus_one), m);
//expr_ref precondition2(m_autil.mk_lt(i, mk_strlen(H)), m);
expr_ref precondition2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m);
expr_ref _precondition(m.mk_and(precondition1, precondition2), m);
expr_ref precondition(_precondition);
th_rewriter rw(m);
rw(precondition);
expr_ref premise(u.str.mk_contains(H, N), m); expr_ref premise(u.str.mk_contains(H, N), m);
ctx.internalize(premise, false); ctx.internalize(premise, false);
expr_ref conclusion(m_autil.mk_ge(e, zero), m); expr_ref conclusion(m_autil.mk_ge(e, zero), m);
expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
SASSERT(containsAxiom); expr_ref finalAxiom(rewrite_implication(precondition, containsAxiom), m);
SASSERT(finalAxiom);
// we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
m_delayed_assertions_todo.push_back(containsAxiom); m_delayed_assertions_todo.push_back(finalAxiom);
} }
} }