diff options
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index 82b065394..af2d8239e 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -13,6 +13,14 @@ Module Z. Definition add_modulo x y modulus := if (modulus <=? x + y) then (x + y) - modulus else (x + y). + (** Logical negation, modulo a number *) + Definition lnot_modulo (v : Z) (modulus : Z) : Z + := Z.lnot v mod modulus. + + (** Boolean negation *) + Definition bneg (v : Z) : Z + := if dec (v = 0) then 1 else 0. + (* most significant bit *) Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2). @@ -76,16 +84,4 @@ Module Z. := if s =? 2^Z.log2 s then mul_split_at_bitwidth (Z.log2 s) x y else ((x * y) mod s, (x * y) / s). - - (** Boolean negation *) - Definition bneg (v : Z) : Z - := if dec (v = 0) then 1 else 0. - - (** Logical negation, modulo a bitwidth *) - Definition lneg (bitwidth : Z) (v : Z) : Z - := (-v) mod 2^bitwidth. - Definition lneg_full (s : Z) (v : Z) : Z - := if s =? 2^Z.log2 s - then lneg (Z.log2 s) v - else (-v) mod s. End Z. |