mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

comment

Browse source
This commit is contained in:
Jakob Rath 2024-01-12 16:32:36 +01:00
parent d8bcca130c
commit 70d2057557
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -773,14 +773,13 @@ namespace polysat {
// If new_lo = new_hi it means that // If new_lo = new_hi it means that
// mod(ceil (lo / 2^k), 2^w) = mod(ceil (hi / 2^k), 2^w) // mod(ceil (lo / 2^k), 2^w) = mod(ceil (hi / 2^k), 2^w)
// or // or
// div (mod(lo + 2^k -1, 2^w), 2^k) = div (mod(hi + 2^k - 1, 2^w), 2^k) // div (mod(lo + 2^k - 1, 2^w), 2^k) = div (mod(hi + 2^k - 1, 2^w), 2^k)
// but we also have lo != hi. // but we also have lo != hi.
// Assume lo < hi // Assume lo < hi
// - it means 2^k does not divide any of [lo, hi[ // - it means 2^k does not divide any of [lo, hi[
// so x*2^k cannot be in [lo, hi[ // so x*2^k cannot be in [lo, hi[
// Assume lo > hi // Assume lo > hi
// - then the constraint is x*2^k not in [lo, 0[, [0, hi[ // - then the constraint is x*2^k not in [lo, 0[, [0, hi[
// - then new_lo = new_hi = 0
// - it means 2^k does not divide any of [hi, lo[ // - it means 2^k does not divide any of [hi, lo[
// - therefore the interval [lo, hi[ contains all the divisors of 2^k // - therefore the interval [lo, hi[ contains all the divisors of 2^k
// //