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

Move helper functions

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 10:10:27 +01:00
parent 6eeb022048
commit 3a11350142
2 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/polysat/number.h
View file

@ -27,4 +27,22 @@ namespace polysat {
return val - mod(val, rational::power_of_two(k));
}
/** floor(a / 2^k) for a >= 0 */
inline rational div2k_floor(rational const& a, unsigned k)
{
SASSERT(a >= 0); // machine_div2k rounds towards 0
return machine_div2k(a, k);
}
/** ceil(a / 2^k) for a >= 0 */
inline rational div2k_ceil(rational const& a, unsigned k)
{
// Note: ceil(a/b) == floor((a-1)/b) + 1 for integers a,b and b > 0
// Special case for a = 0, because machine_div2k(a, k) does not return floor(a/2^k), but rounds towards 0 instead.
if (a.is_zero())
return a;
SASSERT(a > 0); // machine_div2k rounds towards 0
return machine_div2k(a - 1, k) + 1;
}
}

16
src/sat/smt/polysat/viable.cpp
View file

@ -1007,22 +1007,6 @@ namespace polysat {
}
rational div2k_floor(rational const& a, unsigned k)
{
SASSERT(a >= 0); // machine_div2k rounds towards 0
return machine_div2k(a, k);
}
rational div2k_ceil(rational const& a, unsigned k)
{
// Note: ceil(a/b) == floor((a-1)/b) + 1 for integers a,b and b > 0
// Special case for a = 0, because machine_div2k(a, k) does not return floor(a/2^k), but rounds towards 0 instead.
if (a.is_zero())
return a;
return machine_div2k(a - 1, k) + 1;
}
/// Let x = concat(y, z) and x not in [lo;hi[.
/// Returns an interval I such that z not in I.
r_interval viable::chop_off_upper(r_interval const& i, unsigned const Ny, unsigned const Nz, rational const* y_fixed_value) {