summaryrefslogtreecommitdiff
path: root/src/theory/fp/fp_converter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/fp_converter.cpp')
-rw-r--r--src/theory/fp/fp_converter.cpp8
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 85482bf6d..858710746 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
}
FpConverter::FpConverter(context::UserContext* user)
- :
+ : d_additionalAssertions(user)
#ifdef CVC4_USE_SYMFPU
+ ,
d_fpMap(user),
d_rmMap(user),
d_boolMap(user),
d_ubvMap(user),
- d_sbvMap(user),
+ d_sbvMap(user)
#endif
- d_additionalAssertions(user)
{
}
+FpConverter::~FpConverter() {}
+
#ifdef CVC4_USE_SYMFPU
Node FpConverter::ufToNode(const fpt &format, const uf &u) const
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback