mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

move to std::vector in replayer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-16 10:08:29 -07:00
parent d383fd851a
commit 1c8e0918d8
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/z3_replayer.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include"symbol.h" #include"symbol.h"
#include"trace.h" #include"trace.h"
#include<sstream> #include<sstream>
#include<vector>
void register_z3_replayer_cmds(z3_replayer & in); void register_z3_replayer_cmds(z3_replayer & in);
@ -46,7 +47,7 @@ struct z3_replayer::imp {
size_t m_ptr; size_t m_ptr;
size_t_map<void *> m_heap; size_t_map<void *> m_heap;
svector<z3_replayer_cmd> m_cmds; svector<z3_replayer_cmd> m_cmds;
vector<std::string> m_cmds_names; std::vector<std::string> m_cmds_names;
enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT }; enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
@ -676,7 +677,9 @@ struct z3_replayer::imp {
void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) { void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
m_cmds.reserve(id+1, 0); m_cmds.reserve(id+1, 0);
m_cmds_names.reserve(id+1, ""); while (static_cast<unsigned>(m_cmds_names.size()) <= id+1) {
m_cmds_names.push_back("");
}
m_cmds[id] = cmd; m_cmds[id] = cmd;
m_cmds_names[id] = name; m_cmds_names[id] = name;
} }