mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

overhaul of error messages. Add warning in dimacs conversion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-04 16:04:37 -07:00
parent e622022bf9
commit 1eb8ccad59
31 changed files with 298 additions and 313 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_algebraic.cpp
View file

@ -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<unsigned>(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<unsigned>(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;
}
{

12
src/api/api_arith.cpp
View file

@ -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);

14
src/api/api_array.cpp
View file

@ -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<sort> 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<sort> 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<Z3_sort>(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<Z3_sort>(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);
}

54
src/api/api_ast.cpp
View file

@ -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<ast*>(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<ast*>(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<ast*>(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)));

2
src/api/api_ast_map.cpp
View file

@ -71,7 +71,7 @@ extern "C" {
RESET_ERROR_CODE();
obj_map<ast, ast*>::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 {

7
src/api/api_ast_vector.cpp
View file

@ -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());

7
src/api/api_bv.cpp
View file

@ -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);
}

31
src/api/api_context.cpp
View file

@ -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";
}
}

20
src/api/api_context.h
View file

@ -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<api::context*>(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

12
src/api/api_datalog.cpp
View file

@ -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));

44
src/api/api_datatype.cpp
View file

@ -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<constructor*>(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<func_decl> 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<func_decl> 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<func_decl> 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<func_decl> 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<func_decl> 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<func_decl> 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<func_decl> 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<func_decl> 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];

146
src/api/api_fpa.cpp
View file

@ -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));

8
src/api/api_goal.cpp
View file

@ -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();

24
src/api/api_model.cpp
View file

@ -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<expr> 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);

26
src/api/api_numeral.cpp
View file

@ -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;

6
src/api/api_opt.cpp
View file

@ -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;
}

4
src/api/api_params.cpp
View file

@ -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);

23
src/api/api_parsers.cpp
View file

@ -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<expr>::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()));

2
src/api/api_polynomial.cpp
View file

@ -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());

4
src/api/api_qe.cpp
View file

@ -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);

44
src/api/api_quant.cpp
View file

@ -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<expr * const*>(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<Z3_sort> types;
ptr_vector<expr> 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);

2
src/api/api_rcf.cpp
View file

@ -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);

2
src/api/api_seq.cpp
View file

@ -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();

20
src/api/api_solver.cpp
View file

@ -145,10 +145,12 @@ extern "C" {
void solver_from_stream(Z3_context c, Z3_solver s, std::istream& is) {
scoped_ptr<cmd_context> 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));

14
src/api/api_stats.cpp
View file

@ -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);

14
src/api/api_tactic.cpp
View file

@ -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));

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

@ -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();

15
src/api/python/z3/z3.py
View file

@ -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)
#########################################

11
src/api/z3_api.h
View file

@ -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 */

21
src/tactic/goal.cpp
View file

@ -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;
}

4
src/tactic/goal.h
View file

@ -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;
};