diff options
Diffstat (limited to 'src/util/roundingmode.h')
-rw-r--r-- | src/util/roundingmode.h | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h new file mode 100644 index 000000000..181755a60 --- /dev/null +++ b/src/util/roundingmode.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file roundingmode.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The definition of rounding mode values. + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ +#include "cvc4_public.h" + +#ifndef CVC4__ROUNDINGMODE_H +#define CVC4__ROUNDINGMODE_H + +#include <fenv.h> + +namespace CVC4 { + +/** + * A concrete instance of the rounding mode sort + */ +enum CVC4_PUBLIC RoundingMode +{ + roundNearestTiesToEven = FE_TONEAREST, + roundTowardPositive = FE_UPWARD, + roundTowardNegative = FE_DOWNWARD, + 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 */ + +/** + * Hash function for rounding mode values. + */ +struct CVC4_PUBLIC RoundingModeHashFunction +{ + inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } +}; /* struct RoundingModeHashFunction */ + +} // namespace CVC4 + +#endif |