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 solve_and with incremental add()/check() API

Browse source 
Replace the batch solve_and(mems) with an incremental interface:
  void add(expr* term, expr* regex, u_dependency* d);
  lbool check();
add() stores each (term, regex, dependency) triple in
m_memberships (vector<tuple<expr_ref, expr_ref, u_dependency*>>); the
dependency is retained for future unsat-core tracking and may be nullptr.
check() decides the accumulated conjunction (the former solve_and body) and
consumes the memberships; an empty conjunction is sat. Update the unit tests
and benchmark to the add()/check() API.

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:31:39 -07:00
parent 022a6505ae
commit 1e09b4e6ae
4 changed files with 57 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -420,9 +420,16 @@ lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf) {
return any_undef ? l_undef : l_false;
}
lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> const& mems) {
if (mems.empty())
return l_undef;
void seq_monadic::add(expr* term, expr* regex, u_dependency* d) {
m_memberships.push_back({ expr_ref(term, m), expr_ref(regex, m), d });
}
lbool seq_monadic::check() {
m_model.reset();
vector<std::tuple<expr_ref, expr_ref, u_dependency*>> memberships;
memberships.swap(m_memberships); // consume the asserted memberships
if (memberships.empty())
return l_true; // empty conjunction is vacuously true
m_pin.reset();
reset_cofactor_cache();
m_budget = 200000;
@ -434,16 +441,16 @@ lbool seq_monadic::solve_and(vector<std::pair<expr*, expr*>> const& mems) {
vector<disjunct> combined;
combined.push_back(disjunct()); // { true }
const unsigned DNF_CAP = 1u << 14;
for (auto const& tr : mems) {
for (auto const& [term, regex, d] : memberships) {
vector<disjunct> dnf_i;
if (!build_membership_dnf(tr.first, tr.second, dnf_i))
if (!build_membership_dnf(term, regex, dnf_i))
return l_undef;
vector<disjunct> next;
for (disjunct const& d : combined) {
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(d);
disjunct D(cd);
for (auto const& c : e)
D.push_back(c);
next.push_back(D);

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

@ -43,7 +43,7 @@ Abstract:
Supports single / multiple / repeated variables. Per-variable extra constraints
(e.g. a base membership intersected with a length-regex) are expressed as an extra
membership passed to `solve_and`.
membership passed to `add` and decided by `check`.
Author:
@ -57,7 +57,9 @@ Author:
#include "ast/rewriter/th_rewriter.h"
#include "util/lbool.h"
#include "util/obj_hashtable.h"
#include "util/dependency.h"
#include <utility>
#include <tuple>
class seq_monadic {
public:
@ -77,9 +79,10 @@ 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
bool m_gen_model = true; // whether solve()/check() 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
vector<std::tuple<expr_ref, expr_ref, u_dependency*>> m_memberships; // asserted (term in regex, dep) for check()
seq_util& u() const { return m_rw.u(); }
seq_util::rex& re() const { return m_rw.u().re; }
@ -100,7 +103,7 @@ private:
// Symbolic transition cofactors in the selected mode. Memoized per regex `r`: the
// returned vector is owned by the cofactor cache and stays valid until the next
// top-level solve()/solve_and() (which resets the cache).
// top-level solve()/check() (which resets the cache).
expr_ref_pair_vector const& derivative_cofactors(expr* r);
// Drop all memoized cofactors and free their owned vectors.
@ -147,13 +150,13 @@ 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().
// solve()/check() 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,
// The model extracted by the last successful solve()/check(): 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.
// until the next solve()/check(). 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
@ -161,12 +164,18 @@ public:
// l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up.
lbool solve(expr* term, expr* R);
// Decide a CONJUNCTION of memberships AND_i (term_i in R_i) jointly: a variable
// Assert a membership (term in regex) to be decided jointly by the next check().
// `d` carries the dependency used for unsat-core tracking and may be nullptr.
// Memberships accumulate until check() consumes them.
void add(expr* term, expr* regex, u_dependency* d);
// Decide the CONJUNCTION of all memberships asserted via add() 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').
// l_true = sat, l_false = unsat, l_undef = gave up.
lbool solve_and(vector<std::pair<expr*, expr*>> const& mems);
// Per-variable extra constraints are expressed as extra memberships (v in R').
// Consumes the asserted memberships. l_true = sat (empty conjunction is sat),
// l_false = unsat, l_undef = gave up.
lbool check();
};

31
src/test/seq_monadic.cpp
View file

@ -129,21 +129,19 @@ class seq_monadic_test {
<< " got=" << s(got) << " expected=" << s(expected) << "\n";
}
// build the membership list: the primary (term in R) plus one (var in R') per extra
// constraint, decided jointly by solve_and.
void add_extra(vector<std::pair<expr*, expr*>>& mems, expr* term, expr* R,
obj_map<expr, expr*> const& ve) {
mems.push_back(std::make_pair(term, R));
for (auto const& kv : ve)
mems.push_back(std::make_pair(kv.m_key, kv.m_value));
// assert the membership list: the primary (term in R) plus one (var in R') per extra
// constraint, decided jointly by check().
void add_extra(expr* term, expr* R, obj_map<expr, expr*> const& ve) {
m_mon.add(term, R, nullptr);
for (auto const& [k, v] : ve)
m_mon.add(k, v, nullptr);
}
void check_extra(char const* name, expr* term, expr* R,
obj_map<expr, expr*> const& ve, lbool expected) {
vector<std::pair<expr*, expr*>> mems;
add_extra(mems, term, R, ve);
add_extra(term, R, ve);
m_mon.set_gen_model(false); // this check does not use the model
lbool got = m_mon.solve_and(mems);
lbool got = m_mon.check();
bool ok = (got == expected);
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name
@ -179,10 +177,9 @@ 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) {
vector<std::pair<expr*, expr*>> mems;
add_extra(mems, term, R, ve);
add_extra(term, R, ve);
m_mon.set_gen_model(true); // this check verifies the extracted model
lbool got = m_mon.solve_and(mems);
lbool got = m_mon.check();
obj_map<expr, expr*> const& model = m_mon.get_model();
bool ok = (got == l_true) && !model.empty();
if (ok) {
@ -201,8 +198,10 @@ 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) {
for (auto const& [t, r] : mems)
m_mon.add(t, r, nullptr);
m_mon.set_gen_model(false); // this check does not use the model
lbool got = m_mon.solve_and(mems);
lbool got = m_mon.check();
bool ok = (got == expected);
if (!ok) ++m_fail;
std::cout << (ok ? " OK " : " FAIL ") << name
@ -335,10 +334,10 @@ public:
check_extra("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI, l_true);
check_witness("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI);
// ---- conjunction of memberships (solve_and): a variable shared across memberships
// ---- conjunction of memberships (add + check): a variable shared across memberships
// ---- is constrained jointly. These are cases that are individually SAT but
// ---- jointly UNSAT -- exactly what independent per-membership solving gets wrong.
std::cout << "=== seq_monadic: conjunction of memberships (solve_and) ===\n";
std::cout << "=== seq_monadic: conjunction of memberships (add + check) ===\n";
expr_ref aaS(star(cat(a, a)), m); // (aa)* : even number of a's
expr_ref a_aaS(cat(a, star(cat(a, a))), m); // a(aa)* : odd number of a's
expr_ref abS(star(ab), m); // (ab)*

15
src/test/seq_monadic_bench.cpp
View file

@ -128,20 +128,23 @@ lbool run_file(
for (expr* assertion : ctx.assertions())
complete = collect(assertion) && complete;
vector<std::pair<expr*, expr*>> memberships;
unsigned n_added = 0;
for (expr* term : terms) {
expr* r = nullptr;
term_re.find(term, r);
memberships.push_back(std::make_pair(term, r));
mon.add(term, r, nullptr);
++n_added;
}
for (auto const& [k, v] : var_re) {
mon.add(k, v, nullptr);
++n_added;
}
for (auto const& entry : var_re)
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()
lbool verdict = n_added == 0
? l_undef
: mon.solve_and(memberships);
: mon.check();
solve_ms = std::chrono::duration<double, std::milli>(
std::chrono::high_resolution_clock::now() - start).count();
return verdict;