mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

allow disabling exceptions from C++. Issue #861

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-04 19:04:43 -08:00
parent 74d3de01b3
commit ddf4bc548f
1 changed files with 26 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/api/c++/z3++.h
View file

@ -132,16 +132,19 @@ namespace z3 {
\brief A Context manages all other Z3 objects, global configuration options, etc. \brief A Context manages all other Z3 objects, global configuration options, etc.
*/ */
class context { class context {
bool m_enable_exceptions;
Z3_context m_ctx; Z3_context m_ctx;
static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
void init(config & c) { void init(config & c) {
m_ctx = Z3_mk_context_rc(c); m_ctx = Z3_mk_context_rc(c);
m_enable_exceptions = true;
Z3_set_error_handler(m_ctx, error_handler); Z3_set_error_handler(m_ctx, error_handler);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT); Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
} }
void init_interp(config & c) { void init_interp(config & c) {
m_ctx = Z3_mk_interpolation_context(c); m_ctx = Z3_mk_interpolation_context(c);
m_enable_exceptions = true;
Z3_set_error_handler(m_ctx, error_handler); Z3_set_error_handler(m_ctx, error_handler);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT); Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
} }
@ -159,12 +162,24 @@ namespace z3 {
/** /**
\brief Auxiliary method used to check for API usage errors. \brief Auxiliary method used to check for API usage errors.
*/ */
void check_error() const { Z3_error_code check_error() const {
Z3_error_code e = Z3_get_error_code(m_ctx); Z3_error_code e = Z3_get_error_code(m_ctx);
if (e != Z3_OK) if (e != Z3_OK && enable_exceptions())
throw exception(Z3_get_error_msg(m_ctx, e)); throw exception(Z3_get_error_msg(m_ctx, e));
return e;
} }
/**
\brief The C++ API uses by defaults exceptions on errors.
For applications that don't work well with exceptions (there should be only few)
you have the ability to turn off exceptions. The tradeoffs are that applications
have to very careful about using check_error() after calls that may result in an errornous
state.
*/
void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
bool enable_exceptions() const { return m_enable_exceptions; }
/** /**
\brief Update global parameter \c param with string \c value. \brief Update global parameter \c param with string \c value.
*/ */
@ -676,8 +691,8 @@ namespace z3 {
\pre is_numeral() \pre is_numeral()
*/ */
int get_numeral_int() const { int get_numeral_int() const {
int result; int result = 0;
if (!is_numeral_i(result)) { if (!is_numeral_i(result) && ctx().enable_exceptions()) {
throw exception("numeral does not fit in machine int"); throw exception("numeral does not fit in machine int");
} }
return result; return result;
@ -691,8 +706,8 @@ namespace z3 {
*/ */
unsigned get_numeral_uint() const { unsigned get_numeral_uint() const {
assert(is_numeral()); assert(is_numeral());
unsigned result; unsigned result = 0;
if (!is_numeral_u(result)) { if (!is_numeral_u(result) && ctx().enable_exceptions()) {
throw exception("numeral does not fit in machine uint"); throw exception("numeral does not fit in machine uint");
} }
return result; return result;
@ -706,8 +721,8 @@ namespace z3 {
*/ */
__int64 get_numeral_int64() const { __int64 get_numeral_int64() const {
assert(is_numeral()); assert(is_numeral());
__int64 result; __int64 result = 0;
if (!is_numeral_i64(result)) { if (!is_numeral_i64(result) && ctx().enable_exceptions()) {
throw exception("numeral does not fit in machine __int64"); throw exception("numeral does not fit in machine __int64");
} }
return result; return result;
@ -721,8 +736,8 @@ namespace z3 {
*/ */
__uint64 get_numeral_uint64() const { __uint64 get_numeral_uint64() const {
assert(is_numeral()); assert(is_numeral());
__uint64 result; __uint64 result = 0;
if (!is_numeral_u64(result)) { if (!is_numeral_u64(result) && ctx().enable_exceptions()) {
throw exception("numeral does not fit in machine __uint64"); throw exception("numeral does not fit in machine __uint64");
} }
return result; return result;
@ -1615,7 +1630,7 @@ namespace z3 {
Z3_ast r = 0; Z3_ast r = 0;
Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
check_error(); check_error();
if (status == Z3_FALSE) if (status == Z3_FALSE && ctx().enable_exceptions())
throw exception("failed to evaluate expression"); throw exception("failed to evaluate expression");
return expr(ctx(), r); return expr(ctx(), r);
} }