diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index bd8caca1ac..44452aea46 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -511,6 +511,99 @@ public: std::cout << (zero_lo_ok ? " OK " : " FAIL ") << "|x| >= 0 is a no-op\n"; + // Length bounds on COMPOUND terms and on several variables at once: the shape the + // SMT-LIB regex benchmarks use (e.g. `x.y.x in R /\ |x|>0 /\ |y|>0`). A bound on + // a concatenation constrains the term as a whole; bounds on the individual + // variables have to be intersected with the split induced by the membership. + std::cout << "=== seq_monadic: length bounds on compound terms ===\n"; + auto check_bounded = [&](char const* name, + auto&& assert_all, lbool expected) { + m_trail.push_scope(); + assert_all(); + lbool got = m_mon.check(); + m_trail.pop_scope(1); + bool ok = got == expected; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + }; + expr_ref t_xyx(xyx(x, y), m); + expr_ref t_xax(xwx(x, "a"), m); + // |x.y.x| is odd-free: x.y.x in (ab)* with |x.y.x| = 2 forces x.y.x = "ab" + check_bounded("x.y.x in (ab)*, |x.y.x| = 2", [&] { + m_mon.add(t_xyx, abS, nullptr); + m_mon.add_len(t_xyx, 2, nullptr); + }, l_true); + check_bounded("x.y.x in (ab)*, |x.y.x| = 3", [&] { + m_mon.add(t_xyx, abS, nullptr); + m_mon.add_len(t_xyx, 3, nullptr); // (ab)* has only even lengths + }, l_false); + // bounds on the individual variables of a compound membership + check_bounded("x.a.x in Sigma*, |x| >= 2, |x.a.x| <= 5", [&] { + m_mon.add(t_xax, sig2, nullptr); + m_mon.add_lo(x, 2, nullptr); + m_mon.add_hi(t_xax, 5, nullptr); + }, l_true); + check_bounded("x.a.x in Sigma*, |x| >= 3, |x.a.x| <= 5", [&] { + m_mon.add(t_xax, sig2, nullptr); + m_mon.add_lo(x, 3, nullptr); // |x.a.x| = 2|x|+1 >= 7 > 5 + m_mon.add_hi(t_xax, 5, nullptr); + }, l_false); + // two variables bounded independently under one membership + check_bounded("x.y.x in (a|b)*, |x| = 1, |y| = 2", [&] { + m_mon.add(t_xyx, abStar, nullptr); + m_mon.add_len(x, 1, nullptr); + m_mon.add_len(y, 2, nullptr); + }, l_true); + check_bounded("x.y.x in a*, |x| >= 1, y in b*", [&] { + m_mon.add(t_xyx, star(a), nullptr); + m_mon.add(y, star(b), nullptr); // y must be both a* and b* -> y = eps + m_mon.add_lo(x, 1, nullptr); + m_mon.add_lo(y, 1, nullptr); // ... but |y| >= 1 + }, l_false); + // the bound is the ONLY reason for unsat: without it the membership is satisfiable + check_bounded("x in a(aa)* (no bound)", [&] { + m_mon.add(x, a_aaS, nullptr); + }, l_true); + check_bounded("x in a(aa)*, |x| = 2", [&] { + m_mon.add(x, a_aaS, nullptr); // only odd lengths + m_mon.add_len(x, 2, nullptr); + }, l_false); + // upper and lower bounds that cross + check_bounded("x in Sigma*, |x| >= 3, |x| <= 2", [&] { + m_mon.add(x, sig2, nullptr); + m_mon.add_lo(x, 3, nullptr); + m_mon.add_hi(x, 2, nullptr); + }, l_false); + + // The IPv6 abbreviation benchmark shape: an intersection of a positive "contains" + // and a complement, restricted to a character range, over x.y.x with both + // variables non-empty. Without the length bounds the answer is trivially sat via + // x = y = epsilon, so the bounds are what make the test meaningful. + { + expr_ref cc(word("::"), m); + expr_ref sig_plus(cat(dot(), dotstar()), m); + expr_ref has_cc(cat(dotstar(), cat(cc, dotstar())), m); + expr_ref two_cc(cat(dotstar(), cat(cc, cat(sig_plus, cat(cc, dotstar())))), m); + expr_ref hexcol(star(alt(rng('0', '9'), + alt(rng('A', 'F'), + alt(rng('a', 'f'), word(":"))))), m); + expr_ref R6(inter(has_cc, inter(comp(two_cc), hexcol)), m); + check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1", [&] { + m_mon.add(t_xyx, R6, nullptr); + m_mon.add_lo(x, 1, nullptr); + m_mon.add_lo(y, 1, nullptr); + }, l_true); + // "::" cannot be split across a repeated x without creating a second group, + // and hexcol forbids everything outside [0-9A-Fa-f:], so a long x is hopeless + check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1, |x.y.x|<=2", [&] { + m_mon.add(t_xyx, R6, nullptr); + m_mon.add_lo(x, 1, nullptr); + m_mon.add_lo(y, 1, nullptr); + m_mon.add_hi(t_xyx, 2, nullptr); // needs >= 3 chars to hold "::" plus x twice + }, l_false); + } + std::cout << "=== seq_monadic: SMT regex end-game ===\n"; { expr_ref_vector assertions(m); diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 804ce15d1b..ed56846553 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -8,14 +8,21 @@ Module Name: 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). + Z3_SEQ_BENCH_DIR, extracts regex memberships and length bounds, and reports + CSV timing. Z3_SEQ_MONADIC_MODE selects "brz" or "light-ant" (default). + + Assertions the harness cannot hand to seq_monadic are DROPPED. The CSV + reports how many were dropped ("dropped") and whether the benchmark was + modelled in full ("complete"). On an incomplete benchmark only an `unsat` + verdict carries over to the original problem: dropping conjuncts weakens it, + so `sat` there says nothing about the benchmark's real status. --*/ #define _CRT_SECURE_NO_WARNINGS #include "ast/ast.h" +#include "ast/arith_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_monadic.h" @@ -75,10 +82,12 @@ lbool run_file( seq_monadic::transition_mode mode, double& solve_ms, bool& parsed, - bool& complete) { + bool& complete, + unsigned& dropped) { solve_ms = 0; parsed = false; complete = false; + dropped = 0; cmd_context ctx(false); ctx.set_ignore_check(true); { @@ -89,6 +98,7 @@ lbool run_file( parsed = true; ast_manager& m = ctx.m(); seq_util u(m); + arith_util a(m); seq_rewriter rw(m); trail_stack undo_trail; seq_monadic mon(rw, undo_trail, mode); @@ -98,19 +108,94 @@ lbool run_file( ptr_vector terms; expr_ref_vector pin(m); - std::function collect = [&](expr* a) { + // Length bounds accumulated per term; lo/hi are the tightest bounds seen. + struct len_bounds { unsigned lo = 0; unsigned hi = UINT_MAX; }; + obj_map bounds; + ptr_vector bounded; + + // seq_monadic models |t| <= hi as a bounded loop, so a huge hi is not usable. + const int64_t MAX_LEN_BOUND = 1 << 16; + const int64_t NO_UPPER = INT64_MAX; + + auto tighten = [&](expr* t, int64_t lo, int64_t hi) { + if (!is_seq_var(t) && !u.str.is_concat(t)) + return false; + if (lo > MAX_LEN_BOUND) + return false; // cannot build Sigma^lo + if (hi != NO_UPPER && hi > MAX_LEN_BOUND) + return false; // dropping it would be unsound + len_bounds b; + if (!bounds.find(t, b)) + bounded.push_back(t); + if (lo > 0) + b.lo = std::max(b.lo, static_cast(lo)); + if (hi < 0) // |t| < 0: record a contradiction + b.lo = std::max(b.lo, 1u), b.hi = 0; + else if (hi != NO_UPPER) + b.hi = std::min(b.hi, static_cast(hi)); + bounds.insert(t, b); + return true; + }; + + // Recognize a linear length constraint (str.len t) k (either argument + // order, optionally negated) and record it as a bound on t. + std::function collect_len = [&](expr* e, bool sign) { + expr* arg = nullptr; + if (m.is_not(e, arg)) + return collect_len(arg, !sign); + // normalize to lhs rhs with op in {<=, <, =} + expr* lhs = nullptr, * rhs = nullptr; + bool le = false, lt = false, eq = false; + if (a.is_le(e, lhs, rhs)) le = true; + else if (a.is_lt(e, lhs, rhs)) lt = true; + else if (a.is_ge(e, rhs, lhs)) le = true; // k >= |t| == |t| <= k + else if (a.is_gt(e, rhs, lhs)) lt = true; + else if (m.is_eq(e, lhs, rhs) && a.is_int(lhs)) eq = true; + else return false; + + expr* t = nullptr; + rational k; + bool len_left; // true: |t| k, else k |t| + if (u.str.is_length(lhs, t) && a.is_numeral(rhs, k)) + len_left = true; + else if (u.str.is_length(rhs, t) && a.is_numeral(lhs, k)) + len_left = false; + else + return false; + if (!k.is_int() || !k.is_int64()) + return false; + int64_t n = k.get_int64(); + if (eq) + return !sign && tighten(t, n, n); // |t| != k is not a bound + int64_t s = lt ? 1 : 0; // strict? + if (len_left) + return sign ? tighten(t, n + 1 - s, INT64_MAX) // !(|t| <= k) == |t| >= k+1 + : tighten(t, 0, n - s); // |t| <= k + return sign ? tighten(t, 0, n - 1 + s) // !(k <= |t|) == |t| <= k-1 + : tighten(t, n + s, INT64_MAX); // k <= |t| + }; + + // Collect what seq_monadic can model. Conjunctions are traversed so that an + // unsupported conjunct does not discard its siblings; every conjunct that cannot be + // modelled is counted in `dropped`. Dropping conjuncts only weakens the problem, so + // an unsat verdict still transfers to the benchmark while a sat verdict does not. + std::function collect = [&](expr* e) { expr* s = nullptr, * r = nullptr; - if (m.is_and(a)) { - for (expr* arg : *to_app(a)) - if (!collect(arg)) - return false; - return true; + if (m.is_and(e)) { + for (expr* arg : *to_app(e)) + collect(arg); + return; + } + if (!u.str.is_in_re(e, s, r)) { + if (!collect_len(e, false)) + complete = false, ++dropped; + return; } - 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; + if (!is_var && !u.str.is_concat(s)) { + complete = false, ++dropped; + return; + } obj_map& map = is_var ? var_re : term_re; expr* previous = nullptr; if (map.find(s, previous)) { @@ -123,11 +208,10 @@ lbool run_file( if (!is_var) terms.push_back(s); } - return true; }; complete = true; for (expr* assertion : ctx.assertions()) - complete = collect(assertion) && complete; + collect(assertion); unsigned n_added = 0; for (expr* term : terms) { @@ -140,6 +224,20 @@ lbool run_file( mon.add(k, v, nullptr); ++n_added; } + for (expr* t : bounded) { + len_bounds b; + bounds.find(t, b); + if (b.lo == b.hi) + mon.add_len(t, b.lo, nullptr); + else { + if (b.lo > 0) + mon.add_lo(t, b.lo, nullptr); + if (b.hi != UINT_MAX) + mon.add_hi(t, b.hi, nullptr); + } + if (b.lo > 0 || b.hi != UINT_MAX) + ++n_added; + } auto start = std::chrono::high_resolution_clock::now(); mon.set_gen_model(false); // benchmark only needs the verdict @@ -158,10 +256,12 @@ void display_row( bool complete, seq_monadic::transition_mode mode, lbool verdict, - double solve_ms) { + double solve_ms, + unsigned dropped) { std::cout << file << "," << tier << "," << status << "," << (complete ? "yes" : "no") << "," << mode_str(mode) << "," << verdict_str(verdict) << "," << solve_ms + << "," << dropped << "\n"; } @@ -175,8 +275,12 @@ void tst_seq_monadic_bench() { 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); + unsigned dropped = 0; + lbool verdict = run_file(file, mode, ms, parsed, complete, dropped); + display_row(file, "", read_status(file), complete, mode, verdict, ms, dropped); + if (!complete) + std::cerr << "INCOMPLETE: " << dropped << " assertion(s) not modelled; " + << "only an unsat verdict transfers to the benchmark\n"; return; } @@ -197,8 +301,9 @@ void tst_seq_monadic_bench() { files.push_back(entry.path().string()); std::sort(files.begin(), files.end()); - std::cout << "file,tier,status,complete,mode,verdict,solve_ms\n"; + std::cout << "file,tier,status,complete,mode,verdict,solve_ms,dropped\n"; unsigned agree = 0, mismatch = 0, undef = 0, unparsed = 0, incomplete = 0; + unsigned incomplete_sat = 0; double total_ms = 0; for (unsigned i = 0; i < files.size(); ++i) { std::string const& file = files[i]; @@ -209,11 +314,16 @@ void tst_seq_monadic_bench() { << 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); + unsigned dropped = 0; + lbool verdict = run_file(file, mode, ms, parsed, complete, dropped); + display_row(relative, tier, status, complete, mode, verdict, ms, dropped); total_ms += ms; if (!parsed) ++unparsed; - if (!complete) ++incomplete; + if (!complete) { + ++incomplete; + // constraints were dropped, so a sat verdict does not transfer + if (verdict == l_true) ++incomplete_sat; + } if (verdict == l_undef) ++undef; else if (complete && (status == "sat" || status == "unsat")) { if (status == verdict_str(verdict)) ++agree; @@ -227,5 +337,6 @@ void tst_seq_monadic_bench() { << " undef=" << undef << " unparsed=" << unparsed << " incomplete=" << incomplete + << " incomplete_sat=" << incomplete_sat << " total_solve_ms=" << total_ms << "\n"; }