mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

interval

Browse source
This commit is contained in:
Jakob Rath 2023-12-21 14:34:42 +01:00
parent 8e84aac36c
commit 93dd0b6054
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/interval.h
View file

@ -71,6 +71,7 @@ namespace polysat {
SASSERT(mod_value.is_power_of_two()); SASSERT(mod_value.is_power_of_two());
SASSERT(0 <= a && a < mod_value); SASSERT(0 <= a && a < mod_value);
SASSERT(0 <= b && b <= mod_value); SASSERT(0 <= b && b <= mod_value);
SASSERT(b != mod_value || a == 0); // b == mod_value only allowed when a == 0
rational x = b - a; rational x = b - a;
if (x.is_neg()) if (x.is_neg())
x += mod_value; x += mod_value;
@ -113,10 +114,7 @@ namespace polysat {
SASSERT(0 <= lo && lo < mod_value); SASSERT(0 <= lo && lo < mod_value);
SASSERT(0 <= hi && hi <= mod_value); SASSERT(0 <= hi && hi <= mod_value);
SASSERT(hi != mod_value || lo == 0); // hi == mod_value only allowed when lo == 0 SASSERT(hi != mod_value || lo == 0); // hi == mod_value only allowed when lo == 0
rational len = hi - lo; return distance(lo, hi, mod_value);
if (len.is_neg())
len += mod_value;
return len;
} }
rational len(rational const& mod_value) const { rational len(rational const& mod_value) const {