mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

split-sets as a standalone rewriter module

Browse source
This commit is contained in:
CEisenhofer 2026-08-06 18:51:54 -07:00
parent 9695ceafbc
commit 882925f876
7 changed files with 1824 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -41,6 +41,7 @@ z3_add_component(rewriter
seq_axioms.cpp
seq_eq_solver.cpp
seq_derive.cpp
seq_split.cpp
seq_subset.cpp
seq_derive.cpp
seq_monadic.cpp

35
src/ast/rewriter/seq_rewriter.h
View file

@ -25,6 +25,7 @@ Notes:
#include "ast/rewriter/rewriter_types.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/seq_subset.h"
#include "ast/rewriter/seq_split.h"
#include "util/params.h"
#include "util/lbool.h"
#include "util/sign.h"
@ -125,6 +126,7 @@ class seq_rewriter {
seq_util m_util;
seq_subset m_subset;
seq_split m_split;
arith_util m_autil;
bool_rewriter m_br;
seq::derive m_derive;
@ -324,7 +326,7 @@ class seq_rewriter {
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m),
m_util(m), m_subset(m_util.re), m_split(*this), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m) {
}
@ -391,6 +393,37 @@ public:
return result;
}
// Split decomposition (sigma) of a regex; see seq_split.h. `oracle` (optional)
// prunes non-viable splits during generation.
bool split(expr* r, split_set& out, unsigned threshold,
split_mode const mode = split_mode::strong, split_oracle const& oracle = {}) {
return m_split.compute(r, out, threshold, mode, oracle);
}
void simplify_split(split_set& s) { m_split.simplify(s); }
// Build the *suspended* sigma(r) split-set term (no expansion); drive it with
// iterate_split. Returns null on a non-regex argument. See seq_split.h.
expr_ref make_split(expr* r) { return m_split.make(r); }
// Create a lazy enumerator over a suspended split-set `node` (typically the
// result of make_split()). See seq_split::iterator for the arguments.
seq_split::iterator iterate_split(expr* node, unsigned threshold,
split_mode const mode = split_mode::strong,
split_oracle const& oracle = {}) {
return m_split.iterate(node, mode, threshold, oracle);
}
// Decompose a membership constraint into a boundary (head, tail) and a set of
// regex splits; see seq_split::split_membership.
std::pair<expr_ref, expr_ref> split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const {
return m_split.split_membership(str, regex, threshold, result);
}
// split-algebra performance counters
split_stats const& get_split_stats() const { return m_split.stats(); }
void reset_split_stats() { m_split.reset_stats(); }
/*
* Construct r1 XOR r2 applying the structural rewrites in
* mk_re_xor (r XOR r = empty, comp/empty/full normalisation, AC

1030
src/ast/rewriter/seq_split.cpp Normal file
View file

File diff suppressed because it is too large Load diff

297
src/ast/rewriter/seq_split.h Normal file
View file

@ -0,0 +1,297 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_split.h
Abstract:
Regex split decomposition: the split function sigma from the paper
"Solving by Splitting". For a regular expression r, sigma(r) is a finite
"split-set" of pairs { <D_i, N_i> } such that
u.v in L(r) iff exists i: u in L(D_i) and v in L(N_i).
The split algebra (intersection, De Morgan complement, left/right
concatenation with a regex) and the cardinality-reducing simplification
heuristics (drop bottom, same-D/same-N merge, subsumption via seq_subset)
follow the paper.
Author:
Clemens Eisenhofer 2026-6-10
--*/
#pragma once
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_subset.h"
#include "util/obj_hashtable.h"
#include <functional>
class seq_rewriter;
// An individual split <D, N>: the left (prefix) regex D and right (suffix)
// regex N. u.v in L(r) for this split iff u in L(D) and v in L(N).
struct split_pair {
expr_ref m_d;
expr_ref m_n;
split_pair(expr* d, expr* n, ast_manager& m) : m_d(d, m), m_n(n, m) {
SASSERT(d && n);
}
};
// A split-set is a union of individual splits.
typedef vector<split_pair> split_set;
// Controls how aggressively sigma expands the Boolean-closure cases:
// strong - fully expand complement / intersection via the split algebra
// (De Morgan / cross product).
// weak - do not perform the (potentially 2^k) Boolean-closure expansion;
// give up (return false) on complement / intersection instead.
enum class split_mode { weak, strong };
// Optional lookahead oracle. Called for each candidate split <D, N> as it is
// generated; returns true to keep it, false to prune it. An empty oracle (the
// default) keeps everything, so sigma is unchanged. See seq_split::compute.
typedef std::function<bool(expr* D, expr* N)> split_oracle;
// Lightweight performance counters for the split algebra (behaviour-neutral;
// read via seq_rewriter::get_split_stats). See seq_split.cpp for where each fires.
struct split_stats {
unsigned m_make = 0; // make(): suspended sigma(r) built
unsigned m_sigma_expand = 0; // expand_fromre(): one sigma rule level
unsigned m_materialize = 0; // materialize(): a split-set drained
unsigned m_splits = 0; // splits produced by iterator::next()
unsigned m_pushes = 0; // candidate <D,N> offered to push()
unsigned m_oracle_prunes = 0; // candidates dropped by the lookahead oracle
unsigned m_intersect = 0; // intersect() calls
unsigned m_intersect_pairs = 0; // pairs formed by intersect() cross-products
unsigned m_complement = 0; // complement() calls
unsigned m_giveups = 0; // iterator give-ups (unsupported/weak/overrun)
unsigned m_threshold_overruns = 0; // threshold hits (intersect/complement/iterator)
unsigned m_max_split_set = 0; // largest materialized split-set seen
unsigned m_dedup_drops = 0; // duplicate <D,N> pairs skipped in intersect
unsigned m_simplify = 0; // simplify() calls
void reset() { *this = split_stats(); }
};
class seq_split {
ast_manager& m;
seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access
seq_subset m_subset; // language-subset checks for subsumption
// --- Suspended split-set representation -------------------------------
// A split-set computation is kept as an `expr` term over a small family of
// locally-declared, uninterpreted function symbols (the split algebra of the
// paper / split-algebra.md). Nothing here is ever asserted to the solver;
// the terms are only used as scratch structure to drive lazy expansion.
//
// empty : SplitSet -- {} (bottom)
// single : Re x Re -> SplitSet -- a single split <D, N>
// from_re : Re -> SplitSet -- the *suspended* sigma(r)
// union : SplitSet x SplitSet -> SplitSet
// inter : SplitSet x SplitSet -> SplitSet
// compl : SplitSet -> SplitSet
// lcat : Re x SplitSet -> SplitSet -- r . S (left-concat onto D)
// rcat : SplitSet x Re -> SplitSet -- S . r (right-concat onto N)
sort* m_seq_sort = nullptr; // sequence sort the decls are built for
sort_ref m_set_sort; // the uninterpreted SplitSet sort
func_decl_ref m_d_empty, m_d_single, m_d_fromre, m_d_union,
m_d_inter, m_d_compl, m_d_lcat, m_d_rcat;
expr_ref m_empty_app; // cached nullary `empty` term
mutable split_stats m_stats; // performance counters (see -st)
seq_util& seq() const;
seq_util::rex& re() const;
// (Re)build the local declarations for `seq_sort` if not already current.
// NB: rebuilding for a new sequence sort invalidates suspended split-set
// terms built for the previous sort (head_normalize degrades to a give-up
// on such stale terms); an iterator must not be used across a sort switch.
void ensure_decls(sort* seq_sort);
// Smart constructors: apply the cheap normalizations the eager engine relies
// on (drop-bottom, eps cancellation, union absorption of empty).
expr_ref mk_empty();
expr_ref mk_single(expr* d, expr* n);
expr_ref mk_fromre(expr* r);
expr_ref mk_union(expr* a, expr* b);
expr_ref mk_inter(expr* a, expr* b);
expr_ref mk_compl(expr* a);
expr_ref mk_lcat(expr* r, expr* s);
expr_ref mk_rcat(expr* s, expr* r);
// Recognizers over the local decls.
bool is_empty_ss(expr* e) const;
bool is_single(expr* e, expr*& d, expr*& n) const;
bool is_fromre(expr* e, expr*& r) const;
bool is_union (expr* e, expr*& a, expr*& b) const;
bool is_inter (expr* e, expr*& a, expr*& b) const;
bool is_compl (expr* e, expr*& a) const;
bool is_lcat (expr* e, expr*& r, expr*& s) const;
bool is_rcat (expr* e, expr*& s, expr*& r) const;
// A term whose head is empty | single | union (ready for the worklist loop).
bool is_frontier(expr* e) const;
// One level of the sigma rules: from_re(r) -> a SplitSet term built from the
// immediate subterms. `ok` is set false on an unsupported shape or on a
// loop bound exceeding `threshold` (the loop rule unfolds eagerly into one
// branch per copy, so it must be capped before allocation).
expr_ref expand_fromre(expr* r, unsigned threshold, bool& ok, obj_hashtable<expr>& deriv_memo);
// Build the single-character regex for a cofactor path condition `pred` (a
// Boolean over the character (:var 0)). Prefer a canonical range /
// union-of-ranges (see seq::range_predicate_to_regex); fall back to
// of_pred(lambda) only for predicates outside the recognized range fragment.
expr_ref mk_charclass_re(expr* pred, sort* seq_sort);
// r == E(r) | RE(LF(delta(r))): build the suspended split-set for `r` by
// peeling one character through the symbolic derivative (Brzozowski cofactors)
// and recursing. Used for complement and intersection to avoid the De Morgan
// / cross-product blow-up. Records `r` in `deriv_memo` (cycle guard). Returns
// a null expr_ref when nullability of `r` is not statically decidable.
expr_ref try_derivative_split(expr* r, sort* seq_sort, obj_hashtable<expr>& deriv_memo);
// Distribute a left/right concatenation over a head-normal split-set.
expr_ref distribute_lcat(expr* r, expr* hs);
expr_ref distribute_rcat(expr* hs, expr* r);
// Materialized split-set -> a `union` of `single`s.
expr_ref from_split_set(split_set const& s);
// Reduce `t` until its head is empty | single | union (one outermost level
// for the lazy nodes; inter/compl are expanded eagerly via `materialize`,
// since the paper's De Morgan / cross-product cannot yield a split lazily).
// `ok` is set false on a give-up (unsupported shape, weak-mode Boolean, or
// threshold overrun).
expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold,
split_oracle const& oracle, bool& ok,
obj_hashtable<expr>& deriv_memo);
// Fully drain a suspended split-set into `out` (used for inter/compl bodies).
// Runs an `iterator` to exhaustion; returns false on a give-up.
bool materialize(expr* node, split_mode mode, unsigned threshold,
split_oracle const& oracle, split_set& out);
// Push <d, n> onto `out`, unless `oracle` rejects it.
void push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const;
// S1 cap S2 = { <D1 cap D2, N1 cap N2> } dropping any pair with a bottom
// component (and any rejected by `oracle`). Returns false on threshold overrun.
bool intersect(split_set const& s1, split_set const& s2, split_set& result,
unsigned threshold, split_oracle const& oracle) const;
// De Morgan complement of a split-set: ~S = cap_{s in S} ~s with
// ~<D,N> = { <~D, .*>, <.*, ~N> } and ~{} = { <.*, .*> }.
bool complement(sort* seq_sort, split_set const& sp, split_set& result,
unsigned threshold, split_oracle const& oracle) const;
// same-D / same-N merge: groups pairs that share a (syntactically identical)
// left (resp. right) component and unions the other component.
void merge_by(split_set& pairs, bool by_left) const;
// Cap on the split-sets materialized for the *Boolean-closure* cases
// (intersection / complement), which cannot be produced lazily and are
// therefore drained in full inside head_normalize. This is a different
// quantity from the caller's `threshold`, which bounds how many splits the
// lazy enumeration may EMIT and is typically huge (a consumer walking the
// splits one at a time may legitimately want arbitrarily many). Reusing
// that value here let the De Morgan fold -- whose `acc` is intersected with a
// 2-element set per element, hence doubles -- run to 2^20 pairs before
// aborting, which is several seconds of pure waste. Overrunning this cap is
// a give-up, so the caller falls through to its other rules; that is sound
// and strictly better than the hang.
static const unsigned BOOL_CLOSURE_CAP = 256;
public:
explicit seq_split(seq_rewriter& rw);
// Performance counters.
split_stats const& stats() const { return m_stats; }
void reset_stats() { m_stats.reset(); }
// Lazy split enumerator. Holds the suspended split-set worklist and produces
// the concrete splits <D, N> one at a time, on demand, instead of computing
// them all up front. Obtain one from seq_split::iterate (or construct it
// directly) and pull splits with next() until it returns false; gave_up() then
// tells a normal exhaustion (false) apart from a give-up (true).
//
// The threshold is supplied by the caller and serves only as a safety cap
// against space bloat (lazy expansion still has to materialize the operands of
// intersection / complement). A threshold overrun, an unsupported regex shape,
// a loop bound exceeding the threshold, or a Boolean-closure case in weak mode
// aborts the enumeration: next() returns false and gave_up() returns true.
// To stop early, simply stop calling next().
//
// `oracle` (optional) prunes non-viable splits as they are produced. It must
// be sound to apply per split: a candidate N can still gain a prefix from a
// factor appended to its right later (concat/star), so the oracle must use a
// "prefix-compatible" test (prune only when N can never match the lookahead,
// even partially), NOT a strict "starts-with" test. The complement body is
// expanded WITHOUT the oracle (inverted orientation); the oracle is re-applied
// to the complement's output fold.
class iterator {
seq_split& m_engine;
ast_manager& m;
split_mode m_mode;
unsigned m_threshold;
split_oracle m_oracle;
expr_ref_vector m_work; // GC-safe worklist of suspended split-sets
unsigned m_count = 0; // splits produced so far (vs. threshold)
bool m_giveup = false;
// Complement ~-regex states already expanded via the symbolic-derivative
// rule; re-encountering one (a cycle) falls back to the De Morgan rule so
// the lazy unfolding terminates. Per-iterator (iterators run concurrently).
obj_hashtable<expr> m_deriv_memo;
public:
iterator(seq_split& engine, expr* node, split_mode mode,
unsigned threshold, split_oracle oracle);
// Compute the next split. On success returns true and sets <d, n>; on
// exhaustion or give-up returns false (see gave_up()). Calling next()
// again after it has returned false keeps returning false.
bool next(expr_ref& d, expr_ref& n);
// Valid after next() has returned false: true iff the enumeration aborted
// (unsupported regex / weak-mode Boolean / threshold overrun) rather than
// running out of splits.
bool gave_up() const { return m_giveup; }
};
// Build the *suspended* sigma(r) as a split-algebra term (no expansion).
// Returns null on a non-regex argument. Drive it with `iterate`.
expr_ref make(expr* r);
// Create a lazy enumerator over a suspended split-set `node` (typically the
// result of make()). See `iterator` for the meaning of the arguments.
iterator iterate(expr* node, split_mode mode, unsigned threshold,
split_oracle const& oracle = {});
// Compute sigma(r), appending to `out` (does not clear it). Thin eager
// wrapper that drains an `iterator` to exhaustion; semantics match the historic
// engine. See `iterator` for the meaning of `threshold`, `mode`, and `oracle`.
bool compute(expr* r, split_set& out, unsigned threshold,
split_mode mode = split_mode::strong, split_oracle const& oracle = {});
// In-place simplification of a split-set: drop bottom components, apply the
// same-D / same-N merge rules, and drop splits subsumed by another (using
// seq_subset). Size-capped to keep the O(n^2) subsumption affordable.
void simplify(split_set& s) const;
// Decompose a membership constraint `str in regex` into a boundary
// (head, tail) with str = head . c . tail (c a constant run consumed into
// the splits by derivatives) and a split-set such that the membership
// holds iff head in D and tail in N for some <D, N> in `result`.
// A null head signals a give-up (threshold / unsupported shape). An
// entirely-constant `str` is fully consumed by derivatives and returns
// ("", "") with the single split <eps, derivative-consumed regex>.
std::pair<expr_ref, expr_ref> split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const;
// Lookahead oracle for the split engine: is the split's right component
// `n_regex` prefix-compatible with the constant character sequence `c`?
// This is sound to apply during split generation — it never drops a viable split.
// Thus, it might not eliminate all cases in order to stay sound
bool split_lookahead_viable(expr* regex, zstring const& c) const;
};

1
src/test/CMakeLists.txt
View file

@ -133,6 +133,7 @@ add_executable(test-z3
scoped_vector.cpp
seq_rewriter.cpp
seq_monadic.cpp
seq_split.cpp
seq_monadic_bench.cpp
simple_parser.cpp
scanner_io.cpp

1
src/test/main.cpp
View file

@ -117,6 +117,7 @@
X(regex_range_collapse) \
X(seq_rewriter) \
X(seq_monadic) \
X(seq_split) \
X(seq_monadic_bench) \
X(check_assumptions) \
X(smt_context) \

460
src/test/seq_split.cpp Normal file
View file

@ -0,0 +1,460 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_split.cpp
Abstract:
Unit tests for the regex split engine (the split function sigma) in ast/rewriter/seq_split.cpp.
Author:
Clemens Eisenhofer 2026-6-22
--*/
#include "ast/ast.h"
#include "ast/reg_decl_plugins.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_split.h"
#include <set>
#include <utility>
struct plugin_registrar {
plugin_registrar(ast_manager& m) { reg_decl_plugins(m); }
};
class seq_split_test {
ast_manager m;
plugin_registrar m_reg;
seq_rewriter m_rw;
seq_split m_split;
seq_util u;
sort_ref m_str; // the sequence (String) sort
sort_ref m_re; // the RegEx sort over m_str
seq_util::rex& re() { return u.re; }
expr_ref eps() { return expr_ref(re().mk_epsilon(m_str), m); } // mk_epsilon takes the seq sort
expr_ref dot() { return expr_ref(re().mk_full_char(m_re), m); } // mk_full_char takes the RegEx sort
expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } // .*
expr_ref empty_re() { return expr_ref(re().mk_empty(m_re), m); } // the bottom regex
expr_ref rappend(expr* a, expr* b) { return m_rw.mk_re_append(a, b); } // the engine's regex concat
expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); }
expr_ref rng(char lo, char hi) {
return expr_ref(re().mk_range(u.str.mk_string(zstring(std::string(1, lo).c_str())),
u.str.mk_string(zstring(std::string(1, hi).c_str()))), m);
}
typedef std::set<std::pair<expr*, expr*>> pair_set;
pair_set as_set(split_set const& s) {
pair_set out;
for (auto const& p : s)
out.insert({ p.m_d.get(), p.m_n.get() });
return out;
}
bool eager(expr* r, split_set& out, unsigned threshold = UINT_MAX,
split_mode mode = split_mode::strong, split_oracle const& oracle = {}) {
return m_split.compute(r, out, threshold, mode, oracle);
}
bool lazy(expr* r, split_set& out, unsigned threshold = UINT_MAX,
split_mode mode = split_mode::strong, split_oracle const& oracle = {}) {
expr_ref node = m_split.make(r);
ENSURE(node);
seq_split::iterator it = m_split.iterate(node, mode, threshold, oracle);
expr_ref d(m), n(m);
while (it.next(d, n))
out.push_back(split_pair(d, n, m));
return !it.gave_up();
}
// assert that the eager and lazy engines agree on sigma(r) as a *set* of
// splits, and report the common cardinality.
unsigned check_agree(expr* r) {
split_set se, sl;
bool oke = eager(r, se);
bool okl = lazy(r, sl);
ENSURE(oke == okl);
if (!oke)
return 0;
ENSURE(as_set(se) == as_set(sl));
return (unsigned)as_set(se).size();
}
public:
seq_split_test() : m_reg(m), m_rw(m), m_split(m_rw), u(m), m_str(m), m_re(m) {
m_str = u.str.mk_string_sort();
m_re = re().mk_re(m_str);
}
void test_eager_epsilon() {
split_set s;
ENSURE(eager(eps(), s));
ENSURE(as_set(s) == pair_set({ { eps().get(), eps().get() } }));
}
void test_eager_char() {
// sigma(.) = { <eps, .>, <., eps> }
expr_ref a = dot();
split_set s;
ENSURE(eager(a, s));
pair_set expected({ { eps().get(), a.get() }, { a.get(), eps().get() } });
ENSURE(as_set(s) == expected);
}
void test_eager_word() {
// sigma("ab") = { <"", "ab">, <"a","b">, <"ab",""> }
split_set s;
ENSURE(eager(word("ab"), s));
pair_set expected({
{ word("").get(), word("ab").get() },
{ word("a").get(), word("b").get() },
{ word("ab").get(), word("").get() },
});
ENSURE(as_set(s) == expected);
}
void test_eager_union() {
// sigma(a | b) = sigma(a) cup sigma(b)
expr_ref a = rng('a', 'a'), b = rng('b', 'b');
expr_ref u_re(re().mk_union(a, b), m);
split_set s;
ENSURE(eager(u_re, s));
pair_set expected({
{ eps().get(), a.get() }, { a.get(), eps().get() },
{ eps().get(), b.get() }, { b.get(), eps().get() },
});
ENSURE(as_set(s) == expected);
}
void test_agree_all() {
expr_ref a = rng('a', 'a'), b = rng('b', 'b');
expr_ref star(re().mk_star(a), m);
expr_ref plus(re().mk_plus(a), m);
expr_ref concat(re().mk_concat(a, b), m);
expr_ref uni(re().mk_union(a, b), m);
expr_ref inter(re().mk_inter(re().mk_star(a), re().mk_star(b)), m);
expr_ref compl_(re().mk_complement(re().mk_star(a)), m);
expr_ref diff(re().mk_diff(re().mk_star(a), re().mk_star(b)), m);
ENSURE(check_agree(eps()) == 1);
ENSURE(check_agree(a) == 2);
ENSURE(check_agree(word("ab")) == 3);
ENSURE(check_agree(uni) == 4);
ENSURE(check_agree(star) == 3); // { <eps,eps>, <a*, a.a*>, <a*.a, a*> }
(void)check_agree(plus);
(void)check_agree(concat);
(void)check_agree(inter); // strong-mode intersection
(void)check_agree(compl_); // strong-mode De Morgan complement
(void)check_agree(diff);
}
void test_lazy_early_stop() {
// a* has 3 splits; pull just the first one and then stop. (Note .* is the
// full_seq special case with a single split, so use a proper char-class body.)
expr_ref star(re().mk_star(rng('a', 'a')), m);
expr_ref node = m_split.make(star);
ENSURE(node);
seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {});
expr_ref d(m), n(m);
unsigned seen = 0;
if (it.next(d, n)) // pull exactly one split, then walk away
++seen;
ENSURE(!it.gave_up()); // stopping early is not a give-up
ENSURE(seen == 1);
}
void test_threshold_giveup() {
expr_ref star(re().mk_star(rng('a', 'a')), m); // 3 splits
split_set s;
ENSURE(!lazy(star, s, /*threshold*/ 1));
// the eager wrapper honours the same cap
split_set s2;
ENSURE(!eager(star, s2, /*threshold*/ 1));
}
void test_weak_vs_strong() {
// ~(.*) is the complemented-star (~(R*)) case: it has no terminating
// derivative peel, so it falls back to the eager De Morgan node ~sigma(a),
// which weak mode refuses (producing even one split would materialize the
// operand split-set). Strong mode performs the eager De Morgan complement.
expr_ref compl_(re().mk_complement(re().mk_star(dot())), m);
// An intersection is expanded lazily through the symbolic derivative
// r = E(r) | RE(LF(delta(r))) (delta distributes over &): one character
// peel, no operand materialization, so weak mode now handles it too.
expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m);
split_set s;
ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); // De Morgan node: weak refuses
s.reset();
ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); // strong: eager De Morgan
// intersection is derivative-expanded (lazy): succeeds in BOTH modes
s.reset();
ENSURE(eager(inter, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(lazy(inter, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(eager(inter, s, UINT_MAX, split_mode::strong));
}
void test_make_non_regex() {
expr_ref not_a_regex(u.str.mk_string(zstring("a")), m); // String, not RegEx
expr_ref node = m_split.make(not_a_regex);
ENSURE(!node);
}
void test_oracle_prunes() {
// sigma(.) without an oracle = { <eps,.>, <.,eps> }; an oracle that keeps
// only splits whose suffix is epsilon must drop one of the two.
expr_ref a = dot();
expr_ref e = eps();
split_oracle keep_eps_suffix = [&](expr*, expr* n) { return n == e.get(); };
split_set se, sl;
ENSURE(eager(a, se, UINT_MAX, split_mode::strong, keep_eps_suffix));
ENSURE(lazy(a, sl, UINT_MAX, split_mode::strong, keep_eps_suffix));
pair_set expected({ { a.get(), e.get() } });
ENSURE(as_set(se) == expected);
ENSURE(as_set(sl) == expected);
}
void test_eager_full_seq() {
// sigma(.*) = { <.*, .*> }
expr_ref ds = dotstar();
split_set s;
ENSURE(eager(ds, s));
ENSURE(as_set(s) == pair_set({ { ds.get(), ds.get() } }));
}
void test_eager_bottom() {
// sigma(empty) = {}
split_set s;
ENSURE(eager(empty_re(), s));
ENSURE(s.empty());
split_set sl;
ENSURE(lazy(empty_re(), sl));
ENSURE(sl.empty());
}
void test_eager_empty_word() {
// sigma(to_re("")) = { <"", ""> } (a single, trivial split)
split_set s;
ENSURE(eager(word(""), s));
ENSURE(as_set(s) == pair_set({ { word("").get(), word("").get() } }));
}
void test_eager_star_content() {
// sigma(a*) = { <eps,eps>, <a*.eps, a.a*>, <a*.a, eps.a*> }
expr_ref a = rng('a', 'a');
expr_ref as(re().mk_star(a), m);
split_set s;
ENSURE(eager(as, s));
pair_set expected({
{ eps().get(), eps().get() },
{ rappend(as, eps()).get(), rappend(a, as).get() },
{ rappend(as, a).get(), rappend(eps(), as).get() },
});
ENSURE(as_set(s) == expected);
}
void test_eager_plus_content() {
// sigma(a+) = a*.sigma(a).a* (the star rule without <eps,eps>)
expr_ref a = rng('a', 'a');
expr_ref as(re().mk_star(a), m);
expr_ref ap(re().mk_plus(a), m);
split_set s;
ENSURE(eager(ap, s));
pair_set expected({
{ rappend(as, eps()).get(), rappend(a, as).get() },
{ rappend(as, a).get(), rappend(eps(), as).get() },
});
ENSURE(as_set(s) == expected);
}
void test_eager_concat_content() {
// sigma(a.b) = sigma(a).b cup a.sigma(b)
expr_ref a = rng('a', 'a'), b = rng('b', 'b');
expr_ref ab(re().mk_concat(a, b), m);
split_set s;
ENSURE(eager(ab, s));
pair_set expected({
{ eps().get(), rappend(a, b).get() }, // <eps, a.b>
{ a.get(), rappend(eps(), b).get() }, // <a, eps.b>
{ rappend(a, eps()).get(), b.get() }, // <a.eps, b>
{ rappend(a, b).get(), eps().get() }, // <a.b, eps>
});
ENSURE(as_set(s) == expected);
}
void test_nary_union() {
// sigma(a|b|c) has 2 splits per char-class
expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c');
expr_ref u3(re().mk_union(a, re().mk_union(b, c)), m);
ENSURE(check_agree(u3) == 6);
}
void test_nary_concat() {
// sigma(a.b.c)
expr_ref a = rng('a', 'a'), b = rng('b', 'b'), c = rng('c', 'c');
expr_ref c3(re().mk_concat(a, re().mk_concat(b, c)), m);
ENSURE(check_agree(c3) >= 4);
}
void test_nested_complement() {
// sigma(~~(a*))
expr_ref cc(re().mk_complement(re().mk_complement(re().mk_star(rng('a', 'a')))), m);
(void)check_agree(cc);
}
void test_determinism() {
expr_ref r(re().mk_concat(rng('a', 'a'), re().mk_star(rng('b', 'b'))), m);
split_set s1, s2;
ENSURE(lazy(r, s1));
ENSURE(lazy(r, s2));
ENSURE(as_set(s1) == as_set(s2));
}
void test_threshold_boundary() {
expr_ref as(re().mk_star(rng('a', 'a')), m); // exactly 3 splits
split_set s;
ENSURE(eager(as, s));
unsigned k = (unsigned)as_set(s).size();
ENSURE(k == 3);
split_set ok_e, ok_l, bad_e, bad_l;
ENSURE(eager(as, ok_e, k));
ENSURE(lazy(as, ok_l, k));
ENSURE(!eager(as, bad_e, k - 1)); // one below threshold; give up
ENSURE(!lazy(as, bad_l, k - 1));
}
void test_early_stop_after_two() {
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits
expr_ref node = m_split.make(as);
ENSURE(node);
seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {});
expr_ref d(m), n(m);
unsigned seen = 0;
while (seen < 2 && it.next(d, n)) // pull two splits on demand, then stop
++seen;
ENSURE(!it.gave_up());
ENSURE(seen == 2);
}
void test_iterator_exhaustion() {
// Pull every split on demand; gave_up() must stay false on a clean
// exhaustion, and next() must keep returning false once drained.
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits
expr_ref node = m_split.make(as);
ENSURE(node);
seq_split::iterator it = m_split.iterate(node, split_mode::strong, UINT_MAX, {});
expr_ref d(m), n(m);
unsigned seen = 0;
while (it.next(d, n))
++seen;
ENSURE(seen == 3);
ENSURE(!it.gave_up());
// idempotent past the end
ENSURE(!it.next(d, n));
ENSURE(!it.gave_up());
}
void test_iterator_giveup() {
// A threshold overrun aborts: next() returns false and gave_up() is true.
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1
expr_ref node = m_split.make(as);
ENSURE(node);
seq_split::iterator it = m_split.iterate(node, split_mode::strong, /*threshold*/ 1, {});
expr_ref d(m), n(m);
unsigned seen = 0;
while (it.next(d, n))
++seen;
ENSURE(it.gave_up()); // aborted, not a clean exhaustion
ENSURE(seen <= 1); // produced at most the capped number
// A weak-mode eager Boolean closure is likewise a give-up: ~(.*) is the
// complemented-star case with no terminating derivative peel, so it needs
// the eager De Morgan node, which weak mode refuses. (An intersection, by
// contrast, is now derivative-expanded and succeeds in weak mode.)
expr_ref cstar(re().mk_complement(re().mk_star(dot())), m);
expr_ref cnode = m_split.make(cstar);
ENSURE(cnode);
seq_split::iterator wit = m_split.iterate(cnode, split_mode::weak, UINT_MAX, {});
ENSURE(!wit.next(d, n));
ENSURE(wit.gave_up());
}
void test_simplify() {
expr_ref regs[] = {
expr_ref(re().mk_star(rng('a', 'a')), m),
expr_ref(re().mk_complement(re().mk_star(rng('a', 'a'))), m),
expr_ref(re().mk_concat(rng('a', 'a'), rng('b', 'b')), m),
};
for (auto& r : regs) {
split_set s;
ENSURE(eager(r, s));
unsigned before = (unsigned)s.size();
m_split.simplify(s);
ENSURE(s.size() <= before);
ENSURE(!s.empty());
// idempotent
split_set s2(s);
m_split.simplify(s2);
ENSURE(as_set(s) == as_set(s2));
}
}
void test_trivial_oracle() {
expr_ref r(re().mk_star(rng('a', 'a')), m);
split_oracle keep_all = [](expr*, expr*) { return true; };
split_set s_no, s_yes;
ENSURE(eager(r, s_no));
ENSURE(eager(r, s_yes, UINT_MAX, split_mode::strong, keep_all));
ENSURE(as_set(s_no) == as_set(s_yes));
}
void run() {
test_eager_epsilon();
test_eager_char();
test_eager_word();
test_eager_union();
test_agree_all();
test_lazy_early_stop();
test_threshold_giveup();
test_weak_vs_strong();
test_make_non_regex();
test_oracle_prunes();
test_eager_full_seq();
test_eager_bottom();
test_eager_empty_word();
test_eager_star_content();
test_eager_plus_content();
test_eager_concat_content();
test_nary_union();
test_nary_concat();
test_nested_complement();
test_determinism();
test_threshold_boundary();
test_early_stop_after_two();
test_iterator_exhaustion();
test_iterator_giveup();
test_simplify();
test_trivial_oracle();
}
};
void tst_seq_split() {
seq_split_test t;
t.run();
}