From ddce973e16dfce7043180ba755642de05b1c0c65 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 31 Jul 2026 14:03:21 -0700 Subject: [PATCH] Add seq monadic benchmark harness (#10330) ## Summary Register the opt-in seq_monadic benchmark harness in test-z3. The harness reads either Z3_SEQ_BENCH_FILE or all SMT2 files under Z3_SEQ_BENCH_DIR, supports Brz and light-Ant modes through Z3_SEQ_MONADIC_MODE, and reports per-file CSV timing and verdict information. --- src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/seq_monadic_bench.cpp | 227 +++++++++++++++++++++++++++++++++ 3 files changed, 229 insertions(+) create mode 100644 src/test/seq_monadic_bench.cpp diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 4f5f667118..6bd0d0bdba 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -133,6 +133,7 @@ add_executable(test-z3 scoped_vector.cpp seq_rewriter.cpp seq_monadic.cpp + seq_monadic_bench.cpp simple_parser.cpp scanner_io.cpp simplex.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 81b926681a..b8d18d3b40 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -117,6 +117,7 @@ X(regex_range_collapse) \ X(seq_rewriter) \ X(seq_monadic) \ + X(seq_monadic_bench) \ X(check_assumptions) \ X(smt_context) \ X(theory_dl) \ diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp new file mode 100644 index 0000000000..36609dad31 --- /dev/null +++ b/src/test/seq_monadic_bench.cpp @@ -0,0 +1,227 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic_bench.cpp + +Abstract: + + Opt-in benchmark harness for seq_monadic. Reads every *.smt2 under + Z3_SEQ_BENCH_DIR, extracts regex memberships, and reports CSV timing. + Z3_SEQ_MONADIC_MODE selects "brz" or "light-ant" (default). + +--*/ + +#define _CRT_SECURE_NO_WARNINGS + +#include "ast/ast.h" +#include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_monadic.h" +#include "cmd_context/cmd_context.h" +#include "parsers/smt2/smt2parser.h" +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { + +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) { + switch (mode) { + case seq_monadic::transition_mode::brzozowski: return "brz"; + case seq_monadic::transition_mode::light_antimirov: return "light-ant"; + } + UNREACHABLE(); + return ""; +} + +seq_monadic::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; +} + +bool is_seq_var(expr* t) { + return is_app(t) && to_app(t)->get_num_args() == 0 && + to_app(t)->get_family_id() == null_family_id; +} + +std::string read_status(std::string const& path) { + std::ifstream in(path); + std::stringstream ss; + ss << in.rdbuf(); + std::smatch match; + std::regex status_re("set-info\\s*:status\\s+(sat|unsat|unknown)"); + std::string text = ss.str(); + return std::regex_search(text, match, status_re) ? match[1].str() : "?"; +} + +lbool run_file( + std::string const& path, + seq_monadic::transition_mode mode, + double& solve_ms, + bool& parsed, + bool& complete) { + solve_ms = 0; + parsed = false; + complete = false; + cmd_context ctx(false); + ctx.set_ignore_check(true); + { + std::ifstream is(path); + if (!is.good() || !parse_smt2_commands(ctx, is)) + return l_undef; + } + parsed = true; + ast_manager& m = ctx.m(); + seq_util u(m); + seq_rewriter rw(m); + seq_monadic mon(rw, mode); + + obj_map var_re; + obj_map term_re; + ptr_vector terms; + expr_ref_vector pin(m); + + std::function collect = [&](expr* a) { + expr* s = nullptr, * r = nullptr; + if (m.is_and(a)) { + for (expr* arg : *to_app(a)) + if (!collect(arg)) + return false; + return true; + } + if (!u.str.is_in_re(a, s, r)) + return false; + bool is_var = is_seq_var(s); + if (!is_var && !u.str.is_concat(s)) + return false; + obj_map& map = is_var ? var_re : term_re; + expr* previous = nullptr; + if (map.find(s, previous)) { + expr_ref intersection = rw.mk_regex_inter_normalize(previous, r); + pin.push_back(intersection); + map.insert(s, intersection); + } + else { + map.insert(s, r); + if (!is_var) + terms.push_back(s); + } + return true; + }; + complete = true; + for (expr* assertion : ctx.assertions()) + complete = collect(assertion) && complete; + + vector> memberships; + for (expr* term : terms) { + expr* r = nullptr; + term_re.find(term, r); + memberships.push_back(std::make_pair(term, r)); + } + for (auto const& entry : var_re) + memberships.push_back(std::make_pair(entry.m_key, entry.m_value)); + + obj_map no_extra; + auto start = std::chrono::high_resolution_clock::now(); + lbool verdict = memberships.empty() + ? l_undef + : mon.solve_and(memberships, no_extra, nullptr); + solve_ms = std::chrono::duration( + std::chrono::high_resolution_clock::now() - start).count(); + return verdict; +} + +void display_row( + std::string const& file, + std::string const& tier, + std::string const& status, + bool complete, + seq_monadic::transition_mode mode, + lbool verdict, + double solve_ms) { + std::cout << file << "," << tier << "," << status << "," + << (complete ? "yes" : "no") << "," << mode_str(mode) + << "," << verdict_str(verdict) << "," << solve_ms + << "\n"; +} + +} + +void tst_seq_monadic_bench() { + namespace fs = std::filesystem; + std::error_code ec; + seq_monadic::transition_mode mode = get_mode(); + + if (char const* file = getenv("Z3_SEQ_BENCH_FILE")) { + double ms = 0; + bool parsed = false, complete = false; + lbool verdict = run_file(file, mode, ms, parsed, complete); + display_row(file, "", read_status(file), complete, mode, verdict, ms); + return; + } + + char const* dir = getenv("Z3_SEQ_BENCH_DIR"); + if (!dir) { + std::cout << "seq_monadic_bench: set Z3_SEQ_BENCH_DIR; " + "optionally set Z3_SEQ_MONADIC_MODE=brz|light-ant\n"; + return; + } + if (!fs::exists(dir, ec)) { + std::cout << "seq_monadic_bench: dir not found: " << dir << "\n"; + return; + } + + std::vector files; + for (auto& entry : fs::recursive_directory_iterator(dir, ec)) + if (entry.is_regular_file() && entry.path().extension() == ".smt2") + files.push_back(entry.path().string()); + std::sort(files.begin(), files.end()); + + std::cout << "file,tier,status,complete,mode,verdict,solve_ms\n"; + unsigned agree = 0, mismatch = 0, undef = 0, unparsed = 0, incomplete = 0; + double total_ms = 0; + for (unsigned i = 0; i < files.size(); ++i) { + std::string const& file = files[i]; + std::string status = read_status(file); + std::string relative = fs::relative(file, dir, ec).generic_string(); + std::string tier = relative.substr(0, relative.find('/')); + std::cerr << "[" << (i + 1) << "/" << files.size() << "] " + << relative << std::endl; + double ms = 0; + bool parsed = false, complete = false; + lbool verdict = run_file(file, mode, ms, parsed, complete); + display_row(relative, tier, status, complete, mode, verdict, ms); + total_ms += ms; + if (!parsed) ++unparsed; + if (!complete) ++incomplete; + if (verdict == l_undef) ++undef; + else if (complete && (status == "sat" || status == "unsat")) { + if (status == verdict_str(verdict)) ++agree; + else ++mismatch; + } + } + std::cout << "# SUMMARY mode=" << mode_str(mode) + << " files=" << files.size() + << " agree=" << agree + << " mismatch=" << mismatch + << " undef=" << undef + << " unparsed=" << unparsed + << " incomplete=" << incomplete + << " total_solve_ms=" << total_ms << "\n"; +}