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

Fixes #564: use std::vector on std::strings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-16 09:26:13 -07:00
parent 0f93853a4c
commit 4ebf392da7
2 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/cmd_context.cpp
View file

@ -1322,7 +1322,7 @@ void cmd_context::restore_func_decls(unsigned old_sz) {
sf_pair const & p = *it; sf_pair const & p = *it;
erase_func_decl_core(p.first, p.second); erase_func_decl_core(p.first, p.second);
} }
m_func_decls_stack.shrink(old_sz); m_func_decls_stack.resize(old_sz);
} }
void cmd_context::restore_psort_decls(unsigned old_sz) { void cmd_context::restore_psort_decls(unsigned old_sz) {
@ -1389,7 +1389,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
if (produce_unsat_cores()) if (produce_unsat_cores())
restore(m(), m_assertion_names, old_sz); restore(m(), m_assertion_names, old_sz);
if (m_interactive_mode) if (m_interactive_mode)
m_assertion_strings.shrink(old_sz); m_assertion_strings.resize(old_sz);
} }
void cmd_context::pop(unsigned n) { void cmd_context::pop(unsigned n) {
@ -1724,8 +1724,8 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
void cmd_context::display_assertions() { void cmd_context::display_assertions() {
if (!m_interactive_mode) if (!m_interactive_mode)
throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)"); throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
vector<std::string>::const_iterator it = m_assertion_strings.begin(); std::vector<std::string>::const_iterator it = m_assertion_strings.begin();
vector<std::string>::const_iterator end = m_assertion_strings.end(); std::vector<std::string>::const_iterator end = m_assertion_strings.end();
regular_stream() << "("; regular_stream() << "(";
for (bool first = true; it != end; ++it) { for (bool first = true; it != end; ++it) {
std::string const & s = *it; std::string const & s = *it;

4
src/cmd_context/cmd_context.h
View file

@ -22,6 +22,7 @@ Notes:
#define CMD_CONTEXT_H_ #define CMD_CONTEXT_H_
#include<sstream> #include<sstream>
#include<vector>
#include"ast.h" #include"ast.h"
#include"ast_printer.h" #include"ast_printer.h"
#include"pdecl.h" #include"pdecl.h"
@ -38,6 +39,7 @@ Notes:
#include"scoped_ptr_vector.h" #include"scoped_ptr_vector.h"
#include"context_params.h" #include"context_params.h"
class func_decls { class func_decls {
func_decl * m_decls; func_decl * m_decls;
public: public:
@ -189,7 +191,7 @@ protected:
// //
ptr_vector<pdecl> m_aux_pdecls; ptr_vector<pdecl> m_aux_pdecls;
ptr_vector<expr> m_assertions; ptr_vector<expr> m_assertions;
vector<std::string> m_assertion_strings; std::vector<std::string> m_assertion_strings;
ptr_vector<expr> m_assertion_names; // named assertions are represented using boolean variables. ptr_vector<expr> m_assertion_names; // named assertions are represented using boolean variables.
struct scope { struct scope {