From a39d5404038b5402b8f366b0c3a164138c5d781c Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 11 Jan 2024 17:07:27 +0100 Subject: [PATCH 1/7] replace: inst of axioms, substr: len(s) axioms --- .../theory_str_noodler/decision_procedure.cpp | 3 +- src/smt/theory_str_noodler/expr_cases.cpp | 16 ++++++++++ src/smt/theory_str_noodler/expr_cases.h | 3 ++ .../theory_str_noodler/theory_str_noodler.cpp | 31 +++++++++++++++++++ 4 files changed, 52 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str_noodler/decision_procedure.cpp b/src/smt/theory_str_noodler/decision_procedure.cpp index e76e5ad634b..9975e78be8c 100644 --- a/src/smt/theory_str_noodler/decision_procedure.cpp +++ b/src/smt/theory_str_noodler/decision_procedure.cpp @@ -839,7 +839,8 @@ namespace smt::noodler { prep_handler.remove_regular(); prep_handler.skip_len_sat(); } - prep_handler.reduce_regular_sequence(1); + // TODO: remove + // prep_handler.reduce_regular_sequence(1); prep_handler.remove_regular(); // Refresh the instance diff --git a/src/smt/theory_str_noodler/expr_cases.cpp b/src/smt/theory_str_noodler/expr_cases.cpp index 4f835e2505f..2eac37205ac 100644 --- a/src/smt/theory_str_noodler/expr_cases.cpp +++ b/src/smt/theory_str_noodler/expr_cases.cpp @@ -33,4 +33,20 @@ 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)) { + 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; +} + } \ 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..9b2cbb14380 100644 --- a/src/smt/theory_str_noodler/expr_cases.h +++ b/src/smt/theory_str_noodler/expr_cases.h @@ -42,5 +42,8 @@ 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); + +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); + } #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..8589b0ed21f 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1172,6 +1172,20 @@ 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); + + literal l_gt_zero = mk_literal(m_util_a.mk_gt(l, zero)); + + string_theory_propagation(xey); + add_axiom({~l_gt_zero, mk_literal(substr_in)}); + add_axiom({~l_gt_zero, mk_eq(xey, s, false)}); + add_axiom({l_gt_zero, mk_eq(v, eps, false)}); + this->predicate_replace.insert(e, v.get()); + // update length variables + util::get_str_variables(s, this->m_util_s, m, this->len_vars); + 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)}); @@ -1398,6 +1412,23 @@ 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* 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); + + 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; + } + 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"); From 08de180a636bc4de588d4a9b12568694fb29caa6 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 12 Jan 2024 08:47:24 +0100 Subject: [PATCH 2/7] preprocess: reverting changes; substr: axioms fixing --- src/smt/theory_str_noodler/decision_procedure.cpp | 3 +-- src/smt/theory_str_noodler/theory_str_noodler.cpp | 11 ++++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_str_noodler/decision_procedure.cpp b/src/smt/theory_str_noodler/decision_procedure.cpp index 9975e78be8c..e76e5ad634b 100644 --- a/src/smt/theory_str_noodler/decision_procedure.cpp +++ b/src/smt/theory_str_noodler/decision_procedure.cpp @@ -839,8 +839,7 @@ namespace smt::noodler { prep_handler.remove_regular(); prep_handler.skip_len_sat(); } - // TODO: remove - // prep_handler.reduce_regular_sequence(1); + prep_handler.reduce_regular_sequence(1); prep_handler.remove_regular(); // Refresh the instance diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 8589b0ed21f..8749f4815a2 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1176,12 +1176,13 @@ namespace smt::noodler { 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); - literal l_gt_zero = mk_literal(m_util_a.mk_gt(l, zero)); - + literal l_ge_zero = mk_literal(m_util_a.mk_ge(l, zero)); string_theory_propagation(xey); - add_axiom({~l_gt_zero, mk_literal(substr_in)}); - add_axiom({~l_gt_zero, mk_eq(xey, s, false)}); - add_axiom({l_gt_zero, mk_eq(v, eps, false)}); + add_axiom({~l_ge_zero, mk_literal(substr_in)}); + 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); From fca4582767468d90b4697f9e28c0f00e12a893ff Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 13 Jan 2024 00:12:00 +0100 Subject: [PATCH 3/7] replace, substr: strenghtening axioms --- .../theory_str_noodler/theory_str_noodler.cpp | 34 +++++++++++-------- 1 file changed, 20 insertions(+), 14 deletions(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 8749f4815a2..c554368c831 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1175,10 +1175,12 @@ namespace smt::noodler { } 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)}); @@ -1186,6 +1188,7 @@ namespace smt::noodler { 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 @@ -1414,6 +1417,20 @@ namespace smt::noodler { 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"); + expr_ref xty = mk_concat(x, mk_concat(t, y)); + expr_ref xsy = mk_concat(x, mk_concat(s, y)); + expr_ref eps(m_util_s.str.mk_string(""), m); + literal a_emp = mk_eq_empty(a); + literal s_emp = mk_eq_empty(s); + + // if s = t -> the result is unchanged + add_axiom({~mk_eq(s, t, false), mk_eq(v, a,false)}); + // 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); @@ -1423,6 +1440,9 @@ namespace smt::noodler { 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)}); @@ -1430,20 +1450,6 @@ namespace smt::noodler { return; } - 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"); - expr_ref xty = mk_concat(x, mk_concat(t, y)); - expr_ref xsy = mk_concat(x, mk_concat(s, y)); - expr_ref eps(m_util_s.str.mk_string(""), m); - literal a_emp = mk_eq_empty(a); - literal s_emp = mk_eq_empty(s); - - // if s = t -> the result is unchanged - add_axiom({~mk_eq(s, t, false), mk_eq(v, a,false)}); - // 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))))}); - 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) { From 0f9ce768590ddc8981cb20e00df6aa4ea1b5842a Mon Sep 17 00:00:00 2001 From: vhavlena Date: Sat, 13 Jan 2024 17:11:13 +0100 Subject: [PATCH 4/7] substr: turn off --- src/smt/theory_str_noodler/theory_str_noodler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index c554368c831..126d33f43fb 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1172,7 +1172,7 @@ 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()) { + } else if(false && 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); From b816ba11164f03e0a871aefea79f678b05343baa Mon Sep 17 00:00:00 2001 From: vhavlena Date: Mon, 15 Jan 2024 19:52:34 +0100 Subject: [PATCH 5/7] substr: special case --- src/smt/theory_str_noodler/expr_cases.cpp | 12 ++++++ src/smt/theory_str_noodler/expr_cases.h | 4 ++ .../theory_str_noodler/theory_str_noodler.cpp | 38 +++++++++++++++++-- 3 files changed, 50 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str_noodler/expr_cases.cpp b/src/smt/theory_str_noodler/expr_cases.cpp index 2eac37205ac..060538e62b7 100644 --- a/src/smt/theory_str_noodler/expr_cases.cpp +++ b/src/smt/theory_str_noodler/expr_cases.cpp @@ -49,4 +49,16 @@ bool is_replace_indexof(expr* rpl_str, expr* rpl_find, ast_manager& m, seq_util& 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 9b2cbb14380..e595c6b6a58 100644 --- a/src/smt/theory_str_noodler/expr_cases.h +++ b/src/smt/theory_str_noodler/expr_cases.h @@ -45,5 +45,9 @@ bool is_contains_index(expr* e, expr*& ind, ast_manager& m, seq_util& m_util_s, 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); + +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 126d33f43fb..0e3d33e3475 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1127,11 +1127,35 @@ namespace smt::noodler { expr_ref zero(m_util_a.mk_int(0), m); expr_ref eps(m_util_s.str.mk_string(""), m); + // expr_ref iplusl(m_util_a.mk_add(l, i), m); + // m_rewrite(iplusl); + // literal nopost = mk_literal(m_util_a.mk_ge(m_util_a.mk_sub(iplusl, ls), zero)); + literal i_ge_0 = mk_literal(m_util_a.mk_ge(i, zero)); literal ls_le_i = mk_literal(m_util_a.mk_le(mk_sub(i, ls), zero)); 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.get_int32() == 0 && 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.get_int32() == 1) { + 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 +1171,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,7 +1197,7 @@ 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(false && 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()) { + } 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); @@ -1215,6 +1240,8 @@ namespace smt::noodler { // substr(s, i, n) = v add_axiom({mk_eq(v, e, false)}); + // add_axiom({~nopost, mk_eq(y, eps, false)}); + // add the replacement substr -> v this->predicate_replace.insert(e, v.get()); // update length variables @@ -1340,10 +1367,11 @@ 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); + // expr_ref iplusl(m_util_a.mk_add(i, l), m); + // literal nopost = mk_literal(m_util_a.mk_ge(m_util_a.mk_sub(iplusl, ls), zero)); literal i_ge_0 = mk_literal(m_util_a.mk_ge(i, zero)); literal ls_le_i = mk_literal(m_util_a.mk_le(mk_sub(i, ls), zero)); literal li_ge_ls = mk_literal(m_util_a.mk_ge(ls_minus_i_l, zero)); @@ -1379,6 +1407,8 @@ namespace smt::noodler { // substr(s, i, n) = v add_axiom({mk_eq(v, e, false)}); + // add_axiom({~nopost, mk_eq(y, eps, false)}); + // add the replacement substr -> v this->predicate_replace.insert(e, v.get()); // update length variables From 8de5f2c8a4a9675d589a8a0998413e6544712b65 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Tue, 16 Jan 2024 12:59:03 +0100 Subject: [PATCH 6/7] cleaning; comments; mimor fix --- src/smt/theory_str_noodler/expr_cases.cpp | 2 +- src/smt/theory_str_noodler/expr_cases.h | 27 +++++++++++++++++-- .../theory_str_noodler/theory_str_noodler.cpp | 10 ------- 3 files changed, 26 insertions(+), 13 deletions(-) diff --git a/src/smt/theory_str_noodler/expr_cases.cpp b/src/smt/theory_str_noodler/expr_cases.cpp index 060538e62b7..3739c1b610d 100644 --- a/src/smt/theory_str_noodler/expr_cases.cpp +++ b/src/smt/theory_str_noodler/expr_cases.cpp @@ -39,7 +39,7 @@ bool is_replace_indexof(expr* rpl_str, expr* rpl_find, ast_manager& m, seq_util& 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)) { + 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; } diff --git a/src/smt/theory_str_noodler/expr_cases.h b/src/smt/theory_str_noodler/expr_cases.h index e595c6b6a58..08b31c7e267 100644 --- a/src/smt/theory_str_noodler/expr_cases.h +++ b/src/smt/theory_str_noodler/expr_cases.h @@ -42,10 +42,33 @@ 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); diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 0e3d33e3475..3b979d4a24d 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1127,10 +1127,6 @@ namespace smt::noodler { expr_ref zero(m_util_a.mk_int(0), m); expr_ref eps(m_util_s.str.mk_string(""), m); - // expr_ref iplusl(m_util_a.mk_add(l, i), m); - // m_rewrite(iplusl); - // literal nopost = mk_literal(m_util_a.mk_ge(m_util_a.mk_sub(iplusl, ls), zero)); - literal i_ge_0 = mk_literal(m_util_a.mk_ge(i, zero)); literal ls_le_i = mk_literal(m_util_a.mk_le(mk_sub(i, ls), zero)); literal li_ge_ls = mk_literal(m_util_a.mk_ge(ls_minus_i_l, zero)); @@ -1240,8 +1236,6 @@ namespace smt::noodler { // substr(s, i, n) = v add_axiom({mk_eq(v, e, false)}); - // add_axiom({~nopost, mk_eq(y, eps, false)}); - // add the replacement substr -> v this->predicate_replace.insert(e, v.get()); // update length variables @@ -1370,8 +1364,6 @@ namespace smt::noodler { expr_ref zero(m_util_a.mk_int(0), m); expr_ref eps(m_util_s.str.mk_string(""), m); - // expr_ref iplusl(m_util_a.mk_add(i, l), m); - // literal nopost = mk_literal(m_util_a.mk_ge(m_util_a.mk_sub(iplusl, ls), zero)); literal i_ge_0 = mk_literal(m_util_a.mk_ge(i, zero)); literal ls_le_i = mk_literal(m_util_a.mk_le(mk_sub(i, ls), zero)); literal li_ge_ls = mk_literal(m_util_a.mk_ge(ls_minus_i_l, zero)); @@ -1407,8 +1399,6 @@ namespace smt::noodler { // substr(s, i, n) = v add_axiom({mk_eq(v, e, false)}); - // add_axiom({~nopost, mk_eq(y, eps, false)}); - // add the replacement substr -> v this->predicate_replace.insert(e, v.get()); // update length variables From 3550de0297424671b403d34f58b5200af9d6b635 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Tue, 23 Jan 2024 19:50:22 +0100 Subject: [PATCH 7/7] minor --- src/smt/theory_str_noodler/theory_str_noodler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 3b979d4a24d..c01dd8104c0 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -1135,7 +1135,7 @@ namespace smt::noodler { expr* num_val, *ind_val; rational num_val_rat; - if(r.get_int32() == 0 && 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.get_int32() == 1) { + 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);