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

display actual content of 'inequality' instances

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 17:29:51 +02:00
parent 9600f812a6
commit 0da1d9b218
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/constraint.cpp
View file

@ -82,6 +82,10 @@ namespace polysat {
return { std::move(lhs), std::move(rhs), m_src };
}
std::ostream& inequality::display(std::ostream& out) const {
return out << m_lhs << (is_strict() ? " < " : " <= ") << m_rhs;
}
pdd const& constraint::to_eq() const {
SASSERT(is_eq());
return to_ule().lhs();

4
src/math/polysat/constraint.h
View file

@ -236,6 +236,8 @@ namespace polysat {
* i=5 -q - 1 <= p - q - 1
*/
inequality rewrite_equiv(int i) const;
std::ostream& display(std::ostream& out) const;
};
class constraint_pp {
@ -248,6 +250,6 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, constraint_pp const& p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return out << i.as_signed_constraint(); }
inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return i.display(out); }
}