4 files changed, 63 insertions, 6 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 5fd0003bf..2938ddcca 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -58,6 +58,7 @@ libcvc5_add_sources(
   result.h
   regexp.cpp
   regexp.h
+  roundingmode.cpp
   roundingmode.h
   safe_print.cpp
   safe_print.h
diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp
index 45fd4272f..071b69912 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.cpp
+++ b/src/util/floatingpoint_literal_symfpu_traits.cpp
@@ -382,11 +382,17 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
 template class wrappedBitVector<true>;
 template class wrappedBitVector<false>;
 
-traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; };
-traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; };
-traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; };
-traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; };
-traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; };
+traits::rm traits::RNE(void)
+{
+  return RoundingMode::ROUND_NEAREST_TIES_TO_EVEN;
+};
+traits::rm traits::RNA(void)
+{
+  return RoundingMode::ROUND_NEAREST_TIES_TO_AWAY;
+};
+traits::rm traits::RTP(void) { return RoundingMode::ROUND_TOWARD_POSITIVE; };
+traits::rm traits::RTN(void) { return RoundingMode::ROUND_TOWARD_NEGATIVE; };
+traits::rm traits::RTZ(void) { return RoundingMode::ROUND_TOWARD_ZERO; };
 // This is a literal back-end so props are actually bools
 // so these can be handled in the same way as the internal assertions above
 
diff --git a/src/util/roundingmode.cpp b/src/util/roundingmode.cpp
new file mode 100644
index 000000000..00aec6635
--- /dev/null
+++ b/src/util/roundingmode.cpp
@@ -0,0 +1,46 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * The definition of rounding mode values.
+ */
+
+#include "roundingmode.h"
+
+#include <iostream>
+
+#include "base/check.h"
+
+namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& os, RoundingMode rm)
+{
+  switch (rm)
+  {
+    case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
+      os << "ROUND_NEAREST_TIES_TO_EVEN";
+      break;
+    case RoundingMode::ROUND_TOWARD_POSITIVE:
+      os << "ROUND_TOWARD_POSITIVE";
+      break;
+    case RoundingMode::ROUND_TOWARD_NEGATIVE:
+      os << "ROUND_TOWARD_NEGATIVE";
+      break;
+    case RoundingMode::ROUND_TOWARD_ZERO: os << "ROUND_TOWARD_ZERO"; break;
+    case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
+      os << "ROUND_NEAREST_TIES_TO_AWAY";
+      break;
+    default: Unreachable();
+  }
+  return os;
+}
+
+}  // namespace cvc5
diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h
index 06b2b54cd..f4edbd00b 100644
--- a/src/util/roundingmode.h
+++ b/src/util/roundingmode.h
@@ -19,6 +19,8 @@
 
 #include <fenv.h>
 
+#include <iosfwd>
+
 namespace cvc5 {
 
 #define CVC5_NUM_ROUNDING_MODES 5
@@ -26,7 +28,7 @@ namespace cvc5 {
 /**
  * A concrete instance of the rounding mode sort
  */
-enum RoundingMode
+enum class RoundingMode
 {
   ROUND_NEAREST_TIES_TO_EVEN = FE_TONEAREST,
   ROUND_TOWARD_POSITIVE = FE_UPWARD,
@@ -46,6 +48,8 @@ struct RoundingModeHashFunction
   inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
 }; /* struct RoundingModeHashFunction */
 
+std::ostream& operator<<(std::ostream& os, RoundingMode s);
+
 }  // namespace cvc5
 
 #endif