From 3701666042df79b72a1476346afe40ed2c32aac6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 27 Jun 2018 13:58:05 -0400 Subject: Remove lneg in favor of lnot_modulo (lneg was wrong) --- src/Util/ZUtil/Definitions.v | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'src/Util/ZUtil') 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. -- cgit v1.2.3