diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-09 15:48:58 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-09 15:48:58 -0500 |
commit | 803106ed9b27337b564ba2d2fa860164e1cbdc69 (patch) | |
tree | 349a862c2cc9e44237c42f67f7ba3faac3bbbc57 /src/Reflection/Z | |
parent | 2ce7543ec71225d31f4742c8d36a1781fa218232 (diff) |
Switch to accurate bounds for lor
When the arguments are, e.g., 2^k - 2 and 2^(k-1)-1, the upper bound is 2^k - 1, not 2^(k-1)-1.
Thanks, Rob
Diffstat (limited to 'src/Reflection/Z')
-rw-r--r-- | src/Reflection/Z/Interpretations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 0da74da09..cfdd8bd08 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -351,7 +351,7 @@ Module ZBounds. Definition lor' : bounds -> bounds -> bounds := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.max lx ly; - upper := 2^(Z.max (Z.log2 (ux+1)) (Z.log2 (uy+1))) - 1 |}. + upper := 2^(Z.max (Z.log2_up (ux+1)) (Z.log2_up (uy+1))) - 1 |}. Definition lor : t -> t -> t := t_map2 lor'. Definition neg' : bounds -> bounds -> bounds := fun int_width v |