diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 8416b063678..ab87c4e2650 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -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()); diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index c541f72d031..597ab9ca6ad 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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); } diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp index d43219f2512..71a98ba0585 100644 --- a/src/sat/sat_cut_simplifier.cpp +++ b/src/sat/sat_cut_simplifier.cpp @@ -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()); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 40f94cdbc69..837547f7227 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -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) { diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp index 412139eb89b..9969ada2f02 100644 --- a/src/test/dl_relation.cpp +++ b/src/test/dl_relation.cpp @@ -36,7 +36,7 @@ namespace datalog { sig.push_back(int_sort); interval_relation& i1 = dynamic_cast(*ip.mk_empty(sig)); - interval_relation& i2 = dynamic_cast(*ip.mk_full(0, sig)); + interval_relation& i2 = dynamic_cast(*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(*br.mk_empty(sig)); - bound_relation& i2 = dynamic_cast(*br.mk_full(0, sig)); + bound_relation& i2 = dynamic_cast(*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 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 u = br.mk_union_fn(*b1, *b2, 0); + scoped_ptr 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 u = br.mk_union_fn(*b1, *b2, 0); + scoped_ptr 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; diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp index c1ba48ea782..dd826bad8b1 100644 --- a/src/test/no_overflow.cpp +++ b/src/test/no_overflow.cpp @@ -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); } diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index 944f64026b5..d716a126868 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -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"; diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 4fdf20c3ae2..15646f216b4 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -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; }