mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

debug var_eqs

Browse source
This commit is contained in:
Lev Nachmanson 2019-04-03 16:02:36 -07:00
parent 7a3a696b6f
commit 98dca454ae
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -91,6 +91,7 @@ namespace nla {
f.m_index = i + 1;
m_todo.push_back(dfs_frame(jv.m_var, 0));
m_dfs_trail.push_back(jv.m_j);
m_marked_trail.push_back(jv.m_var.index());
m_marked[jv.m_var.index()] = true;
}
}
@ -111,4 +112,19 @@ namespace nla {
m_marked_trail.reset();
}
std::ostream& var_eqs::display(std::ostream& out) const {
m_uf.display(out);
unsigned idx = 0;
for (auto const& edges : m_eqs) {
out << signed_var(idx, from_index()) << ": ";
for (auto const& jv : edges) {
out << jv.m_var << " ";
}
out << "\n";
++idx;
}
return out;
}
}

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

@ -50,8 +50,16 @@ public:
return m_sv != other.m_sv;
}
rational rsign() const { return sign() ? rational::minus_one() : rational::one(); }
std::ostream& display(std::ostream& out) const {
return out << (sign()?"-":"") << var();
}
};
inline std::ostream& operator<<(std::ostream& out, signed_var const& sv) {
return sv.display(out);
}
class eq_justification {
lpci m_cs[4];
public:
@ -177,5 +185,7 @@ public:
eq_class equiv_class(signed_var v) { return eq_class(*this, v); }
eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); }
std::ostream& display(std::ostream& out) const;
};
}