From 9c6dc5d2306ac6831477f2dc1261ae39741527f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Dec 2013 19:46:45 -0800
Subject: [PATCH] feat(util/serializer): add hackish write_double/read_double

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/serializer.cpp | 23 +++++++++++++++++++++++
 src/util/serializer.cpp       | 24 ++++++++++++++++++++++++
 src/util/serializer.h         |  4 ++++
 3 files changed, 51 insertions(+)

diff --git a/src/tests/util/serializer.cpp b/src/tests/util/serializer.cpp
index ffe169623..47732bc06 100644
--- a/src/tests/util/serializer.cpp
+++ b/src/tests/util/serializer.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <cstring>
 #include <vector>
 #include <functional>
+#include <cmath>
 #include "util/test.h"
 #include "util/object_serializer.h"
 #include "util/debug.h"
@@ -148,9 +149,31 @@ static void tst3() {
     lean_assert(n5 == m6);
 }
 
+static void tst4() {
+    std::ostringstream out;
+    serializer s(out);
+    double d1, d2, d3, d4, d5;
+    d1 = 0.1;
+    d2 = -0.3;
+    d3 = 0.0;
+    d4 = 12317.123;
+    d5 = std::atan(1.0)*4;
+    s << d1 << d2 << d3 << d4 << d5;
+    std::istringstream in(out.str());
+    deserializer d(in);
+    double o1, o2, o3, o4, o5;
+    d >> o1 >> o2 >> o3 >> o4 >> o5;
+    lean_assert_eq(d1, o1);
+    lean_assert_eq(d2, o2);
+    lean_assert_eq(d3, o3);
+    lean_assert_eq(d4, o4);
+    lean_assert_eq(d5, o5);
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/serializer.cpp b/src/util/serializer.cpp
index 657ff6e64..c914ba0f0 100644
--- a/src/util/serializer.cpp
+++ b/src/util/serializer.cpp
@@ -5,6 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include <limits>
+#include <stdio.h>
+#include <ios>
 #include "util/serializer.h"
 
 namespace lean {
@@ -21,6 +24,19 @@ void serializer_core::write_int(int i) {
     write_unsigned(i);
 }
 
+#define BIG_BUFFER 1024
+
+void serializer_core::write_double(double d) {
+    std::ostringstream out;
+    // TODO(Leo): the following code may miss precision.
+    // We should use std::ios::hexfloat, but it is not supported by
+    // g++ yet.
+    out.flags (std::ios::scientific);
+    out.precision(std::numeric_limits<double>::digits10 + 1);
+    out << std::hex << d;
+    write_string(out.str());
+}
+
 std::string deserializer_core::read_string() {
     std::string r;
     while (true) {
@@ -45,4 +61,12 @@ unsigned deserializer_core::read_unsigned() {
 int deserializer_core::read_int() {
     return read_unsigned();
 }
+
+double deserializer_core::read_double() {
+    // TODO(Leo): use std::hexfloat as soon as it is supported by g++
+    std::istringstream in(read_string());
+    double r;
+    in >> r;
+    return r;
+}
 }
diff --git a/src/util/serializer.h b/src/util/serializer.h
index 25107cd63..8e4e48559 100644
--- a/src/util/serializer.h
+++ b/src/util/serializer.h
@@ -26,6 +26,7 @@ public:
     void write_int(int i);
     void write_char(char c) { m_out.put(c); }
     void write_bool(bool b) { m_out.put(b ? 1 : 0); }
+    void write_double(double b);
 };
 
 typedef extensible_object<serializer_core> serializer;
@@ -36,6 +37,7 @@ inline serializer & operator<<(serializer & s, unsigned i) { s.write_unsigned(i)
 inline serializer & operator<<(serializer & s, int i) { s.write_int(i); return s; }
 inline serializer & operator<<(serializer & s, char c) { s.write_char(c); return s; }
 inline serializer & operator<<(serializer & s, bool b) { s.write_bool(b); return s; }
+inline serializer & operator<<(serializer & s, double b) { s.write_double(b); return s; }
 
 /**
    \brief Low-tech serializer.
@@ -50,6 +52,7 @@ public:
     int read_int();
     char read_char() { return m_in.get(); }
     bool read_bool() { return m_in.get() != 0; }
+    double read_double();
 };
 
 typedef extensible_object<deserializer_core> deserializer;
@@ -59,4 +62,5 @@ inline deserializer & operator>>(deserializer & d, unsigned & i) { i = d.read_un
 inline deserializer & operator>>(deserializer & d, int & i) { i = d.read_int(); return d; }
 inline deserializer & operator>>(deserializer & d, char & c) { c = d.read_char(); return d; }
 inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; }
+inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; }
 }