mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-17 04:25:44 +00:00
Code Activity

split-set checkpoint

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-02 11:14:05 -07:00
parent 2e5f1b1d69
commit 361e0fba75
5 changed files with 367 additions and 1423 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -134,7 +134,6 @@ 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;
@ -334,7 +333,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_split(*this), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m),
m_util(m), m_subset(m_util.re), 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) {
}
@ -413,22 +412,9 @@ 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,
const split_mode 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); }
bool is_subset(expr *r1, expr *r2) const;
// decompose a membership constraint into a set of pairs of regex splits
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);
}
/**
* check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
*/

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

File diff suppressed because it is too large Load diff

216
src/ast/rewriter/seq_split.h
View file

@ -36,25 +36,25 @@ class seq_rewriter;
// default) keeps everything, so sigma is unchanged. See seq_split::compute.
typedef std::function<bool(expr *D, expr *N)> split_oracle;
class split_set2 {
class split_set {
struct imp;
imp *m_imp;
class consumer;
public:
split_set2(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& oracle = split_oracle());
split_set(seq_rewriter &rw, expr *r, unsigned threshold, split_oracle const& filter);
~split_set2();
~split_set();
split_set2(split_set2 const& other);
split_set(split_set const& other);
class iterator {
struct imp;
imp *m_imp;
friend class consumer;
public:
iterator(split_set2 const& s, bool end = false);
iterator(split_set const& s, bool end = false);
~iterator();
iterator &operator++();
std::pair<expr_ref, expr_ref> operator*() const;
@ -68,209 +68,3 @@ public:
iterator begin() const;
iterator end() const;
};
// 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). This is the behaviour the nseq
// solver relies on.
// 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 };
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
seq_util& seq() const;
seq_util::rex& re() const;
// (Re)build the local declarations for `seq_sort` if not already current.
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_app1(expr *e, func_decl *d, expr *&a) const;
bool is_app2(expr *e, func_decl *d, expr*& a, expr*& b) const;
bool is_single(expr *e, expr *&d, expr *&n) const {
return is_app2(e, m_d_single, d, n);
}
bool is_fromre(expr* e, expr*& r) const {
return is_app1(e, m_d_fromre, r);
}
bool is_union (expr* e, expr*& a, expr*& b) const {
return is_app2(e, m_d_union, a, b);
}
bool is_inter (expr* e, expr*& a, expr*& b) const {
return is_app2(e, m_d_inter, a, b);
}
bool is_compl (expr* e, expr*& a) const {
return is_app1(e, m_d_compl, a);
}
bool is_lcat (expr* e, expr*& r, expr*& s) const {
return is_app2(e, m_d_lcat, r, s);
}
bool is_rcat (expr* e, expr*& s, expr*& r) const {
return is_app2(e, m_d_rcat, s, r);
}
// 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.
expr_ref expand_fromre(expr* r, bool& ok);
// 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);
// 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;
public:
explicit seq_split(seq_rewriter& rw);
// 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,
// 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;
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 into a set of pairs of regex splits
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;
};

3
src/smt/seq_regex.cpp
View file

@ -128,6 +128,8 @@ namespace smt {
return;
}
#if 0
// TODO - review
if (th.get_fparams().m_seq_regex_factorization_enabled) {
unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold;
if (threshold == 0)
@ -151,6 +153,7 @@ namespace smt {
}
// fallthrough; decomposition failed
}
#endif
// Convert a non-ground sequence into an additional regex and
// strengthen the original regex constraint into an intersection

607
src/test/seq_split.cpp
View file

@ -7,7 +7,10 @@ Module Name:
Abstract:
Unit tests for the regex split engine (the split function sigma) in ast/rewriter/seq_split.cpp.
Unit tests for the regex split engine (the split function sigma) in
ast/rewriter/seq_split.cpp. The engine is exposed through split_set: a
lazily-iterated split-set constructed from a regex, a size threshold, and an
optional lookahead oracle.
Author:
@ -20,6 +23,7 @@ Author:
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_split.h"
#include "ast/rewriter/th_rewriter.h"
#include <set>
#include <utility>
@ -29,181 +33,305 @@ struct plugin_registrar {
};
class seq_split_test {
ast_manager m;
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_rewriter m_rw;
seq_util u;
sort_ref m_str; // the sequence (String) sort
sort_ref m_re; // the RegEx sort over m_str
expr_ref_vector m_pin; // keeps collected/expected AST nodes alive so that
// pointer identity (hash-consing) is stable across
// the lifetime of a single check.
seq_util::rex& re() { return u.re; }
// pin an expr so its address stays valid for later hash-cons lookups, and
// return the raw pointer used as a set key.
expr* pin(expr* e) { m_pin.push_back(e); return e; }
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 rcat(expr* a, expr* b) { return m_rw.mk_re_append(a, b); } // the engine's raw 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);
return expr_ref(re().mk_range(m_re, static_cast<unsigned>(lo), static_cast<unsigned>(hi)), 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;
// Drain sigma(r) into a set of <D, N> pairs. Returns true when the engine
// ran to a clean exhaustion, false when it gave up (threshold overrun or an
// unsupported regex). Collected nodes are pinned so that the raw pointers
// used as set keys stay valid after the split_set is destroyed.
bool collect(expr* r, pair_set& out, unsigned threshold = UINT_MAX,
split_oracle const& oracle = split_oracle()) {
split_set s(m_rw, r, threshold, oracle);
split_set::iterator it = s.begin(), end = s.end();
for (; it != end; ++it) {
auto const [d, n] = *it;
out.insert({ pin(d), pin(n) });
}
return !it.failed();
}
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();
// Cardinality of sigma(r); requires a clean exhaustion.
unsigned count(expr* r) {
pair_set s;
ENSURE(collect(r, s));
return (unsigned)s.size();
}
public:
seq_split_test() : m_reg(m), m_rw(m), m_split(m_rw), u(m), m_str(m), m_re(m) {
seq_split_test() : m_reg(m), m_rw(m), u(m), m_str(m), m_re(m), m_pin(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_epsilon() {
// sigma(eps) = { <eps, eps> }
pair_set s;
ENSURE(collect(eps(), s));
ENSURE(s == pair_set({ { eps().get(), eps().get() } }));
}
void test_eager_char() {
void test_char() {
// sigma(.) = { <eps, .>, <., eps> }
expr_ref a = dot();
split_set s;
ENSURE(eager(a, s));
pair_set s;
ENSURE(collect(a, s));
pair_set expected({ { eps().get(), a.get() }, { a.get(), eps().get() } });
ENSURE(as_set(s) == expected);
ENSURE(s == expected);
}
void test_eager_word() {
void test_word() {
// sigma("ab") = { <"", "ab">, <"a","b">, <"ab",""> }
split_set s;
ENSURE(eager(word("ab"), s));
pair_set s;
ENSURE(collect(word("ab"), s));
pair_set expected({
{ word("").get(), word("ab").get() },
{ word("a").get(), word("b").get() },
{ word("ab").get(), word("").get() },
{ word("").get(), word("ab").get() },
{ word("a").get(), word("b").get() },
{ word("ab").get(), word("").get() },
});
ENSURE(as_set(s) == expected);
ENSURE(s == expected);
}
void test_eager_union() {
void test_empty_word() {
// sigma(to_re("")) = { <"", ""> } (a single, trivial split)
pair_set s;
ENSURE(collect(word(""), s));
ENSURE(s == pair_set({ { word("").get(), word("").get() } }));
}
void test_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 s;
ENSURE(collect(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);
ENSURE(s == expected);
}
void test_agree_all() {
void test_full_seq() {
// sigma(.*) = { <.*, .*> }
expr_ref ds = dotstar();
pair_set s;
ENSURE(collect(ds, s));
ENSURE(s == pair_set({ { ds.get(), ds.get() } }));
}
void test_bottom() {
// sigma(empty) = {}
pair_set s;
ENSURE(collect(empty_re(), s));
ENSURE(s.empty());
}
void test_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);
pair_set s;
ENSURE(collect(as, s));
pair_set expected({
{ eps().get(), eps().get() },
{ rcat(as, eps()).get(), rcat(a, as).get() },
{ rcat(as, a).get(), rcat(eps(), as).get() },
});
ENSURE(s == expected);
}
void test_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);
pair_set s;
ENSURE(collect(ap, s));
pair_set expected({
{ rcat(as, eps()).get(), rcat(a, as).get() },
{ rcat(as, a).get(), rcat(eps(), as).get() },
});
ENSURE(s == expected);
}
void test_concat_content() {
// sigma(a.b): the engine drops the epsilon-suffix split from the left
// side (it is language-equivalent to a right-side split), giving
// { <eps, a.b>, <a.eps, b>, <a.b, eps> }
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);
expr_ref ab(re().mk_concat(a, b), m);
pair_set s;
ENSURE(collect(ab, s));
pair_set expected({
{ eps().get(), rcat(a, b).get() }, // <eps, a.b>
{ rcat(a, eps()).get(), b.get() }, // <a.eps, b>
{ rcat(a, b).get(), eps().get() }, // <a.b, eps>
});
ENSURE(s == expected);
}
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_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(count(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(count(c3) >= 4);
}
void test_intersection() {
// The engine handles intersection via the split algebra (De Morgan-free
// product). It must run to completion and produce a non-empty set.
expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')),
re().mk_star(rng('b', 'b'))), m);
pair_set s;
ENSURE(collect(inter, s));
ENSURE(!s.empty());
}
void test_complement() {
// strong-mode De Morgan complement
expr_ref compl_(re().mk_complement(re().mk_star(rng('a', 'a'))), m);
pair_set s;
ENSURE(collect(compl_, s));
ENSURE(!s.empty());
}
void test_diff() {
// sigma(a* \ b*) via intersection with the complement
expr_ref diff(re().mk_diff(re().mk_star(rng('a', 'a')),
re().mk_star(rng('b', 'b'))), m);
pair_set s;
ENSURE(collect(diff, s));
ENSURE(!s.empty());
}
void test_nested_complement() {
// sigma(~~(a*)) must still terminate cleanly
expr_ref cc(re().mk_complement(re().mk_complement(re().mk_star(rng('a', 'a')))), m);
pair_set s;
ENSURE(collect(cc, s));
}
void test_determinism() {
// Two independent runs over the same regex yield the identical set.
expr_ref r(re().mk_concat(rng('a', 'a'), re().mk_star(rng('b', 'b'))), m);
pair_set s1, s2;
ENSURE(collect(r, s1));
ENSURE(collect(r, s2));
ENSURE(s1 == s2);
}
void test_threshold_boundary() {
expr_ref as(re().mk_star(rng('a', 'a')), m); // exactly 3 splits
unsigned k = count(as);
ENSURE(k == 3);
pair_set ok;
ENSURE(collect(as, ok, k)); // at threshold: fine
pair_set bad;
ENSURE(!collect(as, bad, k - 1)); // one below threshold: give up
}
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));
// a* has 3 splits; capping at 1 forces a give-up.
expr_ref as(re().mk_star(rng('a', 'a')), m);
pair_set s;
ENSURE(!collect(as, s, /*threshold*/ 1));
}
void test_weak_vs_strong() {
expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m);
expr_ref compl_(re().mk_complement(re().mk_star(dot())), m);
split_set s;
ENSURE(!eager(inter, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(!lazy(inter, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak));
s.reset();
ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak));
// strong mode succeeds for both
s.reset();
ENSURE(eager(inter, s, UINT_MAX, split_mode::strong));
s.reset();
ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong));
void test_early_stop() {
// Pull exactly one split on demand, then walk away. Stopping early is
// not a give-up, even when the full set is larger.
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits
split_set s(m_rw, as, UINT_MAX, {});
split_set::iterator it = s.begin(), end = s.end();
unsigned seen = 0;
if (it != end) {
(void)*it;
++seen;
}
ENSURE(seen == 1);
ENSURE(!it.failed()); // early stop is not a failure
}
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_early_stop_after_two() {
// Pull two splits on demand, then stop.
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits
split_set s(m_rw, as, UINT_MAX, {});
split_set::iterator it = s.begin(), end = s.end();
unsigned seen = 0;
while (seen < 2 && it != end) {
(void)*it;
++it;
++seen;
}
ENSURE(seen == 2);
ENSURE(!it.failed());
}
void test_iterator_exhaustion() {
// Pull every split on demand; failed() must stay false on a clean
// exhaustion, and end() must remain end() once drained.
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits
split_set s(m_rw, as, UINT_MAX, {});
split_set::iterator it = s.begin(), end = s.end();
unsigned seen = 0;
for (; it != end; ++it) {
(void)*it;
++seen;
}
ENSURE(seen == 3);
ENSURE(!it.failed());
// idempotent past the end
ENSURE(it == end);
ENSURE(!it.failed());
}
void test_iterator_giveup() {
// A threshold overrun aborts: the iterator reaches end() with failed().
expr_ref as(re().mk_star(rng('a', 'a')), m); // 3 splits, cap at 1
split_set s(m_rw, as, 1, {});
split_set::iterator it = s.begin(), end = s.end();
unsigned seen = 0;
for (; it != end; ++it) {
(void)*it;
++seen;
}
ENSURE(it.failed()); // aborted, not a clean exhaustion
ENSURE(seen <= 1); // produced at most the capped number
}
void test_oracle_prunes() {
@ -213,233 +341,46 @@ public:
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 Boolean closure is likewise a give-up.
expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m);
expr_ref inode = m_split.make(inter);
ENSURE(inode);
seq_split::iterator wit = m_split.iterate(inode, 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));
}
pair_set s;
ENSURE(collect(a, s, UINT_MAX, keep_eps_suffix));
ENSURE(s == pair_set({ { a.get(), e.get() } }));
}
void test_trivial_oracle() {
// An oracle that keeps everything leaves sigma unchanged.
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));
pair_set s_no, s_yes;
ENSURE(collect(r, s_no));
ENSURE(collect(r, s_yes, UINT_MAX, keep_all));
ENSURE(s_no == 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_epsilon();
test_char();
test_word();
test_empty_word();
test_union();
test_full_seq();
test_bottom();
test_star_content();
test_plus_content();
test_concat_content();
test_nary_union();
test_nary_concat();
test_intersection();
test_complement();
test_diff();
test_nested_complement();
test_determinism();
test_threshold_boundary();
test_threshold_giveup();
test_early_stop();
test_early_stop_after_two();
test_iterator_exhaustion();
test_iterator_giveup();
test_simplify();
test_oracle_prunes();
test_trivial_oracle();
}
};