mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 06:28:18 +00:00
Code Activity

seq_monadic: replace DNF expansion with depth-first search (#10366)

Browse source 
Materializing the monadic decomposition as a DNF is the dominant cost in
the
solver. The product over per-position split degrees (and, for a
conjunction of
memberships, over memberships) is exponential, and the `DNF_CAP` of 2^14
disjuncts meant the solver mostly gave up *structurally* rather than
because the
problem was hard — it paid the full product cost before testing
anything.

This decides the same disjunction by depth-first search, without ever
materializing it.

## How it works

`decide()` -> `prepare()` -> `dfs_membership(0)`.

`prepare()` parses each membership into atoms and records every
variable's
**last occurrence** as a packed `(membership_idx << 32) | atom_idx`.
Positions
compare lexicographically in exactly the order the search visits them,
so
"have I seen this variable for the last time?" is an integer equality.

`dfs_atoms(mi, i, R)` walks one membership:
- end of atoms: the remainder is epsilon, so the branch survives iff `R`
is
nullable (an undecidable nullability propagates as `l_undef` rather than
being
  guessed);
- constant element: consumed by a derivative, `re.empty` prunes
immediately;
- variable: the last atom is a plain membership, otherwise the variable
drives
the derivative automaton from `R` to some live state `q`, one child per
target.

Components are accumulated per variable in `m_groups[vi]` along the
current
branch — pushed on entry, popped on backtracking. The per-variable
emptiness
test runs as soon as the group is complete (the search just passed the
variable's last occurrence) or holds more than one component, which is
the
earliest point an inconsistency can exist. That test has to happen
anyway;
running it there prunes the whole remaining subtree instead of after the
product
has been built.  The search stops at the first satisfying leaf.

A variable shared by several memberships accumulates several components
in the
same branch and they are intersected, so the joint solve falls out of
the search
rather than needing the DNF multiplication.

## Supporting changes

- `group_nonempty` memoizes on the sorted, deduplicated `(state,
target)`
signature of the group, and collapses duplicated components before the
product
  search (which is exponential in component count);
- memoize live split states per regex, and `der_elem` per `(regex,
element)`;
- memoize nullability locally — `seq_rewriter`'s own cache is capped at
10000 and
  `cleanup()` flushes the entire table;
- hoist the cofactor vectors out of the product loop and reference them
instead
  of re-materializing `expr_ref` pairs on every pop;
- `m_budget` becomes a global node budget, and `m_giveup` unwinds the
whole
  search instead of letting sibling branches keep expanding.

Removed: `build_membership_dnf`, `decide_dnf`, `simplify_dnf`, the
`disjunct`
type and `DNF_CAP`.  The persistent cofactor cache and the separate
`guard_set::cache` are kept as-is; both own their pins, so they survive
the
per-`decide` `m_pin` reset.

## Results

Measured against master (4b2e69c66), same bench harness.

**regexes (1545 files), light-antimirov:** 41 benchmarks newly decided
(22 sat, 19 unsat), **no verdict regressions**, and 8.8s -> 2.2s on the
1421
files both versions decide. Unchanged: 2 timeouts, 0 crashes, 0
mismatches
against declared status. Brzozowski mode agrees: 0 mismatches, 0
disagreements
with light-antimirov.

**QF_S (22172 files):** 0 crashes, 0 timeouts, 0 mismatches on the 4089
benchmarks that are complete and have a declared status. Verdicts are
identical
to master.

Unit tests pass in both transition modes.

## Caveat

On the 81 files neither version decides, DFS costs more (62s -> 149s):
it
explores until the 200000-node budget is exhausted, whereas the DNF path
bailed
immediately at its structural 2^14 cap. `m_budget` has not been retuned
since
the per-node cost dropped, so there is likely room to recover most of
that
without losing the 41 newly decided benchmarks.

---------

Co-authored-by: Margus Veanes <margus@microsoft.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
This commit is contained in:
Nikolaj Bjorner 2026-08-02 20:01:20 -07:00 • committed by GitHub
parent 4b2e69c660
commit 079eb4b534
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 425 additions and 253 deletions
Download patch file Download diff file Expand all files Collapse all files

571
src/ast/rewriter/seq_monadic.cpp
View file

@ -8,7 +8,9 @@ Module Name:
Abstract:
Whole-language monadic decomposition for regex membership. See seq_monadic.h.
Automaton-based (product-reachability); reach(q) is never materialized as a regex.
Automaton-based (product-reachability); reach(q) is never materialized as a regex, and
the disjunction produced by the decomposition is never materialized as a DNF: it is
explored as a depth-first search tree with per-variable emptiness pruning.
Generic in the element sort. The decomposition, liveness and product-reachability
are element-agnostic; only the *guard algebra* over the derivative cofactor guards
@ -19,7 +21,6 @@ Abstract:
yields the concrete element used to build a witness sequence.
TODOs:
- if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead)
- create a validation harness: expose certificates for correctness that can be checked.
- consider using expr_ref as alternative to pinned expressions
- revisit parse_term and "the_var" condition. A sequence of units should be allowed
@ -51,17 +52,45 @@ Author:
#include <tuple>
#include <functional>
#include <algorithm>
#include <unordered_set>
expr_ref seq_monadic::der_elem(expr* r, expr* elem) {
expr* cached = nullptr;
if (m_der_cache.find(r, elem, cached))
return expr_ref(cached, m);
expr_ref d = m_rw.mk_derivative(elem, r); // mk_derivative(element, regex)
// Normalize: for a general element sort the derivative by a non-matching constant can
// leave a ground guard (e.g. (= 1 2)) unfolded; simplifying collapses such dead
// branches to re.empty so nullability/emptiness stay decidable.
expr_ref d2(m);
m_thrw(d, d2);
m_pin.push_back(r); // keep the cache keys and value alive
m_pin.push_back(elem);
m_pin.push_back(d2);
m_der_cache.insert(r, elem, d2);
return d2;
}
lbool seq_monadic::nullable(expr* r) {
// Nullability is a structural property, and the seq plugin already computes it as
// part of the regex info -- cached by expr id and, unlike seq_rewriter's op_cache
// (capped at 10000 and flushed whole), never evicted. Use it whenever it is
// determined; only fall back to building the symbolic nullability formula for the
// regexes whose info leaves it undetermined.
lbool i = re().get_info(r).nullable;
if (i != l_undef)
return i;
char v = 0;
if (m_nullable_cache.find(r, v))
return v == 1 ? l_true : v == 0 ? l_false : l_undef;
expr_ref nb = m_rw.is_nullable(r);
lbool res = m.is_true(nb) ? l_true : m.is_false(nb) ? l_false : l_undef;
m_pin.push_back(r);
m_nullable_cache.insert(r, res == l_true ? 1 : res == l_false ? 0 : 2);
return res;
}
expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) {
expr_ref_pair_vector* v = nullptr;
if (m_cofactors.find(r, v))
@ -87,8 +116,7 @@ bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
id.insert(s, k);
states.push_back(s);
succ.push_back(svector<unsigned>());
expr_ref nb = m_rw.is_nullable(s);
maybe_null.push_back(!m.is_false(nb)); // unknown nullability => keep (conservative)
maybe_null.push_back(nullable(s) != l_false); // unknown nullability => keep (conservative)
return k;
};
intern(R);
@ -119,6 +147,26 @@ bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
return true;
}
expr_ref_vector const* seq_monadic::live_states_cached(expr* R) {
expr_ref_vector* v = nullptr;
if (m_live_cache.find(R, v))
return v; // may be null: previously gave up on R
v = alloc(expr_ref_vector, m);
if (!live_states(R, *v)) {
dealloc(v);
v = nullptr;
}
m_pin.push_back(R); // keep the key alive for the cache's lifetime
m_live_cache.insert(R, v);
return v;
}
void seq_monadic::reset_live_cache() {
for (auto const& [k, v] : m_live_cache)
dealloc(v);
m_live_cache.reset();
}
lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* witness_word) {
unsigned n = comps.size();
if (n == 0) {
@ -128,40 +176,61 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
}
expr_ref var0(m.mk_var(0, m_elem_sort), m); // the element variable the guards range over
ptr_vector<expr> start;
for (auto const& c : comps)
start.push_back(c.state);
auto id_key = [&](ptr_vector<expr> const& st) {
std::vector<unsigned> k;
k.reserve(st.size());
for (expr* e : st) k.push_back(e->get_id());
return k;
};
typedef std::vector<unsigned> key;
struct key_hash {
size_t operator()(key const& k) const {
size_t h = 1469598103934665603ull;
for (unsigned x : k)
h = (h ^ x) * 1099511628211ull;
return h;
}
};
// Product states are held in a flat stack of stride n; `visited` owns one copy of the
// id-tuple of every discovered state. Both avoid a per-state heap allocation, which
// dominated the search when this ran per derivative step of the outer decomposition.
ptr_vector<expr> work;
std::unordered_set<key, key_hash> visited;
key kbuf;
kbuf.resize(n);
ptr_vector<expr> st;
st.resize(n);
ptr_vector<expr> cur;
cur.resize(n);
auto fill_key = [&](ptr_vector<expr> const& s) -> key const& {
for (unsigned i = 0; i < n; ++i)
kbuf[i] = s[i]->get_id();
return kbuf;
};
bool undecided = false;
auto is_accept = [&](ptr_vector<expr> const& st) -> bool {
auto is_accept = [&]() -> bool {
for (unsigned i = 0; i < n; ++i) {
if (comps[i].target) {
if (st[i] != comps[i].target) return false;
}
else {
expr_ref nb = m_rw.is_nullable(st[i]);
if (m.is_true(nb)) continue;
if (m.is_false(nb)) return false;
lbool nb = nullable(st[i]);
if (nb == l_true) continue;
if (nb == l_false) return false;
undecided = true; return false;
}
}
return true;
};
std::set<key> visited;
vector<ptr_vector<expr>> work;
// tree of first-discovery edges for witness reconstruction (only built when a
// witness is requested): child-key -> (parent-key, element read on the edge).
std::map<key, std::pair<key, expr*>> parent;
key start_key = id_key(start);
key start_key;
start_key.resize(n);
for (unsigned i = 0; i < n; ++i) {
work.push_back(comps[i].state);
start_key[i] = comps[i].state->get_id();
}
visited.insert(start_key);
auto reconstruct = [&](key end_key) -> expr_ref {
ptr_vector<expr> elems; // collected in accept..start order
@ -180,71 +249,67 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
return expr_ref(u().str.mk_concat(es.size(), es.data(), m_seq_sort), m);
};
work.push_back(start);
visited.insert(start_key);
// Hoisted out of the search loop: the per-component cofactor vectors are owned by the
// cofactor cache and stay valid for the whole search, so they are referenced rather
// than copied (copying re-materialized every branch as expr_ref pairs on every pop).
svector<expr_ref_pair_vector const*> branches;
branches.resize(n);
key st_key;
bool bail = false;
std::function<void(unsigned, guard_set const&)> rec =
[&](unsigned i, guard_set const& acc) {
if (bail) return;
if (i == n) {
key const& ck = fill_key(cur);
if (visited.find(ck) == visited.end()) {
visited.insert(ck);
if (witness_word) {
expr_ref e(m);
if (acc.eval(&e) == l_true) {
m_pin.push_back(e);
parent[ck] = { st_key, e.get() };
}
}
for (unsigned j = 0; j < n; ++j)
work.push_back(cur[j]);
}
return;
}
for (auto const& [g, t] : *branches[i]) {
if (re().is_empty(t)) continue;
guard_set nacc = acc;
nacc.conjoin(g);
lbool ne = nacc.eval(nullptr);
if (ne == l_undef) { bail = true; return; } // non-range / unknown guard
if (ne == l_false) continue; // empty joint guard: prune
cur[i] = t;
rec(i + 1, nacc);
if (bail) return;
}
};
while (!work.empty()) {
if (m_budget == 0) { m_giveup = true; return l_undef; }
if (m_budget == 0 || !m.inc()) { m_giveup = true; return l_undef; }
--m_budget;
if (!m.inc())
return l_undef;
ptr_vector<expr> st = work.back();
work.pop_back();
if (is_accept(st)) {
for (unsigned i = n; i-- > 0; ) {
st[i] = work.back();
work.pop_back();
}
if (is_accept()) {
if (witness_word)
*witness_word = reconstruct(id_key(st));
*witness_word = reconstruct(fill_key(st));
return l_true;
}
if (undecided)
return l_undef;
// per-component cofactor branches (target, guard); expr_ref keeps both alive
// beyond the cached `cof` reference.
vector<vector<std::pair<expr_ref, expr_ref>>> branches;
branches.resize(n);
for (unsigned i = 0; i < n; ++i) {
expr_ref_pair_vector const& cof = derivative_cofactors(st[i]);
for (auto const& [g, t] : cof) {
if (re().is_empty(t)) continue;
branches[i].push_back({ expr_ref(t, m), expr_ref(g, m) });
}
}
for (unsigned i = 0; i < n; ++i)
branches[i] = &derivative_cofactors(st[i]);
// joint transitions = cartesian product of the branches with the guards
// conjoined; prune as soon as the accumulated guard is empty, bail on unknown.
ptr_vector<expr> cur;
cur.resize(n);
key st_key = id_key(st);
bool bail = false;
std::function<void(unsigned, guard_set const&)> rec =
[&](unsigned i, guard_set const& acc) {
if (bail) return;
if (i == n) {
key ck = id_key(cur);
if (visited.find(ck) == visited.end()) {
visited.insert(ck);
if (witness_word) {
expr_ref e(m);
if (acc.eval(&e) == l_true) {
m_pin.push_back(e);
parent[ck] = { st_key, e.get() };
}
}
work.push_back(cur);
}
return;
}
for (auto const& pr : branches[i]) {
guard_set nacc = acc;
nacc.conjoin(pr.second);
lbool ne = nacc.eval(nullptr);
if (ne == l_undef) { bail = true; return; } // non-range / unknown guard
if (ne == l_false) continue; // empty joint guard: prune
cur[i] = pr.first;
rec(i + 1, nacc);
if (bail) return;
}
};
if (witness_word)
st_key = fill_key(st);
guard_set top(m, u(), m_elem_sort, var0, &m_rp_cache);
rec(0, top);
if (bail)
@ -280,135 +345,217 @@ bool seq_monadic::parse_term(expr* t, vector<atom>& atoms, expr*& the_var) {
return false;
}
bool seq_monadic::decompose(vector<atom> const& atoms, unsigned i, expr* R,
vector<disjunct>& out) {
if (m_giveup)
return false;
m_pin.push_back(R);
if (i == atoms.size()) {
expr_ref nb = m_rw.is_nullable(R);
if (m.is_true(nb))
out.push_back(disjunct()); // empty conjunction = true
else if (!m.is_false(nb))
return false; // undecidable nullability => bail
return true;
}
atom const& a = atoms[i];
if (!a.is_var) {
expr_ref d = der_elem(R, a.elem.get());
return decompose(atoms, i + 1, d, out);
}
if (i + 1 == atoms.size()) { // last atom: membership component a.var in R
disjunct D;
D.push_back(component{ a.var.get(), R, nullptr });
out.push_back(D);
return true;
}
// a variable with a non-empty rest: split over the live states q of R (midpoints)
expr_ref_vector Q(m);
if (!live_states(R, Q))
return false;
const unsigned DISJUNCT_CAP = 1u << 13;
for (expr* q : Q) {
vector<disjunct> sub;
if (!decompose(atoms, i + 1, q, sub))
unsigned seq_monadic::var_index(expr* v) {
unsigned vi;
if (m_var_idx.find(v, vi))
return vi;
vi = m_vars.size();
m_var_idx.insert(v, vi);
m_vars.push_back(v);
m_groups.push_back(svector<component>());
return vi;
}
void seq_monadic::reset_search() {
m_atoms.reset();
m_regexes.reset();
m_vars.reset();
m_var_idx.reset();
m_groups.reset();
m_last_occ.reset();
m_group_cache.clear();
m_der_cache.reset();
m_nullable_cache.reset();
m_undef_vars = 0;
reset_live_cache();
}
bool seq_monadic::prepare(membership_vec const& memberships) {
reset_search();
for (auto const& [term, regex, d] : memberships) {
if (!u().is_re(regex, m_seq_sort))
return false;
for (disjunct const& sd : sub) {
if (out.size() > DISJUNCT_CAP || m_budget == 0) { m_giveup = true; return false; }
--m_budget;
disjunct D(sd);
D.push_back(component{ a.var.get(), R, q }); // reach component: a.var drives R -> q
out.push_back(D);
if (!u().is_seq(m_seq_sort, m_elem_sort))
return false;
vector<atom> atoms;
expr* the_var = nullptr;
if (!parse_term(term, atoms, the_var))
return false;
if (!the_var)
return false; // no variable: ground membership, not our case
m_regexes.push_back(regex);
m_atoms.push_back(atoms);
m_pin.push_back(regex);
}
// A variable's component group is complete once the search passes the variable's
// last occurrence; positions are compared in search order, i.e. lexicographically
// on (membership index, atom index).
for (unsigned mi = 0; mi < m_atoms.size(); ++mi) {
vector<atom> const& atoms = m_atoms[mi];
for (unsigned i = 0; i < atoms.size(); ++i) {
if (!atoms[i].is_var)
continue;
expr* v = atoms[i].var.get();
var_index(v);
m_last_occ.insert(v, (static_cast<uint64_t>(mi) << 32) | i);
}
}
simplify_dnf(out);
return true;
}
void seq_monadic::simplify_dnf(vector<disjunct>& dnf) {
std::set<std::vector<std::tuple<unsigned, unsigned, unsigned>>> seen;
vector<disjunct> result;
for (disjunct const& D : dnf) {
bool dead = false;
for (auto const& c : D)
if (re().is_empty(c.state)) { dead = true; break; }
if (dead)
continue;
std::vector<std::tuple<unsigned, unsigned, unsigned>> sig;
sig.reserve(D.size());
for (auto const& c : D)
sig.push_back(std::make_tuple(c.var->get_id(), c.state->get_id(),
c.target ? c.target->get_id() : UINT_MAX));
std::sort(sig.begin(), sig.end());
if (seen.insert(sig).second)
result.push_back(D);
lbool seq_monadic::group_nonempty(unsigned vi) {
svector<component> const& g = m_groups[vi];
group_sig& sig = m_sig_buf;
sig.clear();
for (auto const& c : g)
sig.push_back({ c.state->get_id(), c.target ? c.target->get_id() : UINT_MAX });
std::sort(sig.begin(), sig.end());
sig.erase(std::unique(sig.begin(), sig.end()), sig.end());
auto it = m_group_cache.find(sig);
if (it != m_group_cache.end())
return it->second;
// Collapse duplicated components: they constrain the variable identically, and the
// product search is exponential in the number of components.
svector<component> comps;
if (sig.size() == g.size())
comps = g;
else {
std::set<std::pair<unsigned, unsigned>> seen;
for (auto const& c : g)
if (seen.insert({ c.state->get_id(), c.target ? c.target->get_id() : UINT_MAX }).second)
comps.push_back(c);
}
dnf.swap(result);
lbool r = product_nonempty(comps, nullptr);
m_group_cache.emplace(sig, r); // sig is m_sig_buf; emplace copies it
return r;
}
lbool seq_monadic::leaf() {
if (m_undef_vars > 0)
return l_undef; // some variable's emptiness test gave up
if (!m_config.m_model)
return l_true;
m_model.reset();
for (unsigned vi = 0; vi < m_groups.size(); ++vi) {
if (m_groups[vi].empty())
continue;
expr_ref w(m);
lbool ne = product_nonempty(m_groups[vi], &w);
if (ne != l_true) { // groups were already shown non-empty;
m_model.reset(); // only reachable if the search was cut short
return ne;
}
m_pin.push_back(w);
m_model.insert(m_vars[vi], w.get());
}
return l_true;
}
lbool seq_monadic::dfs_membership(unsigned mi) {
if (mi == m_atoms.size())
return leaf();
return dfs_atoms(mi, 0, m_regexes.get(mi));
}
lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
if (m_giveup)
return l_undef; // unwind the whole search, don't keep branching
if (m_budget == 0 || !m.inc()) {
m_giveup = true;
return l_undef;
}
--m_budget;
vector<atom> const& atoms = m_atoms[mi];
if (i == atoms.size()) { // the rest of this membership is epsilon
lbool nb = nullable(R);
if (nb == l_true)
return dfs_membership(mi + 1);
if (nb == l_false)
return l_false;
return l_undef; // undecidable nullability
}
atom const& a = atoms[i];
if (!a.is_var) { // a constant element is consumed by a derivative
expr_ref d = der_elem(R, a.elem.get());
if (re().is_empty(d))
return l_false;
m_pin.push_back(d);
return dfs_atoms(mi, i + 1, d);
}
// A variable: the last atom is a plain membership in R, otherwise the variable drives
// the derivative automaton from R to some live state q, which splits the search.
bool last_atom = (i + 1 == atoms.size());
ptr_vector<expr> targets;
if (last_atom)
targets.push_back(nullptr);
else {
expr_ref_vector const* Q = live_states_cached(R);
if (!Q)
return l_undef;
for (expr* q : *Q)
targets.push_back(q);
}
unsigned vi = var_index(a.var.get());
uint64_t pos = (static_cast<uint64_t>(mi) << 32) | i;
uint64_t last = 0;
bool finalize = m_last_occ.find(a.var.get(), last) && last == pos;
bool any_undef = false;
for (expr* target : targets) {
m_groups[vi].push_back(component{ a.var.get(), R, target });
// The group's emptiness test has to be run at some point anyway; running it as
// soon as the group is complete (or as soon as it holds several components, where
// an inconsistency can first arise) prunes the entire subtree below.
lbool ne = l_true;
if (re().is_empty(R))
ne = l_false;
else if (finalize || m_groups[vi].size() > 1)
ne = group_nonempty(vi);
lbool r;
if (ne == l_false)
r = l_false;
else {
if (ne == l_undef)
++m_undef_vars;
r = last_atom ? dfs_membership(mi + 1) : dfs_atoms(mi, i + 1, target);
if (ne == l_undef)
--m_undef_vars;
}
m_groups[vi].pop_back();
if (r == l_true)
return l_true;
if (r == l_undef) {
if (m_giveup)
return l_undef;
any_undef = true;
}
}
return any_undef ? l_undef : l_false;
}
lbool seq_monadic::decide(membership_vec const& memberships) {
m_model.reset();
if (memberships.empty())
return l_true; // empty conjunction is vacuously true
reset_search(); // clear the caches before dropping the
m_pin.reset(); // pins that keep their keys alive
m_cofactors.maybe_reset(1u << 16); // cofactors persist across calls (own their pins)
m_rp_cache.maybe_reset(1u << 16);
m_budget = 200000;
m_giveup = false;
if (!prepare(memberships))
return l_undef;
lbool r = dfs_membership(0);
if (r != l_true)
m_model.reset();
return r;
}
lbool seq_monadic::solve(expr* term, expr* R) {
m_pin.reset();
m_cofactors.maybe_reset(1u << 16);
m_rp_cache.maybe_reset(1u << 16);
m_budget = 200000; // global work budget: bail fast on DNF explosion
m_giveup = false;
vector<disjunct> dnf;
if (!build_membership_dnf(term, R, dnf))
return l_undef;
return decide_dnf(dnf);
}
bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector<disjunct>& dnf) {
if (!u().is_re(R, m_seq_sort))
return false;
if (!u().is_seq(m_seq_sort, m_elem_sort))
return false;
vector<atom> atoms;
expr* the_var = nullptr;
if (!parse_term(term, atoms, the_var))
return false;
if (!the_var)
return false; // no variable: ground membership, not our case
m_pin.push_back(R);
return decompose(atoms, 0, R, dnf);
}
lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf) {
m_model.reset();
bool any_undef = false;
for (disjunct const& D : dnf) {
// group components by variable
obj_map<expr, unsigned> idx;
vector<svector<component>> groups;
ptr_vector<expr> group_var;
auto bucket = [&](expr* v) -> unsigned {
unsigned gi;
if (idx.find(v, gi)) return gi;
gi = groups.size(); idx.insert(v, gi);
groups.push_back(svector<component>());
group_var.push_back(v);
return gi;
};
for (auto const& c : D)
groups[bucket(c.var)].push_back(c);
bool has_empty = false, has_undef = false;
obj_map<expr, expr*> local; // var -> witness for this disjunct
for (unsigned gi = 0; gi < groups.size(); ++gi) {
expr_ref w(m);
lbool ne = product_nonempty(groups[gi], m_config.m_model ? &w : nullptr);
if (ne == l_false) { has_empty = true; break; } // this variable has no value
if (ne == l_undef) { has_undef = true; continue; }
if (m_config.m_model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); }
}
if (has_empty) continue;
if (has_undef) { any_undef = true; continue; }
if (m_config.m_model)
for (auto const& [k, v] : local)
m_model.insert(k, v);
return l_true; // all variables satisfiable => sat
}
return any_undef ? l_undef : l_false;
membership_vec mv;
mv.push_back({ expr_ref(term, m), expr_ref(R, m), nullptr });
return decide(mv);
}
void seq_monadic::add(expr* term, expr* regex, void* d) {
@ -441,44 +588,6 @@ void seq_monadic::add_len(expr* term, unsigned len, void* d) {
add(term, regex, d);
}
lbool seq_monadic::decide(membership_vec const& memberships) {
m_model.reset();
if (memberships.empty())
return l_true; // empty conjunction is vacuously true
m_pin.reset();
m_cofactors.maybe_reset(1u << 16);
m_rp_cache.maybe_reset(1u << 16);
m_budget = 200000;
m_giveup = false;
// Multiply the per-membership DNFs: combined = { d ++ e : d in combined, e in dnf_i }.
// A variable shared by several memberships thus gets several components in the same
// disjunct, which decide_dnf/product_nonempty intersect -- enforcing one consistent
// value across all memberships (the joint solve the harness could not do per-term).
vector<disjunct> combined;
combined.push_back(disjunct()); // { true }
const unsigned DNF_CAP = 1u << 14;
for (auto const& [term, regex, d] : memberships) {
vector<disjunct> dnf_i;
if (!build_membership_dnf(term, regex, dnf_i))
return l_undef;
vector<disjunct> next;
for (disjunct const& cd : combined) {
for (disjunct const& e : dnf_i) {
if (next.size() > DNF_CAP || m_budget == 0) { m_giveup = true; return l_undef; }
--m_budget;
disjunct D(cd);
for (auto const& c : e)
D.push_back(c);
next.push_back(D);
}
}
combined.swap(next);
simplify_dnf(combined);
if (combined.empty())
return l_false; // no viable disjunct left => unsat
}
return decide_dnf(combined);
}
void seq_monadic::minimize_core(membership_vec const& memberships) {
m_core.reset();

107
src/ast/rewriter/seq_monadic.h
View file

@ -25,13 +25,22 @@ Abstract:
x.u in R <=> OR_{q live} ( x reaches q in A_R /\ u in q ).
Decomposing u recursively (a leading constant is consumed by a derivative, a leading
variable splits again, the last variable is a plain membership) yields a DNF whose
disjuncts are conjunctions of per-variable *components*:
variable splits again, the last variable is a plain membership) yields a disjunction
of conjunctions of per-variable *components*:
- reach component <var, state0, q> : the variable's value drives the
derivative automaton from state0 to q
- membership component<var, state0, null> : the variable's value is in L(state0)
That disjunction is NEVER materialized as a DNF. Materializing it costs the product
of the per-position split degrees (and, for a conjunction of memberships, the product
over memberships), which is the dominant cost in practice. Instead the decomposition
is explored as a depth-first search tree: one branch at a time, components pushed on
entry and popped on backtracking. A variable's accumulated components are tested for
emptiness as soon as the search passes the variable's LAST occurrence -- the test has
to be done anyway, and doing it there prunes the whole remaining subtree. The search
stops at the first satisfying leaf.
reach(q) is therefore NEVER built as a regex (which state-elimination would blow up
super-polynomially for lattice-shaped automata). Instead the constraints on a
variable are decided directly by a lazy product-reachability search over tuples of
@ -58,10 +67,14 @@ Author:
#include "ast/rewriter/th_rewriter.h"
#include "util/lbool.h"
#include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h"
#include "util/dependency.h"
#include "util/trail.h"
#include <utility>
#include <tuple>
#include <map>
#include <vector>
#include <unordered_map>
class seq_monadic {
public:
@ -110,12 +123,15 @@ private:
sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis
sort* m_elem_sort = nullptr; // element sort of that sequence sort
expr_ref_vector m_pin; // pins derivative states / witnesses referenced later
unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops)
unsigned m_budget = 0; // global work budget (search nodes + product pops)
bool m_giveup = false; // set when the budget is exhausted
config m_config;
obj_map<expr, expr*> m_model; // last extracted model (var -> witness); see get_model()
cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above)
guard_set::cache m_rp_cache; // cofactor guard -> range predicate
obj_pair_map<expr, expr, expr*> m_der_cache; // memoizes der_elem per (regex, element)
obj_map<expr, char> m_nullable_cache; // memoizes nullability (0 false / 1 true / 2 unknown);
// seq_rewriter's own cache is capped and flushed whole
using membership_vec = vector<std::tuple<expr_ref, expr_ref, void*>>;
membership_vec m_memberships; // asserted (term in regex, dep) for check()
ptr_vector<void> m_core; // dependencies of an unsat subset, filled by check() on l_false
@ -140,11 +156,38 @@ private:
// : nullable(current) -- membership component (w in L(state))
struct component { expr* var; expr* state; expr* target; };
typedef svector<component> disjunct; // a conjunction of components (a DNF disjunct)
// ---- depth-first search state; valid for the duration of one decide()/solve() ----
vector<vector<atom>> m_atoms; // parsed atoms, one entry per membership
expr_ref_vector m_regexes; // regex of each membership (parallel to m_atoms)
ptr_vector<expr> m_vars; // variables occurring in the memberships
obj_map<expr, unsigned> m_var_idx; // variable -> index into m_vars / m_groups
vector<svector<component>> m_groups; // components accumulated on the current branch
obj_map<expr, uint64_t> m_last_occ; // variable -> last (membership, atom) position
unsigned m_undef_vars = 0; // depth of groups whose emptiness test gave up
// memo for the per-variable emptiness test, keyed by the sorted, deduplicated
// (state, target) signature of the variable's component group
typedef std::vector<std::pair<unsigned, unsigned>> group_sig;
struct group_sig_hash {
size_t operator()(group_sig const& s) const {
size_t h = 1469598103934665603ull;
for (auto const& p : s) {
h = (h ^ p.first) * 1099511628211ull;
h = (h ^ p.second) * 1099511628211ull;
}
return h;
}
};
group_sig m_sig_buf; // reused by group_nonempty (avoids allocating per lookup)
std::unordered_map<group_sig, lbool, group_sig_hash> m_group_cache;
obj_map<expr, expr_ref_vector*> m_live_cache; // regex -> live split states (null = gave up)
// Brzozowski derivative of regex `r` by the concrete element `elem`.
// Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on
// (r, elem): the search revisits the same constant step on many branches.
expr_ref der_elem(expr* r, expr* elem);
// Memoized nullability of a derivative state: l_true / l_false / l_undef (unknown).
lbool nullable(expr* r);
// Symbolic transition cofactors in the selected mode. Memoized per regex `r` in
// m_cofactors: the returned vector is owned by that cache (see the cofactor_cache
// class above for the persistence/reset policy).
@ -154,6 +197,11 @@ private:
// least-fixpoint). These are the split states q. Returns false on a cap overrun.
bool live_states(expr* R, expr_ref_vector& out);
// Memoized live_states. Returns null if the computation gave up for this regex.
expr_ref_vector const* live_states_cached(expr* R);
void reset_live_cache();
// Product-reachability emptiness of a conjunction of components (all on one
// variable). l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up
// (cap overrun, non-range guard, or undecidable nullability).
@ -165,26 +213,40 @@ private:
// Flatten a str.++ term into atoms; false on an unsupported shape (non-constant unit).
bool parse_term(expr* term, vector<atom>& atoms, expr*& the_var);
// Monadic decomposition: append to `out` the DNF disjuncts for atoms[i..] in R,
// threading the current derivative state R. Returns false on give-up.
bool decompose(vector<atom> const& atoms, unsigned i, expr* R,
vector<disjunct>& out);
// Drop all search state accumulated by the previous decide()/solve().
void reset_search();
// Drop disjuncts with a syntactically-empty component and dedup identical disjuncts.
void simplify_dnf(vector<disjunct>& dnf);
// Parse every membership into atoms, register its variables and record each
// variable's last occurrence. Sets m_seq_sort/m_elem_sort. False on an
// unsupported shape.
bool prepare(membership_vec const& memberships);
// Build the DNF over primitive per-variable components for one membership term in R.
// Sets m_seq_sort/m_elem_sort; false on an unsupported shape or give-up.
bool build_membership_dnf(expr* term, expr* R, vector<disjunct>& dnf);
// Index of `v` in m_vars / m_groups, registering it on first sight.
unsigned var_index(expr* v);
// Decide a DNF (over primitive components): sat iff some disjunct has every variable
// group non-empty. On l_true, when model generation is enabled, fills m_model
// (var -> witness).
lbool decide_dnf(vector<disjunct> const& dnf);
// Depth-first search over the monadic decomposition. dfs_membership(mi) starts
// membership `mi` (or reaches a leaf when every membership is consumed);
// dfs_atoms(mi, i, R) continues membership `mi` at atom `i` with derivative state R.
// l_true = a satisfying branch was found (m_model is filled when model generation is
// enabled), l_false = every branch below is empty, l_undef = gave up.
lbool dfs_membership(unsigned mi);
lbool dfs_atoms(unsigned mi, unsigned i, expr* R);
// Emptiness of the components accumulated for variable `vi` on the current branch,
// memoized on their signature. Duplicated components are collapsed before the
// product search (they constrain the variable identically).
lbool group_nonempty(unsigned vi);
// All memberships consumed: every variable group has already been shown non-empty,
// so this only extracts witnesses when model generation is enabled.
lbool leaf();
// Decide a CONJUNCTION of memberships jointly (the core algorithm behind check()):
// multiplies the per-membership DNFs and decides emptiness. Does not touch
// m_memberships or m_core; fills m_model on l_true when model generation is enabled.
// explores the joint decomposition of all memberships depth-first. A variable shared
// by several memberships accumulates several components in the same branch, which are
// intersected -- enforcing one consistent value across all memberships. Does not
// touch m_memberships or m_core; fills m_model on l_true when model generation is
// enabled.
lbool decide(membership_vec const& memberships);
// Given an unsatisfiable membership set, extract a minimal unsatisfiable subset by
@ -199,9 +261,10 @@ public:
seq_monadic(seq_rewriter& rw, trail_stack& undo_trail,
transition_mode mode = transition_mode::light_antimirov) :
m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail),
m_pin(rw.m()), m_config(mode), m_cofactors(rw.m()), m_rp_cache(rw.m()) {}
m_pin(rw.m()), m_config(mode), m_cofactors(rw.m()), m_rp_cache(rw.m()),
m_regexes(rw.m()) {}
~seq_monadic() = default;
~seq_monadic() { reset_live_cache(); }
transition_mode mode() const { return m_config.m_mode; }