mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

Revert "Use nullptr, not 0 in the C++ API impl."

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-12-04 12:06:44 -08:00 • committed by GitHub
parent 0223846b4f
commit 3b54575340
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 34 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -159,7 +159,7 @@ namespace z3 {
m_ctx = Z3_mk_context_rc(c); m_ctx = Z3_mk_context_rc(c);
m_enable_exceptions = true; m_enable_exceptions = true;
m_rounding_mode = RNA; m_rounding_mode = RNA;
Z3_set_error_handler(m_ctx, nullptr); Z3_set_error_handler(m_ctx, 0);
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT); Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
} }
@ -483,12 +483,12 @@ namespace z3 {
protected: protected:
Z3_ast m_ast; Z3_ast m_ast;
public: public:
ast(context & c):object(c), m_ast(nullptr) {} ast(context & c):object(c), m_ast(0) {}
ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); } ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); } ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); } ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
operator Z3_ast() const { return m_ast; } operator Z3_ast() const { return m_ast; }
operator bool() const { return m_ast != nullptr; } operator bool() const { return m_ast != 0; }
ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; } ast & operator=(ast const & s) { Z3_inc_ref(s.ctx(), s.m_ast); if (m_ast) Z3_dec_ref(ctx(), m_ast); m_ctx = s.m_ctx; m_ast = s.m_ast; return *this; }
Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
@ -1264,7 +1264,7 @@ namespace z3 {
inline expr operator+(expr const & a, expr const & b) { inline expr operator+(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b }; Z3_ast args[2] = { a, b };
r = Z3_mk_add(a.ctx(), 2, args); r = Z3_mk_add(a.ctx(), 2, args);
@ -1294,7 +1294,7 @@ namespace z3 {
inline expr operator*(expr const & a, expr const & b) { inline expr operator*(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b }; Z3_ast args[2] = { a, b };
r = Z3_mk_mul(a.ctx(), 2, args); r = Z3_mk_mul(a.ctx(), 2, args);
@ -1318,7 +1318,7 @@ namespace z3 {
inline expr operator>=(expr const & a, expr const & b) { inline expr operator>=(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
r = Z3_mk_ge(a.ctx(), a, b); r = Z3_mk_ge(a.ctx(), a, b);
} }
@ -1335,7 +1335,7 @@ namespace z3 {
inline expr operator/(expr const & a, expr const & b) { inline expr operator/(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
r = Z3_mk_div(a.ctx(), a, b); r = Z3_mk_div(a.ctx(), a, b);
} }
@ -1356,7 +1356,7 @@ namespace z3 {
inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; } inline expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
inline expr operator-(expr const & a) { inline expr operator-(expr const & a) {
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith()) { if (a.is_arith()) {
r = Z3_mk_unary_minus(a.ctx(), a); r = Z3_mk_unary_minus(a.ctx(), a);
} }
@ -1376,7 +1376,7 @@ namespace z3 {
inline expr operator-(expr const & a, expr const & b) { inline expr operator-(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b }; Z3_ast args[2] = { a, b };
r = Z3_mk_sub(a.ctx(), 2, args); r = Z3_mk_sub(a.ctx(), 2, args);
@ -1399,7 +1399,7 @@ namespace z3 {
inline expr operator<=(expr const & a, expr const & b) { inline expr operator<=(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
r = Z3_mk_le(a.ctx(), a, b); r = Z3_mk_le(a.ctx(), a, b);
} }
@ -1424,7 +1424,7 @@ namespace z3 {
inline expr operator<(expr const & a, expr const & b) { inline expr operator<(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
r = Z3_mk_lt(a.ctx(), a, b); r = Z3_mk_lt(a.ctx(), a, b);
} }
@ -1446,7 +1446,7 @@ namespace z3 {
inline expr operator>(expr const & a, expr const & b) { inline expr operator>(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
Z3_ast r = nullptr; Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) { if (a.is_arith() && b.is_arith()) {
r = Z3_mk_gt(a.ctx(), a, b); r = Z3_mk_gt(a.ctx(), a, b);
} }
@ -1771,50 +1771,50 @@ namespace z3 {
inline expr forall(expr const & x, expr const & b) { inline expr forall(expr const & x, expr const & b) {
check_context(x, b); check_context(x, b);
Z3_app vars[] = {(Z3_app) x}; Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr forall(expr const & x1, expr const & x2, expr const & b) { inline expr forall(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr forall(expr_vector const & xs, expr const & b) { inline expr forall(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs); array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr exists(expr const & x, expr const & b) { inline expr exists(expr const & x, expr const & b) {
check_context(x, b); check_context(x, b);
Z3_app vars[] = {(Z3_app) x}; Z3_app vars[] = {(Z3_app) x};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr exists(expr const & x1, expr const & x2, expr const & b) { inline expr exists(expr const & x1, expr const & x2, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x1, b); check_context(x2, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x1, b); check_context(x2, b); check_context(x3, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) {
check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr exists(expr_vector const & xs, expr const & b) { inline expr exists(expr_vector const & xs, expr const & b) {
array<Z3_app> vars(xs); array<Z3_app> vars(xs);
Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, nullptr, b); b.check_error(); return expr(b.ctx(), r); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
} }
inline expr lambda(expr const & x, expr const & b) { inline expr lambda(expr const & x, expr const & b) {
check_context(x, b); check_context(x, b);
@ -2035,7 +2035,7 @@ namespace z3 {
expr eval(expr const & n, bool model_completion=false) const { expr eval(expr const & n, bool model_completion=false) const {
check_context(*this, n); check_context(*this, n);
Z3_ast r = nullptr; Z3_ast r = 0;
bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
check_error(); check_error();
if (status == false && ctx().enable_exceptions()) if (status == false && ctx().enable_exceptions())
@ -2098,7 +2098,7 @@ namespace z3 {
Z3_stats_inc_ref(ctx(), m_stats); Z3_stats_inc_ref(ctx(), m_stats);
} }
public: public:
stats(context & c):object(c), m_stats(nullptr) {} stats(context & c):object(c), m_stats(0) {}
stats(context & c, Z3_stats e):object(c) { init(e); } stats(context & c, Z3_stats e):object(c) { init(e); }
stats(stats const & s):object(s) { init(s.m_stats); } stats(stats const & s):object(s) { init(s.m_stats); }
~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
@ -2216,7 +2216,7 @@ namespace z3 {
std::string to_smt2(char const* status = "unknown") { std::string to_smt2(char const* status = "unknown") {
array<Z3_ast> es(assertions()); array<Z3_ast> es(assertions());
Z3_ast const* fmls = es.ptr(); Z3_ast const* fmls = es.ptr();
Z3_ast fml = nullptr; Z3_ast fml = 0;
unsigned sz = es.size(); unsigned sz = es.size();
if (sz > 0) { if (sz > 0) {
--sz; --sz;
@ -2366,7 +2366,7 @@ namespace z3 {
return model(ctx(), new_m); return model(ctx(), new_m);
} }
model get_model() const { model get_model() const {
Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, nullptr); Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
check_error(); check_error();
return model(ctx(), new_m); return model(ctx(), new_m);
} }
@ -2607,11 +2607,11 @@ namespace z3 {
assert(e.is_bool()); assert(e.is_bool());
std::stringstream strm; std::stringstream strm;
strm << weight; strm << weight;
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), nullptr)); return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0));
} }
handle add(expr const& e, char const* weight) { handle add(expr const& e, char const* weight) {
assert(e.is_bool()); assert(e.is_bool());
return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, nullptr)); return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0));
} }
handle maximize(expr const& e) { handle maximize(expr const& e) {
return handle(Z3_optimize_maximize(ctx(), m_opt, e)); return handle(Z3_optimize_maximize(ctx(), m_opt, e));
@ -2625,7 +2625,7 @@ namespace z3 {
void pop() { void pop() {
Z3_optimize_pop(ctx(), m_opt); Z3_optimize_pop(ctx(), m_opt);
} }
check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, nullptr); check_error(); return to_check_result(r); } check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
check_result check(expr_vector const& asms) { check_result check(expr_vector const& asms) {
unsigned n = asms.size(); unsigned n = asms.size();
array<Z3_ast> _asms(n); array<Z3_ast> _asms(n);
@ -2694,7 +2694,7 @@ namespace z3 {
void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); } void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); }
std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); } std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); }
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); } param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); }
std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, nullptr); } std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); }
std::string to_string(expr_vector const& queries) { std::string to_string(expr_vector const& queries) {
array<Z3_ast> qs(queries); array<Z3_ast> qs(queries);
return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr()); return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
@ -2702,7 +2702,7 @@ namespace z3 {
void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); } void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); } void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
}; };
inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, nullptr); } inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
inline tactic fail_if(probe const & p) { inline tactic fail_if(probe const & p) {
Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
@ -2969,7 +2969,7 @@ namespace z3 {
return expr(ctx(), r); return expr(ctx(), r);
} }
inline expr func_decl::operator()() const { inline expr func_decl::operator()() const {
Z3_ast r = Z3_mk_app(ctx(), *this, 0, nullptr); Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0);
ctx().check_error(); ctx().check_error();
return expr(ctx(), r); return expr(ctx(), r);
} }
@ -3253,13 +3253,13 @@ namespace z3 {
inline expr_vector context::parse_string(char const* s) { inline expr_vector context::parse_string(char const* s) {
Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, nullptr, nullptr, 0, nullptr, nullptr); Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
check_error(); check_error();
return expr_vector(*this, r); return expr_vector(*this, r);
} }
inline expr_vector context::parse_file(char const* s) { inline expr_vector context::parse_file(char const* s) {
Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, nullptr, nullptr, 0, nullptr, nullptr); Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
check_error(); check_error();
return expr_vector(*this, r); return expr_vector(*this, r);
} }