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

Fixed some partial automaton soundness problems

Browse source
This commit is contained in:
CEisenhofer 2026-07-02 18:58:17 +02:00
parent 195a0486aa
commit e8884faa23
6 changed files with 539 additions and 251 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/compare_seq_solvers.py
View file

@ -37,9 +37,9 @@ COMMON_ARGS = ["model_validate=true"]
# All three configurations are always run.
SOLVERS = {
"nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
"smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true"],
"smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true", "smt.nseq.regex_dynamic_decomposition=false"],
"nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
"smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false"],
"smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=true"],
"seq": ["smt.string_solver=seq"],
}

31
src/ast/rewriter/seq_split.cpp
View file

@ -223,7 +223,7 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul
split_set acc;
push(acc, oracle, r.mk_complement(sp[0].m_d), full);
push(acc, oracle, full, r.mk_complement(sp[0].m_n));
for (unsigned i = 1; i < sp.size(); ++i) {
for (unsigned i = 1; i < sp.size(); i++) {
split_set next;
push(next, oracle, r.mk_complement(sp[i].m_d), full);
push(next, oracle, full, r.mk_complement(sp[i].m_n));
@ -300,7 +300,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
}
}
expr_ref acc = mk_empty();
for (unsigned i = 0; i <= str.length(); ++i) {
for (unsigned i = 0; i <= str.length(); i++) {
const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), m);
const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), m);
acc = mk_union(acc, mk_single(p, q));
@ -338,7 +338,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
app* ap = to_app(r);
const unsigned n = ap->get_num_args();
expr_ref acc = mk_empty();
for (unsigned i = 0; i < n; ++i) {
for (unsigned i = 0; i < n; i++) {
expr_ref left(m), right(m);
if (i == 0)
left = rex.mk_epsilon(seq_sort);
@ -381,8 +381,9 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
app* ap = to_app(r);
const unsigned n = ap->get_num_args();
expr_ref acc = mk_fromre(ap->get_arg(0));
for (unsigned i = 1; i < n; ++i)
for (unsigned i = 1; i < n; i++) {
acc = mk_inter(acc, mk_fromre(ap->get_arg(i)));
}
return acc;
}
@ -390,10 +391,24 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
if (rex.is_complement(r, a))
return mk_compl(mk_fromre(a));
// abbreviation
// difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b).
if (rex.is_diff(r, a, b))
return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b)));
// abbreviation
// optional: a? = eps | a ; sigma(a?) = sigma(eps | a) = eps cup sigma(a)
if (rex.is_opt(r, a)) {
const expr_ref eps(rex.mk_epsilon(seq_sort), m);
return mk_union(mk_single(eps, eps), mk_fromre(a));
}
// loop
unsigned l, h;
if (rex.is_loop(r, a, l, h)) {
// TODO
}
// bounded loop / ite / other: not handled (paper "v1: bail").
TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";);
ok = false;
@ -624,7 +639,7 @@ void seq_split::simplify(split_set& pairs) const {
// 1. drop pairs with a bottom (empty-language) component.
unsigned w = 0;
for (unsigned i = 0; i < pairs.size(); ++i) {
for (unsigned i = 0; i < pairs.size(); i++) {
if (r.is_empty(pairs[i].m_d) || r.is_empty(pairs[i].m_n))
continue;
if (w != i)
@ -650,7 +665,7 @@ void seq_split::simplify(split_set& pairs) const {
struct row { expr* d; expr* n; unsigned idx; };
vector<row> rows;
for (unsigned i = 0; i < pairs.size(); ++i)
for (unsigned i = 0; i < pairs.size(); i++)
rows.push_back({ pairs[i].m_d.get(), pairs[i].m_n.get(), i });
auto subsumes = [&](row const& a, row const& b) {
@ -769,7 +784,7 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
// Build the constant lookahead c and (if non-empty) an oracle that
// prunes splits whose postfix cannot match c.
zstring c;
for (i = 0; i < run_len; ++i) {
for (i = 0; i < run_len; i++) {
unsigned cv;
VERIFY(seq().str.is_unit(tokens.get(run_start + i), ch));
VERIFY(seq().is_const_char(ch, cv));
@ -791,7 +806,7 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
// of each postfix
if (!c.empty()) {
unsigned w = 0;
for (i = 0; i < result.size(); ++i) {
for (i = 0; i < result.size(); i++) {
expr* d = result[i].m_n;
for (unsigned k = 0; d && !seq().re.is_empty(d) && k < c.length(); ++k) {
d = m_rw.mk_derivative(seq().mk_char(c[k]), d);

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

@ -288,15 +288,12 @@ namespace seq {
bool str_mem::is_trivial(nielsen_node const* n) const {
SASSERT(m_str && m_regex);
if (m_kind == mem_kind::no_loop)
// guard: discharged ⇒ Σ* (accepts all); ε has no non-empty lap-prefix.
return m_discharged || m_str->is_empty();
if (m_regex->is_full_seq())
return true;
if (!m_str->is_empty())
return false;
if (m_kind == mem_kind::stab_view)
// ε ∈ stab(root,Q) iff current state ≡ root (i.e. root ∈ F={root}).
// ε ∈ L_{Q,{s}}(state) iff current state ≡ acceptance state s (=m_root).
return m_regex == m_root;
return n->graph().sg().re_nullable(m_regex) == l_true;
}
@ -304,10 +301,8 @@ namespace seq {
bool str_mem::is_contradiction(nielsen_node const* n) const {
if (!(m_str && m_regex && m_str->is_empty()))
return false;
if (m_kind == mem_kind::no_loop)
return false; // guard acceptance is always true on the empty word
if (m_kind == mem_kind::stab_view)
return m_regex != m_root; // ε ∉ stab(root,Q) when state ≢ root
return m_regex != m_root; // ε ∉ view when current state ≢ acceptance s
return n->graph().sg().re_nullable(m_regex) == l_false;
}
@ -427,11 +422,14 @@ namespace seq {
SASSERT(mem.m_regex != nullptr);
if (mem.is_trivial(this))
return;
// check if root node contains this membership constraint already
if (std::ranges::any_of(str_mems(),
[&](const str_mem &e) { return e.m_regex == mem.m_regex && e.m_str == mem.m_str; }))
// already present, no need to add again
return;
// Skip only a FULLY identical membership. The dedup must compare the
// whole membership (kind/root/ν), not just (m_str,m_regex): a land-state
// view (paper §5.3) shares (m_str,m_regex) with a plain membership on the
// same variable+state, and two land-views on the same state differ only
// in their acceptance root / ν. Deduping on (m_str,m_regex) alone would
// silently drop such a view and lose the constraint (→ unsound leaf).
if (std::ranges::any_of(str_mems(), [&](const str_mem &e) { return e == mem; }))
return; // already present
m_str_mem.push_back(mem);
}
@ -1262,6 +1260,107 @@ namespace seq {
return newly_marked;
}
// -----------------------------------------------------------------------
// Landing decomposition support: Q = states forward-reachable from the head.
// -----------------------------------------------------------------------
void nielsen_graph::collect_reachable_from_head(euf::snode const* head_re, uint_set& Q) const {
Q.reset();
if (!head_re || !head_re->get_expr())
return;
unsigned_vector stack;
stack.push_back(head_re->get_expr()->get_id());
while (!stack.empty()) {
const unsigned s = stack.back();
stack.pop_back();
if (Q.contains(s))
continue;
Q.insert(s);
auto it = m_partial_dfa_out.find(s);
if (it == m_partial_dfa_out.end())
continue;
for (const unsigned edge_idx : it->second) {
if (edge_idx >= m_partial_dfa_edges.size())
continue;
partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx];
if (e.m_dst)
stack.push_back(e.m_dst->get_id());
}
}
}
unsigned nielsen_graph::mark_reachable_projection_edges(euf::snode const* head_re) {
// Generalizes mark_scc_projection_edges to the forward-reachable set:
// mark every edge whose source is reachable from head_re with the current
// extraction index ν, bumping ν iff something new was marked. Views/co-
// views gate on projection_state_in_Q (edges marked ≤ ν), so the ν
// returned here identifies exactly this Q.
uint_set Q;
collect_reachable_from_head(head_re, Q);
unsigned newly_marked = 0;
for (const unsigned src_id : Q) {
auto it = m_partial_dfa_out.find(src_id);
if (it == m_partial_dfa_out.end())
continue;
for (const unsigned edge_idx : it->second) {
if (edge_idx >= m_partial_dfa_edges.size())
continue;
partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx];
if (!e.m_dst || !Q.contains(e.m_dst->get_id()))
continue;
if (e.m_projection_idx == 0)
++newly_marked;
}
}
if (newly_marked == 0)
return m_projection_extract_idx; // Q already covered by the current ν
++m_projection_extract_idx;
const unsigned extract_idx = m_projection_extract_idx;
for (const unsigned src_id : Q) {
auto it = m_partial_dfa_out.find(src_id);
if (it == m_partial_dfa_out.end())
continue;
for (const unsigned edge_idx : it->second) {
if (edge_idx >= m_partial_dfa_edges.size())
continue;
partial_dfa_edge& e = m_partial_dfa_edges[edge_idx];
if (!e.m_dst || !Q.contains(e.m_dst->get_id()))
continue;
if (e.m_projection_idx == 0)
e.m_projection_idx = extract_idx;
}
}
return extract_idx;
}
void nielsen_graph::compute_frontier(uint_set const& Q, svector<euf::snode const*> const& Qstates,
vector<frontier_edge>& out_frontier) {
// One lazy step from each Q state. Derive over the minterms of every
// p ∈ Qstates: δ_mt(p) ∈ Q is an internal edge (recorded, closing cycles
// for a future land-at-R); δ_mt(p) ∉ Q (and ≠ ⊥) is a frontier/escape
// edge. Snapshot Qstates was collected by the caller BEFORE this call,
// so recording internal edges (which appends to m_partial_dfa_edges) does
// not disturb the iteration.
for (euf::snode const* p : Qstates) {
if (!m.inc())
return;
if (!p || !p->is_ground())
continue;
euf::snode_vector mts;
m_sg.compute_minterms(p, mts);
for (euf::snode const* mt : mts) {
euf::snode const* q = m_sg.brzozowski_deriv(p, mt);
if (!q || q->is_fail() || !q->is_ground())
continue;
if (Q.contains(q->get_expr()->get_id()))
record_partial_derivative_edge(p, q); // internal edge
else
out_frontier.push_back(frontier_edge{ p, mt, q });
}
}
}
euf::snode const* nielsen_graph::get_slice(euf::snode const* v, expr* left, expr* right) {
SASSERT(v && v->get_expr() && left && right);
SASSERT(v->is_var());
@ -1804,15 +1903,15 @@ namespace seq {
}
}
// consume leading characters of view / guard memberships (Section 3.3).
// consume leading characters of land-state view memberships (paper §5.3).
// m_regex is the current (plain) derivative state; we gate on whether it
// lies in Q_ν (projection_state_in_Q) and step with the ordinary
// derivative, keeping the view/guard annotation.
// derivative, keeping the view annotation.
for (str_mem& mem : m_str_mem) {
SASSERT(mem.well_formed());
if (mem.is_plain())
continue;
if (consume_view_guard(mem))
if (consume_view(mem))
return simplify_result::conflict;
}
@ -1864,8 +1963,8 @@ namespace seq {
return simplify_result::proceed;
}
bool nielsen_node::consume_view_guard(str_mem& mem) {
SASSERT(!mem.is_plain());
bool nielsen_node::consume_view(str_mem& mem) {
SASSERT(mem.is_view());
euf::sgraph& sg = m_graph.sg();
auto set_regex_conflict = [&]() {
@ -1883,24 +1982,17 @@ namespace seq {
// leave it for apply_regex_if_split.
if (!c->is_ground() || c->kind() == euf::snode_kind::s_ite)
break;
const bool in_Q = m_graph.projection_state_in_Q(c->get_expr(), mem.m_nu);
if (!in_Q) {
if (mem.is_guard()) {
// The run left Q: no lap from the start can complete within Q
// anymore, so the guard is discharged (accepts every suffix).
mem.m_discharged = true;
return false;
}
// view: a^{-1} L_{Q,F}(c) = ∅ when c ∉ Q.
if (!m_graph.projection_state_in_Q(c->get_expr(), mem.m_nu)) {
// a^{-1} L_{Q,F}(c) = ∅ when c ∉ Q.
set_regex_conflict();
return true;
}
// Step with brzozowski_deriv for BOTH concrete and symbolic tokens.
// This is essential: the partial-DFA states (and m_root) are produced
// by brzozowski_deriv, so its canonicalization must be used here too —
// otherwise the guard's resolved state never equals m_root by snode
// identity and laps never close. For a symbolic unit it yields a
// canonical ite residual that apply_regex_if_split later resolves.
// otherwise the resolved state never equals m_root by snode identity.
// For a symbolic unit it yields a canonical ite residual that
// apply_regex_if_split later resolves.
euf::snode const* next = sg.brzozowski_deriv(c, tok);
if (!next)
break;
@ -1908,25 +2000,11 @@ namespace seq {
mem.m_regex = next;
if (next->is_fail()) {
// view: derivative collapsed to ∅ — unsatisfiable.
// guard: the lap can never close through ∅; treat as discharged.
if (mem.is_guard()) { mem.m_discharged = true; return false; }
set_regex_conflict();
return true;
}
if (next->is_ground() && next->kind() != euf::snode_kind::s_ite) {
// concrete next state resolved immediately
if (mem.is_guard() && next == mem.m_root) {
// a non-empty prefix completed a lap r→…→r within Q.
set_regex_conflict();
return true;
}
}
else {
// symbolic ite residual: defer to apply_regex_if_split, which
// resolves the character and (for guards) detects a lap landing
// back on the root.
break;
}
if (!(next->is_ground() && next->kind() != euf::snode_kind::s_ite))
break; // symbolic ite residual: defer to apply_regex_if_split
}
return false;
}
@ -2106,7 +2184,7 @@ namespace seq {
++m_stats.m_num_unknown;
return search_result::unknown;
}
catch(const std::exception&) {
catch(const std::exception& e) {
#ifdef Z3DEBUG
std::string dot = to_dot();
#endif
@ -3381,9 +3459,11 @@ namespace seq {
if (!harvest_mode() && apply_cycle_subsumption(node))
return ++m_stats.m_mod_cycle_subsumption, true;
// Priority 6: CycleDecomp - stabilizer introduction for regex cycles using partial DFA projection
// Priority 6: LandingDecomp - the core branching rule (paper §5.3):
// split the leading variable by its landing state in the explored region
// (land-at-s + escape-via-frontier). Subsumes character unwinding.
// (regex-related: skipped in benchmark-harvest mode)
if (!harvest_mode() && apply_cycle_decomposition(node))
if (!harvest_mode() && apply_landing_decomposition(node))
return ++m_stats.m_mod_star_intr, true;
// Priority 7: GPowerIntr - ground power introduction
@ -3883,12 +3963,17 @@ namespace seq {
if (!first->is_var())
continue;
euf::snode const* R = mem.m_regex;
if (!R->is_ground() || R->kind() == euf::snode_kind::s_ite)
continue;
// R must lie on a detected cycle with a marked SCC snapshot.
// R must lie on a detected cycle in the explored region. Use the
// same reachable-Q snapshot as apply_landing_decomposition so the
// stabilizer view stab(R,Q_ν) matches the land-at-R view.
ensure_automaton_explored(R);
uint_set scc;
if (!collect_scc_for_projection(R, scc))
continue;
const unsigned nu = m_projection_extract_idx;
const unsigned nu = mark_reachable_projection_edges(R);
if (nu == 0)
continue;
@ -3924,105 +4009,156 @@ namespace seq {
}
// -----------------------------------------------------------------------
// Modifier: apply_cycle_decomposition (paper Section "Cycle Decomposition")
// Modifier: apply_landing_decomposition (paper §5.3 "Landing Decomposition")
//
// For a membership x·u ∈ R whose leading variable x sits on a detected cycle
// (R lies in an SCC of the partial DFA) and that does not already carry a
// matching cycle guard for the current SCC snapshot, split
// x → x'·x''
// and attach the two *view*/*guard* primitive constraints (Section 3.3):
// x' ∈ stab(R, Q_ν) -- stabilizer view (F = {R})
// noloop(x'', R, Q_ν) -- cycle guard (two-mode monitor)
// The leading x' is immediately subsumed (its only constraint is the view,
// and stab ⊆ stab trivially), so it is dropped from the primary constraint.
// The core branching rule. For a plain non-primitive membership x·u ∈ R
// (u ≠ ε, x a variable, R a ground regex) we split x by WHERE its value
// lands in the explored region Q — the states forward-reachable from R in
// the partial DFA G — using the frontier partition (Lemma 4.7):
//
// Unlike the old projection-operator encoding, the view and guard are kept
// as *constraint metadata* over the plain state R and the ν-indexed explored
// subautomaton Q_ν — nothing is materialized as a regex, which keeps the
// reachable state space finite (termination).
// Land-at-s (for each s ∈ Q):
// pin x ∈_{Q_ν,{s}} R (land-state view, acceptance F = {s},
// current state = R) and advance to u ∈ s.
// x is removed outright (no split, no guard). s = R is stabilizer
// absorption: one view swallows every lap of the R-cycle.
//
// Escape-via-(p,a) (for each frontier edge p ∈ Q, δ_a(p) ∉ Q):
// substitute x → x1·a·x2 (x1,x2 fresh), pin x1 ∈_{Q_ν,{p}} R,
// drop x1 from the active constraint (it lands at p) leaving
// a·x2·u ∈ p; the normal char-consumption then steps p →a δ_a(p),
// recording the new edge and growing Q.
//
// By Lemma 4.7 the blocks partition Σ*, so the branches are exhaustive and
// pairwise disjoint. Character unwinding is the degenerate Q = {R} case
// (land-at-R = x→ε; escape-via-(R,a) = x→a·x2), so this rule subsumes
// apply_regex_var_split for ground regexes. Views are constraint metadata
// over the plain state R and the ν-indexed explored subautomaton Q_ν
// (projection_state_in_Q) — nothing is materialized as a regex.
// Termination: a landing removes a variable (active term shrinks); each
// escape consumes a fresh state of the finite monotone G.
// -----------------------------------------------------------------------
bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) {
bool nielsen_graph::apply_landing_decomposition(nielsen_node* node) {
if (!m_regex_dynamic_decomposition)
return false;
// Look for a str_mem with a variable-headed string
for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) {
str_mem const& mem = node->str_mems()[mi];
SASSERT(mem.well_formed());
if (!mem.is_plain() || mem.is_primitive())
continue;
euf::snode const* first = mem.m_str->first();
SASSERT(first);
if (!first->is_var())
euf::snode const* x = mem.m_str->first();
SASSERT(x);
if (!x->is_var())
continue;
euf::snode const* R = mem.m_regex;
// R must be a settled ground state; an unresolved symbolic ite is
// left to apply_regex_if_split, a non-ground regex to the var-split
// fallback.
if (!R->is_ground() || R->kind() == euf::snode_kind::s_ite)
continue;
euf::snode const* x = first;
euf::snode const* R = mem.m_regex;
// Lazily explore R's full automaton (once, cached) so that
// collect_scc_for_projection sees the complete SCC of R and the
// stabilizer view / cycle guard gate on a complete Q.
// Eagerly explore R's reachable automaton (once, cached) so the SCC
// gate below and the landing enumeration see the full explored region
// Q — this is the automaton-based landing. Without it the cycle would
// not be recorded before factorization/var_split fire, so landing
// would never trigger. If exploration hits the resource limit Q is
// left partial (a sound under-approximation) and the escape branches
// recover completeness.
ensure_automaton_explored(R);
// R must sit on a cycle (an SCC of the partial DFA).
uint_set scc;
if (!collect_scc_for_projection(R, scc))
continue;
// Mark the SCC edges; this gives a ν identifying the current Q_SCC.
// (We trigger on absence of a matching guard, NOT on novelty.)
mark_scc_projection_edges(scc);
const unsigned nu = m_projection_extract_idx;
if (nu == 0)
continue;
// Trigger: R must sit on a detected cycle in the explored G. This is
// the same gate the old split-and-guard apply_cycle_decomposition
// used; the acyclic growth/unwinding of x is left to the pre-existing
// flow (apply_regex_var_split / apply_regex_factorization). Landing
// then replaces the split+guard on cyclic heads with land-at-s +
// escape, and is exhaustive on its own (frontier partition) so
// preempting var_split at this node loses no words.
{
uint_set scc;
if (!collect_scc_for_projection(R, scc))
continue;
}
// Trigger condition: x must not already carry a cycle guard for the
// current SCC snapshot ν. All states of one SCC share a single ν, so
// the guard is keyed on ν rather than on the (changing) head R: as the
// derivation walks the SCC the head moves, but the lineage is already
// guarded against re-traversing the cycle. An already-decomposed
// variable whose guard refers to a strictly smaller, stale ν is
// re-decomposed to adopt the enlarged SCC.
bool already_guarded = false;
for (str_mem const& g : node->str_mems()) {
if (g.is_guard() && g.m_nu >= nu
&& g.m_str && g.m_str->first() == x) {
already_guarded = true;
break;
// Q = states forward-reachable from R (ids), and their snode handles.
uint_set Q;
collect_reachable_from_head(R, Q);
svector<euf::snode const*> Qstates;
uint_set added;
Qstates.push_back(R);
added.insert(R->get_expr()->get_id());
for (partial_dfa_edge const& e : m_partial_dfa_edges) {
for (expr* ep : { e.m_src, e.m_dst }) {
if (!ep) continue;
const unsigned id = ep->get_id();
if (!Q.contains(id) || added.contains(id)) continue;
euf::snode const* sn = m_sg.find(ep);
if (sn) { added.insert(id); Qstates.push_back(sn); }
}
}
if (already_guarded)
continue;
// One lazy exploration step: record internal (cycle-closing) edges
// and collect the frontier (escape candidates).
vector<frontier_edge> frontier;
compute_frontier(Q, Qstates, frontier);
// Mark the reachable subautomaton, fixing the ν that identifies Q_ν
// for every view created below. ν may be 0 in the Q = {R} bootstrap
// (no in-Q edges yet); a view with ν = 0 denotes exactly {ε} at R,
// which is precisely what unwinding needs.
const unsigned nu = mark_reachable_projection_edges(R);
sort* seq_sort = x->get_expr()->get_sort();
// Construct the replacement x = x' x''
euf::snode const* xp = m_sg.mk(m_sk.mk("cycle", x->get_expr(), R->get_expr(), seq_sort));
euf::snode const* xpp = get_tail(x, compute_length_expr(xp).get());
euf::snode const* xp_xpp = m_sg.mk_concat(xp, xpp);
// (a) LAND-AT-s branches (progress: x removed).
for (euf::snode const* s : Qstates) {
nielsen_node* child = mk_child(node);
mk_edge(node, child, "land", /*progress*/ true);
str_mem& cm = child->m_str_mem[mi];
cm.m_str = m_sg.drop_first(cm.m_str); // u
cm.m_regex = s; // active becomes u ∈ s
// x ∈_{Q_ν,{s}} R : state = R (start), root = s (acceptance).
child->add_str_mem(str_mem::mk_view(m, x, R, s, nu, mem.m_dep));
TRACE(seq, tout << "landing: land x=" << mk_pp(x->get_expr(), m)
<< " at " << mk_pp(s->get_expr(), m)
<< " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n");
}
nielsen_node* child = mk_child(node);
SASSERT(child->m_str_mem[mi] == mem);
nielsen_edge* e = mk_edge(node, child, "cycle decomp", false);
const nielsen_subst s(x, xp_xpp, mem.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
// (b) ESCAPE branches (non-progress: consumes a fresh state, grows Q).
for (frontier_edge const& fe : frontier) {
euf::snode const* p = fe.m_src;
char_set cs = m_seq_regex->minterm_to_char_set(fe.m_mt->get_expr());
if (cs.is_empty())
continue;
euf::snode const* aunit =
m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char())));
euf::snode const* x1 = mk_fresh_var(seq_sort);
// x2 = x[|x1|+1:] (slice tail after the landed prefix and the char)
const expr_ref after =
normalize_arith(m, a.mk_add(compute_length_expr(x1).get(), a.mk_int(1)));
euf::snode const* x2 = get_tail(x, after.get());
euf::snode const* repl = m_sg.mk_concat(x1, m_sg.mk_concat(aunit, x2));
// remove from mi^th element of the child the leading token, as it is immediately subsumed
SASSERT(child->m_str_mem[mi].m_str->first() == xp);
child->m_str_mem[mi].m_str = dir_drop(m_sg, child->m_str_mem[mi].m_str, 1, true);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, "escape", /*progress*/ false);
const nielsen_subst sub(x, repl, mem.m_dep);
e->add_subst(sub);
child->apply_subst(m_sg, sub);
// x' ∈ stab(R, Q_ν) (stabilizer view, F = {R}, current state = R)
child->add_str_mem(str_mem::mk_view(m, xp, R, R, nu, mem.m_dep));
// x1 lands at p: drop it from the active constraint, whose state
// becomes p; the leading a is then consumed by simplify_and_init
// (stepping p →a δ_a(p) and recording the edge).
str_mem& cm = child->m_str_mem[mi];
SASSERT(cm.m_str->first() == x1);
cm.m_str = dir_drop(m_sg, cm.m_str, 1, true); // a·x2·u
cm.m_regex = p;
// x1 ∈_{Q_ν,{p}} R
child->add_str_mem(str_mem::mk_view(m, x1, R, p, nu, mem.m_dep));
TRACE(seq, tout << "landing: escape x=" << mk_pp(x->get_expr(), m)
<< " via (" << mk_pp(p->get_expr(), m) << ", "
<< cs.first_char() << ") R=" << mk_pp(R->get_expr(), m)
<< " nu=" << nu << "\n");
}
// noloop(x'', R, Q_ν) (cycle guard, two-mode monitor, state = R)
child->add_str_mem(str_mem::mk_guard(m, xpp, R, R, nu, mem.m_dep));
TRACE(seq, tout << "cycle_decomp: x=" << mk_pp(x->get_expr(), m)
<< " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n");
#ifdef Z3DEBUG
std::string dot = partial_dfa_to_dot(R, false);
#endif
return true;
}
return false;
@ -4108,29 +4244,6 @@ namespace seq {
// complement bodies against runaway space blow-up.
static const unsigned RF_LAZY_CAP = 1u << 20;
// The cycle machinery (apply_cycle_decomposition) owns variables it has put
// under a noloop guard: factorizing such a variable's membership would split
// it in a way that violates the guard's premise (that the variable is handled
// by the stabilizer/guard decomposition), yielding a spurious conflict. So
// factorization defers whenever the leading token is a guarded variable.
static bool leading_var_guarded(nielsen_node const* node, euf::snode const* lead) {
for (str_mem const& g : node->str_mems())
if (g.is_guard() && g.m_str && g.m_str->first() == lead)
return true;
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);
@ -4267,18 +4380,18 @@ 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))
// A node under landing control carries land-state views; the cycle
// machinery (apply_landing_decomposition / apply_cycle_subsumption) owns
// it, so factorization defers.
for (str_mem const& mem : node->str_mems()) {
if (mem.is_view())
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()) {
node->set_rf_cont(nullptr); // the iterator migrates to child B (or is dropped)
// If the cycle machinery has, in the meantime, put the leading variable
// under a guard, stop factorizing and defer (the iterator is dropped).
if (leading_var_guarded(node, st->m_mem.m_str->first()))
return false;
dep_tracker conflict_dep = nullptr;
switch (rf_step(node, st, conflict_dep)) {
case rf_step_result::branched:
@ -4297,27 +4410,18 @@ namespace seq {
// Fresh: find the first factorizable membership and start an iterator.
for (str_mem const& mem : node->str_mems()) {
SASSERT(mem.well_formed());
SASSERT(!mem.m_str->is_empty()); // should have been eliminated already
// split() handles all regex forms (incl. complement / intersection),
// so the classical restriction is no longer needed.
if (mem.m_str->is_empty() || mem.is_primitive())
if (mem.is_primitive())
continue;
// View / guard memberships (Section 3.3) are handled by the
// cycle machinery and the synchronous product, not by factorization.
// Land-state view memberships (paper §5.3) are handled by the cycle
// machinery and the synchronous product, not by factorization.
if (!mem.is_plain())
continue;
// Defer to the cycle machinery when the leading variable is guarded.
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
@ -4659,7 +4763,7 @@ namespace seq {
// Canonicalize with th_rewriter so that the resolved leaf shares
// its snode id with the corresponding partial-DFA state (which is
// built by brzozowski_deriv); otherwise un-simplified residuals
// like (a|∅)·R≠a·R break view/guard Q-membership and lap checks.
// like (a|∅)·R≠a·R break view Q-membership checks.
euf::snode const* new_regex_snode = mk_rewrite(r);
nielsen_node *child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, "regex if", true);
@ -4669,12 +4773,6 @@ namespace seq {
for (str_mem &cm : child->str_mems()) {
if (cm == mem) {
cm.m_regex = new_regex_snode;
// A guard whose symbolic step lands back on the cycle
// head closed a lap within Q → this branch is dead.
if (cm.is_guard() && new_regex_snode == cm.m_root) {
child->set_general_conflict();
child->set_conflict(backtrack_reason::regex, cm.m_dep);
}
break;
}
}
@ -5599,8 +5697,6 @@ namespace seq {
if (c.m_complemented)
return (c.m_sink || c.m_state != c.m_root) ? l_true : l_false;
return (c.m_state == c.m_root) ? l_true : l_false;
case mem_kind::no_loop:
return l_true; // guard accepts on every prefix it has not failed on
}
return l_undef;
}
@ -5630,15 +5726,6 @@ namespace seq {
r.m_state = d;
return r;
}
case mem_kind::no_loop: {
if (c.m_sink) return r; // discharged: Σ*
if (!projection_state_in_Q(c.m_state->get_expr(), c.m_nu)) { r.m_sink = true; return r; }
euf::snode const* d = m_sg.brzozowski_deriv(c.m_state, mt);
if (!d || d->is_fail()) { r.m_sink = true; return r; } // lap cannot close through ∅
if (d == c.m_root) { r.m_dead = true; return r; } // lap completed → forbidden
r.m_state = d;
return r;
}
}
return r;
}
@ -5733,9 +5820,6 @@ namespace seq {
case mem_kind::stab_view:
out.push_back(prod_comp::mk_view(mem.m_regex, mem.m_root, mem.m_nu, false));
break;
case mem_kind::no_loop:
out.push_back(prod_comp::mk_guard(mem.m_regex, mem.m_root, mem.m_nu, mem.m_discharged));
break;
}
dep = m_dep_mgr.mk_join(dep, mem.m_dep);
found = true;
@ -5743,6 +5827,111 @@ namespace seq {
return found;
}
bool nielsen_graph::product_witness(euf::snode const* var, nielsen_node const& node,
unsigned len, zstring& out) {
// Shortest-accepting-word search over the product of all of var's
// primitive components (plain regexes AND land-state views), optionally
// intersected with Σ^len. Mirrors check_product_emptiness but records
// the spelled word so a SAT-leaf variable pinned to a land-state view
// (F={s}) gets a concrete witness (ε alone is inadmissible when s≠head).
vector<prod_comp> comps0;
dep_tracker d = nullptr;
collect_var_components(var, node, comps0, d);
if (len != UINT_MAX) {
// force exact length via a Σ^len plain component
sort* re_sort = nullptr;
if (!comps0.empty() && comps0[0].m_state)
re_sort = comps0[0].m_state->get_expr()->get_sort();
if (re_sort) {
const expr_ref sigma_n(
m_seq.re.mk_loop(m_seq.re.mk_full_char(re_sort), len, len), m);
comps0.push_back(prod_comp::mk_plain(m_sg.mk(sigma_n)));
}
}
if (comps0.empty()) {
// no constraints: any word of the requested length (default ε)
out = zstring();
for (unsigned i = 0; i < (len == UINT_MAX ? 0u : len); ++i)
out = out + zstring((unsigned)'a');
return true;
}
auto encode = [](vector<prod_comp> const& cs) {
std::vector<unsigned> key;
key.reserve(cs.size() * 3);
for (auto const& c : cs) {
key.push_back(static_cast<unsigned>(c.m_kind));
key.push_back((c.m_complemented ? 1u : 0u) | (c.m_sink ? 2u : 0u) | (c.m_dead ? 4u : 0u));
key.push_back(c.m_state ? c.m_state->id() : UINT_MAX);
}
return key;
};
std::set<std::vector<unsigned>> visited;
// BFS (vector + head index) for a SHORTEST accepting word.
vector<std::pair<vector<prod_comp>, zstring>> work;
work.push_back({ comps0, zstring() });
visited.insert(encode(comps0));
unsigned head = 0;
const unsigned MAX_STATES = 200000;
while (head < work.size()) {
if (!m.inc() || head >= MAX_STATES)
return false;
vector<prod_comp> cur = work[head].first;
zstring w = work[head].second;
++head;
bool any_dead = false;
for (auto const& c : cur) if (c.m_dead) { any_dead = true; break; }
if (any_dead)
continue;
bool all_acc = true, any_undef = false;
for (auto const& c : cur) {
const lbool a = comp_accepting(c);
if (a == l_false) { all_acc = false; break; }
if (a == l_undef) any_undef = true;
}
if (all_acc && !any_undef) {
out = w;
return true;
}
expr* combined = nullptr;
for (auto const& c : cur) {
if (c.m_sink || c.m_dead) continue;
combined = combined ? m_seq.re.mk_inter(combined, c.m_state->get_expr())
: c.m_state->get_expr();
}
if (!combined)
continue;
euf::snode_vector mts;
m_sg.compute_minterms(m_sg.mk(combined), mts);
for (euf::snode const* mt : mts) {
char_set cs = m_seq_regex->minterm_to_char_set(mt->get_expr());
if (cs.is_empty())
continue;
const unsigned ch = cs.first_char();
vector<prod_comp> nxt;
bool dead = false;
for (auto const& c : cur) {
prod_comp e = comp_step(c, mt);
if (e.m_dead) { dead = true; break; }
nxt.push_back(e);
}
if (dead)
continue;
if (visited.insert(encode(nxt)).second)
work.push_back({ nxt, w + zstring(ch) });
}
}
return false;
}
bool nielsen_graph::check_leaf_regex(nielsen_node const& node, dep_tracker& dep) {
SASSERT(m_seq_regex);

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

@ -302,15 +302,17 @@ namespace seq {
<< snode_label_html(p.deq.m_rhs, p.deq.m, false);
}
// kind of a regex membership constraint (paper Section 3.3, "views"):
// kind of a regex membership constraint (paper §5.3, "land-state views"):
// - plain: ordinary u ∈ r
// - stab_view: stabilizer view u ∈_{Q,{root}} root (acceptance set F={root})
// - no_loop: cycle guard noloop(u, root, Q) (two-mode monitor)
// For view/guard, m_regex holds the *current derivative state* (a plain
// regex; starts at m_root) and Q is identified by the ν-index m_nu over
// the partial DFA (projection_state_in_Q). This replaces the old re.proj
// projection operator: m_regex is always a plain regex now.
enum class mem_kind : unsigned char { plain, stab_view, no_loop };
// - stab_view: land-state view u ∈_{Q,{s}} r (acceptance set F={s})
// (the stabilizer is the special case s = r).
// For a view, m_regex holds the *current derivative state* (a plain regex;
// starts at the head r) and m_root holds the landing/acceptance state s.
// Q is identified by the ν-index m_nu over the partial DFA
// (projection_state_in_Q). m_regex is always a plain regex.
// The old two-mode `no_loop` cycle guard has been removed: landing
// decomposition (paper §5.3) needs no guard.
enum class mem_kind : unsigned char { plain, stab_view };
// regex membership constraint: str in regex
// mirrors ZIPT's StrMem
@ -320,11 +322,10 @@ namespace seq {
euf::snode const* m_regex; // assumed to be non-null (plain regex = current run state)
dep_tracker m_dep;
// view / guard annotation (Section 3.3)
// land-state view annotation (paper §5.3)
mem_kind m_kind = mem_kind::plain;
euf::snode const* m_root = nullptr; // cycle head r (view F={r}; guard lap head)
euf::snode const* m_root = nullptr; // landing/acceptance state s (view F={s}; stabilizer: s=head)
unsigned m_nu = 0; // ν: snapshot index identifying Q
bool m_discharged = false; // guard monitor: false=watch, true=discharged
str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, dep_tracker const& dep):
m(m), m_str(str), m_regex(regex), m_dep(dep) {}
@ -336,33 +337,25 @@ namespace seq {
m_kind = other.m_kind;
m_root = other.m_root;
m_nu = other.m_nu;
m_discharged = other.m_discharged;
return *this;
}
// factory for a stabilizer view str ∈_{Q_ν,{root}} root (m_regex=state)
// factory for a land-state view str ∈_{Q_ν,{root}} state (m_regex=state,
// root = landing/acceptance state s; the stabilizer is state=root=head).
static str_mem mk_view(ast_manager& m, euf::snode const* str, euf::snode const* state,
euf::snode const* root, unsigned nu, dep_tracker const& dep) {
str_mem r(m, str, state, dep);
r.m_kind = mem_kind::stab_view; r.m_root = root; r.m_nu = nu;
return r;
}
// factory for a cycle guard noloop(str, root, Q_ν) (m_regex=state)
static str_mem mk_guard(ast_manager& m, euf::snode const* str, euf::snode const* state,
euf::snode const* root, unsigned nu, dep_tracker const& dep) {
str_mem r(m, str, state, dep);
r.m_kind = mem_kind::no_loop; r.m_root = root; r.m_nu = nu;
return r;
}
bool is_plain() const { return m_kind == mem_kind::plain; }
bool is_view() const { return m_kind == mem_kind::stab_view; }
bool is_guard() const { return m_kind == mem_kind::no_loop; }
bool operator==(const str_mem& other) const {
return m_str->similar(other.m_str, m) && m_regex == other.m_regex
&& m_kind == other.m_kind && m_root == other.m_root
&& m_nu == other.m_nu && m_discharged == other.m_discharged;
&& m_nu == other.m_nu;
}
bool operator<(const str_mem& other) const {
@ -747,11 +740,11 @@ namespace seq {
// Returns proceed, conflict, satisfied, or restart.
simplify_result simplify_and_init(ptr_vector<nielsen_edge> const& cur_path);
// Consume leading concrete/symbolic characters of a view/guard membership
// (Section 3.3): gate on Q_ν, step with the ordinary derivative, keeping
// the annotation. Returns true if the constraint died (view left Q, or
// guard completed a lap) — the caller reports a regex conflict.
bool consume_view_guard(str_mem& mem);
// Consume leading concrete/symbolic characters of a land-state view
// membership (paper §5.3): gate on Q_ν, step with the ordinary
// derivative, keeping the annotation. Returns true if the view died
// (left Q or derivative collapsed to ∅) — caller reports a regex conflict.
bool consume_view(str_mem& mem);
// true if all str_eqs are trivial and there are no str_mems
bool is_satisfied() const;
@ -1059,6 +1052,16 @@ namespace seq {
// path of edges from root to sat_node (set when sat_node is set)
ptr_vector<nielsen_edge> const& sat_path() const { return m_sat_path; }
// Model construction (called by seq_model): build a concrete word for
// `var` satisfying ALL its primitive constraints on `node` simultaneously
// (plain regexes AND land-state views), by a shortest-accepting-word
// product search. If len != UINT_MAX the word is forced to that exact
// length (Σ^len factor). Returns true and sets `out` on success. Used
// for view-constrained variables at a SAT leaf, where a land-state view
// (F={s}, s≠head) does not denote a plain regex and ε may be inadmissible.
bool product_witness(euf::snode const* var, nielsen_node const& node,
unsigned len, zstring& out);
// add constraints to the root node from external solver
void add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode* l, smt::enode* r) const;
void add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const;
@ -1253,17 +1256,20 @@ namespace seq {
mem_kind m_kind = mem_kind::plain;
bool m_complemented = false; // ~stab co-view (kind==stab_view)
euf::snode const* m_state = nullptr; // current plain regex state
euf::snode const* m_root = nullptr; // view/guard cycle head
euf::snode const* m_root = nullptr; // land-state view acceptance state s
unsigned m_nu = 0; // ν (Q snapshot)
bool m_sink = false; // co-view became Σ* / guard discharged
bool m_sink = false; // co-view became Σ*
bool m_dead = false; // language collapsed to ∅
static prod_comp mk_plain(euf::snode const* s) { prod_comp c; c.m_state = s; return c; }
static prod_comp mk_view(euf::snode const* s, euf::snode const* root, unsigned nu, bool compl_) {
prod_comp c; c.m_kind = mem_kind::stab_view; c.m_state = s; c.m_root = root; c.m_nu = nu; c.m_complemented = compl_; return c;
}
static prod_comp mk_guard(euf::snode const* s, euf::snode const* root, unsigned nu, bool discharged) {
prod_comp c; c.m_kind = mem_kind::no_loop; c.m_state = s; c.m_root = root; c.m_nu = nu; c.m_sink = discharged; return c;
prod_comp c;
c.m_kind = mem_kind::stab_view;
c.m_state = s;
c.m_root = root;
c.m_nu = nu;
c.m_complemented = compl_;
return c;
}
};
@ -1276,7 +1282,7 @@ namespace seq {
prod_comp comp_step(prod_comp const& c, euf::snode const* mt);
// Build the product components for variable `var` from the node's
// primitive memberships (plain / view / guard). Joins their deps.
// primitive memberships (plain / land-state view). Joins their deps.
bool collect_var_components(euf::snode const* var, nielsen_node const& node,
vector<prod_comp>& out, dep_tracker& dep);
@ -1296,6 +1302,36 @@ namespace seq {
// currently covered edge count for this extraction.
unsigned mark_scc_projection_edges(uint_set const& scc);
// Landing decomposition (paper §5.3): Q is the set of explored states
// forward-reachable from the head r in the partial DFA G, not merely r's
// SCC. These generalize the SCC helpers above.
// Collect (into Q, as expr ids) every state forward-reachable from
// head_re over the recorded partial-DFA edges. Always includes head_re.
void collect_reachable_from_head(euf::snode const* head_re, uint_set& Q) const;
// Mark every forward-reachable edge from head_re with a monotone
// extraction index ν (only previously-unmarked edges), bumping ν iff
// something new was marked. Returns the ν identifying this Q
// (0 if there is nothing marked, i.e. no reachable edge).
unsigned mark_reachable_projection_edges(euf::snode const* head_re);
// A frontier edge (p, mt, q): p ∈ Q, mt a minterm of p, q = δ_mt(p) ∉ Q
// and q ≠ ⊥. The escape candidates of the landing decomposition.
struct frontier_edge {
euf::snode const* m_src; // p ∈ Q
euf::snode const* m_mt; // minterm
euf::snode const* m_dst; // q = δ_mt(p) ∉ Q
};
// One lazy exploration step around Q: for each p ∈ Qstates, take every
// minterm derivative δ_mt(p). If δ_mt(p) ∈ Q record the internal edge
// (closing cycles); otherwise (and ≠ ⊥) append it to out_frontier.
// Q holds expr ids (as produced by collect_reachable_from_head);
// Qstates are the corresponding snode handles (including the head).
void compute_frontier(uint_set const& Q, svector<euf::snode const*> const& Qstates,
vector<frontier_edge>& out_frontier);
euf::snode const* get_slice(euf::snode const* v, expr* left, expr* right);
euf::snode const* get_tail(euf::snode const* v, expr* cnt, bool fwd = true);
@ -1377,10 +1413,18 @@ namespace seq {
// branch into s ∈ th under condition c, and s ∈ el under condition ¬c.
bool apply_regex_if_split(nielsen_node* node);
// cycle decomposition: for a str_mem x·s ∈ R where a partial DFA
// cycle is detected, project SCC onto stabilizer constraint b.
// Rewrites x into x'·x'' with x' ∈ b*, x'' ∈ complement((b ∩ complement(eps)) · Sigma*).
bool apply_cycle_decomposition(nielsen_node* node);
// landing decomposition (paper §5.3): the core branching rule for a
// plain non-primitive membership x·u ∈ R (u ≠ ε, x a variable, R ground).
// Splits x by WHERE its value lands in the explored region Q (states
// forward-reachable from R):
// - land-at-s (for each s ∈ Q): pin x ∈_{Q,{s}} R and advance to u ∈ s
// (no split; s = R is stabilizer/cycle absorption);
// - escape-via-(p,a) (for each frontier edge): x → x1·a·x2 with
// x1 ∈_{Q,{p}} R, advancing to x2·u ∈ δ_a(p) and growing Q.
// By the frontier partition (Lemma 4.7) these branches are exhaustive and
// disjoint; character unwinding is the degenerate Q = {R} case. Replaces
// the old split-and-guard apply_cycle_decomposition.
bool apply_landing_decomposition(nielsen_node* node);
// cycle subsumption: for a str_mem x·rest ∈ R where x is constrained
// to L(Reg_x) ⊆ L(stabilizer of R), simplify to rest ∈ R.
@ -1411,14 +1455,6 @@ 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.

55
src/smt/seq_model.cpp
View file

@ -99,6 +99,7 @@ namespace smt {
m_var_values.reset();
m_var_replacement.reset();
m_var_regex.reset();
m_view_vars.reset();
m_trail.reset();
m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model());
@ -106,6 +107,8 @@ namespace smt {
seq::nielsen_node* sat_node = nielsen.sat_node();
SASSERT(sat_node); // in case we report sat, this has to point to a satisfied Nielsen node!
m_nielsen = &nielsen;
m_sat_node = sat_node;
collect_var_regex_constraints(sat_node);
@ -451,11 +454,45 @@ namespace smt {
SASSERT(var->get_expr());
SASSERT(m_seq.is_seq(var->get_expr()));
auto srt = var->get_expr()->get_sort();
// check if this variable has regex constraints
euf::snode const* re = nullptr;
unsigned key = var_key(var);
if (m_var_regex.find(key, re) && re) {
// Land-state view (paper §5.3): the variable is pinned to L_{Q,{s}}(head),
// which is not a plain regex. Build a witness by the product search over
// ALL of the variable's primitive constraints (view AND any plain regex).
// This is authoritative for a view variable — we must NOT fall through to
// the plain m_var_regex path below, which sees only the plain constraints
// and would emit a word that violates the view (unsound witness).
if (m_nielsen && m_sat_node && m_view_vars.contains(key)) {
expr_ref len_e(m_seq.str.mk_length(var->get_expr()), m);
rational len_val;
unsigned len = UINT_MAX;
if (get_arith_value(len_e, len_val) && len_val.is_unsigned())
len = len_val.get_unsigned();
zstring w;
// Try the arith-assigned length first (keeps the model length-consistent);
// if the view∩plain intersection has no word of that length (the arith
// length and the regex are only loosely coupled), retry unconstrained so
// the emitted word still satisfies every regex/view constraint.
bool ok = m_nielsen->product_witness(var, *m_sat_node, len, w);
if (!ok && len != UINT_MAX)
ok = m_nielsen->product_witness(var, *m_sat_node, UINT_MAX, w);
if (ok) {
expr* witness = m_seq.str.mk_string(w);
m_trail.push_back(witness);
m_factory->register_value(witness);
return witness;
}
IF_VERBOSE(1, verbose_stream() << "nseq view witness failed for "
<< mk_pp(var->get_expr(), m) << "\n");
// product search exhausted: fall through only to the length fallback,
// never to the view-ignoring plain path (guarded by !m_view_vars below).
}
// check if this variable has regex constraints (non-view vars only; a view
// var is fully handled above — its plain constraints are already folded
// into the product search).
euf::snode const* re = nullptr;
if (!m_view_vars.contains(key) && m_var_regex.find(key, re) && re) {
expr* re_expr = re->get_expr();
SASSERT(re_expr);
@ -596,11 +633,13 @@ namespace smt {
if (mem.is_trivial(sat_node))
continue; // empty string in nullable regex: already satisfied, no variable to constrain
VERIFY(mem.is_primitive()); // everything else should have been eliminated already
// TODO(view/guard witness): a stabilizer view / cycle guard does not
// denote a plain regex on the variable; for now skip it during model
// construction (handled by the dedicated view/guard witness below).
if (!mem.is_plain())
// A land-state view (paper §5.3) does not denote a plain regex on the
// variable; mark it so mk_fresh_value builds its witness via the
// product search (which respects the view AND any plain constraints).
if (!mem.is_plain()) {
m_view_vars.insert(var_key(mem.m_str));
continue;
}
unsigned id = var_key(mem.m_str);
euf::snode const* existing = nullptr;
if (m_var_regex.find(id, existing) && existing) {

9
src/smt/seq_model.h
View file

@ -70,6 +70,15 @@ namespace smt {
// collected during init() from the state's str_mem list.
u_map<euf::snode const*> m_var_regex;
// variables carrying a land-state view (paper §5.3) at the SAT leaf; their
// witness is produced by the product search (m_nielsen->product_witness),
// not by some_string_in_re over a plain regex.
uint_set m_view_vars;
// the SAT leaf and its owning graph, captured in init() for view witnesses.
seq::nielsen_graph* m_nielsen = nullptr;
seq::nielsen_node const* m_sat_node = nullptr;
public:
seq_model(ast_manager& m, context& ctx, seq_util& seq,
seq_rewriter& rw, euf::sgraph& sg);