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

re-enable ule rewrite

Browse source
This commit is contained in:
Jakob Rath 2022-09-28 10:53:55 +02:00
parent d09e3eaa37
commit 27b31c88d2
1 changed files with 2 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/ule_constraint.cpp
View file

@ -78,8 +78,8 @@ namespace polysat {
m_lhs = 1, m_rhs = 0;
return;
}
// k <= p => p - k <= - k - 1
if (m_lhs.is_val() && false) {
// k <= p --> p - k <= - k - 1
if (m_lhs.is_val()) {
pdd k = m_lhs;
m_lhs = m_rhs - k;
m_rhs = - k - 1;
@ -94,17 +94,6 @@ namespace polysat {
m_lhs *= x;
SASSERT(m_lhs.leading_coefficient().is_power_of_two());
}
// 1 <= a*p + q <=> 1 <= p + a^-1*q for a odd.
if (m_lhs.is_one() && !m_rhs.leading_coefficient().is_power_of_two()) {
rational lc = m_rhs.leading_coefficient();
rational x, y;
gcd(lc, m_rhs.manager().two_to_N(), x, y);
if (x.is_neg())
x = mod(x, m_rhs.manager().two_to_N());
m_rhs *= x;
SASSERT(m_rhs.leading_coefficient().is_power_of_two());
}
}
std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {