mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Use nullptr consistently instead of 0 or NULL.

Browse source
This commit is contained in:
Bruce Mitchener 2022-08-01 16:36:05 +07:00 • committed by Nikolaj Bjorner
parent bf282b05c8
commit 77e5d6ab19
8 changed files with 25 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_algebraic.cpp
View file

@ -421,7 +421,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_get_poly(c, a);
RESET_ERROR_CODE();
CHECK_IS_ALGEBRAIC(a, 0);
CHECK_IS_ALGEBRAIC(a, nullptr);
algebraic_numbers::manager & _am = am(c);
algebraic_numbers::anum const & av = get_irrational(c, a);
scoped_mpz_vector coeffs(_am.qm());

4
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -326,12 +326,12 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
}
else if (m_fpa_util.is_to_real(f)) {
expr_ref_vector dom(m);
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, NULL, dom.size(), dom.data()), m);
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, nullptr, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m);
result->set_else(else_value);
}
else if (m_fpa_util.is_to_ieee_bv(f)) {
func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, NULL, dom.size(), dom.data()), m);
func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, nullptr, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_ieee_bv_i, dom.size(), dom.data()), m);
result->set_else(else_value);
}

2
src/sat/sat_cut_simplifier.cpp
View file

@ -179,7 +179,7 @@ namespace sat {
for (; m_config.m_enable_units && m_trail_size < s.init_trail_size(); ++m_trail_size) {
literal lit = s.trail_literal(m_trail_size);
m_aig_cuts.add_node(lit, and_op, 0, 0);
m_aig_cuts.add_node(lit, and_op, 0, nullptr);
}
clause_vector clauses(s.clauses());

4
src/smt/theory_special_relations.cpp
View file

@ -135,7 +135,7 @@ namespace smt {
bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) {
SASSERT(m_util.is_special_relation(atm));
relation* r = 0;
relation* r = nullptr;
ast_manager& m = get_manager();
if (!m_relations.find(atm->get_decl(), r)) {
r = alloc(relation, m_util.get_property(atm), atm->get_decl(), m);
@ -470,7 +470,7 @@ namespace smt {
ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(),
lits.size(), lits.data(), 0, 0, params.size(), params.data())));
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
}
lbool theory_special_relations::final_check(relation& r) {

20
src/test/dl_relation.cpp
View file

@ -36,7 +36,7 @@ namespace datalog {
sig.push_back(int_sort);
interval_relation& i1 = dynamic_cast<interval_relation&>(*ip.mk_empty(sig));
interval_relation& i2 = dynamic_cast<interval_relation&>(*ip.mk_full(0, sig));
interval_relation& i2 = dynamic_cast<interval_relation&>(*ip.mk_full(nullptr, sig));
i1.display(std::cout);
i2.display(std::cout);
@ -141,7 +141,7 @@ namespace datalog {
sig.push_back(int_sort);
bound_relation& i1 = dynamic_cast<bound_relation&>(*br.mk_empty(sig));
bound_relation& i2 = dynamic_cast<bound_relation&>(*br.mk_full(0, sig));
bound_relation& i2 = dynamic_cast<bound_relation&>(*br.mk_full(nullptr, sig));
i1.display(std::cout << "empty:\n");
i2.display(std::cout << "full:\n");
@ -212,8 +212,8 @@ namespace datalog {
// test that equivalence classes are expanded.
// { x1 = x3, x0 < x1 x1 < x2} u { x2 = x3, x0 < x3 } = { x0 < x3 }
{
relation_base* b1 = br.mk_full(0, sig);
relation_base* b2 = br.mk_full(0, sig);
relation_base* b1 = br.mk_full(nullptr, sig);
relation_base* b2 = br.mk_full(nullptr, sig);
unsigned x1x3[2] = { 1, 3 };
unsigned x2x3[2] = { 2, 3 };
scoped_ptr<relation_mutator_fn> id1 = br.mk_filter_identical_fn(*b1, 2, x1x3);
@ -229,10 +229,10 @@ namespace datalog {
b2->display(std::cout << "b2:\n");
(*ltx0x3)(*b2);
b2->display(std::cout << "b2:\n");
scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, 0);
scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, nullptr);
b1->display(std::cout << "b1:\n");
b2->display(std::cout << "b2:\n");
(*u)(*b1, *b2, 0);
(*u)(*b1, *b2, nullptr);
b1->display(std::cout << "b1 u b2:\n");
@ -245,8 +245,8 @@ namespace datalog {
// test that equivalence classes are expanded.
// { x1 = x2 = x3, x0 < x1} u { x1 = x3, x0 < x3, x0 < x2 } = { x0 < x2, x0 < x3 }
{
relation_base* b1 = br.mk_full(0, sig);
relation_base* b2 = br.mk_full(0, sig);
relation_base* b1 = br.mk_full(nullptr, sig);
relation_base* b2 = br.mk_full(nullptr, sig);
unsigned x0x3[2] = { 0, 3 };
unsigned x1x3[2] = { 1, 3 };
unsigned x2x3[2] = { 2, 3 };
@ -262,10 +262,10 @@ namespace datalog {
(*id3)(*b2);
(*ltx0x2)(*b2);
(*ltx0x3)(*b2);
scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, 0);
scoped_ptr<relation_union_fn> u = br.mk_union_fn(*b1, *b2, nullptr);
b1->display(std::cout << "b1:\n");
b2->display(std::cout << "b2:\n");
(*u)(*b1, *b2, 0);
(*u)(*b1, *b2, nullptr);
b1->display(std::cout << "b1 u b2:\n");
// TBD check property;

10
src/test/no_overflow.cpp
View file

@ -111,7 +111,7 @@ void test_add(unsigned bvsize, bool is_signed) {
t1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"x"), bv);
t2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"y"), bv);
test_ovfl = Z3_mk_bvadd_no_overflow(ctx, t1, t2, is_signed);
test_udfl = is_signed ? Z3_mk_bvadd_no_underflow(ctx, t1, t2) : NULL;
test_udfl = is_signed ? Z3_mk_bvadd_no_underflow(ctx, t1, t2) : nullptr;
Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, t1, Z3_mk_numeral(ctx, "0", bv)));
@ -196,7 +196,7 @@ void test_sub(unsigned bvsize, bool is_signed) {
t1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"x"), bv);
t2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"y"), bv);
test_ovfl = is_signed ? Z3_mk_bvsub_no_overflow(ctx, t1, t2) : NULL;
test_ovfl = is_signed ? Z3_mk_bvsub_no_overflow(ctx, t1, t2) : nullptr;
test_udfl = Z3_mk_bvsub_no_underflow(ctx, t1, t2, is_signed);
Z3_solver_push(ctx, s);
@ -358,7 +358,7 @@ void test_mul(unsigned bvsize, bool is_signed) {
t1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"x"), bv);
t2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"y"), bv);
test_ovfl = Z3_mk_bvmul_no_overflow(ctx, t1, t2, is_signed);
test_udfl = is_signed ? Z3_mk_bvmul_no_underflow(ctx, t1, t2) : NULL;
test_udfl = is_signed ? Z3_mk_bvmul_no_underflow(ctx, t1, t2) : nullptr;
Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, t1, Z3_mk_numeral(ctx, "1", bv)));
@ -585,7 +585,7 @@ void test_equiv(Equivalence_params params, unsigned bvsize, bool is_signed) {
Z3_ast t2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx,"y"), bv);
Z3_ast real_test = (*params.no_overflow_func)(ctx, t1, t2, is_signed);
Z3_ast cond = NULL;
Z3_ast cond = nullptr;
if (params.non_zero)
{
cond = Z3_mk_not(ctx, Z3_mk_eq(ctx, t2, Z3_mk_int(ctx, 0, bv)));
@ -624,7 +624,7 @@ void test_equiv(Equivalence_params params, unsigned bvsize, bool is_signed) {
Z3_solver_push(ctx, s);
Z3_ast equiv = Z3_mk_iff(ctx, real_test, check);
if (cond != NULL)
if (cond != nullptr)
{
equiv = Z3_mk_implies(ctx, cond, equiv);
}

4
src/test/simplifier.cpp
View file

@ -93,7 +93,7 @@ static void test_datatypes() {
int_list = Z3_mk_list_sort(ctx, Z3_mk_string_symbol(ctx, "int_list"), int_ty,
&nil_decl, &is_nil_decl, &cons_decl, &is_cons_decl, &head_decl, &tail_decl);
nil = Z3_mk_app(ctx, nil_decl, 0, 0);
nil = Z3_mk_app(ctx, nil_decl, 0, nullptr);
Z3_ast a = Z3_simplify(ctx, Z3_mk_app(ctx, is_nil_decl, 1, &nil));
ENSURE(a == Z3_mk_true(ctx));
@ -132,7 +132,7 @@ static void test_skolemize_bug() {
Z3_ast args[2] = { Z3_mk_eq(ctx, Z3_mk_add(ctx, 2, args1), xp),
Z3_mk_ge(ctx, Z3_mk_add(ctx, 2, args2), n0) };
Z3_ast f = Z3_mk_and(ctx, 2, args);
Z3_ast f2 = Z3_mk_exists(ctx, 0, 0, 0, 1, &Real, &x_name, f);
Z3_ast f2 = Z3_mk_exists(ctx, 0, 0, nullptr, 1, &Real, &x_name, f);
std::cout << Z3_ast_to_string(ctx, f2) << "\n";
Z3_ast f3 = Z3_simplify(ctx, f2);
std::cout << Z3_ast_to_string(ctx, f3) << "\n";

4
src/util/memory_manager.cpp
View file

@ -271,7 +271,7 @@ void memory::deallocate(void * p) {
void * memory::allocate(size_t s) {
s = s + sizeof(size_t); // we allocate an extra field!
void * r = malloc(s);
if (r == 0) {
if (r == nullptr) {
throw_out_of_memory();
return nullptr;
}
@ -298,7 +298,7 @@ void* memory::reallocate(void *p, size_t s) {
}
void *r = realloc(real_p, s);
if (r == 0) {
if (r == nullptr) {
throw_out_of_memory();
return nullptr;
}