mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-04 13:13:35 +00:00
Code Activity

Add continuation-regex split service (seq_monadic)

Browse source 
Port seq_monadic to the split_set branch, reimplemented against the
cont_regex / split / split_manager API. Element-sort agnostic: relies on
the derivative engine and th_rewriter, no character-specific reasoning.

- Global derivative-transition graph reused across regexes (intern_state /
  expand_state / build_graph) so states, nullability and cofactor successors
  are computed once.
- embed(r) = <concat(r, epsilon), epsilon>; the epsilon accept-state marks the
  membership (nullable) case uniformly.
- intersect handles general cont_regex, including non-epsilon reach targets N
  (membership BFS + product-reachability paths).
- No budget / reset_pin.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8
This commit is contained in:
Nikolaj Bjorner 2026-07-19 12:08:35 -07:00
parent 6610545c08
commit b616f714ad
6 changed files with 801 additions and 0 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

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

@ -0,0 +1,425 @@
/*++
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
--*/
#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 (edge 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 (edge 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);
};
}

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();
}