From 656d1e6bcb647666c0d628eef5464413353ceb4c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2026 14:17:05 -0700 Subject: [PATCH] Refactor guard_set out of seq_monadic into guard_set.h/.cpp 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 --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/guard_set.cpp | 152 +++++++++++++++++++++++++++ src/ast/rewriter/guard_set.h | 67 ++++++++++++ src/ast/rewriter/seq_monadic.cpp | 170 +------------------------------ 4 files changed, 221 insertions(+), 169 deletions(-) create mode 100644 src/ast/rewriter/guard_set.cpp create mode 100644 src/ast/rewriter/guard_set.h diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index dfcdc1be38..afe18ad3f3 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -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 diff --git a/src/ast/rewriter/guard_set.cpp b/src/ast/rewriter/guard_set.cpp new file mode 100644 index 0000000000..5bdbe40398 --- /dev/null +++ b/src/ast/rewriter/guard_set.cpp @@ -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& 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 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 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); +} diff --git a/src/ast/rewriter/guard_set.h b/src/ast/rewriter/guard_set.h new file mode 100644 index 0000000000..f15f582ac7 --- /dev/null +++ b/src/ast/rewriter/guard_set.h @@ -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& 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 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; +}; diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 18418e7d50..ecc58da3a4 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -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 #include #include @@ -53,172 +51,6 @@ Author: #include #include -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& 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 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 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