From 6592354bbaf5da77ba1ecfa0d8cbf93c9b68ac92 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Aug 2026 14:59:53 -0700 Subject: [PATCH] remove unused code, fix unit tests --- src/ast/rewriter/seq_rewriter.cpp | 52 ------------------------------- src/ast/rewriter/seq_rewriter.h | 2 ++ src/test/seq_monadic.cpp | 14 ++++----- src/test/seq_monadic_bench.cpp | 18 +++++------ 4 files changed, 18 insertions(+), 68 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6b71e47db5..28dfebd5fd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -33,58 +33,6 @@ Authors: #include "params/seq_rewriter_params.hpp" -expr_ref sym_expr::accept(expr* e) { - ast_manager& m = m_t.get_manager(); - expr_ref result(m); - var_subst subst(m); - seq_util u(m); - unsigned r1, r2, r3; - switch (m_ty) { - case t_pred: - result = subst(m_t, 1, &e); - break; - case t_not: - result = m_expr->accept(e); - result = m.mk_not(result); - break; - case t_char: - SASSERT(e->get_sort() == m_t->get_sort()); - SASSERT(e->get_sort() == m_sort); - result = m.mk_eq(e, m_t); - break; - case t_range: - if (u.is_const_char(m_t, r1) && u.is_const_char(e, r2) && u.is_const_char(m_s, r3)) { - result = m.mk_bool_val((r1 <= r2) && (r2 <= r3)); - } - else { - auto a = u.mk_le(m_t, e); - result = m.mk_and(a, u.mk_le(e, m_s)); - } - break; - } - - return result; -} - -std::ostream& sym_expr::display(std::ostream& out) const { - switch (m_ty) { - case t_char: return out << m_t; - case t_range: return out << m_t << ":" << m_s; - case t_pred: return out << m_t; - case t_not: return m_expr->display(out << "not "); - } - return out << "expression type not recognized"; -} - -struct display_expr1 { - ast_manager& m; - display_expr1(ast_manager& m): m(m) {} - std::ostream& display(std::ostream& out, sym_expr* e) const { - return e->display(out); - } -}; - - void seq_rewriter::updt_params(params_ref const & p) { seq_rewriter_params sp(p); m_coalesce_chars = sp.coalesce_chars(); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 1d4cb51eec..dbe3e694f2 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -37,6 +37,7 @@ inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& e return out; } +#if 0 class sym_expr { enum ty { t_char, @@ -80,6 +81,7 @@ public: void inc_ref(sym_expr* s) { if (s) s->inc_ref(); } void dec_ref(sym_expr* s) { if (s) s->dec_ref(); } }; +#endif /** \brief Cheap rewrite rules for seq constraints diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 44452aea46..d7a1942a36 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -44,7 +44,7 @@ class seq_monadic_test { seq_util u; sort_ref m_str; // String sort sort_ref m_re; // RegEx sort over m_str - seq_monadic::transition_mode m_mode; + seq::transition_mode m_mode; u_dependency_manager m_dm; // owns the leaf dependencies used in unsat-core tests unsigned m_fail = 0; @@ -79,8 +79,8 @@ class seq_monadic_test { static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } char const* mode_name() const { switch (m_mode) { - case seq_monadic::transition_mode::brzozowski: return "brz"; - case seq_monadic::transition_mode::light_antimirov: return "light-ant"; + case seq::transition_mode::brzozowski_tm: return "brz"; + case seq::transition_mode::light_antimirov_tm: return "light-ant"; } UNREACHABLE(); return ""; @@ -288,7 +288,7 @@ class seq_monadic_test { } public: - seq_monadic_test(seq_monadic::transition_mode mode) : + seq_monadic_test(seq::transition_mode mode) : m_reg(m), m_rw(m), m_mon(m_rw, m_trail, mode), u(m), m_str(m), m_re(m), m_mode(mode) { m_str = u.str.mk_string_sort(); m_re = re().mk_re(m_str); @@ -297,7 +297,7 @@ public: void run() { std::cout << "=== seq_monadic mode: " << mode_name() << " ===\n"; - if (m_mode == seq_monadic::transition_mode::light_antimirov) + if (m_mode == seq::transition_mode::light_antimirov_tm) check_ant_cofactors(); expr_ref x = var("x"); expr_ref a = word("a"); @@ -710,8 +710,8 @@ public: } void tst_seq_monadic() { - seq_monadic_test brz(seq_monadic::transition_mode::brzozowski); + seq_monadic_test brz(seq::transition_mode::brzozowski_tm); brz.run(); - seq_monadic_test light_ant(seq_monadic::transition_mode::light_antimirov); + seq_monadic_test light_ant(seq::transition_mode::light_antimirov_tm); light_ant.run(); } diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 09fca17cec..7f15244586 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -47,20 +47,20 @@ char const* verdict_str(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } -char const* mode_str(seq_monadic::transition_mode mode) { +char const* mode_str(seq::transition_mode mode) { switch (mode) { - case seq_monadic::transition_mode::brzozowski: return "brz"; - case seq_monadic::transition_mode::light_antimirov: return "light-ant"; + case seq::transition_mode::brzozowski_tm: return "brz"; + case seq::transition_mode::light_antimirov_tm: return "light-ant"; } UNREACHABLE(); return ""; } -seq_monadic::transition_mode get_mode() { +seq::transition_mode get_mode() { char const* mode = getenv("Z3_SEQ_MONADIC_MODE"); if (mode && std::string(mode) == "brz") - return seq_monadic::transition_mode::brzozowski; - return seq_monadic::transition_mode::light_antimirov; + return seq::transition_mode::brzozowski_tm; + return seq::transition_mode::light_antimirov_tm; } bool is_seq_var(expr* t) { @@ -80,7 +80,7 @@ std::string read_status(std::string const& path) { lbool run_file( std::string const& path, - seq_monadic::transition_mode mode, + seq::transition_mode mode, double& solve_ms, bool& parsed, bool& complete, @@ -263,7 +263,7 @@ void display_row( std::string const& tier, std::string const& status, bool complete, - seq_monadic::transition_mode mode, + seq::transition_mode mode, lbool verdict, double solve_ms, unsigned dropped) { @@ -279,7 +279,7 @@ void display_row( void tst_seq_monadic_bench() { namespace fs = std::filesystem; std::error_code ec; - seq_monadic::transition_mode mode = get_mode(); + seq::transition_mode mode = get_mode(); if (char const* file = getenv("Z3_SEQ_BENCH_FILE")) { double ms = 0;