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

inequality::rewrite_equiv

Browse source
This commit is contained in:
Jakob Rath 2023-02-09 16:33:59 +01:00
parent 06cc15d1cc
commit c60a2b10a5
2 changed files with 57 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -46,6 +46,51 @@ namespace polysat {
return inequality(c.rhs(), c.lhs(), src);
}
inequality inequality::rewrite_equiv(int i) const {
pdd const& p = is_strict() ? m_rhs : m_lhs;
pdd const& q = is_strict() ? m_lhs : m_rhs;
pdd lhs = p;
pdd rhs = q;
switch (i) {
case 0:
// p <= q
// p > q
break;
case 1:
// p <= p - q - 1
lhs = p;
rhs = p - q - 1;
break;
case 2:
// q - p <= q
lhs = q - p;
rhs = q;
break;
case 3:
// q - p <= -p - 1
// q - p > -p - 1
lhs = q - p;
rhs = -p - 1;
break;
case 4:
// -q - 1 <= -p - 1
lhs = -q - 1;
rhs = -p - 1;
break;
case 5:
// -q - 1 <= p - q - 1
lhs = -q - 1;
rhs = p - q - 1;
break;
default:
UNREACHABLE();
break;
}
if (is_strict())
swap(lhs, rhs);
return { std::move(lhs), std::move(rhs), m_src };
}
ule_constraint& constraint::to_ule() {
return *dynamic_cast<ule_constraint*>(this);
}

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

@ -226,6 +226,18 @@ namespace polysat {
bool is_strict() const { return m_src.is_negative(); }
signed_constraint as_signed_constraint() const { return m_src; }
operator signed_constraint() const { return m_src; }
/**
* Rewrite to one of six equivalent forms:
*
* i=0 p <= q (unchanged)
* i=1 p <= p - q - 1
* i=2 q - p <= q
* i=3 q - p <= -p - 1
* i=4 -q - 1 <= -p - 1
* i=5 -q - 1 <= p - q - 1
*/
inequality rewrite_equiv(int i) const;
};
class constraint_pp {