3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

remove solver_old

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-14 18:46:49 -08:00
parent cb85b60160
commit ab4033133f
4 changed files with 2 additions and 52 deletions

View file

@ -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));

View file

@ -6,7 +6,8 @@ Module Name:
api_solver.cpp
Abstract:
New solver API
Solver API
Author:

View file

@ -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<iostream>
#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);
}

View file

@ -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