diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 9892ffd35c..39f2ea2a44 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -288,6 +288,22 @@ namespace seq { return mk_deriv_concat(d1, tail); } + // Legacy form where the loop bounds are arguments rather than + // decl parameters: (re.loop r lo hi) and (re.loop r lo). The parser + // accepts these and seq_rewriter normalizes them, but unrewritten + // terms reach here directly. Rewrite to the parameterized form. + if (re().is_loop(r)) { + expr* lo_e = nullptr, * hi_e = nullptr; + rational nlo, nhi; + if (re().is_loop(r, r1, lo_e, hi_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned() && + m_autil.is_numeral(hi_e, nhi) && nhi.is_unsigned()) + return derive_rec(re().mk_loop_proper(r1, nlo.get_unsigned(), nhi.get_unsigned())); + if (re().is_loop(r, r1, lo_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned()) + return derive_rec(re().mk_loop(r1, nlo.get_unsigned())); + } + // δ(r1 \ r2) = δ(r1) ∩ ~δ(r2) if (re().is_diff(r, r1, r2)) { expr_ref d1 = derive_rec(r1); @@ -1567,5 +1583,66 @@ namespace seq { get_cofactors(m_ele, d, result); } + void derive::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + expr_ref_pair_vector brz(m); + 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 = m_re.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)); + } + } diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index e0559bdf1d..08e8631315 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -261,6 +261,25 @@ namespace seq { */ void derivative_cofactors(expr* r, expr_ref_pair_vector& result); + /** + * Compute the Brzozowski cofactors of r (derivative_cofactors above), + * then expose the nondeterminism that a union leaf hides: a target of + * the form (s1 | ... | sn), or (s1 | ... | sn) . tail, is split into + * one cofactor per alternative si (resp. si . tail). Splitting is + * applied recursively, so nested unions are flattened as well. + * + * Splitting can make two originally distinct cofactors reach the same + * target; such cofactors are merged back into a single pair whose + * guard is the disjunction of the original guards. The result is + * therefore still a list of distinct targets, but each one is a + * single Antimirov-style alternative rather than a union state. + * + * The guards are not required to be mutually exclusive after merging, + * and the transition relation is genuinely nondeterministic: a + * character may be accepted by several of the returned guards. + */ + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result); + }; } diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 3420cb46fe..424961dcbe 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -40,6 +40,11 @@ TODOs: explored and we can check the variable intersection membership constraints if the new expansion is feasible. Constant characters are consumed at the same time to also prune the choice. +- separate out "live-state" and enumerator over reachable live states: + - make it share live states between callers. + - make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states. + - make use of DFS exploration of derivatives to extract live states without visiting all states up front. + - use it in seq_regex legacy mode that also has this notion. diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d5f42cbbe9..6b71e47db5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2931,67 +2931,6 @@ 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()); expr *a1, *b1, *a2, *b2; @@ -4286,6 +4225,16 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { result = re().mk_star(re().mk_union(b1, c1)); return BR_REWRITE2; } + // (Σ*·S)* = () | Σ*·S. + // Σ*·S is idempotent under concatenation: Σ*·S·Σ*·S = (Σ*·S·Σ*)·S ⊆ Σ*·S, + // since any prefix is absorbed by Σ*. Hence L·L ⊆ L and L* = () | L. + // Keeping the flat form avoids a large blowup in the derivative automaton. + if (re().is_concat(a, b, c) && re().is_full_seq(b)) { + sort* seq_sort = nullptr; + VERIFY(m_util.is_re(a, seq_sort)); + result = re().mk_union(re().mk_epsilon(seq_sort), a); + return BR_REWRITE1; + } if (m().is_ite(a, c, b1, c1)) { if ((re().is_full_char(b1) || re().is_full_seq(b1)) && (re().is_full_char(c1) || re().is_full_seq(c1))) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c9c5ea989f..5bad5ae3dc 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -480,7 +480,9 @@ public: 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); + void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) { + m_derive.light_ant_derivative_cofactors(r, result); + } // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index d0f45485dd..36310fd3c3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1733,11 +1733,30 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { return i1.complement(); case OP_RE_LOOP: i1 = get_info_rec(e->get_arg(0)); - if (e->get_decl()->get_num_parameters() >= 1) - lower_bound = e->get_decl()->get_parameter(0).get_int(); - if (e->get_decl()->get_num_parameters() == 2) - upper_bound = e->get_decl()->get_parameter(1).get_int(); - return i1.loop(lower_bound, upper_bound); + if (e->get_num_args() == 1) { + if (e->get_decl()->get_num_parameters() >= 1) + lower_bound = e->get_decl()->get_parameter(0).get_int(); + if (e->get_decl()->get_num_parameters() == 2) + upper_bound = e->get_decl()->get_parameter(1).get_int(); + return i1.loop(lower_bound, upper_bound); + } + else { + // legacy form carrying the bounds as arguments: + // (re.loop r lo) and (re.loop r lo hi) + arith_util autil(m); + rational n; + if (e->get_num_args() != 2 && e->get_num_args() != 3) + return unknown_info; + if (!autil.is_numeral(e->get_arg(1), n) || !n.is_unsigned()) + return unknown_info; + lower_bound = n.get_unsigned(); + if (e->get_num_args() == 3) { + if (!autil.is_numeral(e->get_arg(2), n) || !n.is_unsigned()) + return unknown_info; + upper_bound = n.get_unsigned(); + } + return i1.loop(lower_bound, upper_bound); + } case OP_RE_DIFF: if (e->get_num_args() != 2) return unknown_info; diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index ed56846553..09fca17cec 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -25,6 +25,7 @@ Abstract: #include "ast/arith_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_monadic.h" #include "cmd_context/cmd_context.h" #include "parsers/smt2/smt2parser.h" @@ -100,6 +101,7 @@ lbool run_file( seq_util u(m); arith_util a(m); seq_rewriter rw(m); + th_rewriter trw(m); trail_stack undo_trail; seq_monadic mon(rw, undo_trail, mode); @@ -197,6 +199,13 @@ lbool run_file( return; } obj_map& map = is_var ? var_re : term_re; + // Normalize the regex the way asserted_formulas normalizes assertions + // before seq_regex hands them to seq_monadic. Without this the bench + // measures raw parsed regexes, which no production path ever sees. + expr_ref normalized(r, m); + trw(normalized); + pin.push_back(normalized); + r = normalized; expr* previous = nullptr; if (map.find(s, previous)) { expr_ref intersection = rw.mk_regex_inter_normalize(previous, r); diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 9557b9cfc6..ebfdb09e11 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -16,6 +16,8 @@ Tests: 18. Solver: (str.in_re x (re.range x x)) unsat when len(x)=2 19. Solver: inverted symbolic bounds make membership unsatisfiable 20. Solver: contradictory constant lexical bounds are unsatisfiable + 22. re.loop with bounds as arguments agrees with the indexed form + 23. (Σ*·S)* is flattened to () | Σ*·S --*/ #include "ast/arith_decl_plugin.h" @@ -276,7 +278,33 @@ void tst_seq_rewriter() { ENSURE(res == l_true); } - // 20. unsat: contradictory constant lexical bounds. + // 22. (Σ*·S)* is rewritten to the flat form () | Σ*·S. + // Σ*·S is idempotent under concatenation — Σ*·S·Σ*·S = (Σ*·S·Σ*)·S + // is again of the form Σ*·S — so its Kleene star contributes + // nothing beyond the empty word. The star form is exponentially + // more expensive to determinize, so the flat form is kept. + { + expr_ref sigma_star(su.re.mk_full_seq(re_sort), m); + expr_ref b_re(su.re.mk_to_re(su.str.mk_string(zstring('b'))), m); + expr_ref star(su.re.mk_star(su.re.mk_concat(sigma_star, b_re)), m); + expr_ref e(star); + rw(e); + std::cout << "(sigma* b)* flattened: " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_star(e)); + + // Semantics: L* = words ending in "b", plus the empty word. + auto member = [&](char const* w) { + smt_params sp; + smt::context ctx(m, sp); + ctx.assert_expr(su.re.mk_in_re(su.str.mk_string(w), star)); + return ctx.check(); + }; + ENSURE(member("ab") == l_true); + ENSURE(member("") == l_true); + ENSURE(member("ba") == l_false); + } + + // "2024-01-01" < x < "2024-12-31" and x < "2023-01-01". // Since "2023-01-01" < "2024-01-01", no such x exists. if (false) @@ -296,5 +324,30 @@ void tst_seq_rewriter() { } } + // ----------------------------------------------------------------------- + // 22. re.loop with the bounds given as arguments must be interpreted the + // same as the indexed form. get_info used to read the bounds only + // from the decl parameters, which the argument form does not carry, + // so it silently fell back to lo = 0 and reported (ab){1,3} as + // nullable with min_length 0. seq_rewriter normalizes the argument + // form, so this is only observable on paths that bypass it. + // ----------------------------------------------------------------------- + { + arith_util a_util(m); + expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m); + expr_ref indexed(su.re.mk_loop_proper(ab, 1, 3), m); + expr* args[3] = { ab.get(), a_util.mk_int(1), a_util.mk_int(3) }; + expr_ref as_args(m.mk_app(su.get_family_id(), OP_RE_LOOP, 0, nullptr, 3, args), m); + + auto i1 = su.re.get_info(indexed); + auto i2 = su.re.get_info(as_args); + std::cout << "re.loop indexed: " << mk_pp(indexed, m) + << " nullable=" << i1.nullable << " min_length=" << i1.min_length << "\n"; + std::cout << "re.loop arguments: " << mk_pp(as_args, m) + << " nullable=" << i2.nullable << " min_length=" << i2.min_length << "\n"; + ENSURE(i1.nullable == l_false && i1.min_length == 2); + ENSURE(i2.nullable == l_false && i2.min_length == 2); + } + std::cout << "tst_seq_rewriter: all tests passed\n"; }