diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 8567c6b30..9dfd0475b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -641,7 +641,6 @@ namespace smt { } app * theory_str::mk_indexof(expr * haystack, expr * needle) { - // TODO check meaning of the third argument here app * indexof = u.str.mk_index(haystack, needle, mk_int(0)); m_trail.push_back(indexof); // immediately force internalization so that axiom setup does not fail @@ -844,14 +843,7 @@ namespace smt { instantiate_axiom_Contains(e); } else if (u.str.is_index(a)) { instantiate_axiom_Indexof(e); - /* TODO NEXT: Indexof2/Lastindexof rewrite? - } else if (is_Indexof2(e)) { - instantiate_axiom_Indexof2(e); - } else if (is_LastIndexof(e)) { - instantiate_axiom_LastIndexof(e); - */ } else if (u.str.is_extract(a)) { - // TODO check semantics of substr vs. extract instantiate_axiom_Substr(e); } else if (u.str.is_replace(a)) { instantiate_axiom_Replace(e); @@ -1232,27 +1224,37 @@ namespace smt { context & ctx = get_context(); ast_manager & m = get_manager(); - app * expr = e->get_owner(); - if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;); + app * ex = e->get_owner(); + if (axiomatized_terms.contains(ex)) { + TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;); return; } - axiomatized_terms.insert(expr); + SASSERT(ex->get_num_args() == 3); + // if the third argument is exactly the integer 0, we can use this "simple" indexof; + // otherwise, we call the "extended" version + expr * startingPosition = ex->get_arg(2); + rational startingInteger; + if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) { + // "extended" indexof term with prefix + instantiate_axiom_Indexof_extended(e); + return; + } + axiomatized_terms.insert(ex); - TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;); + 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(expr->get_arg(0), expr->get_arg(1)), m); + expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m); SASSERT(condAst); // ----------------------- // true branch expr_ref_vector thenItems(m); // args[0] = x1 . args[1] . x2 - thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2)))); + thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2)))); // indexAst = |x1| thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1))); // args[0] = x3 . x4 @@ -1260,11 +1262,11 @@ namespace smt { // /\ ! contains(x3, args[1]) expr_ref x3(mk_str_var("x3"), m); expr_ref x4(mk_str_var("x4"), m); - expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m); + expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m); SASSERT(tmpLen); - thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4))); + thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4))); thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen)); - thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1)))); + thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1)))); expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m); SASSERT(thenBranch); @@ -1276,26 +1278,42 @@ namespace smt { expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m); SASSERT(breakdownAssert); - expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m); + expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m); SASSERT(reduceToIndex); 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_Indexof2(enode * e) { + void theory_str::instantiate_axiom_Indexof_extended(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); return; } + SASSERT(expr->get_num_args() == 3); axiomatized_terms.insert(expr); - TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); // ------------------------------------------------------------------------------- // if (arg[2] >= length(arg[0])) // ite2 @@ -1327,7 +1345,7 @@ namespace smt { ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1)))); ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen)); ite2ElseItems.push_back(ite3); - expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m); + expr_ref ite2Else(mk_and(ite2ElseItems), m); SASSERT(ite2Else); expr_ref ite2(m.mk_ite( @@ -1350,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) { @@ -8731,8 +8763,8 @@ namespace smt { context & ctx = get_context(); ast_manager & m = get_manager(); - expr_ref_vector assignments(m); - ctx.get_assignments(assignments); + //expr_ref_vector assignments(m); + //ctx.get_assignments(assignments); if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = false; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 3b71a2282..9288bac7c 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -447,7 +447,7 @@ protected: void instantiate_axiom_suffixof(enode * e); void instantiate_axiom_Contains(enode * e); void instantiate_axiom_Indexof(enode * e); - void instantiate_axiom_Indexof2(enode * e); + void instantiate_axiom_Indexof_extended(enode * e); void instantiate_axiom_LastIndexof(enode * e); void instantiate_axiom_Substr(enode * e); void instantiate_axiom_Replace(enode * e);