mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

more general simplification

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-10 04:45:48 -08:00
parent 9c3489ba4b
commit 4c2231897f
1 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -84,7 +84,7 @@ namespace polysat {
m_lhs = m_rhs - k;
m_rhs = - k - 1;
}
// normalize leading coefficient to be a power of 2
// a*p + q <= 0 <=> p + a^-1*q <= 0 for a odd
if (m_rhs.is_zero() && !m_lhs.leading_coefficient().is_power_of_two()) {
rational lc = m_lhs.leading_coefficient();
rational x, y;
@ -95,14 +95,15 @@ namespace polysat {
SASSERT(m_lhs.leading_coefficient().is_power_of_two());
}
if (m_lhs.is_one() && m_rhs.is_monomial() && m_rhs.leading_coefficient().is_odd() && !m_rhs.leading_coefficient().is_one()) {
pdd rhs = m_rhs;
m_rhs = 1;
while (!rhs.is_val()) {
m_rhs *= rhs.manager().mk_var(rhs.var());
SASSERT(rhs.lo().is_zero());
rhs = rhs.hi();
}
// 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());
}
}