mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-08 15:27:46 +00:00
parent e0066df6a9
commit e22a67c12c
1 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/api/z3_replayer.cpp
View file

@ -14,7 +14,7 @@ Author:
Leonardo de Moura (leonardo) 2011-09-22 Leonardo de Moura (leonardo) 2011-09-22
Notes: Notes:
--*/ --*/
#include"vector.h" #include"vector.h"
#include"map.h" #include"map.h"
@ -76,13 +76,13 @@ struct z3_replayer::imp {
} }
if (m_args[pos].m_kind != k) { if (m_args[pos].m_kind != k) {
std::stringstream strm; std::stringstream strm;
strm << "expecting " << kind2string(k) << " at position " strm << "expecting " << kind2string(k) << " at position "
<< pos << " but got " << kind2string(m_args[pos].m_kind); << pos << " but got " << kind2string(m_args[pos].m_kind);
throw z3_replayer_exception(strm.str().c_str()); throw z3_replayer_exception(strm.str().c_str());
} }
} }
struct value { struct value {
value_kind m_kind; value_kind m_kind;
union { union {
__int64 m_int; __int64 m_int;
@ -129,7 +129,7 @@ struct z3_replayer::imp {
break; break;
case DOUBLE: case DOUBLE:
out << v.m_double; out << v.m_double;
break; break;
case STRING: case STRING:
out << v.m_str; out << v.m_str;
break; break;
@ -160,7 +160,7 @@ struct z3_replayer::imp {
char curr() const { return m_curr; } char curr() const { return m_curr; }
void new_line() { m_line++; } void new_line() { m_line++; }
void next() { m_curr = m_stream.get(); } void next() { m_curr = m_stream.get(); }
void read_string_core(char delimiter) { void read_string_core(char delimiter) {
if (curr() != delimiter) if (curr() != delimiter)
throw z3_replayer_exception("invalid string/symbol"); throw z3_replayer_exception("invalid string/symbol");
@ -258,7 +258,7 @@ struct z3_replayer::imp {
} }
bool is_double_char() const { bool is_double_char() const {
return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E';
} }
#if (!defined(strtof)) #if (!defined(strtof))
@ -376,7 +376,7 @@ struct z3_replayer::imp {
} }
} }
else if (k == OBJECT) { else if (k == OBJECT) {
TRACE("z3_replayer_bug", TRACE("z3_replayer_bug",
tout << "args: "; display_args(tout); tout << "\n"; tout << "args: "; display_args(tout); tout << "\n";
tout << "push_back, sz: " << sz << ", m_obj_arrays.size(): " << m_obj_arrays.size() << "\n"; tout << "push_back, sz: " << sz << ", m_obj_arrays.size(): " << m_obj_arrays.size() << "\n";
for (unsigned i = asz - sz; i < asz; i++) { for (unsigned i = asz - sz; i < asz; i++) {
@ -421,7 +421,7 @@ struct z3_replayer::imp {
break; break;
case 'R': case 'R':
// reset // reset
next(); next();
TRACE("z3_replayer", tout << "[" << m_line << "] " << "R\n";); TRACE("z3_replayer", tout << "[" << m_line << "] " << "R\n";);
reset(); reset();
break; break;
@ -432,7 +432,7 @@ struct z3_replayer::imp {
if (m_ptr == 0) { if (m_ptr == 0) {
m_args.push_back(0); m_args.push_back(0);
} }
else { else {
void * obj = 0; void * obj = 0;
if (!m_heap.find(m_ptr, obj)) if (!m_heap.find(m_ptr, obj))
throw z3_replayer_exception("invalid pointer"); throw z3_replayer_exception("invalid pointer");
@ -493,7 +493,7 @@ struct z3_replayer::imp {
next(); skip_blank(); read_double(); next(); skip_blank(); read_double();
TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";); TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";);
m_args.push_back(value(DOUBLE, m_double)); m_args.push_back(value(DOUBLE, m_double));
break; break;
case 'p': case 'p':
case 's': case 's':
case 'u': case 'u':
@ -696,15 +696,15 @@ struct z3_replayer::imp {
m_unsigned_arrays.reset(); m_unsigned_arrays.reset();
m_int_arrays.reset(); m_int_arrays.reset();
} }
}; };
z3_replayer::z3_replayer(std::istream & in) { z3_replayer::z3_replayer(std::istream & in) {
m_imp = alloc(imp, *this, in); m_imp = alloc(imp, *this, in);
register_z3_replayer_cmds(*this); register_z3_replayer_cmds(*this);
} }
z3_replayer::~z3_replayer() { z3_replayer::~z3_replayer() {
dealloc(m_imp); dealloc(m_imp);
} }