mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Mitigate #5763 sequence indexof performance regression

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-28 23:35:53 +00:00 • committed by GitHub
parent 886a82bf18
commit ecb76032aa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 41 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_axioms.cpp
View file

@ -443,6 +443,8 @@ namespace seq {
expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort()));
expr_ref t_eq_empty = mk_eq_empty(t);
add_clause(mk_ge(i, -1));
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
// ~contains(t,s) => indexof(t,s,offset) = -1

4
src/smt/seq_eq_solver.cpp
View file

@ -189,7 +189,9 @@ bool theory_seq::len_based_split(depeq const& e) {
expr_ref_vector const& rs = e.rs;
int offset = 0;
if (!has_len_offset(ls, rs, offset))
// Splitting on equal-length heads (offset = 0) can cause large amounts
// of redundant branching on indexof-heavy problems.
if (!has_len_offset(ls, rs, offset) || offset == 0)
return false;
TRACE(seq, tout << "split based on length\n";);

36
src/test/simplifier.cpp
View file

@ -232,6 +232,41 @@ static void test_sat_smt_ufbv_predicate_model_validation() {
Z3_del_context(ctx);
}
static void test_issue_5763() {
Z3_context ctx = Z3_mk_context(nullptr);
const char* s_result =
Z3_eval_smtlib2_string(ctx,
"(set-logic QF_SLIA)\n"
"(declare-const db_select_s_str_1 String)\n"
"(assert (let ((a!1 (not (<= (str.indexof (str.substr db_select_s_str_1 7 19)\n"
" \" where \"\n"
" 0)\n"
" 0))))\n"
"(let ((a!2 (or a!1\n"
" (= 0\n"
" (str.indexof (str.substr db_select_s_str_1 7 19) \" where \" 0)))))\n"
" (and (= 0 (str.indexof db_select_s_str_1 \"select \" 0))\n"
" (<= 0 (str.indexof (str.substr db_select_s_str_1 7 19) \" from \" 0))\n"
" (not a!2)\n"
" (= (str.substr (str.substr db_select_s_str_1 7 19) 10 9) \"inventory\")))))\n"
"(check-sat)\n");
ENSURE(std::strstr(s_result, "sat") != nullptr);
const char* bv_result =
Z3_eval_smtlib2_string(ctx,
"(declare-const my_fn_a_int_1 Int)\n"
"(declare-const my_fn_b_int_2 Int)\n"
"(assert (let ((a!1 (bvnot (bvor (bvnot ((_ int2bv 64) my_fn_a_int_1))\n"
" (bvnot ((_ int2bv 64) my_fn_b_int_2))))))\n"
"(let ((a!2 (bvor (bvnot (bvor ((_ int2bv 64) my_fn_a_int_1)\n"
" ((_ int2bv 64) my_fn_b_int_2)))\n"
" a!1)))\n"
" (not (= 0 (bv2int (bvnot a!2)))))))\n"
"(check-sat)\n");
ENSURE(std::strstr(bv_result, "sat") != nullptr);
Z3_del_context(ctx);
}
void tst_simplifier() {
test_array();
@ -240,4 +275,5 @@ void tst_simplifier() {
test_bool();
test_skolemize_bug();
test_sat_smt_ufbv_predicate_model_validation();
test_issue_5763();
}