From 18ba14cff81be7a846cdc793f7d012e3a86fdfab Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 7 Sep 2019 09:35:20 -0400 Subject: [PATCH] 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 --- src/smt/theory_str.cpp | 76 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 65 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 37c5b6237..aa0ee2167 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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);