From 1f872e720d99b37d0775098382b17928f8160ffc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Jan 2016 15:19:00 +0000 Subject: [PATCH 1/2] remove m_replay_stack from API context since it's never used Signed-off-by: Nuno Lopes --- src/api/api_context.cpp | 12 ------------ src/api/api_context.h | 1 - 2 files changed, 13 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 75782a28d..47a25f313 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -76,7 +76,6 @@ namespace api { m_sutil(m()), m_last_result(m()), m_ast_trail(m()), - m_replay_stack(), m_pmanager(m_limit) { m_error_code = Z3_OK; @@ -100,23 +99,12 @@ namespace api { m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); - - if (!m_user_ref_count) { - m_replay_stack.push_back(0); - } install_tactics(*this); } context::~context() { - m_last_obj = 0; - if (!m_user_ref_count) { - for (unsigned i = 0; i < m_replay_stack.size(); ++i) { - dealloc(m_replay_stack[i]); - } - m_ast_trail.reset(); - } reset_parser(); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 23c8d3fd2..de492bb45 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -68,7 +68,6 @@ namespace api { ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false unsigned_vector m_ast_lim; - ptr_vector m_replay_stack; ref m_last_obj; //!< reference to the last API object returned by the APIs From 23cc8258fe2ade1bd56f9a7a12d5456cc999d07d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Jan 2016 15:37:58 +0000 Subject: [PATCH 2/2] remove m_ast_lim from API context since that one isn't used either Signed-off-by: Nuno Lopes --- src/api/api_context.h | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/api/api_context.h b/src/api/api_context.h index de492bb45..fa6754120 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,7 +58,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; - datatype_util m_dtutil; + datatype_util m_dtutil; seq_util m_sutil; // Support for old solver API @@ -67,7 +67,6 @@ namespace api { ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false - unsigned_vector m_ast_lim; ref m_last_obj; //!< reference to the last API object returned by the APIs @@ -122,7 +121,7 @@ namespace api { bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } - datatype_util& dtutil() { return m_dtutil; } + datatype_util& dtutil() { return m_dtutil; } seq_util& sutil() { return m_sutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } @@ -180,8 +179,6 @@ namespace api { void interrupt(); void invoke_error_handler(Z3_error_code c); - - static void out_of_memory_handler(void * _ctx); void check_sorts(ast * n);