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

Merge remote-tracking branch 'origin/split_set' into c3

Browse source
This commit is contained in:
CEisenhofer 2026-07-20 15:04:53 +02:00
commit 386f8528b6
7 changed files with 830 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

453
src/ast/rewriter/seq_monadic.cpp Normal file
View file

@ -0,0 +1,453 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_monadic.cpp
Abstract:
Continuation-regex split service and intersection non-emptiness. See
seq_monadic.h.
Automaton-based (product/derivative reachability) and element-sort agnostic:
guard feasibility and successor states are computed entirely by the symbolic
derivative engine (seq_rewriter::brz_derivative_cofactors, which prunes
infeasible guards internally), so there is no character-specific reasoning in
this module. A single global derivative-transition graph is grown lazily and
recycled across every regex, so no derivative is computed twice. th_rewriter is
used to normalize the intersection regex.
Author:
Nikolaj Bjorner / Margus Veanes 2026
Shady parts:
- epsilon transitions appear not accounted for when computing reaching states.
If a regex R contains N by taking a set of epsilon transitions, then it is nullable relative
to N. It suggests a use for a version of nullability that is relative to N.
Deal also with when N itself has epsilon transitions to N1, .., Nk.
- witness extraction is plain wrong. It should generally rely on a choice function that takes a
Boolean expression F[(:var 0)] with a single free variable and synthesize a value for the free
variable such that the expression is true.
For character predicates we can assume that the Boolean expressions are range predicates and we can
use utilities for range predicates. For other types use some best effort, say F is of the form (= (:var 0) value).
Expose the witness function in a self-contained module outside of this file.
- checking intersections with continuation regexes is shady. The nullability check is now really about
whether there is an epsilon transition to the accepting state N. The copilot-generated code ignores this.
Generally, dealing with epsilon state is shady. There are many equivalent ways a state can be epsilon, such
as epsilon*, or comp(.+), etc.
- I don't think there should be a special case for when N is epsilon and having N being nullptr
is uneven.
The code uses "live_states" and "reaching_states" for two cases.
- The code in test_intersect shouldn't be relying on a rewriter. Anything that can be rewritten
could be done prior.
- Remove hard-wired constants such as STATE_CAP.
--*/
#include "ast/rewriter/seq_monadic.h"
#include <set>
#include <vector>
#include <climits>
namespace seq {
// ------------------------------------------------------------------
// global derivative-transition graph (shared / recycled across regexes)
// ------------------------------------------------------------------
unsigned split_manager::intern_state(expr* s) {
unsigned id;
if (m_state_id.find(s, id))
return id; // recycle the global state
id = m_gstate.size();
m_state_id.insert(s, id);
m_gstate.push_back(s);
m_pin.push_back(s);
expr_ref nb = m_rw.is_nullable(s);
m_gmaybe_null.push_back(!m.is_false(nb)); // unknown nullability => keep (conservative)
m_gexpanded.push_back(false);
m_gsucc.push_back(svector<gedge>());
return id;
}
void split_manager::expand_state(unsigned i, bool& ok) {
ok = true;
if (m_gexpanded[i])
return; // successors already computed once
if (!m.inc()) { ok = false; return; }
expr* s = m_gstate[i]; // captured before any interning realloc
expr_ref_pair_vector cof(m);
m_rw.brz_derivative_cofactors(s, cof);
svector<gedge> edges;
for (auto const& [g, t] : cof) {
if (re().is_empty(t)) continue; // engine already pruned infeasible guards
unsigned k = intern_state(t); // may realloc m_gsucc: collect edges first
m_pin.push_back(g);
edges.push_back(gedge{ g, k });
}
for (gedge const& e : edges) // m_gsucc stable now (no more interning)
m_gsucc[i].push_back(e);
m_gexpanded[i] = true;
}
// ------------------------------------------------------------------
// live-state / reachability machinery (projected out of the global graph)
// ------------------------------------------------------------------
void split_manager::build_graph(expr* R, ptr_vector<expr>& states,
vector<svector<unsigned>>& succ,
bool_vector& maybe_null, bool& ok) {
ok = true;
states.reset();
succ.reset();
maybe_null.reset();
obj_map<expr, unsigned> local; // state expr -> local index
svector<unsigned> l2g; // local index -> global id
auto local_of = [&](expr* s) -> unsigned {
unsigned li;
if (local.find(s, li)) return li;
unsigned gid = intern_state(s);
li = states.size();
local.insert(s, li);
l2g.push_back(gid);
states.push_back(s);
maybe_null.push_back(m_gmaybe_null[gid]);
succ.push_back(svector<unsigned>());
return li;
};
local_of(R);
const unsigned STATE_CAP = 1u << 12;
for (unsigned i = 0; i < states.size(); ++i) {
if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; }
unsigned gid = l2g[i];
expand_state(gid, ok);
if (!ok) return;
svector<unsigned> 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]));
}
}
void split_manager::live_states(expr* R, ptr_vector<expr>& out, bool& ok) {
ptr_vector<expr> states;
vector<svector<unsigned>> succ;
bool_vector maybe_null;
build_graph(R, states, succ, maybe_null, ok);
if (!ok) return;
unsigned n = states.size();
bool_vector live;
live.resize(n, false);
for (unsigned i = 0; i < n; ++i)
live[i] = maybe_null[i];
for (bool ch = true; ch; ) {
ch = false;
for (unsigned i = 0; i < n; ++i)
if (!live[i])
for (unsigned j : succ[i])
if (live[j]) { live[i] = true; ch = true; break; }
}
for (unsigned i = 0; i < n; ++i)
if (live[i]) out.push_back(states.get(i));
}
void split_manager::reaching_states(expr* R, expr* N, ptr_vector<expr>& out, bool& ok) {
ptr_vector<expr> states;
vector<svector<unsigned>> succ;
bool_vector maybe_null;
build_graph(R, states, succ, maybe_null, ok);
if (!ok) return;
unsigned n = states.size();
unsigned tgt = UINT_MAX;
for (unsigned i = 0; i < n; ++i)
if (states.get(i) == N) { tgt = i; break; }
if (tgt == UINT_MAX) return; // N unreachable => no midpoints
bool_vector reach;
reach.resize(n, false);
reach[tgt] = true;
for (bool ch = true; ch; ) {
ch = false;
for (unsigned i = 0; i < n; ++i)
if (!reach[i])
for (unsigned j : succ[i])
if (reach[j]) { reach[i] = true; ch = true; break; }
}
for (unsigned i = 0; i < n; ++i)
if (reach[i]) out.push_back(states.get(i));
}
// ------------------------------------------------------------------
// intersection non-emptiness
// ------------------------------------------------------------------
// A component <R_i, N_i> is a membership (nullable) component when N_i is null or
// the epsilon regex; otherwise it is a reach component with structural target N_i.
static bool is_membership(seq_util::rex& re, cont_regex const& cr) {
expr* N = cr.second.get();
return N == nullptr || re.is_epsilon(N);
}
// Flatten the operands of a (possibly nested) re.inter into `out`.
static void flatten_inter(seq_util::rex& re, expr* e, ptr_vector<expr>& out) {
expr* a = nullptr, * b = nullptr;
if (re.is_intersection(e, a, b)) {
flatten_inter(re, a, out);
flatten_inter(re, b, out);
}
else
out.push_back(e);
}
lbool split_manager::intersect(vector<cont_regex> const& crs, unsigned lo, unsigned hi,
expr_ref_vector& seq) {
seq.reset();
unsigned n = crs.size();
if (n == 0) {
// universal language: contains a word of every length; non-empty iff lo <= hi
if (lo > hi) return l_false;
for (unsigned k = 0; k < lo; ++k)
seq.push_back(m.mk_true()); // trivial guard: any element admissible
return l_true;
}
// Fast, robust path when every component is a membership (nullable) component:
// the intersection is non-empty iff some reachable product state is nullable.
bool all_memb = true;
for (auto const& cr : crs)
if (!is_membership(re(), cr)) { all_memb = false; break; }
if (all_memb)
return intersect_membership(crs, lo, hi, seq);
// General case: a tuple product search that also handles reach targets
// N != epsilon via structural target matching.
return intersect_product(crs, lo, hi, seq);
}
lbool split_manager::intersect_membership(vector<cont_regex> const& crs, unsigned lo,
unsigned hi, expr_ref_vector& seq) {
unsigned n = crs.size();
// The normalized intersection regex; the derivative engine handles guard
// feasibility and successor computation internally.
expr_ref P(crs[0].first.get(), m);
for (unsigned i = 1; i < n; ++i)
P = re().mk_inter(P, crs[i].first.get());
m_th(P);
unsigned r0 = intern_state(P.get());
// Search node with witness reconstruction: `guard` is the derivative path
// condition on the incoming edge (a predicate over the element (:var 0)).
struct node { unsigned st; unsigned depth; int parent; expr* guard; };
std::vector<node> nodes;
// Beyond `cap` elements the length no longer changes acceptance, so we cap
// the depth in the visited key to keep the state space finite.
unsigned cap = (hi == UINT_MAX) ? lo : hi;
auto key = [&](unsigned st, unsigned depth) {
return std::make_pair(st, depth < cap ? depth : cap);
};
std::set<std::pair<unsigned, unsigned>> visited;
nodes.push_back(node{ r0, 0, -1, nullptr });
visited.insert(key(r0, 0));
bool undecided = false;
for (size_t head = 0; head < nodes.size(); ++head) {
if (!m.inc()) return l_undef;
int cur = (int) head;
unsigned st = nodes[cur].st; // note: `nodes` may grow below
unsigned depth = nodes[cur].depth;
if (depth >= lo && depth <= hi && m_gmaybe_null[st]) {
expr_ref nb = m_rw.is_nullable(m_gstate[st]);
if (m.is_true(nb)) {
ptr_vector<expr> gs;
for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent)
gs.push_back(nodes[j].guard);
for (unsigned k = gs.size(); k-- > 0; )
seq.push_back(gs[k]);
return l_true;
}
if (!m.is_false(nb))
undecided = true; // undecidable nullability => cannot claim l_false
}
if (depth >= hi)
continue; // cannot extend further
bool ok = true;
expand_state(st, ok);
if (!ok) return l_undef;
for (gedge const& e : m_gsucc[st]) // no interning here => m_gsucc stable
if (visited.insert(key(e.target, depth + 1)).second)
nodes.push_back(node{ e.target, depth + 1, cur, e.guard });
}
return undecided ? l_undef : l_false;
}
lbool split_manager::intersect_product(vector<cont_regex> const& crs, unsigned lo,
unsigned hi, expr_ref_vector& seq) {
unsigned n = crs.size();
bool_vector memb; // per component: membership (nullable) vs reach
ptr_vector<expr> tgt; // per component: reach target (or null)
svector<expr*> start; // start tuple
for (auto const& cr : crs) {
bool mb = is_membership(re(), cr);
memb.push_back(mb);
tgt.push_back(mb ? nullptr : cr.second.get());
start.push_back(cr.first.get());
m_pin.push_back(cr.first.get());
if (!mb) m_pin.push_back(cr.second.get());
}
// Search node: a product tuple, its depth, its parent, and the joint guard on
// the incoming edge (a predicate over the element variable (:var 0)).
struct node { svector<expr*> st; unsigned depth; int parent; expr* guard; };
std::vector<node> nodes;
// Beyond `cap` elements the length no longer changes acceptance, so we cap the
// depth in the visited key to keep the state space finite.
unsigned cap = (hi == UINT_MAX) ? lo : hi;
auto key = [&](svector<expr*> const& st, unsigned depth) {
std::vector<unsigned> k;
k.reserve(st.size() + 1);
for (expr* e : st) k.push_back(e->get_id());
k.push_back(depth < cap ? depth : cap);
return k;
};
auto is_accept = [&](svector<expr*> const& st, bool& undecided) -> bool {
for (unsigned i = 0; i < n; ++i) {
if (memb[i]) {
expr_ref nb = m_rw.is_nullable(st[i]);
if (m.is_true(nb)) continue;
if (m.is_false(nb)) return false;
undecided = true; return false;
}
else if (st[i] != tgt[i])
return false; // reach component: structural target match
}
return true;
};
std::set<std::vector<unsigned>> visited;
nodes.push_back(node{ start, 0, -1, nullptr });
visited.insert(key(start, 0));
bool undecided = false;
for (size_t head = 0; head < nodes.size(); ++head) {
if (!m.inc()) return l_undef;
int cur = (int) head;
svector<expr*> st = nodes[cur].st; // copy: `nodes` may grow below
unsigned depth = nodes[cur].depth;
if (depth >= lo && depth <= hi) {
bool u2 = false;
if (is_accept(st, u2)) {
ptr_vector<expr> gs; // reconstruct the per-position guards
for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent)
gs.push_back(nodes[j].guard);
for (unsigned k = gs.size(); k-- > 0; )
seq.push_back(gs[k]);
return l_true;
}
if (u2) undecided = true;
}
if (depth >= hi)
continue; // cannot extend further
// Joint transitions: cofactors of inter(st_0,...,st_{n-1}). The engine
// prunes infeasible joint guards and yields the product successor as an
// re.inter in source order, which we decompose positionally.
expr_ref P(st[0], m);
for (unsigned i = 1; i < n; ++i)
P = re().mk_inter(P, st[i]);
expr_ref_pair_vector cof(m);
m_rw.brz_derivative_cofactors(P, cof);
for (auto const& [g, t] : cof) {
if (re().is_empty(t)) continue;
svector<expr*> nst;
if (n == 1)
nst.push_back(t);
else {
ptr_vector<expr> ops;
flatten_inter(re(), t, ops);
if (ops.size() != n) { // engine collapsed the product: give up soundly
undecided = true;
continue;
}
for (unsigned i = 0; i < n; ++i) nst.push_back(ops[i]);
}
for (expr* s : nst) m_pin.push_back(s);
m_pin.push_back(g);
if (visited.insert(key(nst, depth + 1)).second)
nodes.push_back(node{ nst, depth + 1, cur, g });
}
}
return undecided ? l_undef : l_false;
}
bool split_manager::test_intersect(vector<cont_regex> const& crs) {
// one-sided cheap check: an obviously-empty start (or reach target) state
// certainly makes the intersection empty. Normalize via th_rewriter first so
// that e.g. concat(empty, epsilon) collapses to the empty regex.
expr_ref tmp(m);
for (auto const& cr : crs) {
m_th(cr.first, tmp);
if (re().is_empty(tmp))
return false;
if (cr.second.get()) {
m_th(cr.second, tmp);
if (re().is_empty(tmp))
return false;
}
}
return true;
}
// ------------------------------------------------------------------
// seq::split / seq::split_iterator
// ------------------------------------------------------------------
split_iterator::split_iterator(split_manager& sm, cont_regex const& cr) {
m_sm = &sm;
m_R = cr.first.get();
m_N = cr.second.get();
bool ok = true;
bool membership = (m_N == nullptr) || sm.re().is_epsilon(m_N);
if (membership)
sm.live_states(m_R, m_mids, ok);
else
sm.reaching_states(m_R, m_N, m_mids, ok);
if (!ok) { m_failed = true; m_mids.reset(); }
}
split_pair split_iterator::operator*() const {
ast_manager& m = m_sm->mgr();
expr* mid = m_mids[m_pos];
cont_regex left(expr_ref(m_R, m), expr_ref(mid, m));
cont_regex right(expr_ref(mid, m), m_N ? expr_ref(m_N, m) : expr_ref(m));
return split_pair(left, right);
}
split_iterator& split_iterator::operator++() {
if (m_pos < m_mids.size()) ++m_pos;
return *this;
}
split::split(split_manager& sm, expr* r)
: m_sm(sm), m_R(r, sm.mgr()), m_N(sm.mgr()) {}
split::split(split_manager& sm, cont_regex const& cr)
: m_sm(sm), m_R(cr.first), m_N(cr.second) {}
split_iterator split::begin() {
return split_iterator(m_sm, cont_regex(m_R, m_N));
}
}

199
src/ast/rewriter/seq_monadic.h Normal file
View file

@ -0,0 +1,199 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_monadic.h
Abstract:
Continuation-regex split service and intersection non-emptiness for regular
expressions, following the design sketched in
paper/bench/eval/monadic-vs-nielsen-eval.md.
* A continuation regex <R, N> (seq::cont_regex) is a pair of regexes. R is
the start state and N is the accept state. A word w is accepted iff
delta_w(R) == N, with one distinguished case: when N is the epsilon regex
(the regex accepting the empty sequence) acceptance is ordinary membership
w in L(R), i.e. delta_w(R) is nullable. This is because the Brzozowski
derivative folds the epsilon tail into nullability (the epsilon state is not
structurally reachable for looping nullable regexes). Every regex R is
embedded as the continuation regex <R.epsilon, epsilon>.
* seq::split exposes, for a continuation regex, an (opaque) iterator of
seq::split_pair splits: uv in <R,N> ==> u in <R,R'> /\ v in <R',N>,
where R' ranges over the live cofactors of R that can still reach N.
* seq::split_manager owns the live-state / reachability machinery shared across
regexes, and decides emptiness of an intersection of continuation regexes.
It maintains one global derivative-transition graph and recycles the states
(and their computed nullability / cofactor successors) across every regex it
processes, so the same derivative is never recomputed.
The module is element-sort agnostic: it does NOT hard-code any character
reasoning. Guard feasibility and successor computation are delegated entirely
to the symbolic derivative engine (seq_rewriter::brz_derivative_cofactors, which
prunes infeasible guards internally and, on an re.inter, yields the product
successor in source order) and to th_rewriter for normalization.
Author:
Nikolaj Bjorner / Margus Veanes 2026
--*/
#pragma once
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "util/lbool.h"
#include "util/obj_hashtable.h"
#include "util/vector.h"
#include <utility>
namespace seq {
// A continuation regex <R, N>: start state R, accept state N. A word w is
// accepted iff delta_w(R) == N. When N is the epsilon regex (or null), the
// accept condition is ordinary membership (delta_w(R) is nullable).
typedef std::pair<expr_ref, expr_ref> cont_regex;
// A split of uv in <R,N> into u in <R,R'> and v in <R',N>.
typedef std::pair<cont_regex, cont_regex> split_pair;
class split_manager;
// Opaque, lazy iterator over the splits of a continuation regex. The internal
// state (the enumerated midpoints R') is computed on construction. `failed()`
// reports a non-ground regex or a resource limit reached while computing
// derivatives.
class split_iterator {
friend class split;
split_manager* m_sm = nullptr;
expr* m_R = nullptr; // start state of the continuation regex
expr* m_N = nullptr; // accept state (epsilon/null => membership)
ptr_vector<expr> m_mids; // enumerated live midpoints R'
unsigned m_pos = 0; // current midpoint index
bool m_failed = false; // non-ground regex / resource limit
split_iterator(split_manager& sm, cont_regex const& cr); // begin
bool at_end() const { return m_failed || m_pos >= m_mids.size(); }
public:
split_iterator() = default; // end sentinel
split_pair operator*() const;
split_iterator& operator++();
bool operator==(split_iterator const& other) const { return at_end() && other.at_end(); }
bool operator!=(split_iterator const& other) const { return !(*this == other); }
bool failed() const { return m_failed; }
};
// A continuation regex together with the manager that can split it.
class split {
split_manager& m_sm;
expr_ref m_R;
expr_ref m_N;
public:
split(split_manager& sm, expr* r);
split(split_manager& sm, cont_regex const& cr);
split_iterator begin();
split_iterator end() { return split_iterator(); }
};
// Manages live states / abstract reachability across the regexes it processes,
// and decides emptiness of intersections of continuation regexes. One global
// derivative-transition graph is grown lazily and shared across every regex, so
// states, their nullability and their cofactor successors are computed once.
class split_manager {
friend class split;
friend class split_iterator;
// A cofactor transition of the global graph: on a guard (a predicate over the
// element variable (:var 0)) the derivative moves to the target state.
struct gedge { expr* guard; unsigned target; };
ast_manager& m;
seq_rewriter& m_rw;
th_rewriter m_th; // regex normalization (element-sort agnostic)
expr_ref_vector m_pin; // keeps interned states / guards alive
// Global reachability graph, reused across every processed regex.
obj_map<expr, unsigned> m_state_id; // regex state -> global id
ptr_vector<expr> m_gstate; // global id -> state
bool_vector m_gmaybe_null; // per state: !is_false(is_nullable)
bool_vector m_gexpanded; // per state: cofactor successors computed
vector<svector<gedge>> m_gsucc; // per state: (guard, target) edges
seq_util& u() const { return m_rw.u(); }
seq_util::rex& re() const { return m_rw.u().re; }
// Intern a state into the global graph (recycles an existing global state),
// computing its nullability lazily. Returns its global id.
unsigned intern_state(expr* s);
// Compute (once) the cofactor successors of the global state `i`, recycling
// any target states already present in the graph. Sets `ok` false on a
// resource limit.
void expand_state(unsigned i, bool& ok);
// Reachable derivative states of R with their transition graph and per-state
// (possible) nullability, projected out of the global graph. Sets `ok` false
// on cap overrun / resource limit.
void build_graph(expr* R, ptr_vector<expr>& states,
vector<svector<unsigned>>& succ, bool_vector& maybe_null, bool& ok);
// Live reachable derivative states of R (can reach a nullable state).
void live_states(expr* R, ptr_vector<expr>& out, bool& ok);
// Reachable derivative states of R from which the state N is reachable.
void reaching_states(expr* R, expr* N, ptr_vector<expr>& out, bool& ok);
// Non-emptiness of an all-membership intersection: BFS over the normalized
// product state inter(R_0,...,R_{n-1}) with an is_nullable acceptance test.
lbool intersect_membership(vector<cont_regex> const& crs, unsigned lo, unsigned hi,
expr_ref_vector& seq);
// Product-reachability of a tuple of continuation regexes (handles general N,
// i.e. reach targets N != epsilon), decomposing the engine's product successor.
lbool intersect_product(vector<cont_regex> const& crs, unsigned lo, unsigned hi,
expr_ref_vector& seq);
public:
split_manager(seq_rewriter& rw)
: m(rw.m()), m_rw(rw), m_th(rw.m()), m_pin(rw.m()) {}
ast_manager& mgr() const { return m; }
seq_rewriter& rw() const { return m_rw; }
void pin(expr* e) { m_pin.push_back(e); }
// Embed a regex R as the continuation regex <R.epsilon, epsilon>. The
// epsilon accept-state marks the membership (nullable) case uniformly.
cont_regex embed(expr* r) {
sort* ss = nullptr;
VERIFY(u().is_re(r, ss));
expr_ref eps(re().mk_epsilon(ss), m);
expr_ref start(re().mk_concat(r, eps), m);
return cont_regex(start, eps);
}
split mk_split(expr* r) { return split(*this, r); }
split mk_split(cont_regex const& cr) { return split(*this, cr); }
// Emptiness of the intersection of the continuation regexes `crs`, restricted
// to words of at least `lo` and at most `hi` elements (hi == UINT_MAX for no
// upper bound). A component <R_i, N_i> accepts a word w iff delta_w(R_i) == N_i,
// where an epsilon (or null) N_i means the nullable/membership case. Feasibility
// is decided by the derivative engine (element-sort agnostic). On l_true a
// witness is returned in `seq`: one guard predicate over (:var 0) per position.
// l_false = empty, l_true = non-empty, l_undef = gave up
// (cap overrun, undecidable nullability, or a product target that could not
// be decomposed).
lbool intersect(vector<cont_regex> const& crs, unsigned lo, unsigned hi, expr_ref_vector& seq);
// Cheap, sound one-sided partial check: false only when the intersection is
// certainly empty; true otherwise (may be a false positive).
bool test_intersect(vector<cont_regex> const& crs);
};
}

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

@ -336,7 +336,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_op_cache(m), m_es(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m) {
}
ast_manager & m() const { return m_util.get_manager(); }

1
src/test/CMakeLists.txt
View file

@ -25,6 +25,7 @@ add_executable(test-z3
parametric_datatype.cpp
arith_rewriter.cpp
seq_rewriter.cpp
seq_monadic.cpp
arith_simplifier_plugin.cpp
ast.cpp
bdd.cpp

1
src/test/main.cpp
View file

@ -116,6 +116,7 @@
X(range_predicate) \
X(regex_range_collapse) \
X(seq_rewriter) \
X(seq_monadic) \
X(check_assumptions) \
X(smt_context) \
X(theory_dl) \

174
src/test/seq_monadic.cpp Normal file
View file

@ -0,0 +1,174 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
seq_monadic.cpp
Abstract:
Unit tests for the continuation-regex split service in
ast/rewriter/seq_monadic.{h,cpp}: seq::split_manager::intersect (element-sort
agnostic intersection non-emptiness, decided by the derivative engine) and the
seq::split midpoint iterator.
Author:
Nikolaj Bjorner / Margus Veanes 2026
--*/
#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_monadic.h"
#include <iostream>
#include <climits>
namespace {
struct plugin_registrar {
plugin_registrar(ast_manager& m) { reg_decl_plugins(m); }
};
class seq_monadic_test {
ast_manager m;
plugin_registrar m_reg;
seq_rewriter m_rw;
seq::split_manager m_sm;
seq_util u;
sort_ref m_str; // String sort
sort_ref m_re; // RegEx sort over m_str
unsigned m_fail = 0;
seq_util::rex& re() { return u.re; }
// regex builders
expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); }
expr_ref cat(expr* a, expr* b) { return expr_ref(re().mk_concat(a, b), m); }
expr_ref alt(expr* a, expr* b) { return expr_ref(re().mk_union(a, b), m); }
expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); }
expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); }
expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); }
expr_ref none() { return expr_ref(re().mk_empty(m_re), m); }
expr_ref rng(char lo, char hi) {
char sl[2] = { lo, 0 }, sh[2] = { hi, 0 };
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); }
static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; }
// intersection non-emptiness of the given membership regexes, words of length in [lo,hi]
lbool inter(std::initializer_list<expr*> rs, unsigned lo, unsigned hi) {
vector<seq::cont_regex> crs;
for (expr* r : rs) crs.push_back(m_sm.embed(r));
expr_ref_vector wit(m);
return m_sm.intersect(crs, lo, hi, wit);
}
// intersection non-emptiness of a single reach continuation regex <R, N>
lbool reach(expr* R, expr* N, unsigned lo, unsigned hi) {
vector<seq::cont_regex> crs;
crs.push_back(seq::cont_regex(expr_ref(R, m), expr_ref(N, m)));
expr_ref_vector wit(m);
return m_sm.intersect(crs, lo, hi, wit);
}
void check(char const* name, lbool got, lbool expected) {
bool ok = (got == expected);
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name
<< " got=" << s(got) << " expected=" << s(expected) << "\n";
}
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();
m_re = re().mk_re(m_str);
}
void run() {
expr_ref a = word("a");
expr_ref b = word("b");
expr_ref ab = cat(a, b);
expr_ref sig = dotstar(); // Sigma*
expr_ref saas = cat(sig, cat(cat(a, a), sig)); // Sigma* a a Sigma*
expr_ref sbbs = cat(sig, cat(cat(b, b), sig)); // Sigma* b b Sigma*
expr_ref digitp = cat(rng('0', '9'), star(rng('0', '9'))); // [0-9]+
std::cout << "=== split_manager::intersect (membership) ===\n";
check("Sigma* ", inter({ sig }, 0, UINT_MAX), l_true);
check("empty regex ", inter({ none() }, 0, UINT_MAX), l_false);
check("~Sigma* ", inter({ comp(sig) }, 0, UINT_MAX), l_false);
// a* & b* = { epsilon }
check("a* & b* (any length) ", inter({ star(a), star(b) }, 0, UINT_MAX), l_true);
check("a* & b* (>= 1 char) ", inter({ star(a), star(b) }, 1, UINT_MAX), l_false);
// Sigma*aaSigma* & Sigma*bbSigma* has a common word (e.g. aabb)
check("SaaS & SbbS ", inter({ saas, sbbs }, 0, UINT_MAX), l_true);
// (a|b)* intersect ~(SaaS) intersect ~(SbbS) is non-empty (alternating words)
check("(a|b)* & ~SaaS & ~SbbS ",
inter({ star(alt(a, b)), comp(saas), comp(sbbs) }, 0, UINT_MAX), l_true);
// nested complement (L3-03) non-empty
check("L3-03 nested complement ",
inter({ comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))) }, 0, UINT_MAX), l_true);
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);
check("a* length 2..2 ", inter({ star(a) }, 2, 2), l_true);
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);
std::cout << "=== split_manager::intersect (reach, general N) ===\n";
{
expr_ref aSig = cat(a, sig); // a . Sigma*
// <Sigma*, Sigma*>: delta_epsilon(Sigma*) == Sigma* already at depth 0
check("<S*,S*> len0 ", reach(sig, sig, 0, UINT_MAX), l_true);
// <Sigma*, empty>: Sigma* never derives to the empty regex
check("<S*,empty> ", reach(sig, none(), 0, UINT_MAX), l_false);
// <a.Sigma*, Sigma*>: reached exactly after consuming one element
check("<a.S*,S*> len1 ", reach(aSig, sig, 1, 1), l_true);
check("<a.S*,S*> len0 ", reach(aSig, sig, 0, 0), l_false);
}
std::cout << "=== split_manager::test_intersect ===\n";
{
vector<seq::cont_regex> good, bad;
good.push_back(m_sm.embed(sig));
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);
}
std::cout << "=== split midpoint iterator ===\n";
{
seq::split sp = m_sm.mk_split(star(alt(a, b)));
seq::split_iterator it = sp.begin();
bool failed = it.failed();
unsigned count = 0;
for (; it != sp.end(); ++it) {
seq::split_pair pr = *it;
// left = <R, mid>, right = <mid, null>: the shared midpoint agrees
if (pr.first.second.get() != pr.second.first.get()) ++m_fail;
++count;
}
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);
}
std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " ("
<< m_fail << " fail) ===\n";
ENSURE(m_fail == 0);
}
};
}
void tst_seq_monadic() {
seq_monadic_test t;
t.run();
}