From 63ad8f94471bad4f85382bb629f9373b0d7ae8d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Aug 2026 15:57:08 -0700 Subject: [PATCH] Add lazy regex live-state traversal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554 --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/seq_derive.cpp | 11 +- src/ast/rewriter/seq_derive.h | 6 +- src/ast/rewriter/seq_monadic.cpp | 84 +-------- src/ast/rewriter/seq_monadic.h | 21 +-- src/ast/rewriter/seq_regex_live.cpp | 279 ++++++++++++++++++++++++++++ src/ast/rewriter/seq_regex_live.h | 81 ++++++++ src/smt/seq_regex.cpp | 107 +---------- src/smt/seq_regex.h | 47 +---- 9 files changed, 397 insertions(+), 240 deletions(-) create mode 100644 src/ast/rewriter/seq_regex_live.cpp create mode 100644 src/ast/rewriter/seq_regex_live.h diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index afe18ad3f3..5dd3e2e578 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -48,6 +48,7 @@ z3_add_component(rewriter seq_range_predicate.cpp seq_rewriter.cpp seq_regex_bisim.cpp + seq_regex_live.cpp seq_skolem.cpp term_enumeration.cpp th_rewriter.cpp diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 1876f4ddfb..b04516de63 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -39,7 +39,8 @@ namespace seq { m_br(m), m_re(re), m_trail(m), - m_cofactor_cache(m), + m_brz_cofactor_cache(m), + m_ant_cofactor_cache(m), m_ele(m), m_path_expr(m) { m_br.set_flat_and_or(false); @@ -1572,15 +1573,18 @@ namespace seq { } expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *r) { + cofactor_cache& cache = + mode == transition_mode::light_antimirov_tm ? + m_ant_cofactor_cache : m_brz_cofactor_cache; expr_ref_pair_vector *v = nullptr; - if (m_cofactor_cache.find(r, v)) + if (cache.find(r, v)) return *v; v = alloc(expr_ref_pair_vector, m); if (mode == transition_mode::light_antimirov_tm) light_ant_derivative_cofactors(r, *v); else derivative_cofactors(r, *v); - m_cofactor_cache.insert(r, v); // takes ownership of v and pins the key r + cache.insert(r, v); // takes ownership of v and pins the key r return *v; } @@ -1659,4 +1663,3 @@ namespace seq { } } - diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 46ec0157fe..1a91b9e2e7 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -95,7 +95,8 @@ namespace seq { obj_pair_map m_atop_cache, m_btop_cache; // post-simplify cache expr_ref_vector m_trail; // pin cached results - cofactor_cache m_cofactor_cache; + cofactor_cache m_brz_cofactor_cache; + cofactor_cache m_ant_cofactor_cache; // Op cache for ITE-hoisting operations (union, inter, concat, complement) // Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement @@ -276,7 +277,8 @@ namespace seq { expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r); void maybe_reset_cached_cofactors(unsigned cap) { - m_cofactor_cache.maybe_reset(cap); + m_brz_cofactor_cache.maybe_reset(cap); + m_ant_cofactor_cache.maybe_reset(cap); } /** diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index a0265f0803..26d11c6a20 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -131,76 +131,6 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r); } -bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { - obj_map id; - expr_ref_vector states(m); - vector> succ; - bool_vector maybe_null; - auto intern = [&](expr* s) -> unsigned { - unsigned k; - if (id.find(s, k)) return k; - k = states.size(); - id.insert(s, k); - states.push_back(s); - succ.push_back(svector()); - maybe_null.push_back(nullable(s) != l_false); // unknown nullability => keep (conservative) - return k; - }; - intern(R); - const unsigned STATE_CAP = 1u << 12; - for (unsigned i = 0; i < states.size(); ++i) { - if (states.size() > STATE_CAP) { - m_stats.inc_bail(bail_reason::state_cap); - return false; - } - if (!m.inc()) { - m_stats.inc_bail(bail_reason::resource); - return false; - } - expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i)); - for (auto const& [g, t] : cof) { - if (re().is_empty(t)) continue; - unsigned k = intern(t); // MUST precede succ[i] indexing: intern may - succ[i].push_back(k); // grow (realloc) succ, invalidating succ[i]& - } - } - unsigned n = states.size(); - bool_vector live; - live.resize(n, false); - for (unsigned i = 0; i < n; ++i) - live[i] = maybe_null[i]; - for (bool ch = true; ch; ) { - ch = false; - for (unsigned i = 0; i < n; ++i) - if (!live[i]) - for (unsigned j : succ[i]) - if (live[j]) { live[i] = true; ch = true; break; } - } - for (unsigned i = 0; i < n; ++i) - if (live[i]) { out.push_back(states.get(i)); m_pin.push_back(states.get(i)); } - return true; -} - -expr_ref_vector const* seq_monadic::live_states_cached(expr* R) { - expr_ref_vector* v = nullptr; - if (m_live_cache.find(R, v)) - return v; // may be null: previously gave up on R - v = alloc(expr_ref_vector, m); - if (!live_states(R, *v)) { - dealloc(v); - v = nullptr; - } - m_pin.push_back(R); // keep the key alive for the cache's lifetime - m_live_cache.insert(R, v); - return v; -} - -void seq_monadic::reset_live_cache() { - for (auto const& [k, v] : m_live_cache) - dealloc(v); - m_live_cache.reset(); -} - lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* witness_word) { unsigned n = comps.size(); if (n == 0) { @@ -417,7 +347,7 @@ void seq_monadic::reset_search() { m_der_cache.reset(); m_nullable_cache.reset(); m_undef_vars = 0; - reset_live_cache(); + m_live_states.reset(); } bool seq_monadic::prepare(membership_vec const& memberships) { @@ -550,11 +480,15 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { if (last_atom) targets.push_back(nullptr); else { - expr_ref_vector const* Q = live_states_cached(R); - if (!Q) - return l_undef; - for (expr* q : *Q) + auto live = m_live_states.reachable_live(R); + for (expr* q : live) targets.push_back(q); + if (live.failed()) { + m_stats.inc_bail( + live.failure_reason() == seq::live_states::failure::state_cap ? + bail_reason::state_cap : bail_reason::resource); + return l_undef; + } } unsigned vi = var_index(a.var.get()); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index eaa0bb3638..c9d0508eb0 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -63,6 +63,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_range_predicate.h" +#include "ast/rewriter/seq_regex_live.h" #include "ast/rewriter/guard_set.h" #include "ast/rewriter/th_rewriter.h" #include "util/lbool.h" @@ -166,7 +167,7 @@ class seq_monadic { }; group_sig m_sig_buf; // reused by group_nonempty (avoids allocating per lookup) std::unordered_map m_group_cache; - obj_map m_live_cache; // regex -> live split states (null = gave up) + seq::live_states m_live_states; // Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on // (r, elem): the search revisits the same constant step on many branches. @@ -175,20 +176,10 @@ class seq_monadic { // Memoized nullability of a derivative state: l_true / l_false / l_undef (unknown). lbool nullable(expr* r); - // Symbolic transition cofactors in the selected mode. Memoized per regex `r` in - // m_cofactors: the returned vector is owned by that cache (see the cofactor_cache - // class above for the persistence/reset policy). + // Symbolic transition cofactors in the selected mode. The returned vector is owned + // by seq_rewriter's mode-specific cofactor cache. expr_ref_pair_vector const& derivative_cofactors(expr* r); - // Live reachable derivative states of R (BFS over cofactor targets + liveness - // least-fixpoint). These are the split states q. Returns false on a cap overrun. - bool live_states(expr* R, expr_ref_vector& out); - - // Memoized live_states. Returns null if the computation gave up for this regex. - expr_ref_vector const* live_states_cached(expr* R); - - void reset_live_cache(); - // Product-reachability emptiness of a conjunction of components (all on one // variable). l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up // (cap overrun, non-range guard, or undecidable nullability). @@ -249,9 +240,9 @@ public: seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), - m_regexes(rw.m()) {} + m_regexes(rw.m()), m_live_states(rw, mode, 1u << 12) {} - ~seq_monadic() { reset_live_cache(); } + ~seq_monadic() = default; void collect_statistics(::statistics &st) const; diff --git a/src/ast/rewriter/seq_regex_live.cpp b/src/ast/rewriter/seq_regex_live.cpp new file mode 100644 index 0000000000..853a6b0bd1 --- /dev/null +++ b/src/ast/rewriter/seq_regex_live.cpp @@ -0,0 +1,279 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_regex_live.cpp + +Abstract: + + Shared lazy live-state traversal for regular-expression derivatives. + +--*/ + +#include "ast/rewriter/seq_regex_live.h" +#include "ast/rewriter/seq_rewriter.h" +#include "util/obj_hashtable.h" +#include "util/uint_set.h" + +namespace seq { + + struct live_states::search { + svector m_to_explore; + unsigned m_explore_head = 0; + uint_set m_seen; + vector> m_predecessors; + bool_vector m_live; + bool_vector m_closed; + svector m_live_frontier; + failure m_failure = failure::none; + bool m_complete = false; + }; + + struct live_states::imp { + seq_rewriter& m_rw; + ast_manager& m; + seq_util::rex& m_re; + transition_mode m_mode; + unsigned m_max_states; + obj_map m_ids; + expr_ref_vector m_states; + vector> m_successors; + svector m_nullable; + bool_vector m_expanded; + obj_map m_searches; + + imp(seq_rewriter& rw, transition_mode mode, unsigned max_states) : + m_rw(rw), + m(rw.m()), + m_re(rw.u().re), + m_mode(mode), + m_max_states(max_states), + m_states(m) { + } + + ~imp() { + reset(); + } + + unsigned intern(expr* r) { + unsigned id = 0; + if (m_ids.find(r, id)) + return id; + id = m_states.size(); + m_ids.insert(r, id); + m_states.push_back(r); + m_successors.push_back(svector()); + m_nullable.push_back(2); + m_expanded.push_back(false); + return id; + } + + void resize(search& s) { + unsigned size = m_states.size(); + if (s.m_predecessors.size() < size) + s.m_predecessors.resize(size); + if (s.m_live.size() < size) + s.m_live.resize(size, false); + if (s.m_closed.size() < size) + s.m_closed.resize(size, false); + } + + char nullable(unsigned id) { + if (m_nullable[id] != 2) + return m_nullable[id]; + expr* r = m_states.get(id); + lbool n = m_re.get_info(r).nullable; + if (n == l_undef) { + expr_ref f = m_rw.is_nullable(r); + n = m.is_true(f) ? l_true : m.is_false(f) ? l_false : l_undef; + } + m_nullable[id] = n == l_true ? 1 : n == l_false ? 0 : 3; + return m_nullable[id]; + } + + void mark_live(search& s, unsigned id) { + svector todo; + todo.push_back(id); + while (!todo.empty()) { + id = todo.back(); + todo.pop_back(); + if (!s.m_seen.contains(id) || s.m_live[id]) + continue; + s.m_live[id] = true; + s.m_live_frontier.push_back(id); + for (unsigned predecessor : s.m_predecessors[id]) + todo.push_back(predecessor); + } + } + + bool add_state(search& s, unsigned id) { + if (s.m_seen.contains(id)) + return true; + if (s.m_to_explore.size() >= m_max_states) { + s.m_failure = failure::state_cap; + return false; + } + resize(s); + s.m_seen.insert(id); + s.m_to_explore.push_back(id); + if (nullable(id) != 0) + mark_live(s, id); + return true; + } + + bool expand_state(unsigned id, failure& f) { + if (m_expanded[id]) + return true; + if (!m.inc()) { + f = failure::resource; + return false; + } + m_expanded[id] = true; + nullable(id); + auto const& cofactors = m_rw.get_derive().get_cached_cofactors(m_mode, m_states.get(id)); + for (auto const& [guard, target] : cofactors) { + if (m_re.is_empty(target)) + continue; + unsigned target_id = intern(target); + if (!m_successors[id].contains(target_id)) + m_successors[id].push_back(target_id); + } + return true; + } + + void close(search& s) { + for (unsigned id : s.m_to_explore) + if (!s.m_live[id]) + s.m_closed[id] = true; + s.m_complete = true; + } + + void expand(search& s) { + if (s.m_complete || s.m_failure != failure::none) + return; + if (s.m_explore_head == s.m_to_explore.size()) { + close(s); + return; + } + + unsigned id = s.m_to_explore[s.m_explore_head++]; + if (!expand_state(id, s.m_failure)) + return; + resize(s); + for (unsigned target : m_successors[id]) { + if (!add_state(s, target)) + return; + if (!s.m_predecessors[target].contains(id)) + s.m_predecessors[target].push_back(id); + if (s.m_live[target]) + mark_live(s, id); + } + } + + bool ensure(search& s, unsigned index) { + while (index >= s.m_live_frontier.size() && + !s.m_complete && + s.m_failure == failure::none) + expand(s); + return index < s.m_live_frontier.size(); + } + + search* get_search(expr* root) { + search* s = nullptr; + if (m_searches.find(root, s)) + return s; + s = alloc(search); + unsigned root_id = intern(root); + add_state(*s, root_id); + m_searches.insert(root, s); + return s; + } + + void reset() { + for (auto const& [root, s] : m_searches) + dealloc(s); + m_searches.reset(); + m_ids.reset(); + m_states.reset(); + m_successors.reset(); + m_nullable.reset(); + m_expanded.reset(); + } + }; + + live_states::live_states(seq_rewriter& rw, transition_mode mode, unsigned max_states) : + m_imp(alloc(imp, rw, mode, max_states)) { + } + + live_states::~live_states() { + dealloc(m_imp); + } + + expr* live_states::iterator::operator*() const { + return m_owner->get_live(m_search, m_index); + } + + live_states::iterator& live_states::iterator::operator++() { + ++m_index; + return *this; + } + + bool live_states::iterator::operator!=(iterator const& other) const { + if (other.m_end) + return m_owner->ensure(m_search, m_index); + return m_owner != other.m_owner || + m_search != other.m_search || + m_index != other.m_index || + m_end != other.m_end; + } + + live_states::iterator live_states::reachable::begin() const { + return iterator(m_owner, m_search, 0, false); + } + + live_states::iterator live_states::reachable::end() const { + return iterator(m_owner, m_search, 0, true); + } + + bool live_states::reachable::failed() const { + return m_owner->get_failure(m_search) != failure::none; + } + + live_states::failure live_states::reachable::failure_reason() const { + return m_owner->get_failure(m_search); + } + + bool live_states::reachable::is_dead() { + return !m_owner->ensure(m_search, 0) && !failed(); + } + + live_states::reachable live_states::reachable_live(expr* r) { + return reachable(this, m_imp->get_search(r)); + } + + bool live_states::contains(expr* r) const { + return m_imp->m_ids.contains(r); + } + + unsigned live_states::state_id(expr* r) { + return m_imp->intern(r) + 1; + } + + void live_states::reset() { + m_imp->reset(); + } + + bool live_states::ensure(search* s, unsigned index) { + return m_imp->ensure(*s, index); + } + + expr* live_states::get_live(search* s, unsigned index) const { + return m_imp->m_states.get(s->m_live_frontier[index]); + } + + live_states::failure live_states::get_failure(search* s) const { + return s->m_failure; + } + +} diff --git a/src/ast/rewriter/seq_regex_live.h b/src/ast/rewriter/seq_regex_live.h new file mode 100644 index 0000000000..5a297e66ff --- /dev/null +++ b/src/ast/rewriter/seq_regex_live.h @@ -0,0 +1,81 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_regex_live.h + +Abstract: + + Shared lazy live-state traversal for regular-expression derivatives. + +--*/ +#pragma once + +#include "ast/rewriter/seq_derive.h" +#include "ast/ast.h" + +class seq_rewriter; + +namespace seq { + + class live_states { + struct search; + struct imp; + + public: + enum class failure { + none, + state_cap, + resource + }; + + class iterator { + live_states* m_owner = nullptr; + search* m_search = nullptr; + unsigned m_index = 0; + bool m_end = false; + + public: + iterator(live_states* owner, search* s, unsigned index, bool end) : + m_owner(owner), m_search(s), m_index(index), m_end(end) {} + expr* operator*() const; + iterator& operator++(); + bool operator!=(iterator const& other) const; + }; + + class reachable { + live_states* m_owner = nullptr; + search* m_search = nullptr; + + public: + reachable(live_states* owner, search* s) : + m_owner(owner), m_search(s) {} + iterator begin() const; + iterator end() const; + bool failed() const; + failure failure_reason() const; + bool is_dead(); + }; + + private: + imp* m_imp; + + bool ensure(search* s, unsigned index); + expr* get_live(search* s, unsigned index) const; + failure get_failure(search* s) const; + + public: + live_states(seq_rewriter& rw, + transition_mode mode = transition_mode::brzozowski_tm, + unsigned max_states = UINT_MAX); + ~live_states(); + live_states(live_states const&) = delete; + live_states& operator=(live_states const&) = delete; + + reachable reachable_live(expr* r); + bool contains(expr* r) const; + unsigned state_id(expr* r); + void reset(); + }; +} diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 1951266165..59336556c1 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -31,8 +31,7 @@ namespace smt { ctx(th.get_context()), m(th.get_manager()), m_monadic(seq_rw(), ctx.get_trail_stack()), - m_state_to_expr(m), - m_state_graph(state_graph::state_pp(this, pp_state)) { + m_live_states(seq_rw(), seq::transition_mode::brzozowski_tm, 10000) { m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); }); } @@ -640,8 +639,8 @@ namespace smt { } if (info.interpreted) { - update_state_graph(r); - if (m_state_graph.is_dead(get_state_id(r))) { + auto live = m_live_states.reachable_live(r); + if (live.is_dead()) { STRACE(seq_regex_brief, tout << "(dead) ";); th.add_axiom(~lit); return true; @@ -665,8 +664,7 @@ namespace smt { /** * Propagate the atom (accept s i r) * - * Propagation triggers updating the state graph for dead state detection: - * (accept s i r) => update_state_graph(r) + * Propagation triggers derivative reachability for dead state detection: * (accept s i r) & dead(r) => false * * Propagation is also blocked under certain conditions to throttle @@ -1292,101 +1290,10 @@ namespace smt { return sk().mk("re.first", n, a().mk_int(r->get_id()), elem_sort); } - /** - * Dead state elimination using the state_graph class - */ - - unsigned seq_regex::get_state_id(expr* e) { - // Assign increasing IDs starting from 1 - if (!m_expr_to_state.contains(e)) { - m_state_to_expr.push_back(e); - unsigned new_id = m_state_to_expr.size(); - m_expr_to_state.insert(e, new_id); - STRACE(seq_regex_brief, tout << "new(" << expr_id_str(e) - << ")=" << state_str(e) << " ";); - STRACE(seq_regex, tout - << "New state ID: " << new_id - << " = " << mk_pp(e, m) << std::endl;); - SASSERT(get_expr_from_id(new_id) == e); - } - return m_expr_to_state.find(e); - } - expr* seq_regex::get_expr_from_id(unsigned id) { - SASSERT(id >= 1); - SASSERT(id <= m_state_to_expr.size()); - return m_state_to_expr.get(id - 1); - } - - bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) { - // TBD: This can be used to optimize the state graph: - // return false here if it is known that r1 -> r2 can never be - // in a cycle. There are various easy syntactic checks on r1 and r2 - // that can be used to infer this (e.g. star height, or length if - // both are star-free). - // This check need not be sound, but if it is not, some dead states - // will be missed. - return true; - } - - /* - Update the state graph with expression r and all its derivatives. - */ - bool seq_regex::update_state_graph(expr* r) { - unsigned r_id = get_state_id(r); - if (m_state_graph.is_done(r_id)) return false; - if (m_state_graph.get_size() >= m_max_state_graph_size) { - STRACE(seq_regex, tout << "Warning: ignored state graph update -- max size of seen states reached!" << std::endl;); - STRACE(seq_regex_brief, tout << "(MAX SIZE REACHED) ";); - return false; - } - STRACE(seq_regex, tout << "Updating state graph for regex " - << mk_pp(r, m) << ") ";); - - STRACE(state_graph, - if (!m_state_graph.is_seen(r_id)) - tout << std::endl << "state(" << r_id << ") = " << re().to_str(r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;); - // Add state - m_state_graph.add_state(r_id); - STRACE(seq_regex, tout << "Updating state graph for regex " - << mk_pp(r, m) << ") " << std::endl;); - STRACE(seq_regex_brief, tout << std::endl << "USG(" - << state_str(r) << ") ";); - expr_ref r_nullable = is_nullable_wrapper(r); - if (m.is_true(r_nullable)) { - m_state_graph.mark_live(r_id); - } - else { - // Add edges to all derivatives - expr_ref_vector derivatives(m); - STRACE(seq_regex_verbose, tout - << "getting all derivs: " << r_id << " " << std::endl;); - get_derivative_targets(r, derivatives); - for (auto const& dr: derivatives) { - unsigned dr_id = get_state_id(dr); - STRACE(seq_regex_verbose, tout - << std::endl << " traversing deriv: " << dr_id << " ";); - STRACE(state_graph, - if (!m_state_graph.is_seen(dr_id)) - tout << "state(" << dr_id << ") = " << re().to_str(dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;); - // Add state - m_state_graph.add_state(dr_id); - bool maybecycle = can_be_in_cycle(r, dr); - m_state_graph.add_edge(r_id, dr_id, maybecycle); - } - m_state_graph.mark_done(r_id); - } - - STRACE(seq_regex, m_state_graph.display(tout);); - STRACE(seq_regex_brief, tout << std::endl;); - STRACE(seq_regex_brief, m_state_graph.display(tout);); - return true; - } - std::string seq_regex::state_str(expr* e) { - if (m_expr_to_state.contains(e)) - return std::to_string(get_state_id(e)); - else - return expr_id_str(e); + if (m_live_states.contains(e)) + return std::to_string(m_live_states.state_id(e)); + return expr_id_str(e); } std::string seq_regex::expr_id_str(expr* e) { return std::string("id") + std::to_string(e->get_id()); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index eaa68dc781..b1832cfffb 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -17,9 +17,9 @@ Author: #pragma once #include "util/scoped_vector.h" -#include "util/state_graph.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_monadic.h" +#include "ast/rewriter/seq_regex_live.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "smt/smt_context.h" @@ -56,13 +56,6 @@ Author: (next states) d(r1)=r2: r2 is the derivative of r1 n(r1)=b: b = whether r1 is nullable or not - USG(r): updating state graph for regex r (add all derivatives) - - -tr:state_graph - This is the tracing done by util/state_graph, the data structure - that seq_regex uses to track live and dead regexes, which can - altneratively be used to get a high-level picture of what states - are being explored and updated as the solver progresses. -tr:seq_regex_verbose Used for some more frequent tracing (in the style of seq_regex, @@ -72,21 +65,12 @@ Author: These are the underlying sequence theory tracing, often used by the rewriter. - DEBUGGING AND VIEWING STATE GRAPH GRAPHICAL OUTPUT + DEBUGGING -dbg:seq_regex Debugging that checks invariants. Currently, checks that derivative normal form is correctly preserved in the rewriter. - -dbg:state_graph - Debugging for the state graph, which - 1. Checks state graph invariants, and - 2. Generates the files .z3-state-graph.dgml and .z3-state-graph.dot - which can be used to visually view the state graph being explored, - during or after executing Z3. - The output can be viewed: - - Using Visual Studio for .dgml - - Using a tool such as xdot (`xdot .z3-state-graph.dot`) for .dot */ namespace smt { @@ -163,23 +147,9 @@ namespace smt { unsigned m_monadic_assumption_generation = UINT_MAX; unsigned m_monadic_fallback_generation = UINT_MAX; - /* - state_graph for dead state detection, and associated methods - */ - ptr_addr_map m_expr_to_state; - expr_ref_vector m_state_to_expr; - state_graph m_state_graph; + seq::live_states m_live_states; /* map from uninterpreted regex constants to assigned regex expressions by EQ */ // expr_map m_const_to_expr; - unsigned m_max_state_graph_size { 10000 }; - // Convert between expressions and states (IDs) - unsigned get_state_id(expr* e); - expr* get_expr_from_id(unsigned id); - // Cycle-detection heuristic - // Note: Doesn't need to be sound or complete (doesn't affect soundness) - bool can_be_in_cycle(expr* r1, expr* r2); - // Update the graph - bool update_state_graph(expr* r); // Printing expressions for seq_regex_brief std::string state_str(expr* e); @@ -239,17 +209,6 @@ namespace smt { seq_regex_ptr must be a pointer to seq_regex and the id must be a valid state id or else nothing is printed. */ - static void pp_state(void* seq_regex_ptr, std::ostream& out, unsigned id, bool html_encode) { - seq_regex* sr = (seq_regex*)seq_regex_ptr; - if (sr) { - seq_util::rex re_util(sr->re()); - if (1 <= id && id <= sr->m_state_to_expr.size()) { - expr* r = sr->get_expr_from_id(id); - seq_util::rex::pp(re_util, r, html_encode).display(out); - } - } - } - bool block_if_empty(expr* r, literal lit); void add_monadic_membership(literal lit, expr* s, expr* r); // Expand a term through theory_seq's solution map, but substitute a sub-term only