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

integrate contains and indexof in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2018-03-08 12:37:44 -05:00
parent d1407e843d
commit bf6975122b
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_str.cpp
View file

@ -1284,6 +1284,21 @@ namespace smt {
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
{
// heuristic: integrate with str.contains information
// (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 zeroAst(mk_int(0), m);
// (H contains N) <==> (H indexof N, i) >= 0
expr_ref premise(u.str.mk_contains(haystack, needle), m);
ctx.internalize(premise, false);
expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
SASSERT(containsAxiom);
// we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
m_delayed_axiom_setup_terms.push_back(containsAxiom);
}
}
void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
@ -1353,6 +1368,20 @@ namespace smt {
expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
SASSERT(reduceTerm);
assert_axiom(reduceTerm);
{
// heuristic: integrate with str.contains information
// (but don't introduce it if it isn't already in the instance)
expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
// (H contains N) <==> (H indexof N, i) >= 0
expr_ref premise(u.str.mk_contains(haystack, needle), m);
ctx.internalize(premise, false);
expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
SASSERT(containsAxiom);
// we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
m_delayed_axiom_setup_terms.push_back(containsAxiom);
}
}
void theory_str::instantiate_axiom_LastIndexof(enode * e) {