mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-07 03:35:47 +00:00
Code Activity

Fix seq nth/indexof interaction timeout (issue #3508)

Browse source 
Add a lazy bridging check between nth(s,idx) and indexof(s,unit(c),0)
terms that already coexist over the same base sequence s:

  0 <= idx & idx < len(s) & nth(s,idx) = c => indexof(s,unit(c),0) <= idx

Unlike the previous (reverted) attempt, this does not add a bridging
axiom eagerly whenever nth/at/extract axioms fire. Instead:
- add_nth_term/add_indexof_term record existing nth_i and single-char
  indexof(...,0) terms (via relevant_eh) without creating any new terms.
- check_nth_indexof(), invoked from final_check_eh (mirroring the
  check_contains pattern), only adds the bridging clause when both a
  matching nth term and indexof term already exist over sequences with
  the same root enode, and the nth value is already known-equal to the
  indexof's search character. An obj_pair_hashtable cache prevents
  duplicate instantiation across backtracking.

This targets the actual root cause identified via a minimized repro
(nth and indexof co-occurring over the same sequence, which previously
required expensive case-split/segmentation reasoning to connect) while
avoiding the axiom-instantiation blowup that caused CI regressions in
the previous eager approach.

Verified: minimized repro and full issue #3508 script now solve
instantly (previously timed out); full unit test suite (99/99) and
the z3test regression benchmark suite pass with no failures or
timeouts.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-27 02:39:33 -07:00
parent 329a20e836
commit ff452c0470
2 changed files with 99 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

87
src/smt/theory_seq.cpp
View file

@ -265,6 +265,8 @@ theory_seq::theory_seq(context& ctx):
m_ubv_string(m),
m_length(m),
m_length_limit(m),
m_nth_terms(m),
m_indexof_terms(m),
m_mg(nullptr),
m_rewrite(m),
m_str_rewrite(m),
@ -374,6 +376,10 @@ final_check_status theory_seq::final_check_eh(unsigned level) {
TRACEFIN("propagate_contains");
return FC_CONTINUE;
}
if (check_nth_indexof()) {
TRACEFIN("check_nth_indexof");
return FC_CONTINUE;
}
if (check_int_string()) {
++m_stats.m_int_string;
TRACEFIN("int_string");
@ -673,6 +679,82 @@ bool theory_seq::check_contains() {
return m_new_propagation || ctx.inconsistent();
}
void theory_seq::add_nth_term(expr* n) {
m_nth_terms.push_back(n);
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_nth_terms));
}
void theory_seq::add_indexof_term(expr* n) {
expr* t = nullptr, *s = nullptr, *offset = nullptr;
if (!m_util.str.is_index(n, t, s, offset))
return;
// only handle indexof(t, unit(c), 0) shaped terms - searching for a single character from the start.
if (!m_util.str.is_unit(s))
return;
rational r;
if (!m_autil.is_numeral(offset, r) || !r.is_zero())
return;
m_indexof_terms.push_back(n);
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_indexof_terms));
}
/**
Lazily bridge nth(s,idx) and indexof(s,unit(c),0) terms that already coexist
over the same base sequence s, without creating any new nth/indexof terms:
0 <= idx & idx < len(s) & nth(s,idx) = c => indexof(s,unit(c),0) <= idx
This captures: if s contains c at position idx (a valid index), then the first
occurrence of c in s is at or before idx.
*/
bool theory_seq::check_nth_indexof() {
struct remove_nth_indexof_map : public trail {
ast_manager& m;
obj_pair_hashtable<expr, expr>& m_map;
expr* a, *b;
remove_nth_indexof_map(ast_manager& m, obj_pair_hashtable<expr, expr>& map, expr* a, expr* b):
m(m), m_map(map), a(a), b(b) {}
void undo() override {
m_map.erase(std::make_pair(a, b));
m.dec_ref(a);
m.dec_ref(b);
}
};
bool change = false;
for (expr* nth : m_nth_terms) {
expr* s = nullptr, *idx = nullptr;
if (!m_util.str.is_nth_i(nth, s, idx))
continue;
for (expr* idxof : m_indexof_terms) {
expr* t = nullptr, *unit_c = nullptr, *offset = nullptr;
VERIFY(m_util.str.is_index(idxof, t, unit_c, offset));
if (!ctx.e_internalized(s) || !ctx.e_internalized(t))
continue;
if (ctx.get_enode(s)->get_root() != ctx.get_enode(t)->get_root())
continue;
auto key = std::make_pair(nth, idxof);
if (m_nth_indexof_cache.contains(key))
continue;
expr* c = nullptr;
VERIFY(m_util.str.is_unit(unit_c, c));
expr_ref unit_nth(m_util.str.mk_unit(nth), m);
literal nth_eq_c = mk_eq(unit_nth, unit_c, false);
if (ctx.get_assignment(nth_eq_c) != l_true)
continue;
m.inc_ref(nth);
m.inc_ref(idxof);
m_nth_indexof_cache.insert(key);
get_trail_stack().push(remove_nth_indexof_map(m, m_nth_indexof_cache, nth, idxof));
literal idx_ge_0 = m_ax.mk_ge(idx, 0);
literal idx_lt_len_s = ~m_ax.mk_ge(mk_sub(idx, mk_len(s)), 0);
literal idxof_le_idx = m_ax.mk_ge(mk_sub(idx, idxof), 0);
add_axiom(~idx_ge_0, ~idx_lt_len_s, ~nth_eq_c, idxof_le_idx);
change = true;
}
}
return change;
}
bool theory_seq::check_lts() {
if (m_lts.empty() || m_lts_checked) {
return false;
@ -3452,6 +3534,11 @@ void theory_seq::relevant_eh(expr* _n) {
enque_axiom(n);
}
if (m_util.str.is_nth_i(n))
add_nth_term(n);
if (m_util.str.is_index(n))
add_indexof_term(n);
if (m_util.str.is_itos(n) ||
m_util.str.is_stoi(n)) {
add_int_string(n);

12
src/smt/theory_seq.h
View file

@ -465,6 +465,18 @@ namespace smt {
bool check_extensionality(expr* e1, enode* n1, enode* n2);
bool check_contains();
bool check_lts();
// bridge nth(s,idx) = c and indexof(s, unit(c), 0) terms that already
// coexist over the same base sequence s: if 0 <= idx < len(s) and
// nth(s,idx) is known-equal to c, then indexof(s,unit(c),0) <= idx.
// This is only checked lazily, over terms that already exist, so it
// never creates new nth/indexof terms (avoiding eager instantiation blowup).
expr_ref_vector m_nth_terms; // is_nth_i(s, idx) terms seen so far
expr_ref_vector m_indexof_terms; // is_index(t, u, offset) terms (offset absent or 0) seen so far
obj_pair_hashtable<expr, expr> m_nth_indexof_cache; // (nth term, indexof term) pairs already bridged
void add_nth_term(expr* n);
void add_indexof_term(expr* n);
bool check_nth_indexof();
dependency* m_eq_deps { nullptr };
bool solve_eqs(unsigned start);
bool solve_eq(unsigned idx);