mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

remove unused fields

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-24 19:57:43 -07:00
parent 6a6f9b1892
commit 9f6eb4f455
2 changed files with 1 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -484,8 +484,6 @@ namespace seq {
nielsen_node* m_tgt;
vector<nielsen_subst> m_subst;
vector<char_subst> m_char_subst; // character-level substitutions (mirrors ZIPT's SubstC)
ptr_vector<str_eq> m_side_str_eq; // side constraints: string equalities
ptr_vector<str_mem> m_side_str_mem; // side constraints: regex memberships
vector<int_constraint> m_side_int; // side constraints: integer equalities/inequalities
bool m_is_progress; // does this edge represent progress?
bool m_len_constraints_computed = false; // lazily computed substitution length constraints
@ -503,12 +501,9 @@ namespace seq {
vector<char_subst> const& char_substs() const { return m_char_subst; }
void add_char_subst(char_subst const& s) { m_char_subst.push_back(s); }
void add_side_str_eq(str_eq* eq) { m_side_str_eq.push_back(eq); }
void add_side_str_mem(str_mem* mem) { m_side_str_mem.push_back(mem); }
void add_side_int(int_constraint const& ic) { m_side_int.push_back(ic); }
ptr_vector<str_eq> const& side_str_eq() const { return m_side_str_eq; }
ptr_vector<str_mem> const& side_str_mem() const { return m_side_str_mem; }
vector<int_constraint> const& side_int() const { return m_side_int; }
bool is_progress() const { return m_is_progress; }

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

@ -605,26 +605,6 @@ namespace seq {
out << "?" << cs.m_var->id()
<< " &#8594; ?" << cs.m_val->id();
}
// side constraints: string equalities
for (auto const* eq : e->side_str_eq()) {
if (!first) out << "<br/>";
first = false;
out << "<font color=\"gray\">"
<< snode_label_html(eq->m_lhs, m)
<< " = "
<< snode_label_html(eq->m_rhs, m)
<< "</font>";
}
// side constraints: regex memberships
for (auto const* mem : e->side_str_mem()) {
if (!first) out << "<br/>";
first = false;
out << "<font color=\"gray\">"
<< snode_label_html(mem->m_str, m)
<< " &#8712; "
<< snode_label_html(mem->m_regex, m)
<< "</font>";
}
// side constraints: integer equalities/inequalities
for (auto const& ic : e->side_int()) {
if (!first) out << "<br/>";