mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

remove deprecated API functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-14 17:05:15 -08:00
parent 0f602d652a
commit bea68cd194
6 changed files with 53 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
scripts/update_api.py
View file

@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }
log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
log_h.write('void _Z3_append_log(char const * msg);\n')
##
exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg_ex(ctx, c)); }\n')
exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
##
core_py.write('# Automatically generated file\n')
core_py.write('import sys, os\n')
@ -404,7 +404,7 @@ def mk_py_wrappers():
if len(params) > 0 and param_type(params[0]) == CONTEXT:
core_py.write(" err = lib().Z3_get_error_code(a0)\n")
core_py.write(" if err != Z3_OK:\n")
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n")
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg(a0, err))\n")
if result == STRING:
core_py.write(" return _to_pystr(r)\n")
elif result != VOID:
@ -477,7 +477,7 @@ def mk_dotnet_wrappers():
dotnet.write(" LIB.Z3_set_error_handler(a0, a1);\n")
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
dotnet.write(" }\n\n")
for name, result, params in _dotnet_decls:
if result == STRING:
@ -525,7 +525,7 @@ def mk_dotnet_wrappers():
if len(params) > 0 and param_type(params[0]) == CONTEXT:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
if result == STRING:
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
elif result != VOID:
@ -1276,7 +1276,7 @@ def mk_ml():
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n')
ml_native.write(' if err <> OK then\n')
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n')
ml_native.write(' raise (Exception (ML2C.n_get_error_msg a0 (int_of_error_code err)))\n')
ml_native.write(' else\n')
if result == VOID and len(op) == 0:
ml_native.write(' ()\n')

10
src/api/api_context.cpp
View file

@ -33,7 +33,7 @@ void install_tactics(tactic_manager & ctx);
namespace api {
static void default_error_handler(Z3_context ctx, Z3_error_code c) {
printf("Error: %s\n", Z3_get_error_msg_ex(ctx, c));
printf("Error: %s\n", Z3_get_error_msg(ctx, c));
exit(1);
}
@ -531,7 +531,7 @@ extern "C" {
SET_ERROR_CODE(e);
}
static char const * _get_error_msg_ex(Z3_context c, Z3_error_code err) {
static char const * _get_error_msg(Z3_context c, Z3_error_code err) {
switch(err) {
case Z3_OK: return "ok";
case Z3_SORT_ERROR: return "type error";
@ -551,9 +551,9 @@ extern "C" {
}
Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
LOG_Z3_get_error_msg_ex(c, err);
return _get_error_msg_ex(c, err);
Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) {
LOG_Z3_get_error_msg(c, err);
return _get_error_msg(c, err);
}

2
src/api/api_solver.cpp
View file

@ -391,7 +391,6 @@ extern "C" {
}
#if 0
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
Z3_solver s,
unsigned num_terms,
@ -407,6 +406,5 @@ extern "C" {
return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
#endif
};

35
src/api/z3_api.h
View file

@ -5323,9 +5323,9 @@ BEGIN_MLAPI_EXCLUDE
/**
\brief Return a string describing the given error code.
def_API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
*/
Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
END_MLAPI_EXCLUDE
#ifdef ML4only
#include <mlx_get_error_msg.idl>
@ -7216,6 +7216,37 @@ END_MLAPI_EXCLUDE
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
unsigned num_assumptions, Z3_ast const assumptions[]);
#ifdef CorML4
/**
\brief Retrieve congruence class representatives for terms.
The function can be used for relying on Z3 to identify equal terms under the current
set of assumptions. The array of terms and array of class identifiers should have
the same length. The class identifiers are numerals that are assigned to the same
value for their corresponding terms if the current context forces the terms to be
equal. You cannot deduce that terms corresponding to different numerals must be all different,
(especially when using non-convex theories).
All implied equalities are returned by this call.
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
The function return Z3_L_FALSE if the current assertions are not satisfiable.
def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*/
Z3_lbool Z3_API Z3_get_implied_equalities(
Z3_context c,
Z3_solver s,
unsigned num_terms,
Z3_ast const terms[],
unsigned class_ids[]
);
#endif
/**
\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions

13
src/muz/pdr/pdr_context.cpp
View file

@ -738,6 +738,7 @@ namespace pdr {
// model_node
void model_node::set_closed() {
TRACE("pdr", tout << state() << "\n";);
pt().close(state());
m_closed = true;
}
@ -1149,17 +1150,21 @@ namespace pdr {
ast_manager& m = n->pt().get_manager();
if (!n->get_model_ptr()) {
if (models.find(n->state(), md)) {
TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
TRACE("pdr", tout << n->state() << "\n";);
model_ref mr(md);
n->set_model(mr);
datalog::rule const* rule = rules.find(n->state());
n->set_rule(rule);
}
else {
TRACE("pdr", tout << "no model for " << n->state() << "\n";);
IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
verbose_stream() << mk_pp(n->state(), m) << "\n";);
verbose_stream() << n->state() << "\n";);
}
}
else {
TRACE("pdr", tout << n->state() << "\n";);
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
}
@ -2027,11 +2032,11 @@ namespace pdr {
switch (expand_state(n, cube, uses_level)) {
case l_true:
if (n.level() == 0) {
TRACE("pdr", tout << "reachable at level 0\n";);
TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
close_node(n);
}
else {
TRACE("pdr", tout << "node: " << &n << "\n";);
TRACE("pdr", n.display(tout, 0););
create_children(n);
}
break;

2
src/muz/pdr/pdr_context.h
View file

@ -240,7 +240,7 @@ namespace pdr {
void check_pre_closed();
void set_closed();
void set_open();
void set_pre_closed() { m_closed = true; }
void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; }
void reset() { m_children.reset(); }
void set_rule(datalog::rule const* r) { m_rule = r; }