mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-12 10:06:23 +00:00
Code Activity

Skip factorization in case we already eliminated some cycle

Browse source
This commit is contained in:
CEisenhofer 2026-07-01 19:05:38 +02:00
parent 706f62286e
commit b7ef51ca04
3 changed files with 32 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/seq/seq_nielsen.cpp
View file

@ -4115,6 +4115,17 @@ namespace seq {
return false;
}
bool nielsen_graph::mem_has_cycle_token(str_mem const& mem) const {
static const symbol cycle_sym("cycle");
SASSERT(mem.m_str);
for (euf::snode const* t : mem.m_str->collect_tokens()) {
expr* const e = t->get_expr();
if (e && m_sk.is_skolem(cycle_sym, e))
return true;
}
return false;
}
rf_state* nielsen_graph::mk_rf_state(nielsen_node* /*node*/, str_mem const& mem) {
euf::snode const* const first = mem.m_str->first();
SASSERT(first);
@ -4251,6 +4262,10 @@ namespace seq {
if (m_regex_factorization_threshold == 0)
return false;
for (str_mem const& mem : node->str_mems())
if (mem.is_view() || mem.is_guard() || mem_has_cycle_token(mem))
return false;
// Continuation: resume the iterator handed down to this node by its
// parent's "remaining splits" branch.
if (rf_state* st = node->rf_cont()) {
@ -4292,6 +4307,12 @@ namespace seq {
if (leading_var_guarded(node, mem.m_str->first()))
continue;
// Defer when the membership mentions a cycle stabilizer token: the
// cycle machinery owns it, and factorizing it re-expands the cycle
// structure indefinitely (see mem_has_cycle_token).
if (mem_has_cycle_token(mem))
continue;
rf_state* st = mk_rf_state(node, mem);
if (!st)
continue; // unsupported regex shape → try the next membership
@ -5077,16 +5098,11 @@ namespace seq {
// not true anymore since we might have done a hot-restart where we previously created the child:
//SASSERT(n->outgoing().empty());
SASSERT(n->is_currently_conflict());
if (n->m_conflict_external_literal != sat::null_literal) {
std::cout << "Node " << n->id() << std::endl;
if (n->m_conflict_external_literal != sat::null_literal)
// We know from the outer solver that this literal is assigned true and contradicts node constraint
deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
}
if (n->m_conflict_internal) {
std::cout << "Node " << n->id() << std::endl;
if (n->m_conflict_internal)
deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
}
}
return deps;
}

8
src/smt/seq/seq_nielsen.h
View file

@ -1399,6 +1399,14 @@ namespace seq {
// disjunction is refuted → the continuation node is a regex conflict.
bool apply_regex_factorization(nielsen_node* node);
// True if the membership's string mentions a `cycle` stabilizer token
// (the (cycle x R) Skolem minted by apply_cycle_decomposition). Such a
// membership is owned by the cycle machinery; factorization must defer to
// it — re-splitting it re-expands the very structure the cycle rule is
// trying to close, and the fresh slice variables each cycle step mints
// defeat the exact-structural loop-cut → non-termination.
bool mem_has_cycle_token(str_mem const& mem) const;
// Build a suspended factorization (boundary head/tail + split iterator)
// for `mem`. Returns null if the regex shape is unsupported (the engine
// cannot even start a split). Allocated into m_rf_states.

1
src/smt/theory_nseq.cpp
View file

@ -1005,6 +1005,7 @@ namespace smt {
m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager);
m_nielsen.set_regex_dynamic_decomposition(get_fparams().m_nseq_regex_dynamic_decomposition);
m_nielsen.set_harvest(get_fparams().m_nseq_harvest);
m_nielsen.set_harvest_dir(get_fparams().m_nseq_harvest_dir.str());