From bf3117840e143458b04956847e0e2e68945bf8b9 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 20 Jul 2026 19:13:36 +0200 Subject: [PATCH] Some more tests for seq_monadic Bug fix in seq_monadic Update benchmark script --- scripts/compare_seq_solvers.py | 5 +- src/ast/rewriter/seq_monadic.cpp | 8 ++- src/test/seq_monadic.cpp | 102 +++++++++++++++++++++++++++++++ 3 files changed, 112 insertions(+), 3 deletions(-) diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py index 47133c4cd8..3f547f49ab 100644 --- a/scripts/compare_seq_solvers.py +++ b/scripts/compare_seq_solvers.py @@ -3,7 +3,8 @@ Compare z3 string solver configurations, and optionally against external solvers. We always run three z3 configurations: - nseq_md monadic decomposition (parikh off, eager regex factorization) + nseq_md monadic decomposition (parikh off, lazy regex factorization) + nseq_md2 monadic decomposition via automaton (parikh off, lazy regex factorization via automaton) nseq_pa parikh (parikh on, no regex factorization) seq the old/baseline string solver @@ -38,6 +39,8 @@ COMMON_ARGS = ["model_validate=true"] 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=false", "smt.nseq.regex_dynamic_decomposition=false"], + "nseq_md2": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false", + "smt.nseq.monadic_split=true", "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "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_dynamic_decomposition=true"], "seq": ["smt.string_solver=seq"], diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index c5d3339c41..1bf12d96f7 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -133,8 +133,12 @@ namespace seq { svector tgts; // snapshot: local_of may realloc m_gsucc for (gedge const& e : m_gsucc[gid]) tgts.push_back(e.target); - for (unsigned t : tgts) - succ[i].push_back(local_of(m_gstate[t])); + for (unsigned t : tgts) { + // hoist local_of out of the subscript: it may push_back onto succ + // (reallocating it), which would dangle a succ[i] taken first. + unsigned li = local_of(m_gstate[t]); + succ[i].push_back(li); + } } } diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 2161ed79b5..2af12ca6d4 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -57,6 +57,9 @@ class seq_monadic_test { return expr_ref(re().mk_range(u.str.mk_string(zstring(sl)), u.str.mk_string(zstring(sh))), m); } expr_ref loop(expr* r, unsigned lo, unsigned hi) { return expr_ref(re().mk_loop(r, lo, hi), m); } + expr_ref plus(expr* a) { return cat(a, star(a)); } + expr_ref inter2(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); } + expr_ref eps() { return expr_ref(re().mk_epsilon(m_str), m); } static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } @@ -83,6 +86,23 @@ class seq_monadic_test { << " got=" << s(got) << " expected=" << s(expected) << "\n"; } + // Enumerate the midpoints of sigma(r); report count and whether the shared + // midpoint of each split pair agrees (left.second == right.first). + unsigned split_count(expr* r, bool& failed, bool& consistent) { + seq::split sp = m_sm.mk_split(r); + seq::split_iterator it = sp.begin(); + failed = it.failed(); + consistent = true; + unsigned count = 0; + for (; it != sp.end(); ++it) { + seq::split_pair pr = *it; + if (pr.first.second.get() != pr.second.first.get()) + consistent = false; + ++count; + } + return count; + } + public: seq_monadic_test() : m_reg(m), m_rw(m), m_sm(m_rw), u(m), m_str(m), m_re(m) { m_str = u.str.mk_string_sort(); @@ -115,6 +135,28 @@ public: check("L3-03 nested complement ", inter({ comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))) }, 0, UINT_MAX), l_true); + // concrete words + check("abc & abc ", inter({ word("abc"), word("abc") }, 0, UINT_MAX), l_true); + check("abc & abd ", inter({ word("abc"), word("abd") }, 0, UINT_MAX), l_false); + check("abc & S*cS* ", inter({ word("abc"), cat(sig, cat(word("c"), sig)) }, 0, UINT_MAX), l_true); + check("abc & S*zS* ", inter({ word("abc"), cat(sig, cat(word("z"), sig)) }, 0, UINT_MAX), l_false); + // epsilon vs star / plus + check("eps & a* ", inter({ eps(), star(a) }, 0, UINT_MAX), l_true); + check("eps & a+ ", inter({ eps(), plus(a) }, 0, UINT_MAX), l_false); + check("a+ & a* ", inter({ plus(a), star(a) }, 0, UINT_MAX), l_true); + // unions + check("(a|b) & (b|c) ", inter({ alt(a, b), alt(b, word("c")) }, 0, UINT_MAX), l_true); + check("(a|b) & (c|d) ", inter({ alt(a, b), alt(word("c"), word("d")) }, 0, UINT_MAX), l_false); + // complement fundamentals + check("~empty (= S*) ", inter({ comp(none()) }, 0, UINT_MAX), l_true); + check("~(a*) ", inter({ comp(star(a)) }, 0, UINT_MAX), l_true); + check("(a|b)* & ~((a|b)*) ", inter({ star(alt(a, b)), comp(star(alt(a, b))) }, 0, UINT_MAX), l_false); + check("a* & ~(a*) ", inter({ star(a), comp(star(a)) }, 0, UINT_MAX), l_false); + check("~(a*) | a* (= S*) ", inter({ alt(comp(star(a)), star(a)) }, 0, UINT_MAX), l_true); + // three-way intersections + check("a* & (a|b)* & S*aS* ", inter({ star(a), star(alt(a, b)), cat(sig, cat(a, sig)) }, 0, UINT_MAX), l_true); + check("a* & b* & S*aS* ", inter({ star(a), star(b), cat(sig, cat(a, sig)) }, 0, UINT_MAX), l_false); + std::cout << "=== split_manager::intersect (length bounds) ===\n"; check("[0-9]+ length 0..0 ", inter({ digitp }, 0, 0), l_false); check("[0-9]+ length 1..1 ", inter({ digitp }, 1, 1), l_true); @@ -122,6 +164,22 @@ public: check("a* & b* length 3..3 ", inter({ star(a), star(b) }, 3, 3), l_false); check("[0-9]{2} & [0-9]+ len 2 ", inter({ loop(rng('0','9'), 2, 2), digitp }, 2, 2), l_true); check("[0-9]{2} len 3 ", inter({ loop(rng('0','9'), 2, 2) }, 3, 3), l_false); + check("(a|b) len 1 ", inter({ alt(a, b) }, 1, 1), l_true); + check("(a|b) len 2 ", inter({ alt(a, b) }, 2, 2), l_false); + check("abc len 3 ", inter({ word("abc") }, 3, 3), l_true); + check("abc len 2 ", inter({ word("abc") }, 2, 2), l_false); + check("a* len 0 ", inter({ star(a) }, 0, 0), l_true); + // parity / counting via periodic stars + check("(aa)* len 2 ", inter({ star(cat(a, a)) }, 2, 2), l_true); + check("(aa)* len 3 ", inter({ star(cat(a, a)) }, 3, 3), l_false); + check("(aa)* len 4 ", inter({ star(cat(a, a)) }, 4, 4), l_true); + check("(aa)* & (aaa)* len 6 ", inter({ star(cat(a, a)), star(cat(a, cat(a, a))) }, 6, 6), l_true); + check("(aa)* & (aaa)* len 3 ", inter({ star(cat(a, a)), star(cat(a, cat(a, a))) }, 3, 3), l_false); + // length must both admit an 'a' and stay empty-word: contradiction at len 0 + check("a* & S*aS* len 0 ", inter({ star(a), cat(sig, cat(a, sig)) }, 0, 0), l_false); + check("[0-9]{2,4} len 3 ", inter({ loop(rng('0','9'), 2, 4) }, 3, 3), l_true); + check("[0-9]{2,4} len 5 ", inter({ loop(rng('0','9'), 2, 4) }, 5, 5), l_false); + check("[0-9]{2,4} len 1 ", inter({ loop(rng('0','9'), 2, 4) }, 1, 1), l_false); std::cout << "=== split_manager::intersect (reach, general N) ===\n"; { @@ -133,6 +191,16 @@ public: // : reached exactly after consuming one element check(" len1 ", reach(aSig, sig, 1, 1), l_true); check(" len0 ", reach(aSig, sig, 0, 0), l_false); + // via a self-loop: still on target after one step + check(" len1 ", reach(sig, sig, 1, 1), l_true); + // : a* is its own 'a'-derivative (fixpoint state) + check(" len0 ", reach(star(a), star(a), 0, 0), l_true); + check(" len1 ", reach(star(a), star(a), 1, 1), l_true); + // : the empty word already sits on the target + check(" len0 ", reach(none(), none(), 0, 0), l_true); + // : after the first 'a' the state is the S* fixpoint, so it + // stays on target for every further element (reachable at len2 too) + check(" len2 ", reach(aSig, sig, 2, 2), l_true); } std::cout << "=== split_manager::test_intersect ===\n"; @@ -142,6 +210,18 @@ public: bad.push_back(m_sm.embed(none())); check("test_intersect Sigma* ", m_sm.test_intersect(good) ? l_true : l_false, l_true); check("test_intersect empty ", m_sm.test_intersect(bad) ? l_true : l_false, l_false); + + // one-sided: a+ and b+ are disjoint but neither is *syntactically* + // empty, so the cheap check does NOT detect it (allowed false positive) + vector disjoint; + disjoint.push_back(m_sm.embed(plus(a))); + disjoint.push_back(m_sm.embed(plus(b))); + check("test_intersect a+,b+ ", m_sm.test_intersect(disjoint) ? l_true : l_false, l_true); + + // concat(empty, a) normalizes to the empty regex → detected + vector normempty; + normempty.push_back(m_sm.embed(cat(none(), a))); + check("test_intersect empty-concat", m_sm.test_intersect(normempty) ? l_true : l_false, l_false); } std::cout << "=== split midpoint iterator ===\n"; @@ -159,6 +239,28 @@ public: check("(a|b)* split not failed ", failed ? l_true : l_false, l_false); check("(a|b)* has >=1 midpoint ", count > 0 ? l_true : l_false, l_true); } + { + bool failed, consistent; + unsigned c; + // empty regex: no live states, so no midpoints (and not a failure) + c = split_count(none(), failed, consistent); + check("split(empty) not failed ", failed ? l_true : l_false, l_false); + check("split(empty) 0 midpoints ", c == 0 ? l_true : l_false, l_true); + // finite word: at least one live midpoint, all pairs consistent + c = split_count(word("a"), failed, consistent); + check("split(a) not failed ", failed ? l_true : l_false, l_false); + check("split(a) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + check("split(a) consistent ", consistent ? l_true : l_false, l_true); + // epsilon: the (single, nullable) start state is a live midpoint + c = split_count(eps(), failed, consistent); + check("split(eps) not failed ", failed ? l_true : l_false, l_false); + check("split(eps) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + // ground finite word a.b.c (concat form): several live midpoints + c = split_count(cat(a, cat(b, word("c"))), failed, consistent); + check("split(a.b.c) not failed ", failed ? l_true : l_false, l_false); + check("split(a.b.c) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + check("split(a.b.c) consistent ", consistent ? l_true : l_false, l_true); + } std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " (" << m_fail << " fail) ===\n";