From cdfc19a8856be9b803ac472bcddfda7dbe33f1d5 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 09:11:19 +0700 Subject: [PATCH] Use nullptr. --- src/api/api_ast.cpp | 10 +++---- src/api/api_goal.cpp | 2 +- src/api/api_quant.cpp | 8 +++--- src/api/api_solver.cpp | 8 +++--- src/ast/ast.cpp | 2 +- src/ast/normal_forms/defined_names.cpp | 2 +- src/ast/normal_forms/name_exprs.cpp | 2 +- src/model/model.cpp | 4 +-- src/muz/spacer/spacer_context.cpp | 2 +- src/muz/spacer/spacer_proof_utils.cpp | 2 +- src/opt/opt_context.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/qe/qe_lite.cpp | 2 +- src/qe/qe_solve_plugin.cpp | 2 +- src/sat/ba_solver.cpp | 2 +- src/sat/sat_drat.cpp | 2 +- src/sat/sat_local_search.cpp | 2 +- src/sat/sat_local_search.h | 2 +- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_solver.cpp | 8 +++--- src/sat/tactic/goal2sat.cpp | 6 ++--- src/smt/smt_context.h | 2 +- src/smt/smt_model_checker.cpp | 2 +- src/smt/tactic/smt_tactic.cpp | 4 +-- src/smt/theory_lra.cpp | 14 +++++----- src/smt/theory_pb.cpp | 32 +++++++++++------------ src/smt/theory_pb.h | 2 +- src/smt/theory_seq.cpp | 4 +-- src/smt/theory_str.cpp | 26 +++++++++--------- src/smt/theory_str.h | 2 +- src/solver/parallel_tactic.cpp | 2 +- src/solver/solver_na2as.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/lia2card_tactic.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 2 +- src/tactic/generic_model_converter.h | 2 +- src/tactic/portfolio/solver2lookahead.cpp | 2 +- src/tactic/proof_converter.cpp | 2 +- src/tactic/sine_filter.cpp | 2 +- src/tactic/tactical.cpp | 4 +-- src/test/main.cpp | 6 ++--- src/test/smt2print_parse.cpp | 2 +- src/util/lp/nra_solver.cpp | 2 +- src/util/obj_ref.h | 2 +- 44 files changed, 98 insertions(+), 98 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 52be66e77..a28315cda 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -468,7 +468,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_symbol_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; @@ -486,7 +486,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_sort_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -504,7 +504,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_ast_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -522,7 +522,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_func_decl_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -596,7 +596,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_domain(c, d, i); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (i >= to_func_decl(d)->get_arity()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index cb3bb7478..3d75c3dba 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -163,7 +163,7 @@ extern "C" { if (to_goal_ref(g)->mc()) (*to_goal_ref(g)->mc())(m_ref->m_model); RETURN_Z3(of_model(m_ref)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) { diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 6d6d19d56..49aa09727 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -155,7 +155,7 @@ extern "C" { expr_ref result(mk_c(c)->m()); if (num_decls == 0) { SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); - RETURN_Z3(0); + RETURN_Z3(nullptr); } sort* const* ts = reinterpret_cast(types); @@ -166,7 +166,7 @@ extern "C" { result = mk_c(c)->m().mk_lambda(names.size(), ts, names.c_ptr(), to_expr(body)); mk_c(c)->save_ast_trail(result.get()); return of_ast(result.get()); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, @@ -178,7 +178,7 @@ extern "C" { RESET_ERROR_CODE(); if (num_decls == 0) { SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); - RETURN_Z3(0); + RETURN_Z3(nullptr); } svector _names; @@ -196,7 +196,7 @@ extern "C" { result = mk_c(c)->m().mk_lambda(_vars.size(), _vars.c_ptr(), _names.c_ptr(), result); mk_c(c)->save_ast_trail(result.get()); return of_ast(result.get()); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 5a4537a4a..fc4e01f3a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -369,7 +369,7 @@ extern "C" { v->m_ast_vector.push_back(f); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { @@ -384,7 +384,7 @@ extern "C" { v->m_ast_vector.push_back(f); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { @@ -631,7 +631,7 @@ extern "C" { } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); - return 0; + return nullptr; } } Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); @@ -644,7 +644,7 @@ extern "C" { to_ast_vector_ref(vs).push_back(a); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 65d3c7821..8750425a8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -424,7 +424,7 @@ sort * get_sort(expr const * n) { return to_quantifier(n)->get_sort(); default: UNREACHABLE(); - return 0; + return nullptr; } } diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index b63c947a9..88ded842f 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -221,7 +221,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i))); } array_util autil(m); - func_decl * f = 0; + func_decl * f = nullptr; if (autil.is_as_array(n2, f)) { n3 = m.mk_app(f, args.size()-1, args.c_ptr() + 1); } diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp index 5e9af1c2d..bb2543b3e 100644 --- a/src/ast/normal_forms/name_exprs.cpp +++ b/src/ast/normal_forms/name_exprs.cpp @@ -127,7 +127,7 @@ class name_nested_formulas : public name_exprs_core { ast_manager & m; expr * m_root; - pred(ast_manager & m):m(m), m_root(0) {} + pred(ast_manager & m):m(m), m_root(nullptr) {} bool operator()(expr * t) override { TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m) << "\n";); diff --git a/src/model/model.cpp b/src/model/model.cpp index 83adfc87e..a1fdfc980 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -351,7 +351,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) { expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) { - if (!e) return expr_ref(0, m); + if (!e) return expr_ref(nullptr, m); TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";); @@ -453,7 +453,7 @@ void model::remove_decls(ptr_vector & decls, func_decl_set const & s) expr_ref model::get_inlined_const_interp(func_decl* f) { expr* v = get_const_interp(f); - if (!v) return expr_ref(0, m); + if (!v) return expr_ref(nullptr, m); top_sort st(m); expr_ref result1(v, m); expr_ref result2 = cleanup_expr(st, v, UINT_MAX); diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index dd6656954..30b68ebf6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1325,7 +1325,7 @@ bool pred_transformer::is_qblocked (pob &n) { // assert cti s->assert_expr(n.post()); - lbool res = s->check_sat(0, 0); + lbool res = s->check_sat(0, nullptr); // if (res == l_false) { // expr_ref_vector core(m); diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index ed02513f1..a73d24d49 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -600,7 +600,7 @@ namespace spacer { proof* hypothesis_reducer::reduce_core(proof* pf) { SASSERT(m.is_false(m.get_fact(pf))); - proof *res = NULL; + proof *res = nullptr; ptr_vector todo; todo.push_back(pf); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b1296f71e..87da85af5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -281,7 +281,7 @@ namespace opt { symbol pri = optp.priority(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); - lbool is_sat = s.check_sat(0,0); + lbool is_sat = s.check_sat(0,nullptr); TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 403ea4c85..1a16b817b 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2608,7 +2608,7 @@ namespace smt2 { check_rparen("invalid get-value command, ')' expected"); model_ref md; - if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == 0) + if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == nullptr) throw cmd_exception("model is not available"); if (index != 0) { m_ctx.get_opt()->get_box_model(md, index); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index da45d17ca..d900bff5d 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -394,7 +394,7 @@ namespace eq { expr* const* args = &e; if (is_lambda(q)) { r = q; - pr = 0; + pr = nullptr; return; } flatten_args(q, num_args, args); diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp index 6ec840de1..dae1faf6f 100644 --- a/src/qe/qe_solve_plugin.cpp +++ b/src/qe/qe_solve_plugin.cpp @@ -156,7 +156,7 @@ namespace qe { std::swap(e1, e2); } // y + -1*x == 0 --> y = x - expr *a0 = 0, *a1 = 0, *x = 0; + expr *a0 = nullptr, *a1 = nullptr, *x = nullptr; if (a.is_zero(e2) && a.is_add(e1, a0, a1)) { if (a.is_times_minus_one(a1, x)) { e1 = a0; diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index de6635d09..4f06c2e98 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1527,7 +1527,7 @@ namespace sat { return p; } - ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { + ba_solver::ba_solver(): m_solver(nullptr), m_lookahead(nullptr), m_unit_walk(nullptr), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); m_num_propagations_since_pop = 0; } diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 00a3fa076..932e9b35e 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -26,7 +26,7 @@ Notes: namespace sat { drat::drat(solver& s): s(s), - m_out(0), + m_out(nullptr), m_inconsistent(false), m_check_unsat(false), m_check_sat(false), diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index af2447fc2..9b79e2964 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -529,7 +529,7 @@ namespace sat { } lbool local_search::check() { - return check(0, 0); + return check(0, nullptr); } #define PROGRESS(tries, flips) \ diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 8a63898c3..5fd69a740 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -277,7 +277,7 @@ namespace sat { lbool check(); - lbool check(unsigned sz, literal const* assumptions, parallel* p = 0); + lbool check(unsigned sz, literal const* assumptions, parallel* p = nullptr); local_search_config& config() { return m_config; } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index c252efb69..bbc1106bb 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -33,7 +33,7 @@ namespace sat { } lookahead::scoped_ext::~scoped_ext() { - if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(0); + if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(nullptr); } lookahead::scoped_assumptions::scoped_assumptions(lookahead& p, literal_vector const& lits): p(p), lits(lits) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 59cb2aac4..b58d2296b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -66,13 +66,13 @@ namespace sat { m_next_simplify = 0; m_num_checkpoints = 0; m_simplifications = 0; - m_ext = 0; + m_ext = nullptr; m_cuber = nullptr; m_mc.set_solver(this); } solver::~solver() { - m_ext = 0; + m_ext = nullptr; SASSERT(check_invariant()); TRACE("sat", tout << "Delete clauses\n";); del_clauses(m_clauses); @@ -1157,7 +1157,7 @@ namespace sat { srch.config().set_config(m_config); srch.import(*this, false); scoped_rl.push_child(&srch.rlimit()); - lbool r = srch.check(num_lits, lits, 0); + lbool r = srch.check(num_lits, lits, nullptr); m_model = srch.get_model(); // srch.collect_statistics(m_aux_stats); return r; @@ -1294,7 +1294,7 @@ namespace sat { if (!canceled) { rlimit().reset_cancel(); } - set_par(0, 0); + set_par(nullptr, 0); ls.reset(); uw.reset(); if (finished_id == -1) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index dc4dfc3a8..d42a28ac0 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -72,7 +72,7 @@ struct goal2sat::imp { imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): m(_m), pb(m), - m_ext(0), + m_ext(nullptr), m_solver(s), m_map(map), m_dep2asm(dep2asm), @@ -1063,7 +1063,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { expr_ref sat2goal::mc::lit2expr(sat::literal l) { if (!m_var2expr.get(l.var())) { - app* aux = m.mk_fresh_const(0, m.mk_bool_sort()); + app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); m_var2expr.set(l.var(), aux); if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); m_gmc->hide(aux->get_decl()); @@ -1107,7 +1107,7 @@ struct sat2goal::imp { SASSERT(m_lit2expr.get((~l).index()) == 0); app* aux = mc ? mc->var2expr(l.var()) : nullptr; if (!aux) { - aux = m.mk_fresh_const(0, m.mk_bool_sort()); + aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); if (mc) { mc->insert(l.var(), aux, true); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ff92f6f95..5733829a3 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -565,7 +565,7 @@ namespace smt { return m_asserted_formulas.has_quantifiers(); } - fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = 0) { + fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) { return m_fingerprints.insert(data, data_hash, num_args, args, def); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index c3af41dcf..02b0e16be 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -577,7 +577,7 @@ namespace smt { } if (inst.m_def) { - m_context->internalize_assertion(inst.m_def, 0, gen); + m_context->internalize_assertion(inst.m_def, nullptr, gen); } TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n"; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 50fe47985..6aa365383 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -217,7 +217,7 @@ public: model_ref md; m_ctx->get_model(md); buffer r; - m_ctx->get_relevant_labels(0, r); + m_ctx->get_relevant_labels(nullptr, r); labels_vec rv; rv.append(r.size(), r.c_ptr()); model_converter_ref mc; @@ -270,7 +270,7 @@ public: model_ref md; m_ctx->get_model(md); buffer r; - m_ctx->get_relevant_labels(0, r); + m_ctx->get_relevant_labels(nullptr, r); labels_vec rv; rv.append(r.size(), r.c_ptr()); in->add(model_and_labels2model_converter(md.get(), rv)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5b1de851e..db031d043 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1054,7 +1054,7 @@ public: // to_int (to_real x) = x // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1 void mk_to_int_axiom(app* n) { - expr* x = 0, *y = 0; + expr* x = nullptr, *y = nullptr; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { mk_axiom(th.mk_eq(y, n, false)); @@ -1070,7 +1070,7 @@ public: // is_int(x) <=> to_real(to_int(x)) = x void mk_is_int_axiom(app* n) { - expr* x = 0; + expr* x = nullptr; VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); @@ -1450,7 +1450,7 @@ public: st = FC_GIVEUP; break; } - if (m_not_handled != 0) { + if (m_not_handled != nullptr) { TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); st = FC_GIVEUP; } @@ -2080,12 +2080,12 @@ public: m_core2.push_back(~c); } m_core2.push_back(lit); - justification * js = 0; + justification * js = nullptr; if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(), m_params.size(), m_params.c_ptr()); } - ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } else { ctx().assign( @@ -2140,7 +2140,7 @@ public: rational const& k1 = b.get_value(); lp_bounds & bounds = m_bounds[v]; - lp_api::bound* end = 0; + lp_api::bound* end = nullptr; lp_api::bound* lo_inf = end, *lo_sup = end; lp_api::bound* hi_inf = end, *hi_sup = end; @@ -2798,7 +2798,7 @@ public: justification* js = ctx().mk_justification( ext_theory_eq_propagation_justification( - get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, 0)); + get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); TRACE("arith", for (unsigned i = 0; i < m_core.size(); ++i) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index e389c819e..2fb0187f8 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -897,7 +897,7 @@ namespace smt { void theory_pb::watch_literal(literal lit, card* c) { init_watch(lit.var()); ptr_vector* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()]; - if (cards == 0) { + if (cards == nullptr) { cards = alloc(ptr_vector); m_var_infos[lit.var()].m_lit_cwatch[lit.sign()] = cards; } @@ -961,13 +961,13 @@ namespace smt { void theory_pb::add_clause(card& c, literal_vector const& lits) { m_stats.m_num_conflicts++; context& ctx = get_context(); - justification* js = 0; + justification* js = nullptr; c.inc_propagations(*this); if (!resolve_conflict(c, lits)) { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } SASSERT(ctx.inconsistent()); } @@ -1027,7 +1027,7 @@ namespace smt { } void theory_pb::assign_eh(bool_var v, bool is_true) { - ptr_vector* ineqs = 0; + ptr_vector* ineqs = nullptr; context& ctx = get_context(); literal nlit(v, is_true); init_watch(v); @@ -1060,7 +1060,7 @@ namespace smt { } ptr_vector* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()]; - if (cards != 0 && !cards->empty() && !ctx.inconsistent()) { + if (cards != nullptr && !cards->empty() && !ctx.inconsistent()) { ptr_vector::iterator it = cards->begin(), it2 = it, end = cards->end(); for (; it != end; ++it) { if (ctx.get_assignment((*it)->lit()) != l_true) { @@ -1088,7 +1088,7 @@ namespace smt { } card* crd = m_var_infos[v].m_card; - if (crd != 0 && !ctx.inconsistent()) { + if (crd != nullptr && !ctx.inconsistent()) { crd->init_watch(*this, is_true); } @@ -1527,7 +1527,7 @@ namespace smt { else { z++; clear_watch(*c); - m_var_infos[v].m_card = 0; + m_var_infos[v].m_card = nullptr; dealloc(c); m_card_trail[i] = null_bool_var; ctx.remove_watch(v); @@ -1671,7 +1671,7 @@ namespace smt { if (v != null_bool_var) { card* c = m_var_infos[v].m_card; clear_watch(*c); - m_var_infos[v].m_card = 0; + m_var_infos[v].m_card = nullptr; dealloc(c); } } @@ -1774,11 +1774,11 @@ namespace smt { context& ctx = get_context(); TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - " << lits << "\n"; display(tout, c, true);); - justification* js = 0; + justification* js = nullptr; if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } @@ -1894,11 +1894,11 @@ namespace smt { break; case b_justification::JUSTIFICATION: { justification* j = js.get_justification(); - card_justification* pbj = 0; + card_justification* pbj = nullptr; if (j->get_from_theory() == get_id()) { pbj = dynamic_cast(j); } - if (pbj != 0) { + if (pbj != nullptr) { card& c2 = pbj->get_card(); result = card2expr(c2); } @@ -2170,11 +2170,11 @@ namespace smt { VERIFY(internalize_card(atl, false)); bool_var abv = ctx.get_bool_var(atl); m_antecedents.push_back(literal(abv)); - justification* js = 0; + justification* js = nullptr; if (proofs_enabled()) { - js = 0; // + js = nullptr; } - ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) { @@ -2403,7 +2403,7 @@ namespace smt { } #endif SASSERT(validate_antecedents(m_antecedents)); - ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0))); + ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr))); DEBUG_CODE( m_antecedents.push_back(~alit); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 7e9c55a12..3a0ee723f 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -258,7 +258,7 @@ namespace smt { card_watch* m_lit_cwatch[2]; card* m_card; - var_info(): m_var_watch(0), m_ineq(0), m_card(0) + var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr) { m_lit_watch[0] = nullptr; m_lit_watch[1] = nullptr; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 857691b8b..233be9e31 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1120,7 +1120,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons break; } if (flag) { - expr* nl_fst = 0; + expr* nl_fst = nullptr; if (e.rs().size()>1 && is_var(e.rs().get(0))) nl_fst = e.rs().get(0); if (nl_fst && nl_fst != r_fst) { @@ -1173,7 +1173,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons break; } if (flag) { - expr* nl_fst = 0; + expr* nl_fst = nullptr; if (e.rs().size()>1 && is_var(e.rs().get(0))) nl_fst = e.rs().get(0); if (nl_fst && nl_fst != r_fst) { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index aadcb63a7..d902aa533 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6745,8 +6745,8 @@ namespace smt { } unsigned theory_str::estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2) { - ENSURE(aut1 != NULL); - ENSURE(aut2 != NULL); + ENSURE(aut1 != nullptr); + ENSURE(aut2 != nullptr); return _qmul(aut1->num_states(), aut2->num_states()); } @@ -6999,7 +6999,7 @@ namespace smt { * and the equality with 0 is based on whether solutions of length 0 are allowed. */ void theory_str::find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -7051,7 +7051,7 @@ namespace smt { * if it exists, or -1 otherwise. */ bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); if (aut->final_states().size() < 1) { // no solutions at all @@ -7161,7 +7161,7 @@ namespace smt { * if a shorter solution exists, or -1 otherwise. */ bool theory_str::refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); if (aut->final_states().empty()) { // no solutions at all! @@ -7280,7 +7280,7 @@ namespace smt { return retval; } else { TRACE("str", tout << "ERROR: unrecognized automaton path constraint " << mk_pp(cond, m) << ", cannot translate" << std::endl;); - retval = NULL; + retval = nullptr; return retval; } } @@ -7293,7 +7293,7 @@ namespace smt { * are returned in `characterConstraints`. */ expr_ref theory_str::generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -10582,12 +10582,12 @@ namespace smt { } } // foreach(term in str_in_re_terms) - eautomaton * aut_inter = NULL; + eautomaton * aut_inter = nullptr; CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;); for (svector::iterator aut_it = intersect_constraints.begin(); aut_it != intersect_constraints.end(); ++aut_it) { regex_automaton_under_assumptions aut = *aut_it; - if (aut_inter == NULL) { + if (aut_inter == nullptr) { // start somewhere aut_inter = aut.get_automaton(); used_intersect_constraints.push_back(aut); @@ -10637,7 +10637,7 @@ namespace smt { } } } // foreach(entry in intersect_constraints) - if (aut_inter != NULL) { + if (aut_inter != nullptr) { aut_inter->compress(); } TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;); @@ -10668,7 +10668,7 @@ namespace smt { } conflict_lhs = mk_and(conflict_terms); - if (used_intersect_constraints.size() > 1 && aut_inter != NULL) { + if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) { // check whether the intersection is only the empty string unsigned initial_state = aut_inter->init(); if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) { @@ -10686,7 +10686,7 @@ namespace smt { } } - if (aut_inter != NULL && aut_inter->is_empty()) { + if (aut_inter != nullptr && aut_inter->is_empty()) { TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;); expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); assert_axiom(conflict_clause); @@ -12231,7 +12231,7 @@ namespace smt { // - in the same EQC as freeVar if (term_appears_as_subterm(freeVar, re_str)) { TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;); - return NULL; + return nullptr; } } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 419084091..b626c5b07 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -164,7 +164,7 @@ protected: rational upper_bound; public: regex_automaton_under_assumptions() : - re_term(NULL), aut(NULL), polarity(false), + re_term(nullptr), aut(nullptr), polarity(false), assume_lower_bound(false), assume_upper_bound(false) {} regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) : diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 142ba4bb8..f0bb65315 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -676,7 +676,7 @@ public: fail_if_proof_generation("parallel-tactic", g); ast_manager& m = g->m(); solver* s = m_solver->translate(m, m_params); - solver_state* st = alloc(solver_state, 0, s, m_params); + solver_state* st = alloc(solver_state, nullptr, s, m_params); m_queue.add_task(st); expr_ref_vector clauses(m); ptr_vector assumptions; diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 41853b19a..a3fcd0e0b 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -31,7 +31,7 @@ solver_na2as::solver_na2as(ast_manager & m): solver_na2as::~solver_na2as() {} void solver_na2as::assert_expr_core2(expr * t, expr * a) { - if (a == 0) { + if (a == nullptr) { assert_expr_core(t); } else { diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index c15285703..b713c3055 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -204,7 +204,7 @@ class degree_shift_tactic : public tactic { for (auto const& kv : m_var2degree) { SASSERT(kv.m_value.is_int()); SASSERT(kv.m_value >= rational(2)); - app * fresh = m.mk_fresh_const(0, kv.m_key->get_decl()->get_range()); + app * fresh = m.mk_fresh_const(nullptr, kv.m_key->get_decl()->get_range()); m_pinned.push_back(fresh); m_var2var.insert(kv.m_key, fresh); if (m_produce_models) { diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 88e4a5583..027b6d91c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -36,7 +36,7 @@ class lia2card_tactic : public tactic { expr* m_expr; bound(unsigned lo, unsigned hi, expr* b): m_lo(lo), m_hi(hi), m_expr(b) {} - bound(): m_lo(0), m_hi(0), m_expr(0) {} + bound(): m_lo(0), m_hi(0), m_expr(nullptr) {} }; struct lia_rewriter_cfg : public default_rewriter_cfg { diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index a864d9631..185f23d13 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -148,7 +148,7 @@ public: // translate enumeration constants to bit-vectors. for (expr* v : vars) { - func_decl* f = 0; + func_decl* f = nullptr; if (is_app(v) && is_uninterp_const(v) && m_rewriter.enum2bv().find(to_app(v)->get_decl(), f)) { bvars.push_back(m.mk_const(f)); } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index c67dd5eff..69bc35a3f 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -45,7 +45,7 @@ public: void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } - void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); } + void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); } void add(func_decl * d, expr* e); diff --git a/src/tactic/portfolio/solver2lookahead.cpp b/src/tactic/portfolio/solver2lookahead.cpp index 0c18ab079..63b28793d 100644 --- a/src/tactic/portfolio/solver2lookahead.cpp +++ b/src/tactic/portfolio/solver2lookahead.cpp @@ -20,5 +20,5 @@ Notes: #include "solver/solver.h" solver * mk_solver2lookahead(solver* s) { - return 0; + return nullptr; } diff --git a/src/tactic/proof_converter.cpp b/src/tactic/proof_converter.cpp index f1a209487..faa9a36db 100644 --- a/src/tactic/proof_converter.cpp +++ b/src/tactic/proof_converter.cpp @@ -130,7 +130,7 @@ proof_ref apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_ for (unsigned i = 0; i < sz; i++) { proof_ref pr(m); SASSERT(pc2s[i]); // proof production is enabled - pr = pc2s[i]->operator()(m, 0, 0); + pr = pc2s[i]->operator()(m, 0, nullptr); prs.push_back(pr); } return (*pc1)(m, sz, prs.c_ptr()); diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index b1db12964..1612670a4 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -54,7 +54,7 @@ public: TRACE("sine", tout << new_forms.size();); g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) { - g->assert_expr(new_forms.get(i), 0, 0); + g->assert_expr(new_forms.get(i), nullptr, nullptr); } g->inc_depth(); g->updt_prec(goal::OVER); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 43087f50f..a71ea738c 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -636,7 +636,7 @@ public: else { SASSERT(is_decided_unsat(r2)); - if (cores_enabled && r2[0]->dep(0) != 0) { + if (cores_enabled && r2[0]->dep(0) != nullptr) { expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m); *new_dep = r2[0]->dep(0); core_buffer.set(i, new_dep); @@ -674,7 +674,7 @@ public: ast_translation translator(*(managers[i]), m, false); goal_ref_buffer * r = goals_vect[i]; unsigned j = result.size(); - if (r != 0) { + if (r != nullptr) { for (unsigned k = 0; k < r->size(); k++) { result.push_back((*r)[k]->translate(translator)); } diff --git a/src/test/main.cpp b/src/test/main.cpp index d330610d9..811b67407 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -78,11 +78,11 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t int i = 1; while (i < argc) { char * arg = argv[i]; - char * eq_pos = 0; + char * eq_pos = nullptr; if (arg[0] == '-' || arg[0] == '/') { char * opt_name = arg + 1; - char * opt_arg = 0; + char * opt_arg = nullptr; char * colon = strchr(arg, ':'); if (colon) { opt_arg = colon + 1; @@ -97,7 +97,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t else if (strcmp(opt_name, "v") == 0) { if (!opt_arg) error("option argument (/v:level) is missing."); - long lvl = strtol(opt_arg, 0, 10); + long lvl = strtol(opt_arg, nullptr, 10); set_verbosity_level(lvl); } else if (strcmp(opt_name, "w") == 0) { diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 99ffb726c..81b7ba1e9 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -19,7 +19,7 @@ void test_print(Z3_context ctx, Z3_ast_vector av) { Z3_ast a = Z3_mk_and(ctx, Z3_ast_vector_size(ctx, av), args); Z3_inc_ref(ctx, a); delete[] args; - char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a); + char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", nullptr, nullptr, nullptr, 0, nullptr, a); Z3_dec_ref(ctx, a); std::cout << "spec1: benchmark->string\n" << spec1 << "\n"; diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index 0d28058e8..200bdd2bc 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -154,7 +154,7 @@ namespace nra { polynomial::polynomial* ps[1] = { p }; bool even[1] = { false }; nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even); - m_nlsat->mk_clause(1, &lit, 0); + m_nlsat->mk_clause(1, &lit, nullptr); } void add_constraint(unsigned idx) { diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 885601375..8908f2cdd 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -115,7 +115,7 @@ public: */ T * steal() { T * r = m_obj; - m_obj = 0; + m_obj = nullptr; return r; } };