mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

adding commments

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-13 14:26:43 -07:00
parent a2e23377ba
commit 50d3e67e61
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/var_eqs.cpp
View file

@ -27,7 +27,7 @@ var_eqs::var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack(*this) {}
void var_eqs::push() {
m_trail_lim.push_back(m_trail.size());
get_trail_stack().push_scope();
m_stack.push_scope();
}
void var_eqs::pop(unsigned n) {
@ -41,7 +41,7 @@ void var_eqs::pop(unsigned n) {
}
m_trail_lim.shrink(m_trail_lim.size() - n);
m_trail.shrink(old_sz);
get_trail_stack().pop_scope(n);
m_stack.pop_scope(n);
}
void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) {

6
src/util/lp/var_eqs.h
View file

@ -180,6 +180,7 @@ public:
// union find event handlers
void set_merge_handler(var_eqs_merge_handler* mh) { m_merge_handler = mh; }
// this method is required by union_find
trail_stack<var_eqs> & get_trail_stack() { return m_stack; }
void unmerge_eh(unsigned i, unsigned j) {
@ -200,9 +201,8 @@ public:
signed_var(v2), signed_var(v1));
}
}
}; // end of var_eqs
inline std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); }
};
inline std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); }
}