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

add virtual destructor to z3::object class

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-01 16:20:05 -07:00
parent 231a985bf9
commit 19eb7225ea
1 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/api/c++/z3++.h
View file

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