diff --git a/src/smt/theory_str_noodler/expr_cases.cpp b/src/smt/theory_str_noodler/expr_cases.cpp index 4f835e2505f..3739c1b610d 100644 --- a/src/smt/theory_str_noodler/expr_cases.cpp +++ b/src/smt/theory_str_noodler/expr_cases.cpp @@ -33,4 +33,32 @@ bool is_contains_index(expr* e, expr*& ind, ast_manager& m, seq_util& m_util_s, return false; } +bool is_replace_indexof(expr* rpl_str, expr* rpl_find, ast_manager& m, seq_util& m_util_s, arith_util& m_util_a, expr*& ind) { + expr* sub_str = nullptr, *sub_start = nullptr, *sub_len = nullptr; + + if(m_util_s.str.is_extract(rpl_str, sub_str, sub_start, sub_len)) { + expr*ind_str = nullptr, *ind_find = nullptr, *ind_start = nullptr, *add = nullptr; + rational one(1); + if(m_util_a.is_zero(sub_start) && m_util_a.is_add(sub_len, add, ind) && m_util_a.is_numeral(add, one) && m_util_s.str.is_index(ind, ind_str, ind_find, ind_start) && one.get_int32() == 1) { + if(ind_find->hash() != rpl_find->hash() || sub_str->hash() != ind_str->hash() || !m_util_a.is_zero(ind_start)) { + return false; + } + return true; + } + } + return false; +} + +bool is_indexof_add(expr* e, expr* index_str, ast_manager& m, seq_util& m_util_s, arith_util& m_util_a, expr*& val, expr*& ind_find) { + expr * ind = nullptr, *ind_str = nullptr, *ind_start = nullptr; + if(m_util_a.is_add(e, val, ind) && m_util_s.str.is_index(ind, ind_str, ind_find, ind_start)) { + if(ind_str->hash() != index_str->hash()) { + return false; + } + return true; + } + return false; +} + + } \ No newline at end of file diff --git a/src/smt/theory_str_noodler/expr_cases.h b/src/smt/theory_str_noodler/expr_cases.h index bbd589bcd6d..08b31c7e267 100644 --- a/src/smt/theory_str_noodler/expr_cases.h +++ b/src/smt/theory_str_noodler/expr_cases.h @@ -42,5 +42,35 @@ namespace smt::noodler::expr_cases { */ bool is_contains_index(expr* e, expr*& ind, ast_manager& m, seq_util& m_util_s, arith_util& m_util_a); +/** + * @brief Check if the given constraint @p rpl_str is of the form + * (str.substr s 0 (1 + str.indexof s ( @p rpl_find ) 0)) + * + * @param rpl_str Constraint of the replace + * @param rpl_find Replace find + * @param m Ast manager + * @param m_util_s string ast util + * @param m_util_a arith ast util + * @param[out] ind Extracted (str.indexof s ( @p rpl_find ) 0) + * @return true <-> if of the particular form. + */ +bool is_replace_indexof(expr* rpl_str, expr* rpl_find, ast_manager& m, seq_util& m_util_s, arith_util& m_util_a, expr*& ind); + +/** + * @brief Check if the given contraint @p e is of the form + * (( @p val ) + (str.indexof ( @p index_str ) ( @p ind_find ) n ) + * + * @param e Constraint to be checked + * @param index_str Required index of parameter + * @param m Ast manager + * @param m_util_s string ast util + * @param m_util_a arith ast util + * @param[out] val Extracted addition value + * @param[out] ind_find Extracted indexof find + * @return true <-> if of the particular form. + */ +bool is_indexof_add(expr* e, expr* index_str, ast_manager& m, seq_util& m_util_s, arith_util& m_util_a, expr*& val, expr*& ind_find); + + } #endif diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 25400e5a027..c01dd8104c0 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1132,6 +1132,26 @@ namespace smt::noodler { literal li_ge_ls = mk_literal(m_util_a.mk_ge(ls_minus_i_l, zero)); literal l_ge_zero = mk_literal(m_util_a.mk_ge(l, zero)); literal ls_le_0 = mk_literal(m_util_a.mk_le(ls, zero)); + + expr* num_val, *ind_val; + rational num_val_rat; + if(r.is_zero() && expr_cases::is_indexof_add(l, s, m, m_util_s, m_util_a, num_val, ind_val) && m_util_a.is_numeral(num_val, num_val_rat) && num_val_rat.is_one()) { + literal l_gt_zero = mk_literal(m_util_a.mk_le(l, zero)); + expr_ref v = mk_str_var_fresh("substr"); + expr_ref sub(m_util_a.mk_add(l, m_util_a.mk_int(-1)), m); + m_rewrite(sub); + expr_ref substr(m_util_s.str.mk_substr(s, i, sub), m); + expr_ref conc = mk_concat(substr, ind_val); + string_theory_propagation(conc); + + add_axiom({l_gt_zero, mk_eq(e, conc, false)}); + add_axiom({mk_eq(v, e, false)}); + + // add the replacement substr -> v + this->predicate_replace.insert(e, v.get()); + util::get_str_variables(s, this->m_util_s, m, this->len_vars); + return; + } expr_ref x(m_util_s.str.mk_string(""), m); expr_ref v = mk_str_var_fresh("substr"); @@ -1147,11 +1167,12 @@ namespace smt::noodler { expr_ref le(m_util_s.str.mk_length(v), m); expr_ref y = mk_str_var_fresh("post_substr"); - expr_ref xe(m_util_s.str.mk_concat(x, v), m); - expr_ref xey(m_util_s.str.mk_concat(x, v, y), m); rational rl; expr * num_len; + expr_ref xe(m_util_s.str.mk_concat(x, v), m); + expr_ref xey(m_util_s.str.mk_concat(x, v, y), m); + if(m_util_a.is_numeral(l, rl)) { int lval = rl.get_int32(); expr_ref substr_re(m); @@ -1172,6 +1193,24 @@ namespace smt::noodler { } else if(util::is_len_sub(l, s, m, m_util_s, m_util_a, num_len) && m_util_a.is_numeral(num_len, rl) && rl == r) { xe = expr_ref(m_util_s.str.mk_concat(x, v), m); xey = expr_ref(m_util_s.str.mk_concat(x, v), m); + } else if(m_util_a.is_zero(i) && util::is_len_sub(l, s, m, m_util_s, m_util_a, num_len) && m_util_a.is_numeral(num_len, rl) && rl.is_minus_one()) { + expr_ref substr_re(m_util_s.re.mk_full_char(nullptr), m); + expr_ref substr_in(m_util_s.re.mk_in_re(y, substr_re), m); + expr_ref ly(m_util_s.str.mk_length(y), m); + + literal l_ge_zero = mk_literal(m_util_a.mk_ge(l, zero)); + string_theory_propagation(xey); + add_axiom({~l_ge_zero, mk_literal(substr_in)}); + add_axiom({~l_ge_zero, mk_eq(ly, m_util_a.mk_int(1), false)}); + add_axiom({~l_ge_zero, mk_eq(xey, s, false)}); + add_axiom({~l_ge_zero, mk_eq(le, l, false)}); + add_axiom({l_ge_zero, mk_eq(v, eps, false)}); + add_axiom({mk_eq(v, e, false)}); + this->predicate_replace.insert(e, v.get()); + // update length variables + util::get_str_variables(s, this->m_util_s, m, this->len_vars); + this->var_eqs.add(expr_ref(l, m), v); + return; } else { // 0 <= i <= |s| && 0 <= l <= |s| - i -> |v| = l add_axiom({~i_ge_0, ~ls_le_i, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false)}); @@ -1322,7 +1361,6 @@ namespace smt::noodler { expr_ref lx(m_util_s.str.mk_length(x), m); expr_ref le(m_util_s.str.mk_length(v), m); expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m); - expr_ref zero(m_util_a.mk_int(0), m); expr_ref eps(m_util_s.str.mk_string(""), m); @@ -1398,6 +1436,7 @@ namespace smt::noodler { context& ctx = get_context(); expr* a = nullptr, *s = nullptr, *t = nullptr; VERIFY(m_util_s.str.is_replace(r, a, s, t)); + expr_ref v = mk_str_var_fresh("replace"); expr_ref x = mk_str_var_fresh("replace_left"); expr_ref y = mk_str_var_fresh("replace_right"); @@ -1412,6 +1451,25 @@ namespace smt::noodler { // s = eps -> |v| = |a| + |t| add_axiom({~s_emp, mk_literal(m.mk_eq(m_util_s.str.mk_length(v), m_util_a.mk_add(m_util_s.str.mk_length(a), m_util_s.str.mk_length(t))))}); + expr* indexof = nullptr; + if(expr_cases::is_replace_indexof(a, s, m, m_util_s, m_util_a, indexof)) { + expr_ref minus_one(m_util_a.mk_int(-1), m); + expr_ref v = mk_str_var_fresh("replace"); + expr_ref eps(m_util_s.str.mk_string(""), m); + literal ind_eq_m1 = mk_eq(indexof, minus_one, false); + expr_ref len_a_m1(m_util_a.mk_sub(m_util_s.str.mk_length(a), m_util_a.mk_int(1)), m); + expr_ref substr(m_util_s.str.mk_substr(a, m_util_a.mk_int(0), len_a_m1), m); + + + // s = eps -> v = t.a + add_axiom({~s_emp, mk_eq(v, mk_concat(t, a),false)}); + add_axiom({ind_eq_m1, mk_eq(v, mk_concat(substr, t),false)}); + add_axiom({~ind_eq_m1, mk_eq(v, eps, false)}); + add_axiom({mk_eq(v, r, false)}); + predicate_replace.insert(r, v.get()); + return; + } + zstring str_a, str_b; // str.replace "A" s t where a = "A" if(m_util_s.str.is_string(a, str_a) && str_a.length() == 1) {