diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c1f982997..8451c00c5 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -209,22 +209,6 @@ namespace api { } } } -#if 0 - void context::persist_ast(ast * n, unsigned num_scopes) { - // persist_ast is irrelevant when m_user_ref_count == true - if (m_user_ref_count) - return; - if (num_scopes > m_ast_lim.size()) { - num_scopes = m_ast_lim.size(); - } - SASSERT(m_replay_stack.size() > num_scopes); - unsigned j = m_replay_stack.size() - num_scopes - 1; - if (!m_replay_stack[j]) { - m_replay_stack[j] = alloc(ast_ref_vector, m()); - } - m_replay_stack[j]->push_back(n); - } -#endif void context::save_ast_trail(ast * n) { SASSERT(m().contains(n)); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6112a8cd2..b568f3613 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -6,7 +6,8 @@ Module Name: api_solver.cpp Abstract: - New solver API + + Solver API Author: diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp deleted file mode 100644 index b4911698c..000000000 --- a/src/api/api_solver_old.cpp +++ /dev/null @@ -1,33 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_solver_old.cpp - -Abstract: - OLD API for using solvers. - - This has been deprecated - -Author: - - Leonardo de Moura (leonardo) 2012-02-29. - -Revision History: - ---*/ -#include -#include"z3.h" -#include"api_log_macros.h" -#include"api_context.h" - - -void Z3_display_statistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_smt_kernel().display_statistics(s); -} - -void Z3_display_istatistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_smt_kernel().display_istatistics(s); -} - diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 4492a4c0f..cc72aaa4c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1552,8 +1552,6 @@ extern "C" { \conly \sa Z3_del_context - \conly \deprecated Use #Z3_mk_context_rc - def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) */ #ifdef CorML3