mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove api_context::m_search as it's always constant (false)
This commit is contained in:
parent
853ce099ec
commit
afdf80509a
|
@ -86,7 +86,6 @@ namespace api {
|
|||
|
||||
m_error_code = Z3_OK;
|
||||
m_print_mode = Z3_PRINT_SMTLIB_FULL;
|
||||
m_searching = false;
|
||||
|
||||
|
||||
m_interruptable = nullptr;
|
||||
|
@ -156,12 +155,6 @@ namespace api {
|
|||
}
|
||||
}
|
||||
|
||||
void context::check_searching() {
|
||||
if (m_searching) {
|
||||
set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed.
|
||||
}
|
||||
}
|
||||
|
||||
char * context::mk_external_string(char const * str) {
|
||||
m_string_buffer = str?str:"";
|
||||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
|
|
|
@ -114,7 +114,6 @@ namespace api {
|
|||
Z3_error_code m_error_code;
|
||||
Z3_error_handler * m_error_handler;
|
||||
std::string m_exception_msg; // catch the message associated with a Z3 exception
|
||||
bool m_searching;
|
||||
Z3_ast_print_mode m_print_mode;
|
||||
|
||||
event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
|
||||
|
@ -170,8 +169,6 @@ namespace api {
|
|||
void set_error_code(Z3_error_code err, char const* opt_msg);
|
||||
void set_error_code(Z3_error_code err, std::string &&opt_msg);
|
||||
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
|
||||
// Sign an error if solver is searching
|
||||
void check_searching();
|
||||
|
||||
unsigned add_object(api::object* o);
|
||||
void del_object(api::object* o);
|
||||
|
@ -259,7 +256,6 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*
|
|||
#define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
|
||||
#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
|
||||
#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
|
||||
#define CHECK_SEARCHING(c) mk_c(c)->check_searching();
|
||||
inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
|
||||
#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
|
||||
inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
|
||||
|
|
|
@ -736,7 +736,6 @@ extern "C" {
|
|||
LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
init_solver(c, s);
|
||||
lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(num_terms, terms), class_ids);
|
||||
return static_cast<Z3_lbool>(result);
|
||||
|
@ -752,7 +751,6 @@ extern "C" {
|
|||
LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences);
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
init_solver(c, s);
|
||||
expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
|
||||
ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
|
||||
|
|
Loading…
Reference in a new issue