From 1eb8ccad59b8ea2c12b1ec8e7e712c7891b252d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Jul 2018 16:04:37 -0700 Subject: [PATCH] overhaul of error messages. Add warning in dimacs conversion Signed-off-by: Nikolaj Bjorner --- src/api/api_algebraic.cpp | 16 ++-- src/api/api_arith.cpp | 12 +-- src/api/api_array.cpp | 14 ++-- src/api/api_ast.cpp | 54 +++++++------- src/api/api_ast_map.cpp | 2 +- src/api/api_ast_vector.cpp | 7 +- src/api/api_bv.cpp | 7 +- src/api/api_context.cpp | 31 ++++---- src/api/api_context.h | 20 ++--- src/api/api_datalog.cpp | 12 +-- src/api/api_datatype.cpp | 44 +++++------ src/api/api_fpa.cpp | 146 ++++++++++++++++++------------------- src/api/api_goal.cpp | 8 +- src/api/api_model.cpp | 24 +++--- src/api/api_numeral.cpp | 26 +++---- src/api/api_opt.cpp | 6 +- src/api/api_params.cpp | 4 +- src/api/api_parsers.cpp | 23 ++---- src/api/api_polynomial.cpp | 2 +- src/api/api_qe.cpp | 4 +- src/api/api_quant.cpp | 44 +++++------ src/api/api_rcf.cpp | 2 +- src/api/api_seq.cpp | 2 +- src/api/api_solver.cpp | 20 ++--- src/api/api_stats.cpp | 14 ++-- src/api/api_tactic.cpp | 14 ++-- src/api/c++/z3++.h | 2 +- src/api/python/z3/z3.py | 15 +--- src/api/z3_api.h | 11 --- src/tactic/goal.cpp | 21 ++++++ src/tactic/goal.h | 4 +- 31 files changed, 298 insertions(+), 313 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 47d91209e..1bb1b6a51 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -29,14 +29,14 @@ Notes: #define CHECK_IS_ALGEBRAIC(ARG, RET) { \ if (!Z3_algebraic_is_value_core(c, ARG)) { \ - SET_ERROR_CODE(Z3_INVALID_ARG); \ + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); \ return RET; \ } \ } #define CHECK_IS_ALGEBRAIC_X(ARG, RET) { \ if (!Z3_algebraic_is_value_core(c, ARG)) { \ - SET_ERROR_CODE(Z3_INVALID_ARG); \ + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); \ RETURN_Z3(RET); \ } \ } @@ -196,7 +196,7 @@ extern "C" { CHECK_IS_ALGEBRAIC_X(b, nullptr); if ((is_rational(c, b) && get_rational(c, b).is_zero()) || (!is_rational(c, b) && am(c).is_zero(get_irrational(c, b)))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } BIN_OP(/,div); @@ -211,7 +211,7 @@ extern "C" { if (k % 2 == 0) { if ((is_rational(c, a) && get_rational(c, a).is_neg()) || (!is_rational(c, a) && am(c).is_neg(get_irrational(c, a)))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -360,13 +360,13 @@ extern "C" { expr2polynomial converter(mk_c(c)->m(), pm, nullptr, true); if (!converter.to_polynomial(to_expr(p), _p, d) || static_cast(max_var(_p)) >= n + 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } algebraic_numbers::manager & _am = am(c); scoped_anum_vector as(_am); if (!to_anum_vector(c, n, a, as)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } scoped_anum_vector roots(_am); @@ -396,13 +396,13 @@ extern "C" { expr2polynomial converter(mk_c(c)->m(), pm, nullptr, true); if (!converter.to_polynomial(to_expr(p), _p, d) || static_cast(max_var(_p)) >= n) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } algebraic_numbers::manager & _am = am(c); scoped_anum_vector as(_am); if (!to_anum_vector(c, n, a, as)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } { diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index f245dfd18..f46f56ef2 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -51,7 +51,7 @@ extern "C" { LOG_Z3_mk_real(c, num, den); RESET_ERROR_CODE(); if (den == 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } sort* s = mk_c(c)->m().mk_sort(mk_c(c)->get_arith_fid(), REAL_SORT); @@ -97,7 +97,7 @@ extern "C" { LOG_Z3_mk_sub(c, num_args, args); RESET_ERROR_CODE(); if (num_args == 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } expr* r = to_expr(args[0]); @@ -129,7 +129,7 @@ extern "C" { LOG_Z3_get_algebraic_number_lower(c, a, precision); RESET_ERROR_CODE(); if (!Z3_is_algebraic_number(c, a)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } expr * e = to_expr(a); @@ -147,7 +147,7 @@ extern "C" { LOG_Z3_get_algebraic_number_upper(c, a, precision); RESET_ERROR_CODE(); if (!Z3_is_algebraic_number(c, a)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } expr * e = to_expr(a); @@ -167,7 +167,7 @@ extern "C" { rational val; ast * _a = to_ast(a); if (!is_expr(_a) || !mk_c(c)->autil().is_numeral(to_expr(_a), val)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } expr * r = mk_c(c)->autil().mk_numeral(numerator(val), true); @@ -183,7 +183,7 @@ extern "C" { rational val; ast * _a = to_ast(a); if (!is_expr(_a) || !mk_c(c)->autil().is_numeral(to_expr(_a), val)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } expr * r = mk_c(c)->autil().mk_numeral(denominator(val), true); diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index 31391e218..a9f5d7d70 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -58,7 +58,7 @@ extern "C" { sort * a_ty = m.get_sort(_a); sort * i_ty = m.get_sort(_i); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } sort * domain[2] = {a_ty, i_ty}; @@ -81,7 +81,7 @@ extern "C" { sort * a_ty = m.get_sort(_a); // sort * i_ty = m.get_sort(_i); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } ptr_vector domain; @@ -113,7 +113,7 @@ extern "C" { sort * i_ty = m.get_sort(_i); sort * v_ty = m.get_sort(_v); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } sort * domain[3] = {a_ty, i_ty, v_ty}; @@ -136,7 +136,7 @@ extern "C" { sort * a_ty = m.get_sort(_a); sort * v_ty = m.get_sort(_v); if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } ptr_vector domain; @@ -163,7 +163,7 @@ extern "C" { LOG_Z3_mk_map(c, f, n, args); RESET_ERROR_CODE(); if (n == 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ast_manager & m = mk_c(c)->m(); @@ -298,7 +298,7 @@ extern "C" { Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(0).get_ast()); RETURN_Z3(r); } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); Z3_CATCH_RETURN(nullptr); } @@ -314,7 +314,7 @@ extern "C" { Z3_sort r = reinterpret_cast(to_sort(t)->get_parameter(n-1).get_ast()); RETURN_Z3(r); } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 0753d3ffe..5828b0fcd 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -48,7 +48,7 @@ extern "C" { LOG_Z3_mk_int_symbol(c, i); RESET_ERROR_CODE(); if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; } Z3_symbol result = of_symbol(symbol(i)); @@ -281,7 +281,7 @@ extern "C" { if (_s.is_numerical()) { return _s.get_num(); } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return -1; Z3_CATCH_RETURN(-1); } @@ -355,7 +355,7 @@ extern "C" { LOG_Z3_get_app_decl(c, a); RESET_ERROR_CODE(); if (!is_app(reinterpret_cast(a))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(of_func_decl(to_app(a)->get_decl())); @@ -371,11 +371,11 @@ extern "C" { LOG_Z3_get_app_arg(c, a, i); RESET_ERROR_CODE(); if (!is_app(reinterpret_cast(a))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } if (i >= to_app(a)->get_num_args()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(of_ast(to_app(a)->get_arg(i))); @@ -398,7 +398,7 @@ extern "C" { LOG_Z3_get_decl_parameter_kind(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return Z3_PARAMETER_INT; } parameter const& p = to_func_decl(d)->get_parameters()[idx]; @@ -430,12 +430,12 @@ extern "C" { LOG_Z3_get_decl_int_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0; } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_int()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return p.get_int(); @@ -447,12 +447,12 @@ extern "C" { LOG_Z3_get_decl_double_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0; } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_double()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return p.get_double(); @@ -464,12 +464,12 @@ extern "C" { LOG_Z3_get_decl_symbol_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_symbol()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } return of_symbol(p.get_symbol()); @@ -481,12 +481,12 @@ extern "C" { LOG_Z3_get_decl_sort_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_ast() || !is_sort(p.get_ast())) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(of_sort(to_sort(p.get_ast()))); @@ -498,12 +498,12 @@ extern "C" { LOG_Z3_get_decl_ast_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_ast()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(of_ast(p.get_ast())); @@ -515,12 +515,12 @@ extern "C" { LOG_Z3_get_decl_func_decl_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_ast() || !is_func_decl(p.get_ast())) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(of_func_decl(to_func_decl(p.get_ast()))); @@ -532,12 +532,12 @@ extern "C" { LOG_Z3_get_decl_rational_parameter(c, d, idx); RESET_ERROR_CODE(); if (idx >= to_func_decl(d)->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } parameter const& p = to_func_decl(d)->get_parameters()[idx]; if (!p.is_rational()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } return mk_c(c)->mk_external_string(p.get_rational().to_string()); @@ -584,7 +584,7 @@ extern "C" { LOG_Z3_get_domain(c, d, i); RESET_ERROR_CODE(); if (i >= to_func_decl(d)->get_arity()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } Z3_sort r = of_sort(to_func_decl(d)->get_domain(i)); @@ -740,7 +740,7 @@ extern "C" { case AST_APP: { app* e = to_app(a); if (e->get_num_args() != num_args) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); } else { a = m.mk_app(e->get_decl(), num_args, args); @@ -749,7 +749,7 @@ extern "C" { } case AST_QUANTIFIER: { if (num_args != 1) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); } else { a = m.update_quantifier(to_quantifier(a), args[0]); @@ -779,7 +779,7 @@ extern "C" { expr * r = nullptr; for (unsigned i = 0; i < num_exprs; i++) { if (m.get_sort(from[i]) != m.get_sort(to[i])) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(of_expr(nullptr)); } SASSERT(from[i]->get_ref_count() > 0); @@ -1212,14 +1212,14 @@ extern "C" { RESET_ERROR_CODE(); ast* _a = reinterpret_cast(a); if (!_a || _a->get_kind() != AST_VAR) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } var* va = to_var(_a); if (va) { return va->get_idx(); } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; Z3_CATCH_RETURN(0); } @@ -1230,7 +1230,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(a, nullptr); if (c == target) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } SASSERT(mk_c(c)->m().contains(to_ast(a))); diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp index 17dd086b5..44cadc691 100644 --- a/src/api/api_ast_map.cpp +++ b/src/api/api_ast_map.cpp @@ -71,7 +71,7 @@ extern "C" { RESET_ERROR_CODE(); obj_map::obj_map_entry * entry = to_ast_map_ref(m).find_core(to_ast(k)); if (entry == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } else { diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp index ae5adecea..5fe19a7d5 100644 --- a/src/api/api_ast_vector.cpp +++ b/src/api/api_ast_vector.cpp @@ -65,7 +65,7 @@ extern "C" { LOG_Z3_ast_vector_get(c, v, i); RESET_ERROR_CODE(); if (i >= to_ast_vector_ref(v).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } // Remark: Don't need to invoke save_object. @@ -79,7 +79,7 @@ extern "C" { LOG_Z3_ast_vector_set(c, v, i, a); RESET_ERROR_CODE(); if (i >= to_ast_vector_ref(v).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return; } to_ast_vector_ref(v).set(i, to_ast(a)); @@ -107,8 +107,7 @@ extern "C" { LOG_Z3_ast_vector_translate(c, v, t); RESET_ERROR_CODE(); if (c == t) { - SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(nullptr); + RETURN_Z3(v); } ast_translation translator(mk_c(c)->m(), mk_c(t)->m()); Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, *mk_c(t), mk_c(t)->m()); diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 1876d930d..bd603aa6d 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -27,9 +27,6 @@ extern "C" { Z3_TRY; LOG_Z3_mk_bv_sort(c, sz); RESET_ERROR_CODE(); - if (sz == 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); - } parameter p(sz); Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->get_bv_fid(), BV_SORT, 1, &p)); RETURN_Z3(r); @@ -163,7 +160,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ // Not logging this one, since it is just syntax sugar. unsigned sz = Z3_get_bv_sort_size(c, s); if (sz == 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "zero length bit-vector supplied"); return nullptr; } Z3_ast x = Z3_mk_int64(c, 1, s); @@ -393,7 +390,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ if (to_sort(t)->get_family_id() == mk_c(c)->get_bv_fid() && to_sort(t)->get_decl_kind() == BV_SORT) { return to_sort(t)->get_parameter(0).get_int(); } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "sort is not a bit-vector"); return 0; Z3_CATCH_RETURN(0); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 295977a06..673d0b1c9 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -144,9 +144,11 @@ namespace api { } } - void context::set_error_code(Z3_error_code err) { + void context::set_error_code(Z3_error_code err, char const* opt_msg) { m_error_code = err; if (err != Z3_OK) { + m_exception_msg.clear(); + if (opt_msg) m_exception_msg = opt_msg; invoke_error_handler(err); } } @@ -159,7 +161,7 @@ namespace api { void context::check_searching() { if (m_searching) { - set_error_code(Z3_INVALID_USAGE); // TBD: error code could be fixed. + set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed. } } @@ -248,25 +250,24 @@ namespace api { if (ex.has_error_code()) { switch(ex.error_code()) { case ERR_MEMOUT: - set_error_code(Z3_MEMOUT_FAIL); + set_error_code(Z3_MEMOUT_FAIL, nullptr); break; case ERR_PARSER: - set_error_code(Z3_PARSER_ERROR); + set_error_code(Z3_PARSER_ERROR, ex.msg()); break; case ERR_INI_FILE: - set_error_code(Z3_INVALID_ARG); + set_error_code(Z3_INVALID_ARG, nullptr); break; case ERR_OPEN_FILE: - set_error_code(Z3_FILE_ACCESS_ERROR); + set_error_code(Z3_FILE_ACCESS_ERROR, nullptr); break; default: - set_error_code(Z3_INTERNAL_FATAL); + set_error_code(Z3_INTERNAL_FATAL, nullptr); break; } } else { - m_exception_msg = ex.msg(); - set_error_code(Z3_EXCEPTION); + set_error_code(Z3_EXCEPTION, ex.msg()); } } @@ -301,7 +302,7 @@ namespace api { case AST_FUNC_DECL: break; } - set_error_code(Z3_SORT_ERROR); + set_error_code(Z3_SORT_ERROR, nullptr); } } @@ -379,7 +380,7 @@ extern "C" { LOG_Z3_dec_ref(c, a); RESET_ERROR_CODE(); if (to_ast(a)->get_ref_count() == 0) { - SET_ERROR_CODE(Z3_DEC_REF_ERROR); + SET_ERROR_CODE(Z3_DEC_REF_ERROR, nullptr); return; } mk_c(c)->m().dec_ref(to_ast(a)); @@ -440,10 +441,14 @@ extern "C" { } void Z3_API Z3_set_error(Z3_context c, Z3_error_code e) { - SET_ERROR_CODE(e); + SET_ERROR_CODE(e, nullptr); } static char const * _get_error_msg(Z3_context c, Z3_error_code err) { + if (c) { + char const* msg = mk_c(c)->get_exception_msg(); + if (msg && *msg) return msg; + } switch(err) { case Z3_OK: return "ok"; case Z3_SORT_ERROR: return "type error"; @@ -457,7 +462,7 @@ extern "C" { case Z3_INTERNAL_FATAL: return "internal error"; case Z3_INVALID_USAGE: return "invalid usage"; case Z3_DEC_REF_ERROR: return "invalid dec_ref command"; - case Z3_EXCEPTION: return c == nullptr ? "Z3 exception" : mk_c(c)->get_exception_msg(); + case Z3_EXCEPTION: return "Z3 exception"; default: return "unknown"; } } diff --git a/src/api/api_context.h b/src/api/api_context.h index 50e89113d..a6f55d1aa 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -141,7 +141,7 @@ namespace api { Z3_error_code get_error_code() const { return m_error_code; } void reset_error_code(); - void set_error_code(Z3_error_code err); + void set_error_code(Z3_error_code err, char const* opt_msg); void set_error_handler(Z3_error_handler h) { m_error_handler = h; } // Sign an error if solver is searching void check_searching(); @@ -219,14 +219,6 @@ namespace api { // // ------------------------ smt_params & fparams() { return m_fparams; } - - // ------------------------ - // - // Parser interface - // - // ------------------------ - - std::string m_parser_error_buffer; }; @@ -234,14 +226,14 @@ namespace api { inline api::context * mk_c(Z3_context c) { return reinterpret_cast(c); } #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); } -#define SET_ERROR_CODE(ERR) { mk_c(c)->set_error_code(ERR); } -#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } -#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } +#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); return _ret_; } } +#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)); } -#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); 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); } #endif diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index fd31a65f8..b0a4def55 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -157,7 +157,7 @@ extern "C" { RESET_ERROR_CODE(); sort * r = to_sort(s); if (Z3_get_sort_kind(c, s) != Z3_RELATION_SORT) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "sort should be a relation"); return 0; } return r->get_num_parameters(); @@ -170,18 +170,18 @@ extern "C" { RESET_ERROR_CODE(); sort * r = to_sort(s); if (Z3_get_sort_kind(c, s) != Z3_RELATION_SORT) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "sort should be a relation"); RETURN_Z3(nullptr); } if (col >= r->get_num_parameters()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } parameter const& p = r->get_parameter(col); if (!p.is_ast() || !is_sort(p.get_ast())) { UNREACHABLE(); warning_msg("Sort parameter expected at %d", col); - SET_ERROR_CODE(Z3_INTERNAL_FATAL); + SET_ERROR_CODE(Z3_INTERNAL_FATAL, "sort parameter expected"); RETURN_Z3(nullptr); } Z3_sort res = of_sort(to_sort(p.get_ast())); @@ -364,7 +364,7 @@ extern "C" { install_dl_collect_cmds(coll, ctx); ctx.set_ignore_check(true); if (!parse_smt2_commands(ctx, s)) { - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); return nullptr; } @@ -408,7 +408,7 @@ extern "C" { LOG_Z3_fixedpoint_from_file(c, d, s); std::ifstream is(s); if (!is) { - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); RETURN_Z3(nullptr); } RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is)); diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 799e537ea..0c2544643 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -56,7 +56,7 @@ extern "C" { del_datatype_decl(dt); if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -118,7 +118,7 @@ extern "C" { del_datatype_decl(dt); if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -180,7 +180,7 @@ extern "C" { del_datatype_decl(decl); if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -274,7 +274,7 @@ extern "C" { RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); if (!constr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } ast_manager& m = mk_c(c)->m(); @@ -282,7 +282,7 @@ extern "C" { func_decl* f = reinterpret_cast(constr)->m_constructor.get(); if (!f) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } if (constructor_decl) { @@ -353,7 +353,7 @@ extern "C" { del_datatype_decl(data); if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -416,7 +416,7 @@ extern "C" { del_datatype_decls(datas.size(), datas.c_ptr()); if (!ok) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return; } @@ -445,7 +445,7 @@ extern "C" { datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return dt_util.get_datatype_constructors(_t)->size(); @@ -458,12 +458,12 @@ extern "C" { sort * _t = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx >= decls.size()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } func_decl* decl = (decls)[idx]; @@ -488,12 +488,12 @@ extern "C" { datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx >= decls.size()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } func_decl* decl = (decls)[idx]; @@ -511,23 +511,23 @@ extern "C" { datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & decls = *dt_util.get_datatype_constructors(_t); if (idx_c >= decls.size()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } func_decl* decl = (decls)[idx_c]; if (decl->get_arity() <= idx_a) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & accs = *dt_util.get_constructor_accessors(decl); SASSERT(accs.size() == decl->get_arity()); if (accs.size() <= idx_a) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } decl = (accs)[idx_a]; @@ -543,7 +543,7 @@ extern "C" { sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } Z3_func_decl r = get_datatype_sort_constructor_core(c, t, 0); @@ -558,12 +558,12 @@ extern "C" { sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } ptr_vector const & decls = *dt_util.get_datatype_constructors(tuple); if (decls.size() != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } ptr_vector const & accs = *dt_util.get_constructor_accessors(decls[0]); @@ -578,17 +578,17 @@ extern "C" { sort * tuple = to_sort(t); datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & decls = *dt_util.get_datatype_constructors(tuple); if (decls.size() != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & accs = *dt_util.get_constructor_accessors((decls)[0]); if (accs.size() <= i) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } func_decl* acc = (accs)[i]; diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 261198354..cdc592527 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -175,7 +175,7 @@ extern "C" { LOG_Z3_mk_fpa_sort(c, ebits, sbits); RESET_ERROR_CODE(); if (ebits < 2 || sbits < 3) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "ebits should be at least 2, sbits at least 3"); } api::context * ctx = mk_c(c); sort * s = ctx->fpautil().mk_float_sort(ebits, sbits); @@ -222,7 +222,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(s, nullptr); if (!is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -238,7 +238,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(s, nullptr); if (!is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -255,7 +255,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(s, nullptr); if (!is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -271,7 +271,7 @@ extern "C" { LOG_Z3_mk_fpa_fp(c, sgn, exp, sig); RESET_ERROR_CODE(); if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "bv sorts expected for arguments"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -286,7 +286,7 @@ extern "C" { LOG_Z3_mk_fpa_numeral_float(c, v, ty); RESET_ERROR_CODE(); if (!is_fp_sort(c, ty)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG,"fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -306,7 +306,7 @@ extern "C" { LOG_Z3_mk_fpa_numeral_double(c, v, ty); RESET_ERROR_CODE(); if (!is_fp_sort(c, ty)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -323,7 +323,7 @@ extern "C" { LOG_Z3_mk_fpa_numeral_int(c, v, ty); RESET_ERROR_CODE(); if (!is_fp_sort(c, ty)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -343,7 +343,7 @@ extern "C" { LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty); RESET_ERROR_CODE(); if (!is_fp_sort(c, ty)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -363,7 +363,7 @@ extern "C" { LOG_Z3_mk_fpa_numeral_int64_uint64(c, sgn, exp, sig, ty); RESET_ERROR_CODE(); if (!is_fp_sort(c, ty)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -383,7 +383,7 @@ extern "C" { LOG_Z3_mk_fpa_abs(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -398,7 +398,7 @@ extern "C" { LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -413,7 +413,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -428,7 +428,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -443,7 +443,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -458,7 +458,7 @@ extern "C" { LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -473,7 +473,7 @@ extern "C" { LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t1) || !is_fp(c, t2) || !is_fp(c, t3)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -488,7 +488,7 @@ extern "C" { LOG_Z3_mk_fpa_sqrt(c, rm, t); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -503,7 +503,7 @@ extern "C" { LOG_Z3_mk_fpa_rem(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -518,7 +518,7 @@ extern "C" { LOG_Z3_mk_fpa_round_to_integral(c, rm, t); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -533,7 +533,7 @@ extern "C" { LOG_Z3_mk_fpa_min(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -548,7 +548,7 @@ extern "C" { LOG_Z3_mk_fpa_max(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -563,7 +563,7 @@ extern "C" { LOG_Z3_mk_fpa_leq(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -578,7 +578,7 @@ extern "C" { LOG_Z3_mk_fpa_lt(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -593,7 +593,7 @@ extern "C" { LOG_Z3_mk_fpa_geq(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -608,7 +608,7 @@ extern "C" { LOG_Z3_mk_fpa_gt(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -623,7 +623,7 @@ extern "C" { LOG_Z3_mk_fpa_eq(c, t1, t2); RESET_ERROR_CODE(); if (!is_fp(c, t1) || !is_fp(c, t2)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -638,7 +638,7 @@ extern "C" { LOG_Z3_mk_fpa_is_normal(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -653,7 +653,7 @@ extern "C" { LOG_Z3_mk_fpa_is_subnormal(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -668,7 +668,7 @@ extern "C" { LOG_Z3_mk_fpa_is_zero(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -683,7 +683,7 @@ extern "C" { LOG_Z3_mk_fpa_is_infinite(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -698,7 +698,7 @@ extern "C" { LOG_Z3_mk_fpa_is_nan(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -713,7 +713,7 @@ extern "C" { LOG_Z3_mk_fpa_is_negative(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -728,7 +728,7 @@ extern "C" { LOG_Z3_mk_fpa_is_positive(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -744,14 +744,14 @@ extern "C" { LOG_Z3_mk_fpa_to_fp_bv(c, bv, s); RESET_ERROR_CODE(); if (!is_bv(c, bv) || !is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "bv then fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!ctx->bvutil().is_bv(to_expr(bv)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "bv sort the flaot sort expected"); return nullptr; } expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv)); @@ -769,7 +769,7 @@ extern "C" { if (!fu.is_rm(to_expr(rm)) || !fu.is_float(to_expr(t)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); return nullptr; } expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); @@ -787,7 +787,7 @@ extern "C" { if (!fu.is_rm(to_expr(rm)) || !ctx->autil().is_real(to_expr(t)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); return nullptr; } expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); @@ -805,7 +805,7 @@ extern "C" { if (!fu.is_rm(to_expr(rm)) || !ctx->bvutil().is_bv(to_expr(t)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); return nullptr; } expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); @@ -823,7 +823,7 @@ extern "C" { if (!fu.is_rm(to_expr(rm)) || !ctx->bvutil().is_bv(to_expr(t)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); return nullptr; } expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t)); @@ -837,7 +837,7 @@ extern "C" { LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -852,7 +852,7 @@ extern "C" { LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz); RESET_ERROR_CODE(); if (!is_rm(c, rm) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -867,7 +867,7 @@ extern "C" { LOG_Z3_mk_fpa_to_real(c, t); RESET_ERROR_CODE(); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -884,7 +884,7 @@ extern "C" { CHECK_NON_NULL(s, 0); CHECK_VALID_AST(s, 0); if (!is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(0); } return mk_c(c)->fpautil().get_ebits(to_sort(s)); @@ -898,7 +898,7 @@ extern "C" { CHECK_NON_NULL(s, 0); CHECK_VALID_AST(s, 0); if (!is_fp_sort(c, s)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(0); } return mk_c(c)->fpautil().get_sbits(to_sort(s)); @@ -912,7 +912,7 @@ extern "C" { CHECK_NON_NULL(t, 0); CHECK_VALID_AST(t, 0); if (sgn == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "sign cannot be a nullpointer"); return 0; } ast_manager & m = mk_c(c)->m(); @@ -921,13 +921,13 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return 0; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); if (!r || mpfm.is_nan(val)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return 0; } *sgn = mpfm.sgn(val); @@ -948,13 +948,13 @@ extern "C" { api::context * ctx = mk_c(c); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); RETURN_Z3(nullptr); } scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); if (!r || mpfm.is_nan(val)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return nullptr; } app * a; @@ -981,13 +981,13 @@ extern "C" { SASSERT(plugin != 0); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); RETURN_Z3(nullptr); } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); RETURN_Z3(nullptr); } unsigned sbits = val.get().get_sbits(); @@ -1014,13 +1014,13 @@ extern "C" { SASSERT(plugin != 0); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return ""; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return ""; } unsigned sbits = val.get().get_sbits(); @@ -1042,7 +1042,7 @@ extern "C" { CHECK_NON_NULL(t, 0); CHECK_VALID_AST(t, 0); if (n == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid nullptr argument"); return 0; } ast_manager & m = mk_c(c)->m(); @@ -1053,7 +1053,7 @@ extern "C" { SASSERT(plugin != 0); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; return 0; } @@ -1063,7 +1063,7 @@ extern "C" { if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val)) || !mpzm.is_uint64(z)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; return 0; } @@ -1085,13 +1085,13 @@ extern "C" { SASSERT(plugin != 0); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return ""; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); return ""; } unsigned ebits = val.get().get_ebits(); @@ -1120,7 +1120,7 @@ extern "C" { CHECK_NON_NULL(t, 0); CHECK_VALID_AST(t, 0); if (n == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid null argument"); return 0; } ast_manager & m = mk_c(c)->m(); @@ -1130,14 +1130,14 @@ extern "C" { SASSERT(plugin != 0); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; return 0; } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); *n = 0; return 0; } @@ -1169,13 +1169,13 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); expr * e = to_expr(t); if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); RETURN_Z3(nullptr); } scoped_mpf val(mpfm); bool r = plugin->is_numeral(e, val); if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN"); RETURN_Z3(nullptr); } unsigned ebits = val.get().get_ebits(); @@ -1204,7 +1204,7 @@ extern "C" { CHECK_NON_NULL(t, nullptr); CHECK_VALID_AST(t, nullptr); if (!is_fp(c, t)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); @@ -1223,7 +1223,7 @@ extern "C" { !ctx->autil().is_int(to_expr(exp)) || !ctx->autil().is_real(to_expr(sig)) || !fu.is_float(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(exp), to_expr(sig)); @@ -1239,7 +1239,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_nan(to_expr(t)); @@ -1253,7 +1253,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_inf(to_expr(t)); @@ -1267,7 +1267,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_zero(to_expr(t)); @@ -1281,7 +1281,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_normal(to_expr(t)); @@ -1295,7 +1295,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_subnormal(to_expr(t)); @@ -1309,7 +1309,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_positive(to_expr(t)); @@ -1323,7 +1323,7 @@ extern "C" { api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); if (!is_expr(t) || !fu.is_numeral(to_expr(t))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return fu.is_negative(to_expr(t)); diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index ae48a3f6f..090553df5 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -30,7 +30,7 @@ extern "C" { LOG_Z3_mk_goal(c, models, unsat_cores, proofs); RESET_ERROR_CODE(); if (proofs != 0 && !mk_c(c)->m().proofs_enabled()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "proofs are required, but proofs are not enabled on the context"); RETURN_Z3(nullptr); } Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c)); @@ -119,7 +119,7 @@ extern "C" { LOG_Z3_goal_formula(c, g, idx); RESET_ERROR_CODE(); if (idx >= to_goal_ref(g)->size()) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } expr * result = to_goal_ref(g)->form(idx); @@ -198,6 +198,10 @@ extern "C" { LOG_Z3_goal_to_dimacs_string(c, g); RESET_ERROR_CODE(); std::ostringstream buffer; + if (!to_goal_ref(g)->is_cnf()) { + warning_msg("goal is not in CNF. This will produce a propositional abstraction. " + "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); + } to_goal_ref(g)->display_dimacs(buffer); // Hack for removing the trailing '\n' std::string result = buffer.str(); diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 7eb7d2fdd..e9dd3580b 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -94,7 +94,7 @@ extern "C" { CHECK_NON_NULL(m, nullptr); func_interp * _fi = to_model_ref(m)->get_func_interp(to_func_decl(f)); if (!_fi) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, *mk_c(c), to_model_ref(m)); @@ -123,7 +123,7 @@ extern "C" { RETURN_Z3(of_func_decl(_m->get_constant(i))); } else { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -142,7 +142,7 @@ extern "C" { CHECK_NON_NULL(m, nullptr); model * _m = to_model_ref(m); if (i >= _m->get_num_functions()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; } return of_func_decl(_m->get_function(i)); @@ -187,7 +187,7 @@ extern "C" { LOG_Z3_model_get_sort(c, m, i); RESET_ERROR_CODE(); if (i >= to_model_ref(m)->get_num_uninterpreted_sorts()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } sort * s = to_model_ref(m)->get_uninterpreted_sort(i); @@ -200,7 +200,7 @@ extern "C" { LOG_Z3_model_get_sort_universe(c, m, s); RESET_ERROR_CODE(); if (!to_model_ref(m)->has_uninterpreted_sort(to_sort(s))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } ptr_vector const & universe = to_model_ref(m)->get_universe(to_sort(s)); @@ -242,7 +242,7 @@ extern "C" { RETURN_Z3(of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast()))); } else { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -269,7 +269,7 @@ extern "C" { RESET_ERROR_CODE(); func_decl* d = to_func_decl(f); if (d->get_arity() != 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); } else { model* mdl = to_model_ref(m); @@ -313,7 +313,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_NON_NULL(f, nullptr); if (i >= to_func_interp_ref(f)->num_entries()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, *mk_c(c), to_func_interp(f)->m_model.get()); @@ -364,7 +364,7 @@ extern "C" { func_interp* _fi = to_func_interp_ref(fi); expr* _value = to_expr(value); if (to_ast_vector_ref(args).size() != _fi->get_arity()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return; } // check sorts of value @@ -416,7 +416,7 @@ extern "C" { LOG_Z3_func_entry_get_arg(c, e, i); RESET_ERROR_CODE(); if (i >= to_func_entry(e)->m_func_interp->get_arity()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } expr * r = to_func_entry(e)->m_func_entry->get_arg(i); @@ -434,7 +434,7 @@ extern "C" { if (g) { return g->num_entries(); } - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0; } return 0; @@ -448,7 +448,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_NON_NULL(m, 0); if (j >= get_model_func_num_entries_core(c, m, i)) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0; } Z3_func_decl d = get_model_func_decl_core(c, m, i); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index de9886571..b5458cff2 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -40,7 +40,7 @@ bool is_numeral_sort(Z3_context c, Z3_sort ty) { bool check_numeral_sort(Z3_context c, Z3_sort ty) { bool is_num = is_numeral_sort(c, ty); if (!is_num) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); } return is_num; } @@ -55,7 +55,7 @@ extern "C" { RETURN_Z3(nullptr); } if (!n) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } sort * _ty = to_sort(ty); @@ -72,7 +72,7 @@ extern "C" { (('p' == *m) || ('P' == *m) || ('+' == *m))))) { - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); RETURN_Z3(nullptr); } ++m; @@ -162,7 +162,7 @@ extern "C" { RESET_ERROR_CODE(); expr* e = to_expr(a); if (!e) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } if (mk_c(c)->autil().is_numeral(e, r)) { @@ -221,7 +221,7 @@ extern "C" { return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); } else { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } } @@ -234,7 +234,7 @@ extern "C" { RESET_ERROR_CODE(); expr* e = to_expr(a); if (!e) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } rational r; @@ -256,7 +256,7 @@ extern "C" { return mk_c(c)->mk_external_string(r.to_string()); } else { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } Z3_CATCH_RETURN(""); @@ -281,7 +281,7 @@ extern "C" { return Z3_FALSE; } } - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } @@ -293,7 +293,7 @@ extern "C" { LOG_Z3_get_numeral_int(c, v, i); RESET_ERROR_CODE(); if (!i) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } int64_t l; @@ -311,7 +311,7 @@ extern "C" { LOG_Z3_get_numeral_uint(c, v, u); RESET_ERROR_CODE(); if (!u) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } uint64_t l; @@ -329,7 +329,7 @@ extern "C" { LOG_Z3_get_numeral_uint64(c, v, u); RESET_ERROR_CODE(); if (!u) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } rational r; @@ -349,7 +349,7 @@ extern "C" { LOG_Z3_get_numeral_int64(c, v, i); RESET_ERROR_CODE(); if (!i) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } rational r; @@ -368,7 +368,7 @@ extern "C" { LOG_Z3_get_numeral_rational_int64(c, v, num, den); RESET_ERROR_CODE(); if (!num || !den) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; } rational r; diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 4bb146e39..71f92eeba 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -318,17 +318,15 @@ extern "C" { ctx->set_ignore_check(true); try { if (!parse_smt2_commands(*ctx.get(), s)) { - mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return; } } catch (z3_exception& e) { errstrm << e.msg(); - mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return; } diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index d021ed6ad..9d9f5157c 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -171,7 +171,7 @@ extern "C" { LOG_Z3_param_descrs_get_name(c, p, i); RESET_ERROR_CODE(); if (i >= to_param_descrs_ptr(p)->size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } Z3_symbol result = of_symbol(to_param_descrs_ptr(p)->get_param_name(i)); @@ -185,7 +185,7 @@ extern "C" { RESET_ERROR_CODE(); char const* result = to_param_descrs_ptr(p)->get_descr(to_symbol(s)); if (result == nullptr) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } return mk_c(c)->mk_external_string(result); diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index d791dc2a5..b88f273f9 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -30,15 +30,6 @@ Revision History: extern "C" { - - Z3_string Z3_API Z3_get_parser_error(Z3_context c) { - Z3_TRY; - LOG_Z3_get_parser_error(c); - RESET_ERROR_CODE(); - return mk_c(c)->m_parser_error_buffer.c_str(); - Z3_CATCH_RETURN(""); - } - // --------------- // Support for SMTLIB2 @@ -70,16 +61,14 @@ extern "C" { try { if (!parse_smt2_commands(*ctx.get(), is)) { ctx = nullptr; - mk_c(c)->m_parser_error_buffer = errstrm.str(); - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return of_ast_vector(v); } } catch (z3_exception& e) { errstrm << e.msg(); - mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return of_ast_vector(v); } ptr_vector::const_iterator it = ctx->begin_assertions(); @@ -118,7 +107,7 @@ extern "C" { LOG_Z3_parse_smtlib2_string(c, file_name, num_sorts, sort_names, sorts, num_decls, decl_names, decls); std::ifstream is(file_name); if (!is) { - SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR); + SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); return nullptr; } Z3_ast_vector r = parse_smtlib2_stream(false, c, is, num_sorts, sort_names, sorts, num_decls, decl_names, decls); @@ -141,15 +130,13 @@ extern "C" { ctx->set_diagnostic_stream(ous); try { if (!parse_smt2_commands(*ctx.get(), is)) { - mk_c(c)->m_parser_error_buffer = ous.str(); - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str()); RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } } catch (z3_exception& e) { if (ous.str().empty()) ous << e.msg(); - mk_c(c)->m_parser_error_buffer = ous.str(); - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str()); RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); } RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 35ece4a59..8c5fc99c9 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -49,7 +49,7 @@ extern "C" { default_expr2polynomial converter(mk_c(c)->m(), pm); if (!converter.to_polynomial(to_expr(p), _p, d) || !converter.to_polynomial(to_expr(q), _q, d)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return nullptr; } Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 92517b02b..94e83144f 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -55,7 +55,7 @@ extern "C" app_ref_vector vars(mk_c(c)->m ()); if (!to_apps(num_bounds, bound, vars)) { - SET_ERROR_CODE (Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } @@ -141,7 +141,7 @@ extern "C" for (unsigned i = 0; i < vVars.size (); ++i) { app *a = to_app (vVars.get (i)); if (a->get_kind () != AST_APP) { - SET_ERROR_CODE (Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } vApps.push_back (a); diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index b760760a4..6d6d19d56 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -62,11 +62,11 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); if (!mk_c(c)->m().is_bool(to_expr(body))) { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return nullptr; } if (num_patterns > 0 && num_no_patterns > 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); return nullptr; } expr * const* ps = reinterpret_cast(patterns); @@ -77,7 +77,7 @@ extern "C" { pattern_validator v(mk_c(c)->m()); for (unsigned i = 0; i < num_patterns; i++) { if (!v(num_decls, ps[i], 0, 0)) { - SET_ERROR_CODE(Z3_INVALID_PATTERN); + SET_ERROR_CODE(Z3_INVALID_PATTERN, nullptr); return nullptr; } } @@ -154,7 +154,7 @@ extern "C" { RESET_ERROR_CODE(); expr_ref result(mk_c(c)->m()); if (num_decls == 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); RETURN_Z3(0); } @@ -177,7 +177,7 @@ extern "C" { LOG_Z3_mk_lambda_const(c, num_decls, vars, body); RESET_ERROR_CODE(); if (num_decls == 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); RETURN_Z3(0); } @@ -220,17 +220,17 @@ extern "C" { svector types; ptr_vector bound_asts; if (num_patterns > 0 && num_no_patterns > 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); RETURN_Z3(nullptr); } if (num_bound == 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "number of bound variables is 0"); RETURN_Z3(nullptr); } for (unsigned i = 0; i < num_bound; ++i) { app* a = to_app(bound[i]); if (a->get_kind() != AST_APP) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } symbol s(to_app(a)->get_decl()->get_name()); @@ -238,7 +238,7 @@ extern "C" { types.push_back(of_sort(mk_c(c)->m().get_sort(a))); bound_asts.push_back(a); if (a->get_family_id() != null_family_id || a->get_num_args() != 0) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -259,7 +259,7 @@ extern "C" { for (unsigned i = 0; i < num_no_patterns; ++i) { expr_ref result(mk_c(c)->m()); if (!is_app(to_expr(no_patterns[i]))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } app* pat = to_app(to_expr(no_patterns[i])); @@ -323,7 +323,7 @@ extern "C" { RESET_ERROR_CODE(); for (unsigned i = 0; i < num_patterns; ++i) { if (!is_app(to_expr(terms[i]))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } } @@ -377,7 +377,7 @@ extern "C" { return to_quantifier(_a)->get_weight(); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return 0; } Z3_CATCH_RETURN(0); @@ -392,7 +392,7 @@ extern "C" { return to_quantifier(_a)->get_num_patterns(); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return 0; } Z3_CATCH_RETURN(0); @@ -408,7 +408,7 @@ extern "C" { RETURN_Z3(r); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -424,7 +424,7 @@ extern "C" { return to_quantifier(_a)->get_num_no_patterns(); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return 0; } Z3_CATCH_RETURN(0); @@ -440,7 +440,7 @@ extern "C" { RETURN_Z3(r); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -455,7 +455,7 @@ extern "C" { return of_symbol(to_quantifier(_a)->get_decl_names()[i]); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return nullptr; } Z3_CATCH_RETURN(nullptr); @@ -471,7 +471,7 @@ extern "C" { RETURN_Z3(r); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -487,7 +487,7 @@ extern "C" { RETURN_Z3(r); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); @@ -503,7 +503,7 @@ extern "C" { return to_quantifier(_a)->get_num_decls(); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return 0; } Z3_CATCH_RETURN(0); @@ -518,7 +518,7 @@ extern "C" { return _p->get_num_args(); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); return 0; } Z3_CATCH_RETURN(0); @@ -534,7 +534,7 @@ extern "C" { RETURN_Z3(r); } else { - SET_ERROR_CODE(Z3_SORT_ERROR); + SET_ERROR_CODE(Z3_SORT_ERROR, nullptr); RETURN_Z3(nullptr); } Z3_CATCH_RETURN(nullptr); diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 3d65cb1cd..d92ff155b 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -123,7 +123,7 @@ extern "C" { } if (rz == 0) { // it is the zero polynomial - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } av.shrink(rz); diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 84cfdca32..42979d1ed 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -107,7 +107,7 @@ extern "C" { RESET_ERROR_CODE(); zstring str; if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal"); return ""; } std::string result = str.encode(); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 1c8d205bc..9ad51aaf4 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -145,10 +145,12 @@ extern "C" { void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) { scoped_ptr ctx = alloc(cmd_context, false, &(mk_c(c)->m())); ctx->set_ignore_check(true); + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); if (!parse_smt2_commands(*ctx.get(), is)) { ctx = nullptr; - SET_ERROR_CODE(Z3_PARSER_ERROR); + SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return; } @@ -178,7 +180,7 @@ extern "C" { char const* ext = get_extension(file_name); std::ifstream is(file_name); if (!is) { - SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR); + SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); } else if (ext && std::string("dimacs") == ext) { ast_manager& m = to_solver_ref(s)->get_manager(); @@ -291,7 +293,7 @@ extern "C" { RESET_ERROR_CODE(); init_solver(c, s); if (n > to_solver_ref(s)->get_scope_level()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return; } if (n > 0) @@ -372,7 +374,7 @@ extern "C" { static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { for (unsigned i = 0; i < num_assumptions; i++) { if (!is_expr(to_ast(assumptions[i]))) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression"); return Z3_L_UNDEF; } } @@ -430,7 +432,7 @@ extern "C" { model_ref _m; to_solver_ref(s)->get_model(_m); if (!_m) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current model"); RETURN_Z3(nullptr); } if (_m) { @@ -450,7 +452,7 @@ extern "C" { init_solver(c, s); proof * p = to_solver_ref(s)->get_proof(); if (!p) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "there is no current proof"); RETURN_Z3(nullptr); } mk_c(c)->save_ast_trail(p); @@ -542,7 +544,7 @@ extern "C" { for (ast* e : __assumptions) { if (!is_expr(e)) { _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "assumption is not an expression"); return Z3_L_UNDEF; } _assumptions.push_back(to_expr(e)); @@ -551,7 +553,7 @@ extern "C" { for (ast* a : __variables) { if (!is_expr(a)) { _assumptions.finalize(); _consequences.finalize(); _variables.finalize(); - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "variable is not an expression"); return Z3_L_UNDEF; } _variables.push_back(to_expr(a)); @@ -593,7 +595,7 @@ extern "C" { expr_ref_vector result(m), vars(m); for (ast* a : to_ast_vector_ref(vs)) { if (!is_expr(a)) { - SET_ERROR_CODE(Z3_INVALID_USAGE); + SET_ERROR_CODE(Z3_INVALID_USAGE, "cube contains a non-expression"); } else { vars.push_back(to_expr(a)); diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index 2e1dac4de..2014d57b8 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -67,7 +67,7 @@ extern "C" { LOG_Z3_stats_get_key(c, s, idx); RESET_ERROR_CODE(); if (idx >= to_stats_ref(s).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } return to_stats_ref(s).get_key(idx); @@ -79,7 +79,7 @@ extern "C" { LOG_Z3_stats_is_uint(c, s, idx); RESET_ERROR_CODE(); if (idx >= to_stats_ref(s).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return Z3_FALSE; } return to_stats_ref(s).is_uint(idx); @@ -91,7 +91,7 @@ extern "C" { LOG_Z3_stats_is_double(c, s, idx); RESET_ERROR_CODE(); if (idx >= to_stats_ref(s).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return Z3_FALSE; } return !to_stats_ref(s).is_uint(idx); @@ -103,11 +103,11 @@ extern "C" { LOG_Z3_stats_get_uint_value(c, s, idx); RESET_ERROR_CODE(); if (idx >= to_stats_ref(s).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0; } if (!to_stats_ref(s).is_uint(idx)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0; } return to_stats_ref(s).get_uint_value(idx); @@ -119,11 +119,11 @@ extern "C" { LOG_Z3_stats_get_double_value(c, s, idx); RESET_ERROR_CODE(); if (idx >= to_stats_ref(s).size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return 0.0; } if (to_stats_ref(s).is_uint(idx)) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return 0.0; } return to_stats_ref(s).get_double_value(idx); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 345284fd6..7c0143201 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -52,7 +52,7 @@ extern "C" { RESET_ERROR_CODE(); tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name)); if (t == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } tactic * new_t = t->mk(mk_c(c)->m()); @@ -82,7 +82,7 @@ extern "C" { RESET_ERROR_CODE(); probe_info * p = mk_c(c)->find_probe(symbol(name)); if (p == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } probe * new_p = p->get(); @@ -324,7 +324,7 @@ extern "C" { LOG_Z3_get_tactic_name(c, idx); RESET_ERROR_CODE(); if (idx >= mk_c(c)->num_tactics()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } return mk_c(c)->get_tactic(idx)->get_name().bare_str(); @@ -344,7 +344,7 @@ extern "C" { LOG_Z3_get_probe_name(c, idx); RESET_ERROR_CODE(); if (idx >= mk_c(c)->num_probes()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } return mk_c(c)->get_probe(idx)->get_name().bare_str(); @@ -381,7 +381,7 @@ extern "C" { RESET_ERROR_CODE(); tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name)); if (t == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } return t->get_descr(); @@ -394,7 +394,7 @@ extern "C" { RESET_ERROR_CODE(); probe_info * p = mk_c(c)->find_probe(symbol(name)); if (p == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG); + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } return p->get_descr(); @@ -504,7 +504,7 @@ extern "C" { LOG_Z3_apply_result_get_subgoal(c, r, i); RESET_ERROR_CODE(); if (i > to_apply_result(r)->m_subgoals.size()) { - SET_ERROR_CODE(Z3_IOB); + SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c)); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b68fb2021..a5021360d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -169,7 +169,7 @@ namespace z3 { void check_parser_error() const { Z3_error_code e = Z3_get_error_code(*this); if (e != Z3_OK && enable_exceptions()) { - Z3_string s = Z3_get_parser_error(*this); + Z3_string s = Z3_get_error_message(*this); if (s && *s) Z3_THROW(exception(s)); } check_error(); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 10198fcc5..60a9bd734 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8395,11 +8395,6 @@ def _dict2darray(decls, ctx): i = i + 1 return sz, _names, _decls -def _handle_parse_error(ex, ctx): - msg = Z3_get_parser_error(ctx.ref()) - if msg != "": - raise Z3Exception(msg) - raise ex def parse_smt2_string(s, sorts={}, decls={}, ctx=None): """Parse a string in SMT 2.0 format using the given sorts and decls. @@ -8419,10 +8414,7 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - try: - return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) - except Z3Exception as e: - _handle_parse_error(e, ctx) + return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) def parse_smt2_file(f, sorts={}, decls={}, ctx=None): """Parse a file in SMT 2.0 format using the given sorts and decls. @@ -8432,10 +8424,7 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - try: - return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) - except Z3Exception as e: - _handle_parse_error(e, ctx) + return AstVector(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) ######################################### diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7e12f2fa7..9af548af0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5280,12 +5280,6 @@ extern "C" { Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str); - /** - \brief Retrieve that last error message information generated from parsing. - - def_API('Z3_get_parser_error', STRING, (_in(CONTEXT), )) - */ - Z3_string Z3_API Z3_get_parser_error(Z3_context c); /*@}*/ /** @name Error Handling */ @@ -5332,11 +5326,6 @@ extern "C" { */ Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err); - /** - \brief Return a string describing the given error code. - Retained function name for backwards compatibility within v4.1 - */ - Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err); /*@}*/ /** @name Miscellaneous */ diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index d5d2ee558..203ca2ca0 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -716,3 +716,24 @@ bool is_equal(goal const & s1, goal const & s2) { SASSERT(num1 >= num2); return num1 == num2; } + +bool goal::is_cnf() const { + for (unsigned i = 0; i < size(); i++) { + expr * f = form(i); + if (m_manager.is_or(f)) { + for (expr* l : *to_app(f)) { + if (!is_literal(f)) return false; + } + } + if (!is_literal(f)) return false; + } + return true; +} + +bool goal::is_literal(expr* f) const { + m_manager.is_not(f, f); + if (!is_app(f)) return false; + if (to_app(f)->get_family_id() == m_manager.get_basic_family_id() && + !m_manager.is_false(f) && !m_manager.is_true(f)) return false; + return true; +} diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 2d91bc67f..4125fab99 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -77,7 +77,7 @@ protected: unsigned get_not_idx(expr * f) const; void shrink(unsigned j); void reset_core(); - + bool is_literal(expr* f) const; public: goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false); @@ -159,6 +159,8 @@ public: void set(model_converter* m) { m_mc = m; } void set(proof_converter* p) { m_pc = p; } + bool is_cnf() const; + goal * translate(ast_translation & translator) const; };