mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Z3str3: fix empty-string contradictions (#2538)
* z3str3: str.indexof second argument can be empty string without causing contradictions * z3str3: str.indexof second argument can be empty string without causing contradictions * z3str3: fixups for str.indexof * z3str3: str.indexof code cleanup
This commit is contained in:
Murphy Berzish
Nikolaj Bjorner
parent
bc723fbe89
commit
18ba14cff8
|
|
@ -1326,6 +1326,7 @@ namespace smt {
|
|||
|
||||
void theory_str::instantiate_axiom_Indexof(enode * e) {
|
||||
context & ctx = get_context();
|
||||
th_rewriter & rw = ctx.get_rewriter();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
app * ex = e->get_owner();
|
||||
|
|
@ -1345,13 +1346,21 @@ namespace smt {
|
|||
}
|
||||
axiomatized_terms.insert(ex);
|
||||
|
||||
expr * exHaystack = nullptr;
|
||||
expr * exNeedle = nullptr;
|
||||
expr * exIndex = nullptr;
|
||||
u.str.is_index(ex, exHaystack, exNeedle, exIndex);
|
||||
|
||||
TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
|
||||
|
||||
expr_ref x1(mk_str_var("x1"), m);
|
||||
expr_ref x2(mk_str_var("x2"), m);
|
||||
expr_ref indexAst(mk_int_var("index"), m);
|
||||
|
||||
expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
|
||||
expr_ref condAst1(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
|
||||
expr_ref condAst2(m.mk_not(ctx.mk_eq_atom(exNeedle, mk_string(""))), m);
|
||||
expr_ref condAst(m.mk_and(condAst1, condAst2), m);
|
||||
//expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
|
||||
SASSERT(condAst);
|
||||
|
||||
// -----------------------
|
||||
|
|
@ -1376,7 +1385,11 @@ namespace smt {
|
|||
|
||||
// -----------------------
|
||||
// false branch
|
||||
expr_ref elseBranch(ctx.mk_eq_atom(indexAst, mk_int(-1)), m);
|
||||
expr_ref elseBranch(m.mk_ite(
|
||||
ctx.mk_eq_atom(exNeedle, mk_string("")),
|
||||
ctx.mk_eq_atom(indexAst, mk_int(0)),
|
||||
ctx.mk_eq_atom(indexAst, mk_int(-1))
|
||||
), m);
|
||||
SASSERT(elseBranch);
|
||||
|
||||
expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m);
|
||||
|
|
@ -1386,7 +1399,7 @@ namespace smt {
|
|||
SASSERT(reduceToIndex);
|
||||
|
||||
expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
|
||||
SASSERT(finalAxiom);
|
||||
rw(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
|
||||
{
|
||||
|
|
@ -1408,6 +1421,7 @@ namespace smt {
|
|||
|
||||
void theory_str::instantiate_axiom_Indexof_extended(enode * _e) {
|
||||
context & ctx = get_context();
|
||||
th_rewriter & rw = ctx.get_rewriter();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
app * e = _e->get_owner();
|
||||
|
|
@ -1436,6 +1450,7 @@ namespace smt {
|
|||
|
||||
expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m);
|
||||
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
|
||||
expr_ref empty_string(mk_string(""), m);
|
||||
|
||||
// case split
|
||||
|
||||
|
|
@ -1446,9 +1461,40 @@ namespace smt {
|
|||
assert_implication(premise, conclusion);
|
||||
}
|
||||
|
||||
// case 1.1: N == "" and i out of range
|
||||
{
|
||||
expr_ref premiseNEmpty(ctx.mk_eq_atom(N, empty_string), m);
|
||||
// range check
|
||||
expr_ref premiseRangeLower(m_autil.mk_le(i, minus_one), m);
|
||||
expr_ref premiseRangeUpper(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m);
|
||||
expr_ref premiseRange(m.mk_or(premiseRangeLower, premiseRangeUpper), m);
|
||||
expr_ref premise(m.mk_and(premiseNEmpty, premiseRange), m);
|
||||
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
|
||||
expr_ref finalAxiom(rewrite_implication(premise, conclusion), m);
|
||||
rw(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
||||
// case 1.2: N == "" and i within range
|
||||
{
|
||||
expr_ref premiseNEmpty(ctx.mk_eq_atom(N, empty_string), m);
|
||||
// range check
|
||||
expr_ref premiseRangeLower(m_autil.mk_le(i, minus_one), m);
|
||||
expr_ref premiseRangeUpper(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m);
|
||||
expr_ref premiseRange(m.mk_not(m.mk_or(premiseRangeLower, premiseRangeUpper)), m);
|
||||
expr_ref premise(m.mk_and(premiseNEmpty, premiseRange), m);
|
||||
expr_ref conclusion(ctx.mk_eq_atom(e, i), m);
|
||||
expr_ref finalAxiom(rewrite_implication(premise, conclusion), m);
|
||||
rw(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
||||
// case 2: i = 0
|
||||
{
|
||||
expr_ref premise(ctx.mk_eq_atom(i, zero), m);
|
||||
expr_ref premise1(ctx.mk_eq_atom(i, zero), m);
|
||||
expr_ref premise2(m.mk_not(ctx.mk_eq_atom(N, empty_string)), m);
|
||||
expr_ref premise(m.mk_and(premise1, premise2), m);
|
||||
rw(premise);
|
||||
// reduction to simpler case
|
||||
expr_ref conclusion(ctx.mk_eq_atom(e, mk_indexof(H, N)), m);
|
||||
assert_implication(premise, conclusion);
|
||||
|
|
@ -1459,7 +1505,10 @@ namespace smt {
|
|||
//expr_ref premise(_premise);
|
||||
//th_rewriter rw(m);
|
||||
//rw(premise);
|
||||
expr_ref premise(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m);
|
||||
expr_ref premise1(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m);
|
||||
expr_ref premise2(m.mk_not(ctx.mk_eq_atom(N, empty_string)), m);
|
||||
expr_ref premise(m.mk_and(premise1, premise2), m);
|
||||
rw(premise);
|
||||
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
|
||||
assert_implication(premise, conclusion);
|
||||
}
|
||||
|
|
@ -1469,15 +1518,21 @@ namespace smt {
|
|||
expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
|
||||
assert_implication(premise, conclusion);
|
||||
}
|
||||
// case 4: 0 < i < len(H) and H contains N
|
||||
// case 4: 0 < i < len(H), N non-empty, and H contains N
|
||||
{
|
||||
expr_ref premise1(m_autil.mk_gt(i, zero), m);
|
||||
//expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
|
||||
expr_ref premise2(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 premise3(u.str.mk_contains(H, N), m);
|
||||
expr_ref _premise(m.mk_and(premise1, premise2, premise3), m);
|
||||
expr_ref premise4(m.mk_not(ctx.mk_eq_atom(N, mk_string(""))), m);
|
||||
|
||||
expr_ref_vector premises(m);
|
||||
premises.push_back(premise1);
|
||||
premises.push_back(premise2);
|
||||
premises.push_back(premise3);
|
||||
premises.push_back(premise4);
|
||||
expr_ref _premise(mk_and(premises), m);
|
||||
expr_ref premise(_premise);
|
||||
th_rewriter rw(m);
|
||||
rw(premise);
|
||||
|
||||
expr_ref hd(mk_str_var("hd"), m);
|
||||
|
|
@ -1500,9 +1555,8 @@ namespace smt {
|
|||
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);
|
||||
expr_ref precondition3(m.mk_not(ctx.mk_eq_atom(N, mk_string(""))), m);
|
||||
expr_ref precondition(m.mk_and(precondition1, precondition2, precondition3), m);
|
||||
rw(precondition);
|
||||
|
||||
expr_ref premise(u.str.mk_contains(H, N), m);
|
||||
|
|
|
|||
Loading…
Reference in a new issue