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

Refactor guard_set out of seq_monadic into guard_set.h/.cpp

Browse source 
Extract the guard_set class (element-value set over derivative cofactor
guards) from the anonymous namespace in seq_monadic.cpp into a
self-contained guard_set.h / guard_set.cpp pair.

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 14:17:05 -07:00
parent ddce973e16
commit 656d1e6bcb
4 changed files with 221 additions and 169 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -26,6 +26,7 @@ z3_add_component(rewriter
finite_set_rewriter.cpp
fpa_rewriter.cpp
func_decl_replace.cpp
guard_set.cpp
inj_axiom.cpp
label_rewriter.cpp
macro_replacer.cpp

152
src/ast/rewriter/guard_set.cpp Normal file
View file

@ -0,0 +1,152 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
guard_set.cpp
Abstract:
Implementation of guard_set. See guard_set.h.
Author:
Nikolaj Bjorner / Margus Veanes 2026
--*/
#include "ast/rewriter/guard_set.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
guard_set::guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0)
: m(_m), u(_u), m_sort(elem_sort), m_v0(v0),
m_is_char(_u.is_char(elem_sort)),
m_rp(_u.max_char()), m_guard(_m) {
if (m_is_char) m_rp = seq::range_predicate::top(u.max_char());
else m_guard = m.mk_true();
}
void guard_set::collect_consts(expr* g, ptr_vector<expr>& out) const {
expr* a = nullptr, * b = nullptr;
if (m.is_and(g) || m.is_or(g)) {
for (expr* arg : *to_app(g)) collect_consts(arg, out);
return;
}
if (m.is_not(g, a)) { collect_consts(a, out); return; }
if (m.is_eq(g, a, b)) {
if (a == m_v0 && b != m_v0) out.push_back(b);
else if (b == m_v0 && a != m_v0) out.push_back(a);
}
}
lbool guard_set::eval_at(expr* g, expr* cand) const {
expr* a = nullptr, * b = nullptr;
if (m.is_true(g)) return l_true;
if (m.is_false(g)) return l_false;
if (m.is_not(g, a)) {
lbool r = eval_at(a, cand);
return r == l_undef ? l_undef : (r == l_true ? l_false : l_true);
}
if (m.is_and(g)) {
lbool r = l_true;
for (expr* arg : *to_app(g)) {
lbool e = eval_at(arg, cand);
if (e == l_false) return l_false;
if (e == l_undef) r = l_undef;
}
return r;
}
if (m.is_or(g)) {
lbool r = l_false;
for (expr* arg : *to_app(g)) {
lbool e = eval_at(arg, cand);
if (e == l_true) return l_true;
if (e == l_undef) r = l_undef;
}
return r;
}
if (m.is_eq(g, a, b)) {
expr* other = (a == m_v0) ? b : (b == m_v0 ? a : nullptr);
if (!other) return l_undef;
if (other == m_v0) return l_true;
return (cand == other) ? l_true : l_false; // canonical values: identity == equality
}
return l_undef;
}
bool guard_set::mk_fresh(ptr_vector<expr> const& consts, expr_ref& out) const {
if (m.is_bool(m_sort)) {
bool hasT = false, hasF = false;
for (expr* c : consts) { if (m.is_true(c)) hasT = true; else if (m.is_false(c)) hasF = true; }
if (!hasT) { out = m.mk_true(); return true; }
if (!hasF) { out = m.mk_false(); return true; }
return false;
}
arith_util a(m);
if (a.is_int_real(m_sort)) {
rational mx(0); bool any = false;
for (expr* c : consts) {
rational v;
if (a.is_numeral(c, v)) { if (!any || v > mx) mx = v; any = true; }
}
out = a.mk_numeral(any ? mx + rational(1) : rational(0), a.is_int(m_sort));
return true;
}
bv_util bv(m);
if (bv.is_bv_sort(m_sort)) {
unsigned sz = bv.get_bv_size(m_sort);
for (unsigned k = 0; k <= consts.size(); ++k) {
rational kv(k);
bool clash = false;
for (expr* c : consts) {
rational v; unsigned bsz = 0;
if (bv.is_numeral(c, v, bsz) && v == kv) { clash = true; break; }
}
if (!clash) { out = bv.mk_numeral(kv, sz); return true; }
}
return false;
}
return false;
}
lbool guard_set::generic_eval(expr_ref* witness) const {
ptr_vector<expr> consts;
collect_consts(m_guard, consts);
bool saw_undef = false;
for (expr* c : consts) {
lbool r = eval_at(m_guard, c);
if (r == l_true) { if (witness) *witness = expr_ref(c, m); return l_true; }
if (r == l_undef) saw_undef = true;
}
expr_ref fresh(m);
if (mk_fresh(consts, fresh)) {
lbool r = eval_at(m_guard, fresh);
if (r == l_true) { if (witness) *witness = fresh; return l_true; }
if (r == l_undef) saw_undef = true;
}
else
saw_undef = true; // the "distinct from all mentioned values" region is untested
return saw_undef ? l_undef : l_false;
}
void guard_set::conjoin(expr* g) {
if (!m_ok) return;
if (m_is_char) {
seq::range_predicate s(u.max_char());
if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; }
m_rp = m_rp & s;
}
else
m_guard = m.mk_and(m_guard, g);
}
lbool guard_set::eval(expr_ref* witness) const {
if (!m_ok) return l_undef;
if (m_is_char) {
if (m_rp.is_empty()) return l_false;
if (witness) *witness = expr_ref(u.mk_char(m_rp[0].first), m);
return l_true;
}
return generic_eval(witness);
}

67
src/ast/rewriter/guard_set.h Normal file
View file

@ -0,0 +1,67 @@
/*++
Copyright (c) 2026 Microsoft Corporation
Module Name:
guard_set.h
Abstract:
A conjunction of derivative cofactor guards over the element variable
v0 = (:var 0), interpreted as the set of element values satisfying it.
Two representations by element sort:
* character sort: the exact, compact seq::range_predicate.
* any other sort: the guard predicate kept symbolically and decided by a
candidate basis -- the element values mentioned in the guards, plus one
fresh value. This is sound and complete for the
{true,false,=,<=,and,or,not} grammar the derivatives emit (over a general
element sort only equalities appear).
Extracted from seq_monadic.cpp.
Author:
Nikolaj Bjorner / Margus Veanes 2026
--*/
#pragma once
#include "ast/ast.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_range_collapse.h"
class guard_set {
ast_manager& m;
seq_util& u;
sort* m_sort;
expr* m_v0;
bool m_is_char;
bool m_ok = true; // false: an unsupported guard was conjoined
seq::range_predicate m_rp; // char representation
expr_ref m_guard; // generic representation (conjunction over v0)
// ---- generic path: candidate basis ----
// element values compared to v0 by the equalities in `g`.
void collect_consts(expr* g, ptr_vector<expr>& out) const;
// evaluate `g` at v0 := cand ; l_undef on a construct outside the grammar.
lbool eval_at(expr* g, expr* cand) const;
// a value of m_sort distinct from every element of `consts`, if one can be built.
bool mk_fresh(ptr_vector<expr> const& consts, expr_ref& out) const;
lbool generic_eval(expr_ref* witness) const;
public:
guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0);
bool ok() const { return m_ok; }
// AND in a cofactor guard g (a Boolean over v0).
void conjoin(expr* g);
// l_false = empty, l_true = non-empty (sets *witness if non-null to a concrete
// element of the set), l_undef = unknown / unsupported guard.
lbool eval(expr_ref* witness) const;
};

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

@ -43,9 +43,7 @@ Author:
--*/
#include "ast/rewriter/seq_monadic.h"
#include "ast/rewriter/seq_range_collapse.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/guard_set.h"
#include <set>
#include <vector>
#include <map>
@ -53,172 +51,6 @@ Author:
#include <functional>
#include <algorithm>
namespace {
// A conjunction of derivative cofactor guards over the element variable v0 = (:var 0),
// interpreted as the set of element values satisfying it. Two representations by
// element sort:
// * character sort: the exact, compact seq::range_predicate.
// * any other sort: the guard predicate kept symbolically and decided by a candidate
// basis -- the element values mentioned in the guards, plus one fresh value. This
// is sound and complete for the {true,false,=,<=,and,or,not} grammar the derivatives
// emit (over a general element sort only equalities appear).
class guard_set {
ast_manager& m;
seq_util& u;
sort* m_sort;
expr* m_v0;
bool m_is_char;
bool m_ok = true; // false: an unsupported guard was conjoined
seq::range_predicate m_rp; // char representation
expr_ref m_guard; // generic representation (conjunction over v0)
// ---- generic path: candidate basis ----
// element values compared to v0 by the equalities in `g`.
void collect_consts(expr* g, ptr_vector<expr>& out) const {
expr* a = nullptr, * b = nullptr;
if (m.is_and(g) || m.is_or(g)) {
for (expr* arg : *to_app(g)) collect_consts(arg, out);
return;
}
if (m.is_not(g, a)) { collect_consts(a, out); return; }
if (m.is_eq(g, a, b)) {
if (a == m_v0 && b != m_v0) out.push_back(b);
else if (b == m_v0 && a != m_v0) out.push_back(a);
}
}
// evaluate `g` at v0 := cand ; l_undef on a construct outside the grammar.
lbool eval_at(expr* g, expr* cand) const {
expr* a = nullptr, * b = nullptr;
if (m.is_true(g)) return l_true;
if (m.is_false(g)) return l_false;
if (m.is_not(g, a)) {
lbool r = eval_at(a, cand);
return r == l_undef ? l_undef : (r == l_true ? l_false : l_true);
}
if (m.is_and(g)) {
lbool r = l_true;
for (expr* arg : *to_app(g)) {
lbool e = eval_at(arg, cand);
if (e == l_false) return l_false;
if (e == l_undef) r = l_undef;
}
return r;
}
if (m.is_or(g)) {
lbool r = l_false;
for (expr* arg : *to_app(g)) {
lbool e = eval_at(arg, cand);
if (e == l_true) return l_true;
if (e == l_undef) r = l_undef;
}
return r;
}
if (m.is_eq(g, a, b)) {
expr* other = (a == m_v0) ? b : (b == m_v0 ? a : nullptr);
if (!other) return l_undef;
if (other == m_v0) return l_true;
return (cand == other) ? l_true : l_false; // canonical values: identity == equality
}
return l_undef;
}
// a value of m_sort distinct from every element of `consts`, if one can be built.
bool mk_fresh(ptr_vector<expr> const& consts, expr_ref& out) const {
if (m.is_bool(m_sort)) {
bool hasT = false, hasF = false;
for (expr* c : consts) { if (m.is_true(c)) hasT = true; else if (m.is_false(c)) hasF = true; }
if (!hasT) { out = m.mk_true(); return true; }
if (!hasF) { out = m.mk_false(); return true; }
return false;
}
arith_util a(m);
if (a.is_int_real(m_sort)) {
rational mx(0); bool any = false;
for (expr* c : consts) {
rational v;
if (a.is_numeral(c, v)) { if (!any || v > mx) mx = v; any = true; }
}
out = a.mk_numeral(any ? mx + rational(1) : rational(0), a.is_int(m_sort));
return true;
}
bv_util bv(m);
if (bv.is_bv_sort(m_sort)) {
unsigned sz = bv.get_bv_size(m_sort);
for (unsigned k = 0; k <= consts.size(); ++k) {
rational kv(k);
bool clash = false;
for (expr* c : consts) {
rational v; unsigned bsz = 0;
if (bv.is_numeral(c, v, bsz) && v == kv) { clash = true; break; }
}
if (!clash) { out = bv.mk_numeral(kv, sz); return true; }
}
return false;
}
return false;
}
lbool generic_eval(expr_ref* witness) const {
ptr_vector<expr> consts;
collect_consts(m_guard, consts);
bool saw_undef = false;
for (expr* c : consts) {
lbool r = eval_at(m_guard, c);
if (r == l_true) { if (witness) *witness = expr_ref(c, m); return l_true; }
if (r == l_undef) saw_undef = true;
}
expr_ref fresh(m);
if (mk_fresh(consts, fresh)) {
lbool r = eval_at(m_guard, fresh);
if (r == l_true) { if (witness) *witness = fresh; return l_true; }
if (r == l_undef) saw_undef = true;
}
else
saw_undef = true; // the "distinct from all mentioned values" region is untested
return saw_undef ? l_undef : l_false;
}
public:
guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0)
: m(_m), u(_u), m_sort(elem_sort), m_v0(v0),
m_is_char(_u.is_char(elem_sort)),
m_rp(_u.max_char()), m_guard(_m) {
if (m_is_char) m_rp = seq::range_predicate::top(u.max_char());
else m_guard = m.mk_true();
}
bool ok() const { return m_ok; }
// AND in a cofactor guard g (a Boolean over v0).
void conjoin(expr* g) {
if (!m_ok) return;
if (m_is_char) {
seq::range_predicate s(u.max_char());
if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; }
m_rp = m_rp & s;
}
else
m_guard = m.mk_and(m_guard, g);
}
// l_false = empty, l_true = non-empty (sets *witness if non-null to a concrete
// element of the set), l_undef = unknown / unsupported guard.
lbool eval(expr_ref* witness) const {
if (!m_ok) return l_undef;
if (m_is_char) {
if (m_rp.is_empty()) return l_false;
if (witness) *witness = expr_ref(u.mk_char(m_rp[0].first), m);
return l_true;
}
return generic_eval(witness);
}
};
}
expr_ref seq_monadic::der_elem(expr* r, expr* elem) {
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