mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-12 01:56:22 +00:00
Code Activity

Regex factorization needs special care when resuming after finding a sat node in-between

Browse source
This commit is contained in:
CEisenhofer 2026-07-01 19:29:29 +02:00
parent b7ef51ca04
commit d1b0cbee34
2 changed files with 22 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2329,7 +2329,7 @@ namespace seq {
// differs), so it would alias the parent's signature, yet it still has
// pending splits to explore — it is not a true recurrence.
{
if (!node->rf_cont() && m_unsat_node_cache.contains(node)) {
if (!node->is_rf_cont() && m_unsat_node_cache.contains(node)) {
node->set_conflict(backtrack_reason::sibling, nullptr /*we use the one of the sibling*/);
node->set_general_conflict();
node->m_unsat_cacheable = true;
@ -2429,12 +2429,17 @@ namespace seq {
// with string-only conflicts and self-contained cuts (see the epilogue).
// -------------------------------------------------------------------
node->canonize_and_compute_final_node_hash();
// A lazy-factorization continuation node (rf_cont set) is EXEMPT from the
// A lazy-factorization continuation node (is_rf_cont) is EXEMPT from the
// loop-cut: it aliases its parent's string signature (only the suspended
// split iterator differs) but is not a true recurrence — it still has
// pending splits. The iterator is finite, so the continuation chain
// terminates on its own (exhaustion → regex conflict).
if (!node->rf_cont()) {
// terminates on its own (exhaustion → regex conflict). The exemption uses
// the STICKY is_rf_cont() marker, not the live rf_cont() pointer: the
// pointer is nulled once the node is extended, but on a hot-restart the
// node is re-traversed without re-extending, and it must stay exempt (else
// it is wrongly cut as a sibling of the ancestor it aliases, pruning a
// branch that may still lead to SAT).
if (!node->is_rf_cont()) {
auto it = m_siblings.find(node);
if (it != m_siblings.end() && !it->second.empty()) {
nielsen_node* anc = it->second.back(); // deepest sibling still on the path

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

@ -600,6 +600,14 @@ namespace seq {
// split iterator so factorization resumes from the next split when this
// node is extended. Owned by nielsen_graph::m_rf_states (raw pointer here).
rf_state* m_rf_cont = nullptr;
// Sticky marker: true once this node was ever created as a factorization
// continuation (child B), even after its iterator has been consumed
// (m_rf_cont reset to null when the node is extended). The subsumption
// loop-cut and unsat-cache exemptions (§1.6b) are a PERMANENT structural
// property of a continuation node — it aliases its parent's string
// signature yet is not a recurrence — so they must survive the hot-restart
// re-traversal, where m_rf_cont is already null. See search_dfs.
bool m_is_rf_cont = false;
// number of constraints inherited from the parent node at clone time.
// constraints[0..m_parent_ic_count) are already asserted at the
// parent's solver scope; only [m_parent_ic_count..end) need to be
@ -657,7 +665,11 @@ namespace seq {
// lazy regex factorization continuation (see m_rf_cont).
rf_state* rf_cont() const { return m_rf_cont; }
void set_rf_cont(rf_state* s) { m_rf_cont = s; }
void set_rf_cont(rf_state* s) { m_rf_cont = s; if (s) m_is_rf_cont = true; }
// Sticky: true if this node was ever a factorization continuation, even
// after its iterator has been consumed. Drives the loop-cut / unsat-cache
// exemptions so they persist across the hot-restart re-traversal.
bool is_rf_cont() const { return m_is_rf_cont; }
// returns 0 if hash is unknown
unsigned hash() const {