From fa89910452510133a17dc91c9ab2b70eaacf0681 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 2 Apr 2026 21:09:23 -0700 Subject: [PATCH] Add SASSERT invariants and pre/postconditions to Nielsen seq solver (#9216) * Initial plan * Add SASSERT invariants and pre/postconditions to Nielsen seq solver Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add clarifying comment to m_str_eq.empty() postcondition Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 22 +++++++++++++++++++++- src/smt/seq/seq_nielsen.h | 15 +++++++++++++-- 2 files changed, 34 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 36d711399..c213bb4df 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -127,6 +127,7 @@ namespace seq { if (m_lhs && m_rhs && m_lhs->id() > m_rhs->id()) { std::swap(m_lhs, m_rhs); } + SASSERT(!m_lhs || !m_rhs || m_lhs->id() <= m_rhs->id()); } bool str_eq::is_trivial() const { @@ -235,6 +236,10 @@ namespace seq { // clone regex occurrence tracking m_regex_occurrence = parent.m_regex_occurrence; + + SASSERT(m_str_eq.size() == parent.m_str_eq.size()); + SASSERT(m_str_mem.size() == parent.m_str_mem.size()); + SASSERT(m_constraints.size() == parent.m_constraints.size()); } bool nielsen_node::track_regex_occurrence(unsigned regex_id, unsigned mem_id) { @@ -269,6 +274,7 @@ namespace seq { void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { SASSERT(s.m_var); + SASSERT(s.m_replacement != nullptr); for (auto &eq : m_str_eq) { auto new_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement); auto new_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement); @@ -422,6 +428,7 @@ namespace seq { unsigned id = m_nodes.size(); nielsen_node* n = alloc(nielsen_node, *this, id); m_nodes.push_back(n); + SASSERT(n->id() == m_nodes.size() - 1); return n; } @@ -433,6 +440,8 @@ namespace seq { } nielsen_edge* nielsen_graph::mk_edge(nielsen_node* src, nielsen_node* tgt, bool is_progress) { + SASSERT(src != nullptr); + SASSERT(tgt != nullptr); nielsen_edge* e = alloc(nielsen_edge, src, tgt, is_progress); m_edges.push_back(e); src->add_outgoing(e); @@ -505,6 +514,10 @@ namespace seq { m_dep_mgr.reset(); m_solver.reset(); m_core_solver.reset(); + SASSERT(m_nodes.empty()); + SASSERT(m_edges.empty()); + SASSERT(m_root == nullptr); + SASSERT(m_sat_node == nullptr); } // ----------------------------------------------------------------------- @@ -1193,8 +1206,12 @@ namespace seq { } - if (is_satisfied()) + if (is_satisfied()) { + // pass 1 removed all trivial str_eq entries; is_satisfied() requires + // the remainder to be trivial, so the vector must be empty here. + SASSERT(m_str_eq.empty()); return simplify_result::satisfied; + } return simplify_result::proceed; } @@ -1306,6 +1323,7 @@ namespace seq { verbose_stream() << " side constraint: " << c.fml << "\n"; }); ++m_stats.m_num_sat; + SASSERT(m_sat_node != nullptr); return r; } if (r == search_result::unsat) { @@ -2184,6 +2202,8 @@ namespace seq { } bool nielsen_graph::generate_extensions(nielsen_node *node) { + SASSERT(node != nullptr); + SASSERT(!node->is_currently_conflict()); // The first modifier that produces edges is used and returned immediately. // Priority 1: deterministic modifiers (single child, always progress) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 2af940d7a..4e761a6c2 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -586,8 +586,16 @@ namespace seq { vector const& str_mems() const { return m_str_mem; } vector& str_mems() { return m_str_mem; } - void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); } - void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); } + void add_str_eq(str_eq const& eq) { + SASSERT(eq.m_lhs != nullptr); + SASSERT(eq.m_rhs != nullptr); + m_str_eq.push_back(eq); + } + void add_str_mem(str_mem const& mem) { + SASSERT(mem.m_str != nullptr); + SASSERT(mem.m_regex != nullptr); + m_str_mem.push_back(mem); + } bool add_constraint(constraint const &ic); vector const& constraints() const { return m_constraints; } @@ -857,6 +865,9 @@ namespace seq { void create_root() { SASSERT(!root()); set_root(mk_node()); + SASSERT(m_root != nullptr); + SASSERT(m_root->id() == 0); + SASSERT(m_nodes[0] == m_root); } // path of edges from root to sat_node (set when sat_node is set)