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

seq_regex: couple length bounds into monadic regex solver

Browse source 
Feed arithmetic length lower/upper/exact bounds (via theory_seq
lower_bound/upper_bound) into the monadic regex end-game solver using the
existing add_lo/add_hi/add_len helpers, so proposed witnesses respect length
constraints and length-driven cases resolve directly instead of backtracking
over the model.

Dependencies handed to the monadic solver now encode a union of sorts:
2*lit.index() for membership literals (even) and 2*bound_index+1 for length
bounds (odd). On unsat, the core is decoded back into conflict literals,
materializing the justifying arithmetic bound literals (len>=lo, len<=hi) at
that point. Bounds are recorded in m_monadic_bounds and undone via push_trail.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-08-01 17:14:45 -07:00
parent 07ccba46a1
commit 2bd68a68bd
2 changed files with 97 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/smt/seq_regex.cpp
View file

@ -50,14 +50,76 @@ namespace smt {
return;
m_monadic_memberships.push_back(monadic_membership(m, lit, s, r));
ctx.push_trail(push_back_vector(m_monadic_memberships));
theory_seq::dependency* dep = th.m_dm.mk_leaf(theory_seq::assumption(lit));
m_monadic.add(s, r, dep);
m_monadic.add(s, r, dep_of_literal(lit));
ctx.push_trail(value_trail<unsigned>(m_monadic_generation));
++m_monadic_generation;
TRACE(seq_regex, tout << "monadic add " << lit << ": "
<< mk_pp(s, m) << " in " << mk_pp(r, m) << "\n";);
}
void seq_regex::add_monadic_bounds() {
// add_lo/add_hi/add_len build a length regex .{lo}.* / .{0,hi} / .{len}; keep the
// bound small so the extra membership never itself blows past the monadic solver's
// state cap (a too-large bound would only turn a solvable case into a give-up).
const unsigned MAX_BOUND = 1000;
for (auto const& mem : m_monadic_memberships) {
expr* s = mem.m_s;
expr_ref len = th.mk_len(s);
rational lo, hi;
bool has_lo = th.lower_bound(len, lo) && lo.is_unsigned() && lo.get_unsigned() > 0;
bool has_hi = th.upper_bound(len, hi) && hi.is_unsigned();
if (has_lo && has_hi && lo == hi) {
if (lo.get_unsigned() <= MAX_BOUND)
record_bound(s, len, bound_constraint::LEN, lo.get_unsigned());
continue;
}
if (has_lo && lo.get_unsigned() <= MAX_BOUND)
record_bound(s, len, bound_constraint::LO, lo.get_unsigned());
if (has_hi && hi.get_unsigned() <= MAX_BOUND)
record_bound(s, len, bound_constraint::HI, hi.get_unsigned());
}
}
void seq_regex::record_bound(expr* s, expr* len, bound_constraint::kind_t k, unsigned v) {
for (auto const& b : m_monadic_bounds)
if (b.m_len.get() == len && b.m_kind == k && b.m_value == v)
return; // already asserted at this scope
unsigned idx = m_monadic_bounds.size();
m_monadic_bounds.push_back(bound_constraint(m, k, len, v));
ctx.push_trail(push_back_vector(m_monadic_bounds));
void* dep = dep_of_bound(idx);
switch (k) {
case bound_constraint::LO: m_monadic.add_lo(s, v, dep); break;
case bound_constraint::HI: m_monadic.add_hi(s, v, dep); break;
case bound_constraint::LEN: m_monadic.add_len(s, v, dep); break;
}
TRACE(seq_regex, tout << "monadic bound " << mk_pp(len, m)
<< (k == bound_constraint::LO ? " >= " :
k == bound_constraint::HI ? " <= " : " = ") << v << "\n";);
}
void seq_regex::add_core_literal(void* dep, literal_vector& lits) {
size_t enc = reinterpret_cast<size_t>(dep);
if ((enc & 1) == 0) { // even: monadic membership literal
lits.push_back(to_literal(static_cast<int>(enc >> 1)));
return;
}
// odd: a length bound; materialize its justifying arithmetic literal(s) now.
bound_constraint const& b = m_monadic_bounds[static_cast<unsigned>((enc - 1) >> 1)];
switch (b.m_kind) {
case bound_constraint::LO:
lits.push_back(th.m_ax.mk_ge(b.m_len, b.m_value));
break;
case bound_constraint::HI:
lits.push_back(th.m_ax.mk_le(b.m_len, b.m_value));
break;
case bound_constraint::LEN:
lits.push_back(th.m_ax.mk_ge(b.m_len, b.m_value));
lits.push_back(th.m_ax.mk_le(b.m_len, b.m_value));
break;
}
}
void seq_regex::propagate_accept_legacy(literal lit, expr* s, expr* r) {
expr_ref regex(r, m);
if (!m.is_value(s)) {
@ -109,13 +171,14 @@ namespace smt {
}
++th.m_stats.m_regex_monadic_checks;
add_monadic_bounds();
lbool result = m_monadic.check();
if (result == l_false) {
++th.m_stats.m_regex_monadic_unsat;
theory_seq::dependency* dep = nullptr;
literal_vector lits;
for (void* core_dep : m_monadic.core())
dep = th.m_dm.mk_join(dep, static_cast<theory_seq::dependency*>(core_dep));
th.set_conflict(dep);
add_core_literal(core_dep, lits);
th.set_conflict(nullptr, lits);
return FC_CONTINUE;
}
if (result == l_undef) {

29
src/smt/seq_regex.h
View file

@ -124,9 +124,22 @@ namespace smt {
enode* m_witness;
};
// A length-bound constraint fed to the monadic solver as an extra length regex.
// Recorded so the justifying arithmetic literal(s) can be materialized if the
// bound participates in an unsat core. m_len is the length term (str.len s).
struct bound_constraint {
enum kind_t { LO, HI, LEN };
expr_ref m_len;
kind_t m_kind;
unsigned m_value;
bound_constraint(ast_manager& m, kind_t k, expr* len, unsigned v):
m_len(len, m), m_kind(k), m_value(v) {}
};
seq_monadic m_monadic;
vector<monadic_membership> m_monadic_memberships;
svector<monadic_assumption> m_monadic_assumptions;
vector<bound_constraint> m_monadic_bounds;
unsigned m_monadic_generation = 0;
unsigned m_monadic_assumption_generation = UINT_MAX;
unsigned m_monadic_fallback_generation = UINT_MAX;
@ -220,6 +233,22 @@ namespace smt {
bool block_if_empty(expr* r, literal lit);
void add_monadic_membership(literal lit, expr* s, expr* r);
// Query current arithmetic length bounds of each monadic membership term and feed
// them to the monadic solver (via add_lo/add_hi/add_len) as extra length regexes,
// so proposed witnesses respect length constraints. Recorded in m_monadic_bounds.
void add_monadic_bounds();
void record_bound(expr* s, expr* len, bound_constraint::kind_t k, unsigned v);
// Encode a monadic membership literal / bounds-constraint index as the void*
// dependency handed to the monadic solver: 2*lit.index() for literals (even),
// 2*bounds_index + 1 for bounds constraints (odd). add_core_literal decodes a
// dependency returned by m_monadic.core() into conflict literal(s).
static void* dep_of_literal(literal lit) {
return reinterpret_cast<void*>(static_cast<size_t>(2 * lit.index()));
}
static void* dep_of_bound(unsigned idx) {
return reinterpret_cast<void*>(static_cast<size_t>(2 * idx + 1));
}
void add_core_literal(void* dep, literal_vector& lits);
void propagate_accept_legacy(literal lit, expr* s, expr* r);
void enable_legacy_fallback();