mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

Add SASSERT invariants and pre/postconditions to Nielsen seq solver

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-03 02:11:02 +00:00 • committed by GitHub
parent 4a5ef833f2
commit 0726edcd0a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 32 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/seq/seq_nielsen.cpp
View file

@ -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,10 @@ namespace seq {
}
if (is_satisfied())
if (is_satisfied()) {
SASSERT(m_str_eq.empty());
return simplify_result::satisfied;
}
return simplify_result::proceed;
}
@ -1306,6 +1321,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 +2200,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)

15
src/smt/seq/seq_nielsen.h
View file

@ -586,8 +586,16 @@ namespace seq {
vector<str_mem> const& str_mems() const { return m_str_mem; }
vector<str_mem>& 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<constraint> 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)