From 4f453703f7baf85a16a822a48edc7c6cb95d5a64 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 1 Jan 2015 15:23:02 +0000
Subject: [PATCH] Added arguments of type float to the replayer.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/z3_replayer.cpp | 41 ++++++++++++++++++++++++++++++++++++++---
 src/api/z3_replayer.h   |  1 +
 2 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index acdb10bf6..676ba0c69 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -40,11 +40,12 @@ struct z3_replayer::imp {
     __int64                  m_int64;
     __uint64                 m_uint64;
     double                   m_double;
+    float                    m_float;
     size_t                   m_ptr;
     size_t_map<void *>       m_heap;
     svector<z3_replayer_cmd> m_cmds;
 
-    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY };
+    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
 
     struct value { 
         value_kind m_kind;
@@ -54,6 +55,7 @@ struct z3_replayer::imp {
             double       m_double;
             char const * m_str;
             void *       m_obj;
+            float        m_float;
         };
         value():m_kind(OBJECT), m_int(0) {}
         value(void * obj):m_kind(OBJECT), m_obj(obj) {}
@@ -61,6 +63,7 @@ struct z3_replayer::imp {
         value(value_kind k, __uint64 u):m_kind(k), m_uint(u) {}
         value(value_kind k, __int64 i):m_kind(k), m_int(i) {}
         value(value_kind k, double d):m_kind(k), m_double(d) {}
+        value(value_kind k, float f):m_kind(k), m_float(f) {}
     };
 
     svector<value>              m_args;
@@ -85,9 +88,12 @@ struct z3_replayer::imp {
         case UINT64:
             out << v.m_uint;
             break;
+        case FLOAT:
+            out << v.m_float;
+            break;
         case DOUBLE:
             out << v.m_double;
-            break;
+            break;        
         case STRING:
             out << v.m_str;
             break;
@@ -219,6 +225,19 @@ struct z3_replayer::imp {
         return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; 
     }
 
+    void read_float() {
+        m_string.reset();
+        while (is_double_char()) {
+            m_string.push_back(curr());
+            next();
+        }
+        if (m_string.empty())
+            throw z3_replayer_exception("invalid float");
+        m_string.push_back(0);
+        char * ptr;
+        m_float = strtof(m_string.begin(), &ptr);
+    }
+
     void read_double() {
         m_string.reset();
         while (is_double_char()) {
@@ -407,12 +426,18 @@ struct z3_replayer::imp {
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "U " << m_uint64 << "\n";);
                 m_args.push_back(value(UINT64, m_uint64));
                 break;
+            case 'F':
+                // push float
+                next(); skip_blank(); read_float();
+                TRACE("z3_replayer", tout << "[" << m_line << "] " << "F " << m_float << "\n";);
+                m_args.push_back(value(FLOAT, m_float));
+                break;
             case 'D':
                 // push double
                 next(); skip_blank(); read_double();
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";);
                 m_args.push_back(value(DOUBLE, m_double));
-                break;
+                break;            
             case 'p':
             case 's':
             case 'u':
@@ -516,6 +541,12 @@ struct z3_replayer::imp {
         return m_args[pos].m_uint;
     }
 
+    float get_float(unsigned pos) const {
+        if (pos >= m_args.size() || m_args[pos].m_kind != FLOAT)
+            throw_invalid_reference();
+        return m_args[pos].m_float;
+    }
+
     double get_double(unsigned pos) const {
         if (pos >= m_args.size() || m_args[pos].m_kind != DOUBLE)
             throw_invalid_reference();
@@ -653,6 +684,10 @@ __uint64 z3_replayer::get_uint64(unsigned pos) const {
     return m_imp->get_uint64(pos);
 }
 
+float z3_replayer::get_float(unsigned pos) const {
+    return m_imp->get_float(pos);
+}
+
 double z3_replayer::get_double(unsigned pos) const {
     return m_imp->get_double(pos);
 }
diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h
index 6de4bdb39..6320068ad 100644
--- a/src/api/z3_replayer.h
+++ b/src/api/z3_replayer.h
@@ -42,6 +42,7 @@ public:
     unsigned get_uint(unsigned pos) const;
     __int64 get_int64(unsigned pos) const;
     __uint64 get_uint64(unsigned pos) const;
+    float get_float(unsigned pos) const;
     double get_double(unsigned pos) const;
     bool get_bool(unsigned pos) const;
     Z3_string get_str(unsigned pos) const;