From 7e750757ac9832b70b5c6ca1d15e17cddbd2e6c0 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 13 Oct 2016 11:30:17 -0700 Subject: [PATCH] Initializes RoundingMode::roundNearestTiesToAway to a distinct value. --- src/util/floatingpoint.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 7b18d542a..af909dfa4 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -80,10 +80,12 @@ namespace CVC4 { */ enum CVC4_PUBLIC RoundingMode { roundNearestTiesToEven = FE_TONEAREST, - roundNearestTiesToAway, roundTowardPositive = FE_UPWARD, roundTowardNegative = FE_DOWNWARD, - roundTowardZero = FE_TOWARDZERO + roundTowardZero = FE_TOWARDZERO, + // Initializes this to the diagonalization of the 4 other values. + roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) | + ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) }; /* enum RoundingMode */ struct CVC4_PUBLIC RoundingModeHashFunction { -- 2.30.2