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

create config object

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-02 14:17:22 -07:00
parent b47a94c089
commit ed4a639841
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -396,7 +396,7 @@ lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf) {
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_gen_model ? &w : nullptr);
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_gen_model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); }
@ -482,7 +482,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
void seq_monadic::minimize_core(membership_vec const& memberships) {
m_core.reset();
if (!m_min_core) {
if (!m_config.m_min_core) {
// No minimization: the core is simply every asserted membership's dependency.
for (auto const& [term, regex, d] : memberships)
if (d)

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

@ -94,6 +94,7 @@ private:
void maybe_reset(unsigned cap) { if (m_cache.size() > cap) reset(); }
};
struct config {
ast_manager& m;
seq_rewriter& m_rw;
th_rewriter m_thrw; // normalizes constant-element derivatives (folds
@ -105,7 +106,6 @@ 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()/check() extract a feasible model
bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps)
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)