From 3586b613f7e0cdd404d9c44e51d27d01be08019e Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 2 Oct 2024 22:20:12 +0100
Subject: [PATCH] remove default destructors
---
src/ast/arith_decl_plugin.cpp | 3 --
src/ast/ast_trail.h | 3 +-
src/ast/datatype_decl_plugin.cpp | 5 ----
src/ast/datatype_decl_plugin.h | 1 -
src/ast/expr2polynomial.cpp | 3 --
src/ast/expr2polynomial.h | 1 -
src/ast/fpa/fpa2bv_rewriter.h | 3 --
src/ast/fpa_decl_plugin.cpp | 6 ----
src/ast/fpa_decl_plugin.h | 2 --
src/ast/macros/cond_macro.h | 5 +---
src/ast/macros/macro_finder.cpp | 3 --
src/ast/macros/macro_finder.h | 1 -
src/ast/macros/macro_manager.cpp | 3 --
src/ast/macros/macro_manager.h | 1 -
src/ast/macros/quasi_macros.cpp | 3 --
src/ast/macros/quasi_macros.h | 1 -
src/ast/normal_forms/defined_names.cpp | 5 +---
src/ast/pattern/expr_pattern_match.cpp | 3 --
src/ast/pattern/expr_pattern_match.h | 1 -
src/ast/recfun_decl_plugin.cpp | 3 --
src/ast/recfun_decl_plugin.h | 1 -
src/ast/sls/bvsls_opt_engine.cpp | 4 ---
src/ast/sls/bvsls_opt_engine.h | 1 -
src/cmd_context/cmd_context.cpp | 3 --
src/cmd_context/cmd_context.h | 1 -
src/cmd_context/tactic_cmds.cpp | 4 ---
src/cmd_context/tactic_cmds.h | 3 +-
src/math/lp/core_solver_pretty_printer.cpp | 2 --
src/math/lp/core_solver_pretty_printer.h | 1 -
src/math/lp/core_solver_pretty_printer_def.h | 2 --
src/math/polynomial/algebraic_numbers.cpp | 3 --
src/math/realclosure/mpz_matrix.cpp | 3 --
src/math/realclosure/mpz_matrix.h | 1 -
src/math/realclosure/realclosure.cpp | 2 --
src/model/numeral_factory.cpp | 6 ----
src/model/numeral_factory.h | 2 --
src/model/value_factory.cpp | 3 --
src/model/value_factory.h | 2 +-
src/muz/base/bind_variables.cpp | 3 --
src/muz/base/bind_variables.h | 1 -
src/muz/fp/datalog_parser.cpp | 3 --
src/muz/rel/check_relation.cpp | 2 --
src/muz/rel/check_relation.h | 1 -
src/muz/rel/dl_external_relation.cpp | 3 --
src/muz/rel/dl_external_relation.h | 1 -
src/muz/rel/dl_mk_explanations.cpp | 3 --
src/muz/rel/dl_mk_explanations.h | 2 --
src/muz/transforms/dl_mk_array_blast.cpp | 3 --
src/muz/transforms/dl_mk_array_blast.h | 2 --
.../dl_mk_quantifier_abstraction.cpp | 3 --
.../transforms/dl_mk_quantifier_abstraction.h | 2 --
.../dl_mk_quantifier_instantiation.cpp | 3 --
.../dl_mk_quantifier_instantiation.h | 2 --
src/muz/transforms/dl_mk_scale.cpp | 3 --
src/muz/transforms/dl_mk_scale.h | 1 -
src/nlsat/nlsat_explain.cpp | 3 --
src/nlsat/nlsat_interval_set.cpp | 3 --
src/nlsat/nlsat_interval_set.h | 1 -
src/opt/opt_solver.cpp | 3 --
src/opt/opt_solver.h | 1 -
src/opt/pb_sls.cpp | 3 --
src/parsers/util/simple_parser.cpp | 3 --
src/parsers/util/simple_parser.h | 2 +-
src/sat/sat_local_search.cpp | 7 -----
src/sat/sat_local_search.h | 4 ---
src/sat/sat_model_converter.cpp | 7 -----
src/sat/sat_model_converter.h | 6 ++--
src/sat/smt/euf_proof_checker.cpp | 3 --
src/sat/smt/euf_proof_checker.h | 1 -
src/sat/smt/q_mam.cpp | 3 --
src/sat/smt/specrel_solver.cpp | 3 --
src/sat/smt/specrel_solver.h | 1 -
src/smt/mam.cpp | 3 --
src/smt/qi_queue.cpp | 3 --
src/smt/qi_queue.h | 1 -
src/smt/smt_conflict_resolution.cpp | 3 --
src/smt/smt_conflict_resolution.h | 2 +-
src/smt/smt_theory.cpp | 3 --
src/smt/smt_theory.h | 2 +-
src/smt/theory_arith.h | 1 -
src/smt/theory_arith_core.h | 4 ---
src/smt/theory_bv.cpp | 3 --
src/smt/theory_bv.h | 1 -
src/smt/theory_datatype.cpp | 3 +-
src/solver/assertions/asserted_formulas.cpp | 4 ---
src/solver/assertions/asserted_formulas.h | 1 -
src/solver/check_sat_result.cpp | 3 --
src/solver/check_sat_result.h | 1 -
src/tactic/core/injectivity_tactic.cpp | 3 --
src/tactic/core/simplify_tactic.cpp | 3 --
src/util/hwf.cpp | 4 ---
src/util/hwf.h | 1 -
src/util/map.h | 29 +++++--------------
src/util/obj_hashtable.h | 2 +-
src/util/ref.h | 12 ++++----
95 files changed, 25 insertions(+), 259 deletions(-)
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 67a605869..8e2cbef82 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -34,9 +34,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
m_nums(m_amanager) {
}
- ~algebraic_numbers_wrapper() {
- }
-
unsigned mk_id(algebraic_numbers::anum const & val) {
SASSERT(!m_amanager.is_rational(val));
unsigned idx = m_id_gen.mk();
diff --git a/src/ast/ast_trail.h b/src/ast/ast_trail.h
index 5a76dd537..18c8961e6 100644
--- a/src/ast/ast_trail.h
+++ b/src/ast/ast_trail.h
@@ -33,8 +33,7 @@ class ast2ast_trailmap {
public:
ast2ast_trailmap(ast_manager& m):
m_domain(m),
- m_range(m),
- m_map()
+ m_range(m)
{}
bool find(S* s, T*& t) {
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index cc5c6eb75..e5ab4a806 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -1040,11 +1040,6 @@ namespace datatype {
return m_family_id;
}
-
- util::~util() {
-
- }
-
ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = nullptr;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index ca33b48c1..dcca78970 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -338,7 +338,6 @@ namespace datatype {
public:
util(ast_manager & m);
- ~util();
ast_manager & get_manager() const { return m; }
// sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params);
bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index a69d5b436..3bcd7367a 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -504,9 +504,6 @@ default_expr2polynomial::default_expr2polynomial(ast_manager & am, polynomial::m
expr2polynomial(am, pm, nullptr) {
}
-default_expr2polynomial::~default_expr2polynomial() {
-}
-
bool default_expr2polynomial::is_int(polynomial::var x) const {
return m_is_int[x];
}
diff --git a/src/ast/expr2polynomial.h b/src/ast/expr2polynomial.h
index 1d89587c4..b3356e9e0 100644
--- a/src/ast/expr2polynomial.h
+++ b/src/ast/expr2polynomial.h
@@ -102,7 +102,6 @@ class default_expr2polynomial : public expr2polynomial {
bool_vector m_is_int;
public:
default_expr2polynomial(ast_manager & am, polynomial::manager & pm);
- ~default_expr2polynomial() override;
bool is_int(polynomial::var x) const override;
protected:
polynomial::var mk_var(bool is_int) override;
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 42467c219..f68de5e32 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -36,9 +36,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
- ~fpa2bv_rewriter_cfg() {
- }
-
void cleanup_buffers() {
m_out.finalize();
}
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 76e44278d..3bdc19d5e 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -47,9 +47,6 @@ void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
}
-fpa_decl_plugin::~fpa_decl_plugin() {
-}
-
unsigned fpa_decl_plugin::mk_id(mpf const & v) {
unsigned new_id = m_id_gen.mk();
m_values.reserve(new_id+1);
@@ -961,9 +958,6 @@ fpa_util::fpa_util(ast_manager & m):
m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
}
-fpa_util::~fpa_util() {
-}
-
sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) {
parameter ps[2] = { parameter(ebits), parameter(sbits) };
return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps);
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 0357efa47..39b3fc33c 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -175,7 +175,6 @@ public:
bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
- ~fpa_decl_plugin() override;
void finalize() override;
decl_plugin * mk_fresh() override;
@@ -216,7 +215,6 @@ class fpa_util {
public:
fpa_util(ast_manager & m);
- ~fpa_util();
ast_manager & m() const { return m_manager; }
mpf_manager & fm() const { return m_plugin->fm(); }
diff --git a/src/ast/macros/cond_macro.h b/src/ast/macros/cond_macro.h
index 7e8064ac6..0dc3c1e0b 100644
--- a/src/ast/macros/cond_macro.h
+++ b/src/ast/macros/cond_macro.h
@@ -39,10 +39,7 @@ public:
m_weight(weight) {
SASSERT(!m_hint || !m_cond);
}
-
- ~cond_macro() {
- }
-
+
func_decl * get_f() const { return m_f; }
expr * get_def() const { return m_def; }
diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index bc63aae8e..3006e383c 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -269,9 +269,6 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
m_autil(m) {
}
-macro_finder::~macro_finder() {
-}
-
bool macro_finder::expand_macros(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "starting expand_macros:\n";
m_macro_manager.display(tout););
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 91e5deeb9..fe2722172 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -43,7 +43,6 @@ class macro_finder {
public:
macro_finder(ast_manager & m, macro_manager & mm);
- ~macro_finder();
void operator()(expr_ref_vector const& exprs, proof_ref_vector const& prs, expr_dependency_ref_vector const& deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
void operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
};
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index b7c94b1b5..824573d46 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -41,9 +41,6 @@ macro_manager::macro_manager(ast_manager & m):
m_util.set_forbidden_set(&m_forbidden_set);
}
-macro_manager::~macro_manager() {
-}
-
void macro_manager::push_scope() {
m_scopes.push_back(scope());
scope & s = m_scopes.back();
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 758e3c1a7..9d8831c30 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -64,7 +64,6 @@ class macro_manager {
public:
macro_manager(ast_manager & m);
- ~macro_manager();
void copy_to(macro_manager& dst);
ast_manager & get_manager() const { return m; }
macro_util & get_util() { return m_util; }
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index dff36278d..b65daf063 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -31,9 +31,6 @@ quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
m_new_qsorts(m) {
}
-quasi_macros::~quasi_macros() {
-}
-
void quasi_macros::find_occurrences(expr * e) {
unsigned j;
m_todo.reset();
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 4441f432e..2b5350cf0 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -60,7 +60,6 @@ class quasi_macros {
public:
quasi_macros(ast_manager & m, macro_manager & mm);
- ~quasi_macros();
/**
\brief Find pure function macros and apply them.
diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp
index c931c6fad..4e9ee6263 100644
--- a/src/ast/normal_forms/defined_names.cpp
+++ b/src/ast/normal_forms/defined_names.cpp
@@ -57,7 +57,7 @@ struct defined_names::impl {
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
- virtual ~impl();
+ virtual ~impl() = default;
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
@@ -90,9 +90,6 @@ defined_names::impl::impl(ast_manager & m, char const * prefix):
m_z3name = prefix;
}
-defined_names::impl::~impl() {
-}
-
/**
\brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
where sk is a fresh variable name, and x_i's are the free variables of \c e.
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index 8ae0dcbf2..2fbd99bdf 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -41,9 +41,6 @@ expr_pattern_match::expr_pattern_match(ast_manager & manager):
m_manager(manager), m_precompiled(manager) {
}
-expr_pattern_match::~expr_pattern_match() {
-}
-
bool
expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
if (m_regs.empty()) {
diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h
index 2fd0b4b73..11939e1de 100644
--- a/src/ast/pattern/expr_pattern_match.h
+++ b/src/ast/pattern/expr_pattern_match.h
@@ -116,7 +116,6 @@ class expr_pattern_match {
public:
expr_pattern_match(ast_manager & manager);
- ~expr_pattern_match();
bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
unsigned initialize(quantifier* qf);
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 5f2534a51..cba1932be 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -366,9 +366,6 @@ namespace recfun {
m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
}
- util::~util() {
- }
-
def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range, bool is_generated) {
return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
}
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 73e2b5244..d9fe07dcf 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -237,7 +237,6 @@ namespace recfun {
public:
util(ast_manager &m);
- ~util();
ast_manager & m() { return m_manager; }
family_id get_family_id() const { return m_fid; }
diff --git a/src/ast/sls/bvsls_opt_engine.cpp b/src/ast/sls/bvsls_opt_engine.cpp
index 7dc71cd8c..2f006dc9f 100644
--- a/src/ast/sls/bvsls_opt_engine.cpp
+++ b/src/ast/sls/bvsls_opt_engine.cpp
@@ -28,10 +28,6 @@ bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
m_best_model = alloc(model, m);
}
-bvsls_opt_engine::~bvsls_opt_engine()
-{
-}
-
bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
expr_ref const & objective,
model_ref initial_model,
diff --git a/src/ast/sls/bvsls_opt_engine.h b/src/ast/sls/bvsls_opt_engine.h
index 435fa3af4..25182c156 100644
--- a/src/ast/sls/bvsls_opt_engine.h
+++ b/src/ast/sls/bvsls_opt_engine.h
@@ -31,7 +31,6 @@ class bvsls_opt_engine : public sls_engine {
public:
bvsls_opt_engine(ast_manager & m, params_ref const & p);
- ~bvsls_opt_engine();
class optimization_result {
public:
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e9ca5595f..5f5195bb9 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -2464,9 +2464,6 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner):
m_dt_util(owner.m()) {
}
-cmd_context::dt_eh::~dt_eh() {
-}
-
void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 6dc60c9dd..cd43203a7 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -305,7 +305,6 @@ protected:
public:
void reset() { m_dt_util.reset(); }
dt_eh(cmd_context & owner);
- ~dt_eh() override;
void operator()(sort * dt, pdecl* pd) override;
};
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index a0805110b..b2b858b07 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -27,7 +27,6 @@ Notes:
#include "ast/ast_smt2_pp.h"
#include "tactic/tactic.h"
#include "tactic/tactical.h"
-#include "tactic/probe.h"
#include "solver/check_sat_result.h"
#include "cmd_context/cmd_context_to_goal.h"
#include "cmd_context/echo_tactic.h"
@@ -38,9 +37,6 @@ probe_info::probe_info(symbol const & n, char const * d, probe * p):
m_probe(p) {
}
-probe_info::~probe_info() {
-}
-
class declare_tactic_cmd : public cmd {
symbol m_name;
sexpr * m_decl;
diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h
index 5096ae962..de5fda0a8 100644
--- a/src/cmd_context/tactic_cmds.h
+++ b/src/cmd_context/tactic_cmds.h
@@ -18,12 +18,12 @@ Notes:
#pragma once
#include "ast/ast.h"
+#include "tactic/probe.h"
#include "util/params.h"
#include "util/cmd_context_types.h"
#include "util/ref.h"
class tactic;
-class probe;
typedef tactic* (*tactic_factory)(ast_manager&, const params_ref&);
@@ -52,7 +52,6 @@ class probe_info {
ref<probe> m_probe;
public:
probe_info(symbol const & n, char const * d, probe * p);
- ~probe_info();
symbol get_name() const { return m_name; }
char const * get_descr() const { return m_descr; }
diff --git a/src/math/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp
index 18bef8303..65a9aef97 100644
--- a/src/math/lp/core_solver_pretty_printer.cpp
+++ b/src/math/lp/core_solver_pretty_printer.cpp
@@ -21,7 +21,5 @@ Revision History:
#include "math/lp/core_solver_pretty_printer_def.h"
template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
-template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> > &, std::ostream & out);
-template lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::~core_solver_pretty_printer();
template void lp::core_solver_pretty_printer<lp::mpq, lp::numeric_pair<lp::mpq> >::print();
diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h
index 5bf29d511..c9ab99760 100644
--- a/src/math/lp/core_solver_pretty_printer.h
+++ b/src/math/lp/core_solver_pretty_printer.h
@@ -66,7 +66,6 @@ public:
void init_costs();
- ~core_solver_pretty_printer();
void init_rs_width();
T current_column_norm();
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index cbe67ea36..6d35273af 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -67,8 +67,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_co
}
-template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
-}
template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs_width() {
m_rs_width = static_cast<unsigned>(T_to_string(m_core_solver.get_cost()).size());
for (unsigned i = 0; i < nrows(); i++) {
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index b546df706..6cdd735a1 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -121,9 +121,6 @@ namespace algebraic_numbers {
m_y = pm().mk_var();
}
- ~imp() {
- }
-
bool acell_inv(algebraic_cell const& c) {
auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c));
return s == sign_zero || c.m_sign_lower == (s == sign_neg);
diff --git a/src/math/realclosure/mpz_matrix.cpp b/src/math/realclosure/mpz_matrix.cpp
index 3bbd387c6..701b3b26d 100644
--- a/src/math/realclosure/mpz_matrix.cpp
+++ b/src/math/realclosure/mpz_matrix.cpp
@@ -36,9 +36,6 @@ mpz_matrix_manager::mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_al
m_allocator(a) {
}
-mpz_matrix_manager::~mpz_matrix_manager() {
-}
-
void mpz_matrix_manager::mk(unsigned m, unsigned n, mpz_matrix & A) {
SASSERT(m > 0 && n > 0);
del(A);
diff --git a/src/math/realclosure/mpz_matrix.h b/src/math/realclosure/mpz_matrix.h
index 91fe22681..9eb051ed2 100644
--- a/src/math/realclosure/mpz_matrix.h
+++ b/src/math/realclosure/mpz_matrix.h
@@ -63,7 +63,6 @@ class mpz_matrix_manager {
bool solve_core(mpz_matrix const & A, mpz * b, bool int_solver);
public:
mpz_matrix_manager(unsynch_mpz_manager & nm, small_object_allocator & a);
- ~mpz_matrix_manager();
unsynch_mpz_manager & nm() const { return m_nm; }
void mk(unsigned m, unsigned n, mpz_matrix & A);
void del(mpz_matrix & r);
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index ecea560a5..561d6a6d7 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -410,8 +410,6 @@ namespace realclosure {
sbuffer<unsigned> m_szs; // size of each polynomial in the sequence
public:
scoped_polynomial_seq(imp & m):m_seq_coeffs(m) {}
- ~scoped_polynomial_seq() {
- }
/**
\brief Add a new polynomial to the sequence.
diff --git a/src/model/numeral_factory.cpp b/src/model/numeral_factory.cpp
index ba19ec941..6f7aeeb2c 100644
--- a/src/model/numeral_factory.cpp
+++ b/src/model/numeral_factory.cpp
@@ -28,9 +28,6 @@ arith_factory::arith_factory(ast_manager & m):
m_util(m) {
}
-arith_factory::~arith_factory() {
-}
-
app * arith_factory::mk_num_value(rational const & val, bool is_int) {
return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
}
@@ -40,9 +37,6 @@ bv_factory::bv_factory(ast_manager & m):
m_util(m) {
}
-bv_factory::~bv_factory() {
-}
-
app * bv_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);
}
diff --git a/src/model/numeral_factory.h b/src/model/numeral_factory.h
index 174ea8757..ca917d927 100644
--- a/src/model/numeral_factory.h
+++ b/src/model/numeral_factory.h
@@ -34,7 +34,6 @@ class arith_factory : public numeral_factory {
public:
arith_factory(ast_manager & m);
- ~arith_factory() override;
app * mk_num_value(rational const & val, bool is_int);
};
@@ -46,7 +45,6 @@ class bv_factory : public numeral_factory {
public:
bv_factory(ast_manager & m);
- ~bv_factory() override;
app * mk_num_value(rational const & val, unsigned bv_size);
};
diff --git a/src/model/value_factory.cpp b/src/model/value_factory.cpp
index 30fa82caf..c79919199 100644
--- a/src/model/value_factory.cpp
+++ b/src/model/value_factory.cpp
@@ -25,9 +25,6 @@ value_factory::value_factory(ast_manager & m, family_id fid):
m_fid(fid) {
}
-value_factory::~value_factory() {
-}
-
basic_factory::basic_factory(ast_manager & m, unsigned seed):
value_factory(m, m.get_basic_family_id()), m_rand(seed) {
}
diff --git a/src/model/value_factory.h b/src/model/value_factory.h
index 20c383efe..85515495b 100644
--- a/src/model/value_factory.h
+++ b/src/model/value_factory.h
@@ -31,7 +31,7 @@ protected:
public:
value_factory(ast_manager & m, family_id fid);
- virtual ~value_factory();
+ virtual ~value_factory() = default;
/**
\brief Return some value of the given sort. The result is always different from zero.
diff --git a/src/muz/base/bind_variables.cpp b/src/muz/base/bind_variables.cpp
index 5ac41e0bf..d96a49f67 100644
--- a/src/muz/base/bind_variables.cpp
+++ b/src/muz/base/bind_variables.cpp
@@ -25,9 +25,6 @@ bind_variables::bind_variables(ast_manager & m):
m_vars(m),
m_pinned(m)
{}
-
-bind_variables::~bind_variables() {
-}
expr_ref bind_variables::operator()(expr* fml, bool is_forall) {
if (m_vars.empty()) {
diff --git a/src/muz/base/bind_variables.h b/src/muz/base/bind_variables.h
index e231b7039..4c183b507 100644
--- a/src/muz/base/bind_variables.h
+++ b/src/muz/base/bind_variables.h
@@ -40,7 +40,6 @@ class bind_variables {
expr_ref abstract(expr* fml, cache_t& cache, unsigned scope);
public:
bind_variables(ast_manager & m);
- ~bind_variables();
expr_ref operator()(expr* fml, bool is_forall);
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index a15c80609..c6df500d8 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -267,9 +267,6 @@ public:
next();
}
- dlexer() {
- }
-
void set_stream(std::istream* s, char_reader* r) {
m_input = s;
m_reader = r;
diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp
index 24b109f35..454f6d8bc 100644
--- a/src/muz/rel/check_relation.cpp
+++ b/src/muz/rel/check_relation.cpp
@@ -150,8 +150,6 @@ namespace datalog {
m(rm.get_context().get_manager()),
m_base(nullptr) {
}
- check_relation_plugin::~check_relation_plugin() {
- }
check_relation& check_relation_plugin::get(relation_base& r) {
return dynamic_cast<check_relation&>(r);
}
diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h
index b0b4a8acc..773b45813 100644
--- a/src/muz/rel/check_relation.h
+++ b/src/muz/rel/check_relation.h
@@ -89,7 +89,6 @@ namespace datalog {
unsigned_vector const& cols1, unsigned_vector const& cols2);
public:
check_relation_plugin(relation_manager& rm);
- ~check_relation_plugin() override;
void set_plugin(relation_plugin* p) { m_base = p; }
bool can_handle_signature(const relation_signature & s) override;
diff --git a/src/muz/rel/dl_external_relation.cpp b/src/muz/rel/dl_external_relation.cpp
index a47b0719f..a2e42f640 100644
--- a/src/muz/rel/dl_external_relation.cpp
+++ b/src/muz/rel/dl_external_relation.cpp
@@ -34,9 +34,6 @@ namespace datalog {
{
}
- external_relation::~external_relation() {
- }
-
void external_relation::mk_accessor(decl_kind k, func_decl_ref& fn, const relation_fact& f, bool destructive, expr_ref& res) const {
ast_manager& m = m_rel.get_manager();
family_id fid = get_plugin().get_family_id();
diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h
index 17e9a2364..c8887eeed 100644
--- a/src/muz/rel/dl_external_relation.h
+++ b/src/muz/rel/dl_external_relation.h
@@ -122,7 +122,6 @@ namespace datalog {
void mk_accessor(decl_kind k, func_decl_ref& fn, const relation_fact& f, bool destructive, expr_ref& res) const;
external_relation(external_relation_plugin & p, const relation_signature & s, expr* r);
- ~external_relation() override;
public:
external_relation_plugin & get_plugin() const;
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index a4b704597..2d22e34a9 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -631,9 +631,6 @@ namespace datalog {
);
}
- mk_explanations::~mk_explanations() {
- }
-
func_decl * mk_explanations::get_union_decl(context & ctx) {
ast_manager & m = ctx.get_manager();
sort_ref s(ctx.get_decl_util().mk_rule_sort(), m);
diff --git a/src/muz/rel/dl_mk_explanations.h b/src/muz/rel/dl_mk_explanations.h
index 5491918de..33d5cc8ee 100644
--- a/src/muz/rel/dl_mk_explanations.h
+++ b/src/muz/rel/dl_mk_explanations.h
@@ -65,8 +65,6 @@ namespace datalog {
*/
mk_explanations(context & ctx);
- ~mk_explanations() override;
-
/**
\brief Return explanation predicate that corresponds to \c orig_decl.
*/
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 30b57f2a4..824b298b4 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -38,9 +38,6 @@ namespace datalog {
m_rewriter.updt_params(m_params);
}
- mk_array_blast::~mk_array_blast() {
- }
-
bool mk_array_blast::is_store_def(expr* e, expr*& x, expr*& y) {
if (m.is_eq(e, x, y)) {
if (!a.is_store(y)) {
diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h
index 352c8a248..12102af73 100644
--- a/src/muz/transforms/dl_mk_array_blast.h
+++ b/src/muz/transforms/dl_mk_array_blast.h
@@ -64,8 +64,6 @@ namespace datalog {
\brief Create rule transformer that removes array stores and selects by ackermannization.
*/
mk_array_blast(context & ctx, unsigned priority);
-
- ~mk_array_blast() override;
rule_set * operator()(rule_set const & source) override;
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index b8a68a443..6b321bc75 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -149,9 +149,6 @@ namespace datalog {
m_mc(nullptr) {
}
- mk_quantifier_abstraction::~mk_quantifier_abstraction() {
- }
-
func_decl* mk_quantifier_abstraction::declare_pred(rule_set const& rules, rule_set& dst, func_decl* old_p) {
if (rules.is_output_predicate(old_p)) {
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.h b/src/muz/transforms/dl_mk_quantifier_abstraction.h
index 6cf546a50..33c70c08b 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.h
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.h
@@ -49,8 +49,6 @@ namespace datalog {
public:
mk_quantifier_abstraction(context & ctx, unsigned priority);
-
- ~mk_quantifier_abstraction() override;
rule_set * operator()(rule_set const & source) override;
};
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 61c395b4e..d1fb6400c 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -41,9 +41,6 @@ namespace datalog {
m_cnst2var(m) {
}
- mk_quantifier_instantiation::~mk_quantifier_instantiation() {
- }
-
void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) {
conjs.reset();
qs.reset();
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h
index 5c0c28cd4..716de11f0 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.h
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h
@@ -60,8 +60,6 @@ namespace datalog {
public:
mk_quantifier_instantiation(context & ctx, unsigned priority);
- ~mk_quantifier_instantiation() override;
-
rule_set * operator()(rule_set const & source) override;
};
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index 38305a04e..54cf22ea8 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -110,9 +110,6 @@ namespace datalog {
m_eqs(m) {
}
- mk_scale::~mk_scale() {
- }
-
rule_set * mk_scale::operator()(rule_set const & source) {
if (!m_ctx.scale()) {
return nullptr;
diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h
index a8e42f17e..fcbf4c226 100644
--- a/src/muz/transforms/dl_mk_scale.h
+++ b/src/muz/transforms/dl_mk_scale.h
@@ -42,7 +42,6 @@ namespace datalog {
app_ref mk_constraint(unsigned num_vars, app* q);
public:
mk_scale(context & ctx, unsigned priority = 33039);
- ~mk_scale() override;
rule_set * operator()(rule_set const & source) override;
};
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index a188206b4..cda44bdd4 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -156,9 +156,6 @@ namespace nlsat {
m_minimize_cores = false;
m_signed_project = false;
}
-
- ~imp() {
- }
std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
m_pm.display(out, p, m_solver.display_proc());
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index 76a310f00..872266f5f 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/src/nlsat/nlsat_interval_set.cpp
@@ -112,9 +112,6 @@ namespace nlsat {
m_am(m),
m_allocator(a) {
}
-
- interval_set_manager::~interval_set_manager() {
- }
void interval_set_manager::del(interval_set * s) {
if (s == nullptr)
diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h
index 2e74f33c6..297318912 100644
--- a/src/nlsat/nlsat_interval_set.h
+++ b/src/nlsat/nlsat_interval_set.h
@@ -33,7 +33,6 @@ namespace nlsat {
void del(interval_set * s);
public:
interval_set_manager(anum_manager & m, small_object_allocator & a);
- ~interval_set_manager();
void set_seed(unsigned s) { m_rand.set_seed(s); }
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index aff1301e0..c05949439 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -58,9 +58,6 @@ namespace opt {
}
unsigned opt_solver::m_dump_count = 0;
-
- opt_solver::~opt_solver() {
- }
void opt_solver::updt_params(params_ref const & _p) {
opt_params p(_p);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 66835df48..e614a54fc 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -85,7 +85,6 @@ namespace opt {
bool m_was_unknown;
public:
opt_solver(ast_manager & m, params_ref const & p, generic_model_converter& fm);
- ~opt_solver() override;
solver* translate(ast_manager& m, params_ref const& p) override;
void updt_params(params_ref const& p) override;
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 82802819d..e7cdf9476 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -123,9 +123,6 @@ namespace smt {
one = mpz(1);
}
- ~imp() {
- }
-
void reset() {
init_max_flips();
m_non_greedy_percent = 30;
diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp
index 6c3303e5c..c039fd9a1 100644
--- a/src/parsers/util/simple_parser.cpp
+++ b/src/parsers/util/simple_parser.cpp
@@ -28,9 +28,6 @@ simple_parser::simple_parser(ast_manager & m):
m_exprs(m) {
}
-simple_parser::~simple_parser() {
-}
-
void simple_parser::add_builtin_op(symbol const & s, family_id fid, decl_kind kind) {
SASSERT(!m_builtin.contains(s));
SASSERT(!m_vars.contains(s));
diff --git a/src/parsers/util/simple_parser.h b/src/parsers/util/simple_parser.h
index b40a0d983..c3cc0712e 100644
--- a/src/parsers/util/simple_parser.h
+++ b/src/parsers/util/simple_parser.h
@@ -45,7 +45,7 @@ protected:
expr * parse_expr(scanner & s);
public:
simple_parser(ast_manager & m);
- virtual ~simple_parser();
+ virtual ~simple_parser() = default;
void add_builtin_op(symbol const & s, family_id fid, decl_kind kind);
void add_builtin_op(char const * str, family_id fid, decl_kind kind);
void add_var(symbol const & s, var * v);
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 6e5d3fae3..92b4f7f5c 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -353,9 +353,6 @@ namespace sat {
DEBUG_CODE(verify_unsat_stack(););
}
- local_search::local_search() {
- }
-
void local_search::reinit(solver& s, bool_vector const& phase) {
import(s, true);
for (unsigned i = phase.size(); i-- > 0; )
@@ -419,10 +416,6 @@ namespace sat {
if (_init)
init();
}
-
- local_search::~local_search() {
- }
-
lbool local_search::check() {
return check(0, nullptr, nullptr);
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index b62234522..e8959478e 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -227,10 +227,6 @@ namespace sat {
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
public:
-
- local_search();
-
- ~local_search() override;
reslimit& rlimit() override { return m_limit; }
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index ddb277e9b..fa5720ede 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -23,13 +23,6 @@ Revision History:
namespace sat {
- model_converter::model_converter(): m_exposed_lim(0), m_solver(nullptr) {
- }
-
- model_converter::~model_converter() {
- }
-
-
model_converter& model_converter::operator=(model_converter const& other) {
copy(other);
return *this;
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 7393dc1bb..170886aa6 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -79,9 +79,9 @@ namespace sat {
};
private:
vector<entry> m_entries; // entries accumulated during SAT search
- unsigned m_exposed_lim; // last entry that was exposed to model converter.
+ unsigned m_exposed_lim = 0; // last entry that was exposed to model converter.
bool_vector m_mark; // literals that are used in asserted clauses.
- solver const* m_solver;
+ solver const* m_solver = nullptr;
elim_stackv m_elim_stack;
void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
@@ -95,8 +95,6 @@ namespace sat {
void add_elim_stack(entry & e);
public:
- model_converter();
- ~model_converter();
void set_solver(solver const* s) { m_solver = s; }
void operator()(model & m) const;
model_converter& operator=(model_converter const& other);
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 42cda4bfb..c001ee90f 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -296,9 +296,6 @@ namespace euf {
add_plugin(alloc(bv::theory_checker, m));
}
- theory_checker::~theory_checker() {
- }
-
void theory_checker::add_plugin(theory_checker_plugin* p) {
m_plugins.push_back(p);
p->register_plugins(*this);
diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h
index d84e4d19f..0da57ee9e 100644
--- a/src/sat/smt/euf_proof_checker.h
+++ b/src/sat/smt/euf_proof_checker.h
@@ -45,7 +45,6 @@ namespace euf {
void add_plugin(theory_checker_plugin* p);
public:
theory_checker(ast_manager& m);
- ~theory_checker();
void register_plugin(symbol const& rule, theory_checker_plugin*);
bool check(expr* jst);
expr_ref_vector clause(expr* jst);
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index 1c356f9f2..0fa35cfd4 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -2000,9 +2000,6 @@ namespace q {
m_args.resize(INIT_ARGS_SIZE);
}
- ~interpreter() {
- }
-
void init(code_tree * t) {
TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";);
m_registers.reserve(t->get_num_regs(), nullptr);
diff --git a/src/sat/smt/specrel_solver.cpp b/src/sat/smt/specrel_solver.cpp
index d59029e6b..064e19904 100644
--- a/src/sat/smt/specrel_solver.cpp
+++ b/src/sat/smt/specrel_solver.cpp
@@ -32,9 +32,6 @@ namespace specrel {
ctx.get_egraph().add_plugin(alloc(euf::specrel_plugin, ctx.get_egraph()));
}
- solver::~solver() {
- }
-
void solver::asserted(sat::literal l) {
}
diff --git a/src/sat/smt/specrel_solver.h b/src/sat/smt/specrel_solver.h
index 9ebb76916..51e383bad 100644
--- a/src/sat/smt/specrel_solver.h
+++ b/src/sat/smt/specrel_solver.h
@@ -39,7 +39,6 @@ namespace specrel {
public:
solver(euf::solver& ctx, theory_id id);
- ~solver() override;
bool is_external(bool_var v) override { return false; }
void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a10c243f8..71eeb55cb 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1995,9 +1995,6 @@ namespace {
m_args.resize(INIT_ARGS_SIZE);
}
- ~interpreter() {
- }
-
void init(code_tree * t) {
TRACE("mam_bug", tout << "preparing to match tree:\n" << *t << "\n";);
m_registers.reserve(t->get_num_regs(), nullptr);
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 52399abb6..81d41eeee 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -43,9 +43,6 @@ namespace smt {
m_vals.resize(15, 0.0f);
}
- qi_queue::~qi_queue() {
- }
-
void qi_queue::setup() {
TRACE("qi_cost", tout << "qi_cost: " << m_params.m_qi_cost << "\n";);
if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h
index bdf4bd50e..961dd73e0 100644
--- a/src/smt/qi_queue.h
+++ b/src/smt/qi_queue.h
@@ -80,7 +80,6 @@ namespace smt {
public:
qi_queue(quantifier_manager & qm, context & ctx, qi_params & params);
- ~qi_queue();
void setup();
/**
\brief Insert a new quantifier in the queue, f contains the quantifier and bindings.
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 793243473..90877a963 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -52,9 +52,6 @@ namespace smt {
{
}
- conflict_resolution::~conflict_resolution() {
- }
-
/**
\brief Mark all enodes in a 'proof' tree branch starting at n
n -> ... -> root
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index cf707bd31..87ad19771 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -208,7 +208,7 @@ namespace smt {
vector<watch_list> & watches
);
- virtual ~conflict_resolution();
+ virtual ~conflict_resolution() = default;
virtual bool resolve(b_justification conflict, literal not_l);
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index 0c876e8bc..86f1c1141 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -177,9 +177,6 @@ namespace smt {
m_lazy(true) {
}
- theory::~theory() {
- }
-
smt_params const& theory::get_fparams() const {
return ctx.get_fparams();
}
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 416d626f7..74dfe8aa2 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -388,7 +388,7 @@ namespace smt {
public:
theory(context& ctx, family_id fid);
- virtual ~theory();
+ virtual ~theory() = default;
virtual void setup() {}
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e68f0f53f..e2bc5e7a4 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1054,7 +1054,6 @@ namespace smt {
// -----------------------------------
public:
theory_arith(context& ctx);
- ~theory_arith() override;
theory * mk_fresh(context * new_ctx) override;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 8a2d9f3c9..e4f788f60 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1737,10 +1737,6 @@ namespace smt {
m_bound_watch(null_bool_var) {
}
- template<typename Ext>
- theory_arith<Ext>::~theory_arith() {
- }
-
template<typename Ext>
theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_arith<Ext>, *new_ctx);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 5740285a2..b1fe47b65 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1493,9 +1493,6 @@ namespace smt {
m_bb.set_flat_and_or(false);
}
- theory_bv::~theory_bv() {
- }
-
theory* theory_bv::mk_fresh(context* new_ctx) {
return alloc(theory_bv, *new_ctx);
}
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 72775c1d3..0a7d4bbb2 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -268,7 +268,6 @@ namespace smt {
typedef std::pair<enode*, unsigned> var_enode_pos;
theory_bv(context& ctx);
- ~theory_bv() override;
theory * mk_fresh(context * new_ctx) override;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index b794a44b5..3302199a2 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -762,8 +762,7 @@ namespace smt {
m_util(m),
m_autil(m),
m_sutil(m),
- m_find(*this),
- m_trail_stack() {
+ m_find(*this) {
}
theory_datatype::~theory_datatype() {
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index ee94ac355..94a5edc59 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -89,10 +89,6 @@ void asserted_formulas::setup() {
m_smt_params.m_relevancy_lemma = false;
}
-
-asserted_formulas::~asserted_formulas() {
-}
-
void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
if (inconsistent()) {
return;
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 481af58b7..643cbc046 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -254,7 +254,6 @@ class asserted_formulas {
public:
asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
- ~asserted_formulas();
void finalize();
void updt_params(params_ref const& p);
diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp
index fd7939d95..944f717b9 100644
--- a/src/solver/check_sat_result.cpp
+++ b/src/solver/check_sat_result.cpp
@@ -58,9 +58,6 @@ simple_check_sat_result::simple_check_sat_result(ast_manager & m):
m_proof(m) {
}
-simple_check_sat_result::~simple_check_sat_result() {
-}
-
void simple_check_sat_result::collect_statistics(statistics & st) const {
st.copy(m_stats);
}
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 2269a1444..b992d260d 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -98,7 +98,6 @@ struct simple_check_sat_result : public check_sat_result {
std::string m_unknown;
simple_check_sat_result(ast_manager & m);
- ~simple_check_sat_result() override;
ast_manager& get_manager() const override { return m_proof.get_manager(); }
void collect_statistics(statistics & st) const override;
void get_unsat_core(expr_ref_vector & r) override;
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index e4071628c..640c41277 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -162,9 +162,6 @@ class injectivity_tactic : public tactic {
rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
}
- ~rewriter_eq_cfg() {
- }
-
void cleanup_buffers() {
}
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index ee5cd0f73..6e2068e26 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -31,9 +31,6 @@ struct simplify_tactic::imp {
m_num_steps(0) {
}
- ~imp() {
- }
-
ast_manager & m() const { return m_manager; }
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 8c20a4cda..e48934b5b 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -89,10 +89,6 @@ hwf_manager::hwf_manager() :
// to the precision (not sure about the rounding modes though).
}
-hwf_manager::~hwf_manager()
-{
-}
-
uint64_t RAW(double X) { uint64_t tmp; memcpy(&tmp, &(X), sizeof(uint64_t)); return tmp; }
double DBL(uint64_t X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 209a8fe77..926963937 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -46,7 +46,6 @@ class hwf_manager {
public:
typedef hwf numeral;
hwf_manager();
- ~hwf_manager();
void reset(hwf & o) { set(o, 0); }
void set(hwf & o, int value);
diff --git a/src/util/map.h b/src/util/map.h
index 0068be31b..fb72db01f 100644
--- a/src/util/map.h
+++ b/src/util/map.h
@@ -24,19 +24,6 @@ template<typename Key, typename Value>
struct _key_data {
Key m_key;
Value m_value;
- _key_data() {
- }
- _key_data(Key const & k):
- m_key(k) {
- }
- _key_data(Key const & k, Value const & v):
- m_key(k),
- m_value(v) {
- }
- _key_data(Key const& k, Value&& v):
- m_key(k),
- m_value(std::move(v)) {
- }
};
template<typename Entry, typename HashProc, typename EqProc>
@@ -108,27 +95,27 @@ public:
}
void insert(key const & k, value const & v) {
- m_table.insert(key_data(k, v));
+ m_table.insert(key_data{k, v});
}
void insert(key const& k, value&& v) {
- m_table.insert(key_data(k, std::move(v)));
+ m_table.insert(key_data{k, std::move(v)});
}
bool insert_if_not_there_core(key const & k, value const & v, entry *& et) {
- return m_table.insert_if_not_there_core(key_data(k,v), et);
+ return m_table.insert_if_not_there_core(key_data{k,v}, et);
}
value & insert_if_not_there(key const & k, value const & v) {
- return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
+ return m_table.insert_if_not_there2(key_data{k, v})->get_data().m_value;
}
entry * insert_if_not_there3(key const & k, value const & v) {
- return m_table.insert_if_not_there2(key_data(k, v));
+ return m_table.insert_if_not_there2(key_data{k, v});
}
entry * find_core(key const & k) const {
- return m_table.find_core(key_data(k));
+ return m_table.find_core(key_data{k});
}
bool find(key const & k, value & v) const {
@@ -150,7 +137,7 @@ public:
}
iterator find_iterator(key const & k) const {
- return m_table.find(key_data(k));
+ return m_table.find(key_data{k});
}
value const & find(key const& k) const {
@@ -175,7 +162,7 @@ public:
}
void remove(key const & k) {
- m_table.remove(key_data(k));
+ m_table.remove(key_data{k});
}
void erase(key const & k) {
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index dbb2b776e..2784439a8 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -60,7 +60,7 @@ public:
Value m_value;
key_data() = default;
key_data(Key * k):
- m_key(k), m_value() {
+ m_key(k) {
}
key_data(Key * k, Value const & v):
m_key(k),
diff --git a/src/util/ref.h b/src/util/ref.h
index 849e23b38..22e51b783 100644
--- a/src/util/ref.h
+++ b/src/util/ref.h
@@ -21,7 +21,7 @@ Revision History:
template<typename T>
class ref {
- T * m_ptr;
+ T * m_ptr = nullptr;
void inc_ref() {
if (m_ptr) {
@@ -36,9 +36,7 @@ class ref {
}
public:
- ref():
- m_ptr(nullptr) {
- }
+ ref() = default;
ref(T * ptr):
m_ptr(ptr) {
@@ -50,9 +48,9 @@ public:
inc_ref();
}
- ref (ref && r) noexcept : m_ptr(nullptr) {
- std::swap(m_ptr, r.m_ptr);
- }
+ ref(ref && r) noexcept {
+ std::swap(m_ptr, r.m_ptr);
+ }
~ref() {
dec_ref();