From 19eb7225ea6bc4fab1bc9aa742e203e5344b38f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 16:20:05 -0700 Subject: [PATCH] add virtual destructor to z3::object class Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5d0d9425e52..4025be4fdbf 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -509,7 +509,7 @@ namespace z3 { object::operator=(o); return *this; } - ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); } + ~param_descrs() override { Z3_param_descrs_dec_ref(ctx(), m_descrs); } static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); } static param_descrs global_param_descrs(context& c) { return param_descrs(c, Z3_get_global_param_descrs(c)); } @@ -527,7 +527,7 @@ namespace z3 { public: params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); } params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); } - ~params() { Z3_params_dec_ref(ctx(), m_params); } + ~params() override { Z3_params_dec_ref(ctx(), m_params); } operator Z3_params() const { return m_params; } params & operator=(params const & s) { Z3_params_inc_ref(s.ctx(), s.m_params); @@ -555,7 +555,7 @@ namespace z3 { 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(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() override { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } } operator Z3_ast() const { return m_ast; } operator bool() const { return m_ast != 0; } ast & operator=(ast const & s) { @@ -593,7 +593,7 @@ namespace z3 { ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); } ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); } - ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); } + ~ast_vector_tpl() override { Z3_ast_vector_dec_ref(ctx(), m_vector); } operator Z3_ast_vector() const { return m_vector; } unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } @@ -2528,7 +2528,7 @@ namespace z3 { public: func_entry(context & c, Z3_func_entry e):object(c) { init(e); } func_entry(func_entry const & s):object(s) { init(s.m_entry); } - ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); } + ~func_entry() override { Z3_func_entry_dec_ref(ctx(), m_entry); } operator Z3_func_entry() const { return m_entry; } func_entry & operator=(func_entry const & s) { Z3_func_entry_inc_ref(s.ctx(), s.m_entry); @@ -2551,7 +2551,7 @@ namespace z3 { public: func_interp(context & c, Z3_func_interp e):object(c) { init(e); } func_interp(func_interp const & s):object(s) { init(s.m_interp); } - ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); } + ~func_interp() override { Z3_func_interp_dec_ref(ctx(), m_interp); } operator Z3_func_interp() const { return m_interp; } func_interp & operator=(func_interp const & s) { Z3_func_interp_inc_ref(s.ctx(), s.m_interp); @@ -2585,7 +2585,7 @@ namespace z3 { model(context & c, Z3_model m):object(c) { init(m); } model(model const & s):object(s) { init(s.m_model); } model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); } - ~model() { Z3_model_dec_ref(ctx(), m_model); } + ~model() override { Z3_model_dec_ref(ctx(), m_model); } operator Z3_model() const { return m_model; } model & operator=(model const & s) { Z3_model_inc_ref(s.ctx(), s.m_model); @@ -2665,7 +2665,7 @@ namespace z3 { stats(context & c):object(c), m_stats(0) {} stats(context & c, Z3_stats e):object(c) { init(e); } stats(stats const & s):object(s) { init(s.m_stats); } - ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } + ~stats() override { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } operator Z3_stats() const { return m_stats; } stats & operator=(stats const & s) { Z3_stats_inc_ref(s.ctx(), s.m_stats); @@ -2747,7 +2747,7 @@ namespace z3 { solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); } solver(solver const & s):object(s) { init(s.m_solver); } solver(solver const& s, simplifier const& simp); - ~solver() { Z3_solver_dec_ref(ctx(), m_solver); } + ~solver() override { Z3_solver_dec_ref(ctx(), m_solver); } operator Z3_solver() const { return m_solver; } solver & operator=(solver const & s) { Z3_solver_inc_ref(s.ctx(), s.m_solver); @@ -2968,7 +2968,7 @@ namespace z3 { goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); } goal(context & c, Z3_goal s):object(c) { init(s); } goal(goal const & s):object(s) { init(s.m_goal); } - ~goal() { Z3_goal_dec_ref(ctx(), m_goal); } + ~goal() override { Z3_goal_dec_ref(ctx(), m_goal); } operator Z3_goal() const { return m_goal; } goal & operator=(goal const & s) { Z3_goal_inc_ref(s.ctx(), s.m_goal); @@ -3026,7 +3026,7 @@ namespace z3 { public: apply_result(context & c, Z3_apply_result s):object(c) { init(s); } apply_result(apply_result const & s):object(s) { init(s.m_apply_result); } - ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); } + ~apply_result() override { Z3_apply_result_dec_ref(ctx(), m_apply_result); } operator Z3_apply_result() const { return m_apply_result; } apply_result & operator=(apply_result const & s) { Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result); @@ -3051,7 +3051,7 @@ namespace z3 { tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); } tactic(context & c, Z3_tactic s):object(c) { init(s); } tactic(tactic const & s):object(s) { init(s.m_tactic); } - ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); } + ~tactic() override { Z3_tactic_dec_ref(ctx(), m_tactic); } operator Z3_tactic() const { return m_tactic; } tactic & operator=(tactic const & s) { Z3_tactic_inc_ref(s.ctx(), s.m_tactic); @@ -3137,7 +3137,7 @@ namespace z3 { simplifier(context & c, char const * name):object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); } simplifier(context & c, Z3_simplifier s):object(c) { init(s); } simplifier(simplifier const & s):object(s) { init(s.m_simplifier); } - ~simplifier() { Z3_simplifier_dec_ref(ctx(), m_simplifier); } + ~simplifier() override { Z3_simplifier_dec_ref(ctx(), m_simplifier); } operator Z3_simplifier() const { return m_simplifier; } simplifier & operator=(simplifier const & s) { Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier); @@ -3179,7 +3179,7 @@ namespace z3 { probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); } probe(context & c, Z3_probe s):object(c) { init(s); } probe(probe const & s):object(s) { init(s.m_probe); } - ~probe() { Z3_probe_dec_ref(ctx(), m_probe); } + ~probe() public override { Z3_probe_dec_ref(ctx(), m_probe); } operator Z3_probe() const { return m_probe; } probe & operator=(probe const & s) { Z3_probe_inc_ref(s.ctx(), s.m_probe); @@ -3273,7 +3273,7 @@ namespace z3 { object::operator=(o); return *this; } - ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } + ~optimize() override { Z3_optimize_dec_ref(ctx(), m_opt); } operator Z3_optimize() const { return m_opt; } void add(expr const& e) { assert(e.is_bool()); @@ -3354,7 +3354,7 @@ namespace z3 { public: fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); } - ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } + ~fixedpoint() override { Z3_fixedpoint_dec_ref(ctx(), m_fp); } fixedpoint & operator=(fixedpoint const & o) { Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp); Z3_fixedpoint_dec_ref(ctx(), m_fp);