diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index f9ba950b07..3d9b11c014 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -22,8 +22,6 @@ TODOs: - track unsat cores and expose them as explain functionality - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) - create a validation harness: expose certificates for correctness that can be checked. -- handle transitions into unions and concatenations over unions -- establish a perf harness - extend with lower and upper bound constraints - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership @@ -229,6 +227,13 @@ expr_ref seq_monadic::der_elem(expr* r, expr* elem) { return d2; } +void seq_monadic::derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + if (m_mode == transition_mode::light_antimirov) + m_rw.light_ant_derivative_cofactors(r, result); + else + m_rw.brz_derivative_cofactors(r, result); +} + void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { ok = true; obj_map id; @@ -251,7 +256,7 @@ void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { for (unsigned i = 0; i < states.size(); ++i) { if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } expr_ref_pair_vector cof(m); - m_rw.brz_derivative_cofactors(states.get(i), cof); + derivative_cofactors(states.get(i), cof); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; unsigned k = intern(t); // MUST precede succ[i] indexing: intern may @@ -357,7 +362,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w std::vector>> branches(n); for (unsigned i = 0; i < n; ++i) { expr_ref_pair_vector cof(m); - m_rw.brz_derivative_cofactors(st[i], cof); + derivative_cofactors(st[i], cof); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; m_pin.push_back(t); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index d979134e47..63de75cc5d 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -15,9 +15,9 @@ Abstract: derivatives). Self-contained decision procedure: NO Nielsen splitting (seq_split), NO minterms, - and NO materialization of reach(q) as a regex. It relies only on the symbolic - Brzozowski derivative (brz_derivative_cofactors as a transition regex) and on - automaton product-reachability for emptiness. + and NO materialization of reach(q) as a regex. It uses symbolic derivative + cofactors as Brzozowski states or Brzozowski states post-processed into + light-weight Antimirov states, and automaton product-reachability for emptiness. Method. For a term x.u in R and the whole-language split, x drives the derivative automaton of R from R to some live state q, and the rest u must be accepted from q: @@ -59,10 +59,18 @@ Author: #include class seq_monadic { +public: + enum class transition_mode { + brzozowski, + light_antimirov + }; + +private: ast_manager& m; seq_rewriter& m_rw; th_rewriter m_thrw; // normalizes constant-element derivatives (folds // ground guards so dead states become re.empty) + transition_mode m_mode; sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis sort* m_elem_sort = nullptr; // element sort of that sequence sort expr_ref_vector m_pin; // pins derivative states / witnesses referenced later @@ -86,6 +94,9 @@ class seq_monadic { // Brzozowski derivative of regex `r` by the concrete element `elem`. expr_ref der_elem(expr* r, expr* elem); + // Symbolic transition cofactors in the selected mode. + void derivative_cofactors(expr* r, expr_ref_pair_vector& result); + // Live reachable derivative states of R (BFS over cofactor targets + liveness // least-fixpoint). These are the split states q. Sets `ok` false on a cap overrun. void live_states(expr* R, ptr_vector& out, bool& ok); @@ -119,7 +130,10 @@ class seq_monadic { obj_map* model); public: - seq_monadic(seq_rewriter& rw) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_pin(rw.m()) {} + seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : + m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_mode(mode), m_pin(rw.m()) {} + + transition_mode mode() const { return m_mode; } // Decide (str.in_re term R) for a term that is a concatenation of string variables // (possibly repeated / several distinct) and constant characters. diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 8aed5bf43a..d5f42cbbe9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2931,6 +2931,66 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) { return result; } +void seq_rewriter::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + expr_ref_pair_vector brz(m()); + m_derive.derivative_cofactors(r, brz); + + obj_map target_index; + expr_ref_vector guards(m()); + expr_ref_vector targets(m()); + + auto add = [&](expr* guard, expr* target) { + unsigned index = 0; + if (target_index.find(target, index)) { + expr_ref merged(m()); + m_br.mk_or(guards.get(index), guard, merged); + guards.set(index, merged); + } + else { + target_index.insert(target, targets.size()); + targets.push_back(target); + guards.push_back(guard); + } + }; + + for (auto const& [guard, target] : brz) { + ptr_vector pending; + pending.push_back(target); + while (!pending.empty()) { + expr* t = pending.back(); + pending.pop_back(); + expr* left = nullptr, * right = nullptr; + if (re().is_union(t, left, right)) { + pending.push_back(right); + pending.push_back(left); + } + else if (re().is_concat(t, left, right) && re().is_union(left)) { + ptr_vector heads; + heads.push_back(left); + while (!heads.empty()) { + expr* head = heads.back(); + heads.pop_back(); + expr* a = nullptr, * b = nullptr; + if (re().is_union(head, a, b)) { + heads.push_back(b); + heads.push_back(a); + } + else { + expr_ref split = mk_regex_concat(head, right); + add(guard, split); + } + } + } + else { + add(guard, t); + } + } + } + + result.reset(); + for (unsigned i = 0; i < targets.size(); ++i) + result.push_back(guards.get(i), targets.get(i)); +} expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { expr_ref _r1(r1, m()), _r2(r2, m()); diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index ed84b2dbaf..c9c5ea989f 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -475,6 +475,13 @@ public: m_derive.derivative_cofactors(r, result); } + /* + Compute Brzozowski cofactors, then expose nondeterminism in targets of the + form (s1 | ... | sn) or (s1 | ... | sn) . tail. Cofactors with the same + resulting target are merged by disjoining their guards. + */ + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result); + // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. void elim_condition(expr* elem, expr_ref& cond); diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 5377aac1a3..b1587d77ce 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -40,6 +40,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; unsigned m_fail = 0; seq_util::rex& re() { return u.re; } @@ -51,6 +52,7 @@ class seq_monadic_test { expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); } expr_ref inter(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); } expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); } + expr_ref dot() { return expr_ref(re().mk_full_char(m_re), m); } expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } expr_ref rng(char lo, char hi) { char sl[2] = { lo, 0 }, sh[2] = { hi, 0 }; @@ -70,6 +72,53 @@ class seq_monadic_test { expr_ref xyx(expr* x, expr* y) { return sconcat(x, sconcat(y, x)); } 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"; + } + UNREACHABLE(); + return ""; + } + + bool eval_guard(expr* guard, unsigned ch) { + sort* elem_sort = nullptr; + VERIFY(u.is_seq(m_str, elem_sort)); + expr_ref v0(m.mk_var(0, elem_sort), m); + expr_safe_replace rep(m); + rep.insert(v0, u.str.mk_char(ch)); + expr_ref instantiated(m), simplified(m); + rep(guard, instantiated); + th_rewriter rw(m); + rw(instantiated, simplified); + return m.is_true(simplified); + } + + void check_ant_cofactors() { + expr_ref a = word("a"); + expr_ref any = dotstar(); + expr_ref dot3 = loop(dot(), 3, 3); + expr_ref R = cat(any, cat(a, dot3)); + expr_ref_pair_vector cof(m); + m_rw.light_ant_derivative_cofactors(R, cof); + + bool found_R = false, found_dot3 = false, ok = cof.size() == 2; + for (auto const& [guard, target] : cof) { + if (target == R) { + found_R = eval_guard(guard, 'a') && eval_guard(guard, 'b'); + } + else if (target == dot3) { + found_dot3 = eval_guard(guard, 'a') && !eval_guard(guard, 'b'); + } + else { + ok = false; + } + } + ok = ok && found_R && found_dot3; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") + << mode_name() << " cofactor construction\n"; + } void check(char const* name, expr* term, expr* R, lbool expected) { lbool got = m_mon.solve(term, R); @@ -145,12 +194,16 @@ class seq_monadic_test { } public: - seq_monadic_test() : m_reg(m), m_rw(m), m_mon(m_rw), u(m), m_str(m), m_re(m) { + seq_monadic_test(seq_monadic::transition_mode mode) : + m_reg(m), m_rw(m), m_mon(m_rw, 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); } void run() { + std::cout << "=== seq_monadic mode: " << mode_name() << " ===\n"; + if (m_mode == seq_monadic::transition_mode::light_antimirov) + check_ant_cofactors(); expr_ref x = var("x"); expr_ref a = word("a"); expr_ref b = word("b"); @@ -309,6 +362,8 @@ public: } void tst_seq_monadic() { - seq_monadic_test t; - t.run(); + seq_monadic_test brz(seq_monadic::transition_mode::brzozowski); + brz.run(); + seq_monadic_test light_ant(seq_monadic::transition_mode::light_antimirov); + light_ant.run(); }