mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

inline api_context::reset_error_code()

Browse source
This commit is contained in:
Nuno Lopes 2020-06-29 19:14:17 +01:00
parent aec8000bda
commit 64f1a759a7
2 changed files with 2 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_context.cpp
View file

@ -147,10 +147,6 @@ namespace api {
} }
} }
void context::reset_error_code() {
m_error_code = Z3_OK;
}
void context::check_searching() { void context::check_searching() {
if (m_searching) { if (m_searching) {
set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed.

8
src/api/api_context.h
View file

@ -17,9 +17,7 @@ Author:
Revision History: Revision History:
--*/ --*/
#ifndef API_CONTEXT_H_ #pragma once
#define API_CONTEXT_H_
#include "util/hashtable.h" #include "util/hashtable.h"
#include "util/mutex.h" #include "util/mutex.h"
@ -170,7 +168,7 @@ namespace api {
family_id get_special_relations_fid() const { return m_special_relations_fid; } family_id get_special_relations_fid() const { return m_special_relations_fid; }
Z3_error_code get_error_code() const { return m_error_code; } Z3_error_code get_error_code() const { return m_error_code; }
void reset_error_code(); void reset_error_code() { m_error_code = Z3_OK; }
void set_error_code(Z3_error_code err, char const* opt_msg); void set_error_code(Z3_error_code err, char const* opt_msg);
void set_error_handler(Z3_error_handler h) { m_error_handler = h; } void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
// Sign an error if solver is searching // Sign an error if solver is searching
@ -268,5 +266,3 @@ inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } } #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }
#endif