mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-18 19:14:29 +00:00
Code Activity

Fix typo: rename m_parith to m_parikh in seq_nielsen.h/.cpp

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-11 19:08:11 +00:00
parent 4b2f5e2bb0
commit a51ba544ea
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -433,11 +433,11 @@ namespace seq {
nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver):
m_sg(sg),
m_solver(solver),
m_parith(alloc(seq_parikh, sg)) {
m_parikh(alloc(seq_parikh, sg)) {
}
nielsen_graph::~nielsen_graph() {
dealloc(m_parith);
dealloc(m_parikh);
reset();
}
@ -1041,12 +1041,12 @@ namespace seq {
// Generate modular length constraints (len(str) = min_len + stride·k, etc.)
// and append them to the node's integer constraint list.
m_parith->apply_to_node(node);
m_parikh->apply_to_node(node);
// Lightweight feasibility pre-check: does the Parikh modular constraint
// contradict the variable's current integer bounds? If so, mark this
// node as a Parikh-image conflict immediately (avoids a solver call).
if (!node.is_currently_conflict() && m_parith->check_parikh_conflict(node)) {
if (!node.is_currently_conflict() && m_parikh->check_parikh_conflict(node)) {
node.set_general_conflict(true);
node.set_reason(backtrack_reason::parikh_image);
}
@ -2306,7 +2306,7 @@ namespace seq {
// generated from minterm m_i, ?c must belong to the character
// class described by m_i so that str ∈ derivative(R, m_i).
if (mt->get_expr()) {
char_set cs = m_parith->minterm_to_char_set(mt->get_expr());
char_set cs = m_parikh->minterm_to_char_set(mt->get_expr());
if (!cs.is_empty())
child->add_char_range(fresh_char, cs);
}