Use nullptr consistently instead of 0 or NULL.

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

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

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

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) {

src/test/dl_relation.cpp

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

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

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

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