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_monadic: replace model out-param with gen-model toggle + get_model()

Browse source 
Remove the obj_map<expr,expr*>* model out-parameter from solve/solve_and/
decide_dnf. Add an m_gen_model flag (default true) with set_gen_model(bool),
store the extracted model in m_model (reset at the top of decide_dnf), and
expose get_model(). Switch live_states out to expr_ref_vector and the
product_nonempty state vectors to ptr_vector<expr>. Simplify the concat case
of parse_term with all_of. Disable model generation in the sat-only unit
tests and the benchmark.

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-07-31 20:14:59 -07:00
parent 5650fb2460
commit 773c5496b9
4 changed files with 54 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -80,7 +80,7 @@ void seq_monadic::reset_cofactor_cache() {
m_cofactor_cache.reset();
}
bool seq_monadic::live_states(expr* R, ptr_vector<expr>& out) {
bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
obj_map<expr, unsigned> id;
expr_ref_vector states(m);
vector<svector<unsigned>> succ;
@ -133,11 +133,11 @@ 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
svector<expr*> start;
ptr_vector<expr> start;
for (auto const& c : comps)
start.push_back(c.state);
auto id_key = [&](svector<expr*> const& st) {
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());
@ -146,7 +146,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
typedef std::vector<unsigned> key;
bool undecided = false;
auto is_accept = [&](svector<expr*> const& st) -> bool {
auto is_accept = [&](ptr_vector<expr> const& st) -> bool {
for (unsigned i = 0; i < n; ++i) {
if (comps[i].target) {
if (st[i] != comps[i].target) return false;
@ -162,7 +162,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
};
std::set<key> visited;
std::vector<svector<expr*>> work;
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;
@ -193,7 +193,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
--m_budget;
if (!m.inc())
return l_undef;
svector<expr*> st = work.back();
ptr_vector<expr> st = work.back();
work.pop_back();
if (is_accept(st)) {
if (witness_word)
@ -217,7 +217,7 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
// joint transitions = cartesian product of the branches with the guards
// conjoined; prune as soon as the accumulated guard is empty, bail on unknown.
svector<expr*> cur;
ptr_vector<expr> cur;
cur.resize(n);
key st_key = id_key(st);
bool bail = false;
@ -259,13 +259,8 @@ lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* w
}
bool seq_monadic::parse_term(expr* t, svector<atom>& atoms, expr*& the_var) {
if (u().str.is_concat(t)) {
app* a = to_app(t);
for (unsigned i = 0; i < a->get_num_args(); ++i)
if (!parse_term(a->get_arg(i), atoms, the_var))
return false;
return true;
}
if (u().str.is_concat(t))
return all_of(*to_app(t), [&](expr* arg) { return parse_term(arg, atoms, the_var); });
if (u().str.is_empty(t))
return true; // epsilon: contributes nothing
zstring s;
@ -320,7 +315,7 @@ bool seq_monadic::decompose(svector<atom> const& atoms, unsigned i, expr* R,
return true;
}
// a variable with a non-empty rest: split over the live states q of R (midpoints)
ptr_vector<expr> Q;
expr_ref_vector Q(m);
if (!live_states(R, Q))
return false;
const unsigned DISJUNCT_CAP = 1u << 13;
@ -362,7 +357,14 @@ void seq_monadic::simplify_dnf(vector<disjunct>& dnf) {
}
lbool seq_monadic::solve(expr* term, expr* R) {
return solve(term, R, nullptr);
m_pin.reset();
reset_cofactor_cache();
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) {
@ -380,7 +382,8 @@ bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector<disjunct>& dn
return decompose(atoms, 0, R, dnf);
}
lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf, obj_map<expr, expr*>* model) {
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
@ -402,34 +405,22 @@ lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf, obj_map<expr, expr*>*
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], model ? &w : nullptr);
lbool ne = product_nonempty(groups[gi], m_gen_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 (model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); }
if (m_gen_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 (model)
if (m_gen_model)
for (auto const& [k, v] : local)
model->insert(k, v);
m_model.insert(k, v);
return l_true; // all variables satisfiable => sat
}
return any_undef ? l_undef : l_false;
}
lbool seq_monadic::solve(expr* term, expr* R, obj_map<expr, expr*>* model) {
m_pin.reset();
reset_cofactor_cache();
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, model);
}
lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> const& mems,
obj_map<expr, expr*>* model) {
lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> const& mems) {
if (mems.empty())
return l_undef;
m_pin.reset();
@ -463,5 +454,5 @@ lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> const& mems,
if (combined.empty())
return l_false; // no viable disjunct left => unsat
}
return decide_dnf(combined, model);
return decide_dnf(combined);
}

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

@ -77,6 +77,8 @@ private:
expr_ref_vector m_pin; // pins derivative states / witnesses referenced later
unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops)
bool m_giveup = false; // set when the budget is exhausted
bool m_gen_model = true; // whether solve()/solve_and() extract a feasible model
obj_map<expr, expr*> m_model; // last extracted model (var -> witness); see get_model()
obj_map<expr, expr_ref_pair_vector*> m_cofactor_cache; // memoizes derivative_cofactors per regex
seq_util& u() const { return m_rw.u(); }
@ -106,7 +108,7 @@ private:
// Live reachable derivative states of R (BFS over cofactor targets + liveness
// least-fixpoint). These are the split states q. Returns false on a cap overrun.
bool live_states(expr* R, ptr_vector<expr>& out);
bool live_states(expr* R, expr_ref_vector& out);
// 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
@ -132,8 +134,9 @@ private:
bool build_membership_dnf(expr* term, expr* R, vector<disjunct>& dnf);
// Decide a DNF (over primitive components): sat iff some disjunct has every variable
// group non-empty. On l_true, fills `model` (var -> witness) if non-null.
lbool decide_dnf(vector<disjunct> const& dnf, obj_map<expr, expr*>* model);
// group non-empty. On l_true, when model generation is enabled, fills m_model
// (var -> witness).
lbool decide_dnf(vector<disjunct> const& dnf);
public:
seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) :
@ -143,24 +146,27 @@ public:
transition_mode mode() const { return m_mode; }
// Enable/disable model generation (default: enabled). When enabled, a successful
// solve()/solve_and() extracts a feasible model retrievable via get_model().
void set_gen_model(bool b) { m_gen_model = b; }
// The model extracted by the last successful solve()/solve_and(): var -> witness,
// where each witness is a concrete sequence term (over the element sort) giving one
// satisfying assignment. Witness terms are pinned by the solver and remain valid
// until the next solve()/solve_and(). Only valid when model generation is enabled.
obj_map<expr, expr*> const& get_model() const { return m_model; }
// Decide (str.in_re term R) for a term that is a concatenation of string variables
// (possibly repeated / several distinct) and constant characters.
// l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up.
lbool solve(expr* term, expr* R);
// As above; on l_true, if `model` is non-null it is populated with var -> witness,
// where each witness is a concrete sequence term (over the element sort) giving one
// satisfying assignment. Witness terms are pinned by the solver and remain valid
// until the next call to solve().
lbool solve(expr* term, expr* R, obj_map<expr, expr*>* model);
// Decide a CONJUNCTION of memberships AND_i (term_i in R_i) jointly: a variable
// shared across memberships is constrained consistently (the DNFs are multiplied and
// each variable's constraints intersected). This is the natural extension of single-
// membership solving to a Boolean combination of memberships (a disjunction is the
// union of DNFs; a negated membership ~(t in R) is just t in complement(R)).
// Per-variable extra constraints are expressed here as extra memberships (v in R').
// model as above. l_true = sat, l_false = unsat, l_undef = gave up.
lbool solve_and(vector<std::pair<expr*, expr*>> const& mems,
obj_map<expr, expr*>* model = nullptr);
// l_true = sat, l_false = unsat, l_undef = gave up.
lbool solve_and(vector<std::pair<expr*, expr*>> const& mems);
};

12
src/test/seq_monadic.cpp
View file

@ -121,6 +121,7 @@ class seq_monadic_test {
}
void check(char const* name, expr* term, expr* R, lbool expected) {
m_mon.set_gen_model(false); // this check does not use the model
lbool got = m_mon.solve(term, R);
bool ok = (got == expected);
if (!ok) ++m_fail;
@ -141,7 +142,8 @@ class seq_monadic_test {
obj_map<expr, expr*> const& ve, lbool expected) {
vector<std::pair<expr*, expr*>> mems;
add_extra(mems, term, R, ve);
lbool got = m_mon.solve_and(mems, nullptr);
m_mon.set_gen_model(false); // this check does not use the model
lbool got = m_mon.solve_and(mems);
bool ok = (got == expected);
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name
@ -177,10 +179,11 @@ class seq_monadic_test {
// term a member of R (substitute var -> witness and re-decide by derivatives).
void check_witness(char const* name, expr* term, expr* R,
obj_map<expr, expr*> const& ve) {
obj_map<expr, expr*> model;
vector<std::pair<expr*, expr*>> mems;
add_extra(mems, term, R, ve);
lbool got = m_mon.solve_and(mems, &model);
m_mon.set_gen_model(true); // this check verifies the extracted model
lbool got = m_mon.solve_and(mems);
obj_map<expr, expr*> const& model = m_mon.get_model();
bool ok = (got == l_true) && !model.empty();
if (ok) {
expr_safe_replace rep(m);
@ -198,7 +201,8 @@ class seq_monadic_test {
// decide a conjunction of memberships jointly (shared variables constrained together).
void check_and(char const* name, vector<std::pair<expr*, expr*>> const& mems, lbool expected) {
lbool got = m_mon.solve_and(mems, nullptr);
m_mon.set_gen_model(false); // this check does not use the model
lbool got = m_mon.solve_and(mems);
bool ok = (got == expected);
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name

3
src/test/seq_monadic_bench.cpp
View file

@ -138,9 +138,10 @@ lbool run_file(
memberships.push_back(std::make_pair(entry.m_key, entry.m_value));
auto start = std::chrono::high_resolution_clock::now();
mon.set_gen_model(false); // benchmark only needs the verdict
lbool verdict = memberships.empty()
? l_undef
: mon.solve_and(memberships, nullptr);
: mon.solve_and(memberships);
solve_ms = std::chrono::duration<double, std::milli>(
std::chrono::high_resolution_clock::now() - start).count();
return verdict;