mirror of
https://github.com/Z3Prover/z3
synced 2026-08-07 22:42:20 +00:00
Add readable seq_monadic state display (#10415)
## Summary - add a public `seq_monadic::display(std::ostream&)` API - show configuration, asserted memberships, result artifacts, internal search state, caches, and statistics - distinguish public results from unsat-core minimization searches and clear stale artifacts across calls - add focused display-state coverage ## Testing - `test-z3 seq_monadic` - `test-z3 seq_monadic_bench` - `test-z3 /a` (94 passed) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7
This commit is contained in:
Nikolaj Bjorner
GitHub
parent
26c5a11e17
commit
be03bfa359
3 changed files with 236 additions and 8 deletions
|
|
@ -59,6 +59,36 @@ Author:
|
|||
#include <algorithm>
|
||||
#include <unordered_set>
|
||||
|
||||
namespace {
|
||||
char const* mode_name(seq::transition_mode mode) {
|
||||
switch (mode) {
|
||||
case seq::transition_mode::brzozowski_tm:
|
||||
return "brzozowski";
|
||||
case seq::transition_mode::light_antimirov_tm:
|
||||
return "light-antimirov";
|
||||
default:
|
||||
return "unknown";
|
||||
}
|
||||
}
|
||||
|
||||
char const* bail_name(unsigned i) {
|
||||
static char const* const names[] = {
|
||||
"unsupported",
|
||||
"state-cap",
|
||||
"dnf-cap",
|
||||
"budget",
|
||||
"resource",
|
||||
"nullability",
|
||||
"guard"
|
||||
};
|
||||
return i < std::size(names) ? names[i] : "unknown";
|
||||
}
|
||||
|
||||
char const* result_name(lbool r) {
|
||||
return r == l_true ? "sat" : r == l_false ? "unsat" : "unknown";
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
expr_ref seq_monadic::der_elem(expr* r, expr* elem) {
|
||||
expr* cached = nullptr;
|
||||
|
|
@ -375,6 +405,8 @@ unsigned seq_monadic::var_index(expr* v) {
|
|||
}
|
||||
|
||||
void seq_monadic::reset_search() {
|
||||
m_seq_sort = nullptr;
|
||||
m_elem_sort = nullptr;
|
||||
m_atoms.reset();
|
||||
m_regexes.reset();
|
||||
m_vars.reset();
|
||||
|
|
@ -563,27 +595,31 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
|
|||
}
|
||||
|
||||
lbool seq_monadic::decide(membership_vec const& memberships) {
|
||||
m_last_search_memberships = memberships;
|
||||
m_model.reset();
|
||||
if (memberships.empty())
|
||||
return l_true; // empty conjunction is vacuously true
|
||||
reset_search(); // clear the caches before dropping the
|
||||
m_pin.reset(); // pins that keep their keys alive
|
||||
m_rp_cache.maybe_reset(1u << 16);
|
||||
m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16);
|
||||
m_budget = 200000;
|
||||
m_giveup = false;
|
||||
if (!prepare(memberships))
|
||||
return l_undef;
|
||||
lbool r = dfs_membership(0);
|
||||
lbool r = l_true; // empty conjunction is vacuously true
|
||||
if (!memberships.empty() && !prepare(memberships))
|
||||
r = l_undef;
|
||||
else if (!memberships.empty())
|
||||
r = dfs_membership(0);
|
||||
if (r != l_true)
|
||||
m_model.reset();
|
||||
m_last_search_result = r;
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool seq_monadic::solve(expr* term, expr* R) {
|
||||
m_core.reset();
|
||||
membership_vec mv;
|
||||
mv.push_back({ expr_ref(term, m), expr_ref(R, m), nullptr });
|
||||
return decide(mv);
|
||||
m_last_result = decide(mv);
|
||||
return m_last_result;
|
||||
}
|
||||
|
||||
void seq_monadic::add(expr* term, expr* regex, void* d) {
|
||||
|
|
@ -682,9 +718,132 @@ void seq_monadic::minimize_core(membership_vec const& memberships) {
|
|||
lbool seq_monadic::check() {
|
||||
m_core.reset();
|
||||
lbool r = decide(m_memberships);
|
||||
if (r == l_false)
|
||||
if (r == l_false) {
|
||||
minimize_core(m_memberships);
|
||||
return r;
|
||||
m_model.reset();
|
||||
}
|
||||
m_last_result = r;
|
||||
return m_last_result;
|
||||
}
|
||||
|
||||
std::ostream& seq_monadic::display(std::ostream& out) const {
|
||||
auto display_expr = [&](expr* e) {
|
||||
if (e)
|
||||
out << mk_pp(e, m);
|
||||
else
|
||||
out << "null";
|
||||
};
|
||||
|
||||
out << "(seq-monadic\n"
|
||||
<< " :mode " << mode_name(m_config.m_mode) << "\n"
|
||||
<< " :generate-model " << (m_config.m_model ? "true" : "false") << "\n"
|
||||
<< " :minimize-core " << (m_config.m_min_core ? "true" : "false") << "\n"
|
||||
<< " :last-result " << result_name(m_last_result) << "\n"
|
||||
<< " :budget " << m_budget << "\n"
|
||||
<< " :giveup " << (m_giveup ? "true" : "false") << "\n"
|
||||
<< " :sequence-sort ";
|
||||
if (m_seq_sort)
|
||||
out << mk_pp(m_seq_sort, m);
|
||||
else
|
||||
out << "null";
|
||||
out << "\n :element-sort ";
|
||||
if (m_elem_sort)
|
||||
out << mk_pp(m_elem_sort, m);
|
||||
else
|
||||
out << "null";
|
||||
|
||||
out << "\n :memberships (";
|
||||
for (unsigned i = 0; i < m_memberships.size(); ++i) {
|
||||
auto const& [term, regex, dep] = m_memberships[i];
|
||||
out << "\n [" << i << "] ";
|
||||
display_expr(term);
|
||||
out << " in ";
|
||||
display_expr(regex);
|
||||
out << " :dependency " << dep;
|
||||
}
|
||||
if (!m_memberships.empty())
|
||||
out << "\n ";
|
||||
out << ")\n :model (";
|
||||
for (auto const& [var, value] : m_model) {
|
||||
out << "\n ";
|
||||
display_expr(var);
|
||||
out << " -> ";
|
||||
display_expr(value);
|
||||
}
|
||||
if (!m_model.empty())
|
||||
out << "\n ";
|
||||
out << ")\n :core (";
|
||||
for (void* dep : m_core)
|
||||
out << " " << dep;
|
||||
out << " )";
|
||||
|
||||
out << "\n :last-internal-search\n"
|
||||
<< " (:result " << result_name(m_last_search_result)
|
||||
<< "\n :memberships (";
|
||||
for (unsigned i = 0; i < m_last_search_memberships.size(); ++i) {
|
||||
auto const& [term, regex, dep] = m_last_search_memberships[i];
|
||||
out << "\n [" << i << "] ";
|
||||
display_expr(term);
|
||||
out << " in ";
|
||||
display_expr(regex);
|
||||
out << " :dependency " << dep;
|
||||
}
|
||||
if (!m_last_search_memberships.empty())
|
||||
out << "\n ";
|
||||
out << ")\n :variables (";
|
||||
for (expr* var : m_vars) {
|
||||
out << " ";
|
||||
display_expr(var);
|
||||
}
|
||||
out << " )\n :parsed-memberships (";
|
||||
for (unsigned mi = 0; mi < m_atoms.size(); ++mi) {
|
||||
out << "\n [" << mi << "] :regex ";
|
||||
display_expr(m_regexes.get(mi));
|
||||
out << " :atoms (";
|
||||
for (atom const& a : m_atoms[mi]) {
|
||||
out << " " << (a.is_var ? "var:" : "elem:");
|
||||
display_expr(a.is_var ? a.var.get() : a.elem.get());
|
||||
}
|
||||
out << " )";
|
||||
}
|
||||
if (!m_atoms.empty())
|
||||
out << "\n ";
|
||||
out << ")\n :groups (";
|
||||
for (unsigned vi = 0; vi < m_groups.size(); ++vi) {
|
||||
out << "\n ";
|
||||
display_expr(m_vars[vi]);
|
||||
out << " (";
|
||||
for (component const& c : m_groups[vi]) {
|
||||
out << "\n ";
|
||||
display_expr(c.state);
|
||||
if (c.target) {
|
||||
out << " -> ";
|
||||
display_expr(c.target);
|
||||
}
|
||||
else {
|
||||
out << " nullable";
|
||||
}
|
||||
}
|
||||
if (!m_groups[vi].empty())
|
||||
out << "\n ";
|
||||
out << ")";
|
||||
}
|
||||
if (!m_groups.empty())
|
||||
out << "\n ";
|
||||
out << ")\n"
|
||||
<< " :undefined-variables " << m_undef_vars << "\n"
|
||||
<< " :group-cache-size " << m_group_cache.size() << "\n"
|
||||
<< " :derivative-cache-size " << m_der_cache.size() << "\n"
|
||||
<< " :nullable-cache-size " << m_nullable_cache.size() << "\n"
|
||||
<< " :live-cache-size " << m_live_cache.size() << "\n"
|
||||
<< " :pinned-expressions " << m_pin.size() << ")\n";
|
||||
|
||||
out << " :statistics\n"
|
||||
<< " (:cofactor-calls " << m_stats.m_cofactor_calls << "\n"
|
||||
<< " :states " << m_stats.m_states;
|
||||
for (unsigned i = 0; i < static_cast<unsigned>(bail_reason::num_reasons); ++i)
|
||||
out << "\n :bail-" << bail_name(i) << " " << m_stats.m_bails[i];
|
||||
return out << "))\n";
|
||||
}
|
||||
|
||||
void seq_monadic::collect_statistics(::statistics& st) const {
|
||||
|
|
|
|||
|
|
@ -118,8 +118,11 @@ class seq_monadic {
|
|||
// seq_rewriter's own cache is capped and flushed whole
|
||||
using membership_vec = vector<std::tuple<expr_ref, expr_ref, void*>>;
|
||||
membership_vec m_memberships; // asserted (term in regex, dep) for check()
|
||||
membership_vec m_last_search_memberships; // inputs used by the last internal decide()
|
||||
ptr_vector<void> m_core; // dependencies of an unsat subset, filled by check() on l_false
|
||||
std::function<bool(expr *)> m_is_var; // predicate for whether a term is a sequence variable
|
||||
lbool m_last_result = l_undef; // result of the last public solve()/check()
|
||||
lbool m_last_search_result = l_undef; // result of the last internal decide()
|
||||
|
||||
seq_util& u() const { return m_rw.u(); }
|
||||
seq_util::rex& re() const { return m_rw.u().re; }
|
||||
|
|
@ -252,6 +255,9 @@ public:
|
|||
|
||||
void collect_statistics(::statistics &st) const;
|
||||
|
||||
// Display asserted constraints, result artifacts, search state, caches, and counters.
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
seq::transition_mode mode() const { return m_config.m_mode; }
|
||||
|
||||
// Enable/disable model generation (default: enabled). When enabled, a successful
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@ Author:
|
|||
#include "params/smt_params.h"
|
||||
#include "smt/smt_kernel.h"
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <set>
|
||||
|
||||
namespace {
|
||||
|
|
@ -467,6 +468,68 @@ public:
|
|||
std::cout << (trail_ok ? " OK " : " FAIL ")
|
||||
<< "check preserves assertions and pop removes them\n";
|
||||
|
||||
std::cout << "=== seq_monadic: display ===\n";
|
||||
m_trail.push_scope();
|
||||
unsigned display_dep = 0;
|
||||
m_mon.set_gen_model(true);
|
||||
m_mon.add(x, aaS, &display_dep);
|
||||
lbool display_result = m_mon.check();
|
||||
std::ostringstream display_out;
|
||||
m_mon.display(display_out);
|
||||
std::string display_text = display_out.str();
|
||||
bool display_ok =
|
||||
display_result == l_true &&
|
||||
display_text.find("(seq-monadic") != std::string::npos &&
|
||||
display_text.find(":memberships") != std::string::npos &&
|
||||
display_text.find(":model") != std::string::npos &&
|
||||
display_text.find(":last-result sat") != std::string::npos &&
|
||||
display_text.find(":last-internal-search") != std::string::npos &&
|
||||
display_text.find(":parsed-memberships") != std::string::npos &&
|
||||
display_text.find(":statistics") != std::string::npos &&
|
||||
display_text.find("x") != std::string::npos;
|
||||
m_trail.pop_scope(1);
|
||||
if (!display_ok) ++m_fail;
|
||||
std::cout << (display_ok ? " OK " : " FAIL ")
|
||||
<< "display exposes readable solver state\n";
|
||||
|
||||
m_trail.push_scope();
|
||||
unsigned display_dep1 = 1, display_dep2 = 2;
|
||||
m_mon.set_min_core(true);
|
||||
m_mon.add(x, aaS, &display_dep1);
|
||||
m_mon.add(x, a_aaS, &display_dep2);
|
||||
lbool unsat_display_result = m_mon.check();
|
||||
std::ostringstream unsat_display_out;
|
||||
m_mon.display(unsat_display_out);
|
||||
std::string unsat_display_text = unsat_display_out.str();
|
||||
bool unsat_display_ok =
|
||||
unsat_display_result == l_false &&
|
||||
unsat_display_text.find(":last-result unsat") != std::string::npos &&
|
||||
unsat_display_text.find(":model ()") != std::string::npos &&
|
||||
unsat_display_text.find(":last-internal-search") != std::string::npos;
|
||||
m_trail.pop_scope(1);
|
||||
m_mon.set_min_core(false);
|
||||
if (!unsat_display_ok) ++m_fail;
|
||||
std::cout << (unsat_display_ok ? " OK " : " FAIL ")
|
||||
<< "display distinguishes unsat result from core-search state\n";
|
||||
|
||||
lbool solve_display_result = m_mon.solve(x, aaS);
|
||||
std::ostringstream solve_display_out;
|
||||
m_mon.display(solve_display_out);
|
||||
bool solve_display_ok =
|
||||
solve_display_result == l_true &&
|
||||
solve_display_out.str().find(":core ( )") != std::string::npos;
|
||||
lbool empty_display_result = m_mon.check();
|
||||
std::ostringstream empty_display_out;
|
||||
m_mon.display(empty_display_out);
|
||||
std::string empty_display_text = empty_display_out.str();
|
||||
bool empty_display_ok =
|
||||
empty_display_result == l_true &&
|
||||
empty_display_text.find(":sequence-sort null") != std::string::npos &&
|
||||
empty_display_text.find(":element-sort null") != std::string::npos;
|
||||
if (!solve_display_ok || !empty_display_ok) ++m_fail;
|
||||
std::cout << (solve_display_ok && empty_display_ok ? " OK " : " FAIL ")
|
||||
<< "display clears artifacts across solve and empty check\n";
|
||||
|
||||
std::cout << "=== seq_monadic: length bounds ===\n";
|
||||
auto check_bound = [&](char const* name, expr* regex, unsigned bound, bool is_lo,
|
||||
lbool expected) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue