diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index c4f2e634e..8dc02cc09 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -176,6 +176,28 @@ br_status str_rewriter::mk_str_LastIndexof(expr * haystack, expr * needle, expr_ } } +br_status str_rewriter::mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (Replace " << mk_pp(base, m()) << " " << mk_pp(source, m()) << " " << mk_pp(target, m()) << ")" << std::endl;); + if (m_strutil.is_string(base) && m_strutil.is_string(source) && m_strutil.is_string(target)) { + std::string arg0Str = m_strutil.get_string_constant_value(base); + std::string arg1Str = m_strutil.get_string_constant_value(source); + std::string arg2Str = m_strutil.get_string_constant_value(target); + if (arg0Str.find(arg1Str) != std::string::npos) { + int index1 = arg0Str.find(arg1Str); + int index2 = index1 + arg1Str.length(); + std::string substr0 = arg0Str.substr(0, index1); + std::string substr2 = arg0Str.substr(index2); + std::string replaced = substr0 + arg2Str + substr2; + result = m_strutil.mk_string(replaced); + } else { + result = base; + } + return BR_DONE; + } else { + return BR_FAILED; + } +} + br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); @@ -204,6 +226,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_LASTINDEXOF: SASSERT(num_args == 2); return mk_str_LastIndexof(args[0], args[1], result); + case OP_STR_REPLACE: + SASSERT(num_args == 3); + return mk_str_Replace(args[0], args[1], args[2], result); default: return BR_FAILED; } diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index de399acba..69a7c9579 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -47,6 +47,7 @@ public: br_status mk_str_Indexof(expr * haystack, expr * needle, expr_ref & result); br_status mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, expr_ref & result); br_status mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result); + br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result); bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change); bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 7bd4ec154..526b02f64 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -34,6 +34,7 @@ str_decl_plugin::str_decl_plugin(): m_indexof2_decl(0), m_lastindexof_decl(0), m_substr_decl(0), + m_replace_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -55,6 +56,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_indexof2_decl); DEC_REF(m_lastindexof_decl); DEC_REF(m_substr_decl); + DEC_REF(m_replace_decl); DEC_REF(m_int_sort); } @@ -114,6 +116,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_substr_decl = m->mk_func_decl(symbol("Substring"), 3, d, s, func_decl_info(id, OP_STR_SUBSTR)); m_manager->inc_ref(m_substr_decl); } + + { + sort * d[3] = {s, s, s}; + m_replace_decl = m->mk_func_decl(symbol("Replace"), 3, d, s, func_decl_info(id, OP_STR_REPLACE)); + m_manager->inc_ref(m_replace_decl); + } } decl_plugin * str_decl_plugin::mk_fresh() { @@ -139,6 +147,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_INDEXOF2: return m_indexof2_decl; case OP_STR_LASTINDEXOF: return m_lastindexof_decl; case OP_STR_SUBSTR: return m_substr_decl; + case OP_STR_REPLACE: return m_replace_decl; default: return 0; } } @@ -203,6 +212,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("Indexof2", OP_STR_INDEXOF2)); op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF)); op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR)); + op_names.push_back(builtin_name("Replace", OP_STR_REPLACE)); } void str_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index bd2a70a1e..ee2432c50 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -39,6 +39,7 @@ enum str_op_kind { OP_STR_INDEXOF2, OP_STR_LASTINDEXOF, OP_STR_SUBSTR, + OP_STR_REPLACE, // end LAST_STR_OP }; @@ -59,6 +60,7 @@ protected: func_decl * m_indexof2_decl; func_decl * m_lastindexof_decl; func_decl * m_substr_decl; + func_decl * m_replace_decl; arith_decl_plugin * m_arith_plugin; family_id m_arith_fid; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4f04ede23..1e2107f11 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -612,7 +612,7 @@ bool theory_str::can_propagate() { return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty() || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty() || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty() - || !m_axiom_Substr_todo.empty() + || !m_axiom_Substr_todo.empty() || !m_axiom_Replace_todo.empty() ; } @@ -676,6 +676,11 @@ void theory_str::propagate() { instantiate_axiom_Substr(m_axiom_Substr_todo[i]); } m_axiom_Substr_todo.reset(); + + for (unsigned i = 0; i < m_axiom_Replace_todo.size(); ++i) { + instantiate_axiom_Replace(m_axiom_Replace_todo[i]); + } + m_axiom_Replace_todo.reset(); } } @@ -1192,6 +1197,56 @@ void theory_str::instantiate_axiom_Substr(enode * e) { assert_axiom(finalAxiom); } +void theory_str::instantiate_axiom_Replace(enode * e) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + app * expr = e->get_owner(); + if (axiomatized_terms.contains(expr)) { + TRACE("t_str_detail", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;); + return; + } + axiomatized_terms.insert(expr); + + TRACE("t_str_detail", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;); + + expr_ref x1(mk_str_var("x1"), m); + expr_ref x2(mk_str_var("x2"), m); + expr_ref i1(mk_int_var("i1"), m); + expr_ref result(mk_str_var("result"), m); + + // condAst = Contains(args[0], args[1]) + expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m); + // ----------------------- + // 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)))); + // i1 = |x1| + thenItems.push_back(ctx.mk_eq_atom(i1, mk_strlen(x1))); + // args[0] = x3 . x4 /\ |x3| = |x1| + |args[1]| - 1 /\ ! 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(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m); + thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4))); + thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen)); + thenItems.push_back(m.mk_not(mk_contains(x3, expr->get_arg(1)))); + thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2)))); + // ----------------------- + // false branch + expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m); + + expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m); + SASSERT(breakdownAssert); + + expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m); + SASSERT(reduceToResult); + + expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m); + SASSERT(finalAxiom); + assert_axiom(finalAxiom); +} + void theory_str::attach_new_th_var(enode * n) { context & ctx = get_context(); theory_var v = mk_var(n); @@ -3928,6 +3983,10 @@ void theory_str::set_up_axioms(expr * ex) { } } else if (is_CharAt(ap)) { m_axiom_CharAt_todo.push_back(n); + } else if (is_Substr(ap)) { + m_axiom_Substr_todo.push_back(n); + } else if (is_Replace(ap)) { + m_axiom_Replace_todo.push_back(n); } else if (ap->get_num_args() == 0 && !is_string(ap)) { // if ex is a variable, add it to our list of variables TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); @@ -3942,18 +4001,24 @@ void theory_str::set_up_axioms(expr * ex) { TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort Bool" << std::endl;); // set up axioms for boolean terms - enode * n = ctx.get_enode(ex); - SASSERT(n); - if (is_app(ex)) { - app * ap = to_app(ex); - if (is_StartsWith(ap)) { - m_axiom_StartsWith_todo.push_back(n); - } else if (is_EndsWith(ap)) { - m_axiom_EndsWith_todo.push_back(n); - } else if (is_Contains(ap)) { - m_axiom_Contains_todo.push_back(n); + if (ctx.e_internalized(ex)) { + enode * n = ctx.get_enode(ex); + SASSERT(n); + + if (is_app(ex)) { + app * ap = to_app(ex); + if (is_StartsWith(ap)) { + m_axiom_StartsWith_todo.push_back(n); + } else if (is_EndsWith(ap)) { + m_axiom_EndsWith_todo.push_back(n); + } else if (is_Contains(ap)) { + m_axiom_Contains_todo.push_back(n); + } } + } else { + TRACE("t_str_detail", tout << "WARNING: Bool term " << mk_ismt2_pp(ex, get_manager()) << " not internalized. Skipping to prevent a crash." << std::endl;); + return; } } else if (ex_sort == int_sort) { TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 35a6fe91b..7ee1d4281 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -116,6 +116,7 @@ namespace smt { ptr_vector m_axiom_Indexof2_todo; ptr_vector m_axiom_LastIndexof_todo; ptr_vector m_axiom_Substr_todo; + ptr_vector m_axiom_Replace_todo; // hashtable of all exprs for which we've already set up term-specific axioms -- // this prevents infinite recursive descent with respect to axioms that @@ -202,6 +203,8 @@ namespace smt { bool is_LastIndexof(enode const * n) const { return is_LastIndexof(n->get_owner()); } bool is_Substr(app const * a) const { return a->is_app_of(get_id(), OP_STR_SUBSTR); } bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); } + bool is_Replace(app const * a) const { return a->is_app_of(get_id(), OP_STR_REPLACE); } + bool is_Replace(enode const * n) const { return is_Replace(n->get_owner()); } void instantiate_concat_axiom(enode * cat); void instantiate_basic_string_axioms(enode * str); @@ -215,6 +218,7 @@ namespace smt { void instantiate_axiom_Indexof2(enode * e); void instantiate_axiom_LastIndexof(enode * e); void instantiate_axiom_Substr(enode * e); + void instantiate_axiom_Replace(enode * e); void set_up_axioms(expr * ex); void handle_equality(expr * lhs, expr * rhs);