1 files changed, 34 insertions, 0 deletions
diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp
new file mode 100644
index 000000000..e068eb69a
--- /dev/null
+++ b/src/util/floatingpoint_size.cpp
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file floatingpoint_size.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Martin Brain
+ ** 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 class representing a floating-point format.
+ **/
+#include "util/floatingpoint_size.h"
+
+#include "base/check.h"
+
+namespace CVC4 {
+
+FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size)
+    : d_exp_size(exp_size), d_sig_size(sig_size)
+{
+  Assert(validExponentSize(exp_size));
+  Assert(validSignificandSize(sig_size));
+}
+
+FloatingPointSize::FloatingPointSize(const FloatingPointSize& old)
+    : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size)
+{
+  Assert(validExponentSize(d_exp_size));
+  Assert(validSignificandSize(d_sig_size));
+}
+
+}  // namespace CVC4