mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Added arguments of type float to the replayer.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-01 15:23:02 +00:00
parent 7d61223a3a
commit 4f453703f7
2 changed files with 39 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/api/z3_replayer.cpp
View file

@ -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);
}

1
src/api/z3_replayer.h
View file

@ -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;