mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Remove empty leaf destructors. (#6211)

Browse source
This commit is contained in:
Bruce Mitchener 2022-07-30 16:07:03 +07:00 • committed by GitHub
parent f7fbb78fc8
commit 5d0dea05aa
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
134 changed files with 10 additions and 322 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -29,8 +29,6 @@ public:
updt_params(p);
}
~ackermannize_bv_tactic() override { }
char const* name() const override { return "ackermannize_bv"; }
void operator()(goal_ref const & g, goal_ref_buffer & result) override {

2
src/ackermannization/ackr_model_converter.cpp
View file

@ -40,8 +40,6 @@ public:
fixed_model(false)
{ }
~ackr_model_converter() override { }
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void operator()(model_ref & md) override {

2
src/ackermannization/lackr_model_converter_lazy.cpp
View file

@ -28,8 +28,6 @@ public:
, model_constructor(lmc)
{ }
~lackr_model_converter_lazy() override { }
void operator()(model_ref & md) override {
SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
SASSERT(model_constructor.get());

1
src/api/api_algebraic.cpp
View file

@ -344,7 +344,6 @@ extern "C" {
scoped_anum_vector const & m_as;
public:
vector_var2anum(scoped_anum_vector & as):m_as(as) {}
~vector_var2anum() override {}
algebraic_numbers::manager & m() const override { return m_as.m(); }
bool contains(polynomial::var x) const override { return static_cast<unsigned>(x) < m_as.size(); }
algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); }

1
src/api/api_ast_vector.h
View file

@ -26,7 +26,6 @@ namespace api {
struct Z3_ast_vector_ref : public api::object {
ast_ref_vector m_ast_vector;
Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {}
~Z3_ast_vector_ref() override {}
};
inline Z3_ast_vector_ref * to_ast_vector(Z3_ast_vector v) { return reinterpret_cast<Z3_ast_vector_ref *>(v); }

1
src/api/api_datalog.cpp
View file

@ -52,7 +52,6 @@ namespace api {
m_context(m, m_register_engine, p),
m_trail(m) {}
~fixedpoint_context() override {}
family_id get_family_id() const override { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
void set_state(void* state) {
SASSERT(!m_state);

1
src/api/api_goal.h
View file

@ -23,7 +23,6 @@ Revision History:
struct Z3_goal_ref : public api::object {
goal_ref m_goal;
Z3_goal_ref(api::context& c) : api::object(c) {}
~Z3_goal_ref() override {}
};
inline Z3_goal_ref * to_goal(Z3_goal g) { return reinterpret_cast<Z3_goal_ref *>(g); }

3
src/api/api_model.h
View file

@ -23,7 +23,6 @@ Revision History:
struct Z3_model_ref : public api::object {
model_ref m_model;
Z3_model_ref(api::context& c): api::object(c) {}
~Z3_model_ref() override {}
};
inline Z3_model_ref * to_model(Z3_model s) { return reinterpret_cast<Z3_model_ref *>(s); }
@ -34,7 +33,6 @@ struct Z3_func_interp_ref : public api::object {
model_ref m_model; // must have it to prevent reference to m_func_interp to be killed.
func_interp * m_func_interp;
Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(nullptr) {}
~Z3_func_interp_ref() override {}
};
inline Z3_func_interp_ref * to_func_interp(Z3_func_interp s) { return reinterpret_cast<Z3_func_interp_ref *>(s); }
@ -46,7 +44,6 @@ struct Z3_func_entry_ref : public api::object {
func_interp * m_func_interp;
func_entry const * m_func_entry;
Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(nullptr), m_func_entry(nullptr) {}
~Z3_func_entry_ref() override {}
};
inline Z3_func_entry_ref * to_func_entry(Z3_func_entry s) { return reinterpret_cast<Z3_func_entry_ref *>(s); }

2
src/api/api_parsers.cpp
View file

@ -47,8 +47,6 @@ extern "C" {
ctx->register_plist();
ctx->set_ignore_check(true);
}
~Z3_parser_context_ref() override {}
};
inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast<Z3_parser_context_ref*>(pc); }

1
src/api/api_solver.h
View file

@ -51,7 +51,6 @@ struct Z3_solver_ref : public api::object {
Z3_solver_ref(api::context& c, solver_factory * f):
api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {}
~Z3_solver_ref() override {}
void assert_expr(expr* e);
void assert_expr(expr* e, expr* t);

1
src/api/api_stats.h
View file

@ -23,7 +23,6 @@ Revision History:
struct Z3_stats_ref : public api::object {
statistics m_stats;
Z3_stats_ref(api::context& c): api::object(c) {}
~Z3_stats_ref() override {}
};
inline Z3_stats_ref * to_stats(Z3_stats s) { return reinterpret_cast<Z3_stats_ref *>(s); }

3
src/api/api_tactic.h
View file

@ -28,13 +28,11 @@ namespace api {
struct Z3_tactic_ref : public api::object {
tactic_ref m_tactic;
Z3_tactic_ref(api::context& c): api::object(c) {}
~Z3_tactic_ref() override {}
};
struct Z3_probe_ref : public api::object {
probe_ref m_probe;
Z3_probe_ref(api::context& c):api::object(c) {}
~Z3_probe_ref() override {}
};
inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); }
@ -50,7 +48,6 @@ struct Z3_apply_result_ref : public api::object {
model_converter_ref m_mc;
proof_converter_ref m_pc;
Z3_apply_result_ref(api::context& c, ast_manager & m);
~Z3_apply_result_ref() override {}
};
inline Z3_apply_result_ref * to_apply_result(Z3_apply_result g) { return reinterpret_cast<Z3_apply_result_ref *>(g); }

1
src/ast/array_decl_plugin.h
View file

@ -107,7 +107,6 @@ class array_decl_plugin : public decl_plugin {
bool is_array_sort(sort* s) const;
public:
array_decl_plugin();
~array_decl_plugin() override {}
decl_plugin * mk_fresh() override {
return alloc(array_decl_plugin);

1
src/ast/ast_printer.cpp
View file

@ -26,7 +26,6 @@ class simple_ast_printer_context : public ast_printer_context {
smt2_pp_environment_dbg & env() const { return *(m_env.get()); }
public:
simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); }
~simple_ast_printer_context() override {}
ast_manager & m() const { return m_manager; }
ast_manager & get_ast_manager() override { return m_manager; }
void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); }

1
src/ast/ast_printer.h
View file

@ -45,7 +45,6 @@ public:
class ast_printer_context : public ast_printer {
public:
~ast_printer_context() override {}
virtual ast_manager & get_ast_manager() = 0;
virtual std::ostream & regular_stream();
virtual std::ostream & diagnostic_stream();

1
src/ast/bv_decl_plugin.h
View file

@ -241,7 +241,6 @@ protected:
public:
bv_decl_plugin();
~bv_decl_plugin() override {}
void finalize() override;
decl_plugin * mk_fresh() override { return alloc(bv_decl_plugin); }

1
src/ast/dl_decl_plugin.h
View file

@ -101,7 +101,6 @@ namespace datalog {
public:
dl_decl_plugin();
~dl_decl_plugin() override {}
decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); }

2
src/ast/format.cpp
View file

@ -52,8 +52,6 @@ namespace format_ns {
m_line_break_ext("cr++") {
}
~format_decl_plugin() override {}
void finalize() override {
if (m_format_sort)
m_manager->dec_ref(m_format_sort);

1
src/ast/fpa/fpa2bv_converter.h
View file

@ -239,7 +239,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter {
fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
fpa2bv_converter(m),
m_rw(rw) {}
~fpa2bv_converter_wrapped() override {}
void mk_const(func_decl * f, expr_ref & result) override;
void mk_rm_const(func_decl * f, expr_ref & result) override;
app_ref wrap(expr * e);

9
src/ast/normal_forms/name_exprs.cpp
View file

@ -77,9 +77,6 @@ public:
m_rw(m, m.proofs_enabled(), m_cfg) {
}
~name_exprs_core() override {
}
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
m_cfg.m_def_exprs = &new_defs;
m_cfg.m_def_proofs = &new_def_proofs;
@ -113,9 +110,6 @@ public:
name_exprs_core(m, n, m_pred),
m_pred(m) {
}
~name_quantifier_labels() override {
}
};
name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) {
@ -145,9 +139,6 @@ public:
m_pred(m) {
}
~name_nested_formulas() override {
}
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
m_pred.m_root = n;
TRACE("name_exprs", tout << "operator()\n";);

1
src/ast/pb_decl_plugin.h
View file

@ -52,7 +52,6 @@ class pb_decl_plugin : public decl_plugin {
func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
public:
pb_decl_plugin();
~pb_decl_plugin() override {}
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override {
UNREACHABLE();

2
src/ast/proofs/proof_checker.h
View file

@ -52,8 +52,6 @@ class proof_checker {
public:
hyp_decl_plugin();
~hyp_decl_plugin() override {}
void finalize() override;
decl_plugin * mk_fresh() override { return alloc(hyp_decl_plugin); }

2
src/ast/rewriter/elim_bounds.h
View file

@ -68,8 +68,6 @@ public:
rewriter_tpl<elim_bounds_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m)
{}
~elim_bounds_rw() override {}
};

2
src/ast/rewriter/expr_replacer.cpp
View file

@ -129,8 +129,6 @@ public:
m_r(m, p) {
}
~th_rewriter2expr_replacer() override {}
ast_manager & m() const override { return m_r.m(); }
void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }

1
src/ast/rewriter/push_app_ite.h
View file

@ -49,7 +49,6 @@ protected:
bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
public:
ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {}
~ng_push_app_ite_cfg() override {}
};
struct push_app_ite_rw : public rewriter_tpl<push_app_ite_cfg> {

1
src/ast/rewriter/recfun_replace.h
View file

@ -32,7 +32,6 @@ class recfun_replace : public recfun::replace {
expr_safe_replace m_replace;
public:
recfun_replace(ast_manager& m): m(m), m_replace(m) {}
~recfun_replace() override {}
void reset() override { m_replace.reset(); }
void insert(expr* s, expr* t) override { m_replace.insert(s, t); }
expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; }

2
src/ast/special_relations_decl_plugin.h
View file

@ -40,8 +40,6 @@ class special_relations_decl_plugin : public decl_plugin {
public:
special_relations_decl_plugin();
~special_relations_decl_plugin() override {}
decl_plugin * mk_fresh() override {
return alloc(special_relations_decl_plugin);
}

2
src/cmd_context/basic_cmds.cpp
View file

@ -379,8 +379,6 @@ public:
m_int_real_coercions(":int-real-coercions"),
m_reproducible_resource_limit(":reproducible-resource-limit") {
}
~set_get_option_cmd() override {}
};
class set_option_cmd : public set_get_option_cmd {

1
src/cmd_context/cmd_context.cpp
View file

@ -493,7 +493,6 @@ protected:
public:
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {}
~pp_env() override {}
ast_manager & get_manager() const override { return m_owner.m(); }
arith_util & get_autil() override { return m_autil; }
bv_util & get_bvutil() override { return m_bvutil; }

7
src/cmd_context/pdecl.cpp
View file

@ -147,7 +147,6 @@ class psort_sort : public psort {
sort * get_sort() const { return m_sort; }
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override { return m_sort; }
public:
~psort_sort() override {}
bool is_sort_wrapper() const override { return true; }
char const * hcons_kind() const override { return "psort_sort"; }
unsigned hcons_hash() const override { return m_sort->get_id(); }
@ -171,7 +170,6 @@ class psort_var : public psort {
}
size_t obj_size() const override { return sizeof(psort_var); }
public:
~psort_var() override {}
char const * hcons_kind() const override { return "psort_var"; }
unsigned hcons_hash() const override { return hash_u_u(m_num_params, m_idx); }
bool hcons_eq(psort const * other) const override {
@ -233,7 +231,6 @@ class psort_app : public psort {
}
public:
~psort_app() override {}
char const * hcons_kind() const override { return "psort_app"; }
unsigned hcons_hash() const override {
return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
@ -800,8 +797,6 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
m.m().inc_array_ref(n, s);
}
~app_sort_info() override {}
unsigned obj_size() const override { return sizeof(app_sort_info); }
void finalize(pdecl_manager & m) override {
@ -843,8 +838,6 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
m_indices(n, s) {
}
~indexed_sort_info() override {}
unsigned obj_size() const override { return sizeof(indexed_sort_info); }
void display(std::ostream & out, pdecl_manager const & m) const override {

9
src/cmd_context/pdecl.h
View file

@ -66,7 +66,6 @@ protected:
psort(unsigned id, unsigned num_params):pdecl(id, num_params), m_inst_cache(nullptr) {}
bool is_psort() const override { return true; }
void finalize(pdecl_manager & m) override;
~psort() override {}
virtual void cache(pdecl_manager & m, sort * const * s, sort * r);
virtual sort * find(sort * const * s) const;
public:
@ -98,7 +97,6 @@ protected:
sort * find(sort * const * s);
psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
void finalize(pdecl_manager & m) override;
~psort_decl() override {}
public:
virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) = 0;
virtual sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) { return nullptr; }
@ -120,7 +118,6 @@ protected:
psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p);
size_t obj_size() const override { return sizeof(psort_user_decl); }
void finalize(pdecl_manager & m) override;
~psort_user_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
std::ostream& display(std::ostream & out) const override;
@ -133,7 +130,6 @@ protected:
decl_kind m_kind;
psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k);
size_t obj_size() const override { return sizeof(psort_builtin_decl); }
~psort_builtin_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override;
@ -145,7 +141,6 @@ protected:
friend class pdecl_manager;
psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
size_t obj_size() const override { return sizeof(psort_dt_decl); }
~psort_dt_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
std::ostream& display(std::ostream & out) const override;
@ -196,7 +191,6 @@ class paccessor_decl : public pdecl {
accessor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
symbol const & get_name() const { return m_name; }
ptype const & get_type() const { return m_type; }
~paccessor_decl() override {}
public:
std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
@ -217,7 +211,6 @@ class pconstructor_decl : public pdecl {
symbol const & get_name() const { return m_name; }
symbol const & get_recognizer_name() const { return m_recogniser_name; }
constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pconstructor_decl() override {}
public:
std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
@ -234,7 +227,6 @@ class pdatatype_decl : public psort_decl {
size_t obj_size() const override { return sizeof(pdatatype_decl); }
bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
datatype_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pdatatype_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
std::ostream& display(std::ostream & out) const override;
@ -255,7 +247,6 @@ class pdatatypes_decl : public pdecl {
size_t obj_size() const override { return sizeof(pdatatypes_decl); }
bool fix_missing_refs(symbol & missing);
bool instantiate(pdecl_manager & m, sort * const * s);
~pdatatypes_decl() override {}
public:
pdatatype_decl const * const * children() const { return m_datatypes.data(); }
pdatatype_decl * const * begin() const { return m_datatypes.begin(); }

5
src/cmd_context/simplify_cmd.cpp
View file

@ -46,10 +46,7 @@ public:
p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one.");
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
}
~simplify_cmd() override {
}
void prepare(cmd_context & ctx) override {
parametric_cmd::prepare(ctx);
m_target = nullptr;

1
src/math/automata/boolean_algebra.h
View file

@ -38,7 +38,6 @@ public:
template<class T>
class boolean_algebra : public positive_boolean_algebra<T> {
public:
~boolean_algebra() override {}
virtual T mk_not(T x) = 0;
};

4
src/math/hilbert/heap_trie.h
View file

@ -80,7 +80,6 @@ class heap_trie {
Value m_value;
public:
leaf(): node(leaf_t) {}
~leaf() override {}
Value const& get_value() const { return m_value; }
void set_value(Value const& v) { m_value = v; }
void display(std::ostream& out, unsigned indent) const override {
@ -98,9 +97,6 @@ class heap_trie {
public:
trie(): node(trie_t) {}
~trie() override {
}
node* find_or_insert(Key k, node* n) {
for (unsigned i = 0; i < m_nodes.size(); ++i) {
if (m_nodes[i].first == k) {

9
src/math/subpaving/subpaving.cpp
View file

@ -38,7 +38,6 @@ namespace subpaving {
CTX m_ctx;
public:
context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {}
~context_wrapper() override {}
unsigned num_vars() const override { return m_ctx.num_vars(); }
var mk_var(bool is_int) override { return m_ctx.mk_var(is_int); }
bool is_int(var x) const override { return m_ctx.is_int(x); }
@ -66,8 +65,6 @@ namespace subpaving {
m_as(m)
{}
~context_mpq_wrapper() override {}
unsynch_mpq_manager & qm() const override { return m_ctx.nm(); }
var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@ -108,8 +105,6 @@ namespace subpaving {
m_q2(m_qm) {
}
~context_mpf_wrapper() override {}
unsynch_mpq_manager & qm() const override { return m_qm; }
var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@ -165,8 +160,6 @@ namespace subpaving {
m_qm(qm) {
}
~context_hwf_wrapper() override {}
unsynch_mpq_manager & qm() const override { return m_qm; }
var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {
@ -223,8 +216,6 @@ namespace subpaving {
m_z2(m_qm) {
}
~context_fpoint_wrapper() override {}
unsynch_mpq_manager & qm() const override { return m_qm; }
var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override {

2
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -37,8 +37,6 @@ class subpaving_tactic : public tactic {
e2v.mk_inv(m_inv);
}
~display_var_proc() override {}
ast_manager & m() const { return m_inv.get_manager(); }
void operator()(std::ostream & out, subpaving::var x) const override {

2
src/model/array_factory.h
View file

@ -32,8 +32,6 @@ class array_factory : public struct_factory {
public:
array_factory(ast_manager & m, model_core & md);
~array_factory() override {}
expr * get_some_value(sort * s) override;
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;

1
src/model/datatype_factory.h
View file

@ -32,7 +32,6 @@ class datatype_factory : public struct_factory {
public:
datatype_factory(ast_manager & m, model_core & md);
~datatype_factory() override {}
expr * get_some_value(sort * s) override;
expr * get_fresh_value(sort * s) override;
};

2
src/model/fpa_factory.h
View file

@ -34,8 +34,6 @@ class fpa_value_factory : public value_factory {
value_factory(m, fid),
m_util(m) {}
~fpa_value_factory() override {}
expr * get_some_value(sort * s) override {
mpf_manager & mpfm = m_util.fm();

1
src/model/numeral_factory.h
View file

@ -25,7 +25,6 @@ Revision History:
class numeral_factory : public simple_factory<rational> {
public:
numeral_factory(ast_manager & m, family_id fid):simple_factory<rational>(m, fid) {}
~numeral_factory() override {}
};
class arith_factory : public numeral_factory {

1
src/model/value_factory.h
View file

@ -230,7 +230,6 @@ class user_sort_factory : public simple_factory<unsigned> {
app * mk_value_core(unsigned const & val, sort * s) override;
public:
user_sort_factory(ast_manager & m);
~user_sort_factory() override {}
/**
\brief Make the universe of \c s finite, by preventing new

3
src/muz/base/dl_context.cpp
View file

@ -159,8 +159,6 @@ namespace datalog {
public:
restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {}
~restore_rules() override {}
void undo() override {
ctx.replace_rules(*m_old_rules);
reset();
@ -173,7 +171,6 @@ namespace datalog {
unsigned m_old_size;
public:
restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {}
~restore_vec_size_trail() override {}
void undo() override { m_vector.shrink(m_old_size); }
};

2
src/muz/base/dl_context.h
View file

@ -105,7 +105,6 @@ namespace datalog {
class rel_context_base : public engine_base {
public:
rel_context_base(ast_manager& m, char const* name): engine_base(m, name) {}
~rel_context_base() override {}
virtual relation_manager & get_rmanager() = 0;
virtual const relation_manager & get_rmanager() const = 0;
virtual relation_base & get_relation(func_decl * pred) = 0;
@ -141,7 +140,6 @@ namespace datalog {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
~contains_pred() override {}
bool operator()(expr* e) override {
return ctx.is_predicate(e);

13
src/muz/rel/check_relation.cpp
View file

@ -190,7 +190,6 @@ namespace datalog {
const unsigned * cols1, const unsigned * cols2)
: convenient_join_fn(o1_sig, o2_sig, col_cnt, cols1, cols2), m_join(j)
{}
~join_fn() override {}
relation_base * operator()(const relation_base & r1, const relation_base & r2) override {
check_relation const& t1 = get(r1);
check_relation const& t2 = get(r2);
@ -219,7 +218,6 @@ namespace datalog {
: convenient_join_project_fn(o1_sig, o2_sig, col_cnt, cols1, cols2,
removed_col_cnt, removed_cols), m_join(j)
{}
~join_project_fn() override {}
relation_base * operator()(const relation_base & r1, const relation_base & r2) override {
check_relation const& t1 = get(r1);
check_relation const& t2 = get(r2);
@ -527,8 +525,6 @@ namespace datalog {
m_filter(f) {
}
~filter_identical_fn() override {}
void operator()(relation_base & _r) override {
check_relation& r = get(_r);
check_relation_plugin& p = r.get_plugin();
@ -563,8 +559,6 @@ namespace datalog {
m_condition(condition) {
}
~filter_interpreted_fn() override {}
void operator()(relation_base & tb) override {
check_relation& r = get(tb);
check_relation_plugin& p = r.get_plugin();
@ -590,8 +584,6 @@ namespace datalog {
m_project(p) {
}
~project_fn() override {}
relation_base * operator()(const relation_base & tb) override {
check_relation const& t = get(tb);
check_relation_plugin& p = t.get_plugin();
@ -618,8 +610,6 @@ namespace datalog {
m_permute(permute) {
}
~rename_fn() override {}
relation_base * operator()(const relation_base & _t) override {
check_relation const& t = get(_t);
check_relation_plugin& p = t.get_plugin();
@ -647,7 +637,6 @@ namespace datalog {
m_val(val),
m_col(col)
{}
~filter_equal_fn() override { }
void operator()(relation_base & tb) override {
check_relation & t = get(tb);
check_relation_plugin& p = t.get_plugin();
@ -760,8 +749,6 @@ namespace datalog {
m_cond(cond),
m_xform(xform)
{}
~filter_proj_fn() override {}
relation_base* operator()(const relation_base & tb) override {
check_relation const & t = get(tb);

2
src/muz/rel/dl_base.h
View file

@ -799,7 +799,6 @@ namespace datalog {
protected:
relation_base(relation_plugin & plugin, const relation_signature & s)
: base_ancestor(plugin, s) {}
~relation_base() override {}
public:
virtual relation_base * complement(func_decl* p) const = 0;
@ -1040,7 +1039,6 @@ namespace datalog {
protected:
table_base(table_plugin & plugin, const table_signature & s)
: base_ancestor(plugin, s) {}
~table_base() override {}
public:
table_base * clone() const override;
virtual table_base * complement(func_decl* p, const table_element * func_columns = nullptr) const;

2
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -794,8 +794,6 @@ namespace datalog {
m_delta_indexes(delta_indexes),
m_delta_rels(delta_rels) {}
~union_mapper() override {}
bool operator()(table_element * func_columns) override {
relation_base & otgt_orig = m_tgt.get_inner_rel(func_columns[0]);
const relation_base & osrc = m_src.get_inner_rel(func_columns[1]);

18
src/muz/rel/dl_lazy_table.h
View file

@ -128,8 +128,6 @@ namespace datalog {
m_ref(t)
{}
~lazy_table() override {}
lazy_table_plugin& get_lplugin() const {
return dynamic_cast<lazy_table_plugin&>(table_base::get_plugin());
}
@ -164,7 +162,6 @@ namespace datalog {
m_table = table;
// SASSERT(&p.m_plugin == &table->get_lplugin());
}
~lazy_table_base() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_BASE; }
table_base* force() override { return m_table.get(); }
};
@ -183,7 +180,6 @@ namespace datalog {
m_cols2(col_cnt, cols2),
m_t1(t1.get_ref()),
m_t2(t2.get_ref()) { }
~lazy_table_join() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_JOIN; }
unsigned_vector const& cols1() const { return m_cols1; }
unsigned_vector const& cols2() const { return m_cols2; }
@ -201,7 +197,6 @@ namespace datalog {
: lazy_table_ref(src.get_lplugin(), sig),
m_cols(col_cnt, cols),
m_src(src.get_ref()) {}
~lazy_table_project() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_PROJECT; }
unsigned_vector const& cols() const { return m_cols; }
@ -217,8 +212,7 @@ namespace datalog {
: lazy_table_ref(src.get_lplugin(), sig),
m_cols(col_cnt, cols),
m_src(src.get_ref()) {}
~lazy_table_rename() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_RENAME; }
unsigned_vector const& cols() const { return m_cols; }
lazy_table_ref* src() const { return m_src.get(); }
@ -231,8 +225,7 @@ namespace datalog {
public:
lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
: lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {}
~lazy_table_filter_identical() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_IDENTICAL; }
unsigned_vector const& cols() const { return m_cols; }
lazy_table_ref* src() const { return m_src.get(); }
@ -249,8 +242,7 @@ namespace datalog {
m_col(col),
m_value(value),
m_src(src.get_ref()) {}
~lazy_table_filter_equal() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_EQUAL; }
unsigned col() const { return m_col; }
table_element value() const { return m_value; }
@ -265,8 +257,7 @@ namespace datalog {
lazy_table_filter_interpreted(lazy_table const& src, app* condition)
: lazy_table_ref(src.get_lplugin(), src.get_signature()),
m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {}
~lazy_table_filter_interpreted() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_INTERPRETED; }
app* condition() const { return m_condition; }
lazy_table_ref* src() const { return m_src.get(); }
@ -287,7 +278,6 @@ namespace datalog {
m_src(src.get_ref()),
m_cols1(c1),
m_cols2(c2) {}
~lazy_table_filter_by_negation() override {}
lazy_table_kind kind() const override { return LAZY_TABLE_FILTER_BY_NEGATION; }
lazy_table_ref* tgt() const { return m_tgt.get(); }
lazy_table_ref* src() const { return m_src.get(); }

4
src/muz/rel/dl_relation_manager.cpp
View file

@ -1589,8 +1589,6 @@ namespace datalog {
m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast<table_base *>(nullptr));
}
~default_table_map_fn() override {}
void operator()(table_base & t) override {
SASSERT(t.get_signature()==m_aux_table->get_signature());
if(!m_aux_table->empty()) {
@ -1644,8 +1642,6 @@ namespace datalog {
m_former_row.resize(get_result_signature().size());
}
~default_table_project_with_reduce_fn() override {}
virtual void modify_fact(table_fact & f) const {
unsigned ofs=1;
unsigned r_i=1;

2
src/muz/rel/dl_sparse_table.cpp
View file

@ -406,8 +406,6 @@ namespace datalog {
m_key_fact.resize(t.get_signature().size());
}
~full_signature_key_indexer() override {}
query_result get_matching_offsets(const key_value & key) const override {
unsigned key_len = m_key_cols.size();
for (unsigned i=0; i<key_len; i++) {

7
src/muz/spacer/spacer_generalizers.h
View file

@ -29,7 +29,6 @@ namespace spacer {
class lemma_sanity_checker : public lemma_generalizer {
public:
lemma_sanity_checker(context &ctx) : lemma_generalizer(ctx) {}
~lemma_sanity_checker() override {}
void operator()(lemma_ref &lemma) override;
};
@ -59,7 +58,6 @@ class lemma_bool_inductive_generalizer : public lemma_generalizer {
bool array_only = false)
: lemma_generalizer(ctx), m_failure_limit(failure_limit),
m_array_only(array_only) {}
~lemma_bool_inductive_generalizer() override {}
void operator()(lemma_ref &lemma) override;
void collect_statistics(statistics &st) const override;
@ -83,7 +81,6 @@ class unsat_core_generalizer : public lemma_generalizer {
public:
unsat_core_generalizer(context &ctx) : lemma_generalizer(ctx) {}
~unsat_core_generalizer() override {}
void operator()(lemma_ref &lemma) override;
void collect_statistics(statistics &st) const override;
@ -96,14 +93,12 @@ class lemma_array_eq_generalizer : public lemma_generalizer {
public:
lemma_array_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
~lemma_array_eq_generalizer() override {}
void operator()(lemma_ref &lemma) override;
};
class lemma_eq_generalizer : public lemma_generalizer {
public:
lemma_eq_generalizer(context &ctx) : lemma_generalizer(ctx) {}
~lemma_eq_generalizer() override {}
void operator()(lemma_ref &lemma) override;
};
@ -130,7 +125,6 @@ class lemma_quantifier_generalizer : public lemma_generalizer {
public:
lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true);
~lemma_quantifier_generalizer() override {}
void operator()(lemma_ref &lemma) override;
void collect_statistics(statistics &st) const override;
@ -174,7 +168,6 @@ class limit_num_generalizer : public lemma_generalizer {
public:
limit_num_generalizer(context &ctx, unsigned failure_limit);
~limit_num_generalizer() override {}
void operator()(lemma_ref &lemma) override;

2
src/muz/spacer/spacer_iuc_solver.h
View file

@ -88,8 +88,6 @@ public:
m_old_hyp_reducer(old_hyp_reducer)
{}
~iuc_solver() override {}
/* iuc solver specific */
virtual void get_iuc(expr_ref_vector &core);
void set_split_literals(bool v) { m_split_literals = v; }

2
src/muz/transforms/dl_mk_karr_invariants.cpp
View file

@ -105,8 +105,6 @@ namespace datalog {
add_invariant_model_converter(ast_manager& m): m(m), a(m), m_funcs(m), m_invs(m) {}
~add_invariant_model_converter() override { }
void add(func_decl* p, expr* inv) {
if (!m.is_true(inv)) {
m_funcs.push_back(p);

2
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -46,8 +46,6 @@ namespace datalog {
qa_model_converter(ast_manager& m):
m(m), m_old_funcs(m), m_new_funcs(m) {}
~qa_model_converter() override {}
model_converter * translate(ast_translation & translator) override {
return alloc(qa_model_converter, m);
}

1
src/muz/transforms/dl_mk_rule_inliner.h
View file

@ -195,7 +195,6 @@ namespace datalog {
m_head_visitor(ctx, m_subst),
m_tail_visitor(ctx, m_subst)
{}
~mk_rule_inliner() override { }
rule_set * operator()(rule_set const & source) override;
};

2
src/muz/transforms/dl_mk_scale.cpp
View file

@ -30,8 +30,6 @@ namespace datalog {
public:
scale_model_converter(ast_manager& m): m(m), m_trail(m), a(m) {}
~scale_model_converter() override {}
void add_new2old(func_decl* new_f, func_decl* old_f) {
m_trail.push_back(old_f);
m_trail.push_back(new_f);

2
src/muz/transforms/dl_mk_slice.h
View file

@ -99,8 +99,6 @@ namespace datalog {
*/
mk_slice(context & ctx);
~mk_slice() override { }
rule_set * operator()(rule_set const & source) override;
func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }

1
src/nlsat/nlsat_assignment.h
View file

@ -32,7 +32,6 @@ namespace nlsat {
bool_vector m_assigned;
public:
assignment(anum_manager & _m):m_values(_m) {}
~assignment() override {}
anum_manager & am() const { return m_values.m(); }
void swap(assignment & other) {
m_values.swap(other.m_values);

1
src/opt/maxcore.cpp
View file

@ -100,7 +100,6 @@ private:
struct lns_maxcore : public lns_context {
maxcore& i;
lns_maxcore(maxcore& i) :i(i) {}
~lns_maxcore() override {}
void update_model(model_ref& mdl) override { i.update_assignment(mdl); }
void relax_cores(vector<expr_ref_vector> const& cores) override { i.relax_cores(cores); }
rational cost(model& mdl) override { return i.cost(mdl); }

1
src/opt/maxsmt.h
View file

@ -85,7 +85,6 @@ namespace opt {
public:
maxsmt_solver_base(maxsat_context& c, vector<soft>& soft, unsigned index);
~maxsmt_solver_base() override {}
rational get_lower() const override { return m_lower; }
rational get_upper() const override { return m_upper; }
bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); }

3
src/opt/opt_cmds.cpp
View file

@ -56,9 +56,6 @@ public:
m_opt(opt)
{}
~assert_soft_cmd() override {
}
void reset(cmd_context & ctx) override {
m_idx = 0;
m_formula = nullptr;

2
src/opt/opt_pareto.h
View file

@ -87,7 +87,6 @@ namespace opt {
params_ref & p):
pareto_base(m, cb, s, p) {
}
~gia_pareto() override {}
lbool operator()() override;
};
@ -101,7 +100,6 @@ namespace opt {
params_ref & p):
pareto_base(m, cb, s, p) {
}
~oia_pareto() override {}
lbool operator()() override;
};

2
src/opt/sortmax.cpp
View file

@ -39,8 +39,6 @@ namespace opt {
sortmax(maxsat_context& c, vector<soft>& s, unsigned index):
maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {}
~sortmax() override {}
lbool operator()() override {
if (!init())
return l_undef;

2
src/opt/wmax.cpp
View file

@ -49,8 +49,6 @@ namespace opt {
m_trail(m),
m_defs(m) {}
~wmax() override {}
lbool operator()() override {
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);

2
src/qe/nlarith_util.cpp
View file

@ -1616,7 +1616,6 @@ namespace nlarith {
public:
simple_branch(ast_manager& m, app* cnstr):
m_cnstr(cnstr, m), m_atoms(m) {}
~simple_branch() override {}
app* get_constraint() override { return m_cnstr.get(); }
void get_updates(ptr_vector<app>& atoms, svector<util::atom_update>& updates) override {
for (unsigned i = 0; i < m_atoms.size(); ++i) {
@ -1636,7 +1635,6 @@ namespace nlarith {
public:
ins_rem_branch(ast_manager& m, app* a, app* r, app* cnstr):
simple_branch(m, cnstr) { insert(a); remove(r); }
~ins_rem_branch() override {}
};
/**

3
src/qe/nlqsat.cpp
View file

@ -835,9 +835,6 @@ namespace qe {
m_nftactic = mk_tseitin_cnf_tactic(m);
}
~nlqsat() override {
}
char const* name() const override { return "nlqsat"; }
void updt_params(params_ref const & p) override {

3
src/qe/qe_array_plugin.cpp
View file

@ -27,9 +27,6 @@ namespace qe {
{
}
~array_plugin() override {}
void assign(contains_app& x, expr* fml, rational const& vl) override {
UNREACHABLE();
}

3
src/qe/qe_cmd.cpp
View file

@ -26,9 +26,6 @@ public:
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
}
~qe_cmd() override {
}
void prepare(cmd_context & ctx) override {
parametric_cmd::prepare(ctx);
m_target = nullptr;

2
src/qe/qe_mbi.h
View file

@ -106,7 +106,6 @@ namespace qe {
solver_ref m_solver;
public:
prop_mbi_plugin(solver* s);
~prop_mbi_plugin() override {}
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
void block(expr_ref_vector const& lits) override;
};
@ -134,7 +133,6 @@ namespace qe {
expr_ref_vector& uflits);
public:
uflia_mbi(solver* s, solver* emptySolver);
~uflia_mbi() override {}
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
void project(model_ref& mdl, expr_ref_vector& lits);
void block(expr_ref_vector const& lits) override;

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -115,8 +115,6 @@ public:
return m_solver.get_config().m_incremental;
}
~inc_sat_solver() override {}
solver* translate(ast_manager& dst_m, params_ref const& p) override {
if (m_num_scopes > 0) {
throw default_exception("Cannot translate sat solver at non-base level");

1
src/sat/smt/bv_solver.h
View file

@ -313,7 +313,6 @@ namespace bv {
public:
solver(euf::solver& ctx, theory_id id);
~solver() override {}
void set_lookahead(sat::lookahead* s) override { }
void init_search() override {}
double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;

3
src/sat/smt/q_mam.cpp
View file

@ -3744,9 +3744,6 @@ namespace q {
reset_pp_pc();
}
~mam_impl() override {
}
void add_pattern(quantifier * qa, app * mp) override {
SASSERT(m.is_pattern(mp));
TRACE("trigger_bug", tout << "adding pattern\n" << mk_ismt2_pp(qa, m) << "\n" << mk_ismt2_pp(mp, m) << "\n";);

2
src/sat/smt/q_model_fixer.cpp
View file

@ -45,7 +45,6 @@ namespace q {
arith_util a;
public:
arith_projection(ast_manager& m) : projection_function(m), a(m) {}
~arith_projection() override {}
bool operator()(expr* e1, expr* e2) const override { return lt(a, e1, e2); }
expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); }
};
@ -54,7 +53,6 @@ namespace q {
bv_util bvu;
public:
ubv_projection(ast_manager& m) : projection_function(m), bvu(m) {}
~ubv_projection() override {}
bool operator()(expr* e1, expr* e2) const override { return lt(bvu, e1, e2); }
expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); }
};

1
src/sat/smt/q_model_fixer.h
View file

@ -95,7 +95,6 @@ namespace q {
public:
model_fixer(euf::solver& ctx, solver& qs);
~model_fixer() override {}
/**
* Update model in order to best satisfy quantifiers.

1
src/sat/smt/q_solver.h
View file

@ -65,7 +65,6 @@ namespace q {
public:
solver(euf::solver& ctx, family_id fid);
~solver() override {}
bool is_external(sat::bool_var v) override { return false; }
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override;
void asserted(sat::literal l) override;

1
src/sat/smt/sat_th.h
View file

@ -189,7 +189,6 @@ namespace euf {
public:
th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
~th_euf_solver() override {}
virtual theory_var mk_var(enode* n);
unsigned get_num_vars() const { return m_var2enode.size(); }
euf::enode* e_internalize(expr* e);

4
src/sat/tactic/goal2sat.cpp
View file

@ -93,10 +93,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
updt_params(p);
}
~imp() override {
}
sat::cut_simplifier* aig() {
return m_solver.get_cut_simplifier();
}

1
src/sat/tactic/sat2goal.h
View file

@ -51,7 +51,6 @@ public:
public:
mc(ast_manager& m);
~mc() override {}
// flush model converter from SAT solver to this structure.
void flush_smc(sat::solver& s, atom2bool_var const& map);
void operator()(sat::model& m);

2
src/smt/arith_eq_adapter.cpp
View file

@ -67,8 +67,6 @@ namespace smt {
m_ge(ge) {
}
~arith_eq_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override {
if (!rp.is_relevant(m_n1))
return;

1
src/smt/dyn_ack.cpp
View file

@ -346,7 +346,6 @@ namespace smt {
dyn_ack_clause_del_eh(dyn_ack_manager & m):
m(m) {
}
~dyn_ack_clause_del_eh() override {}
void operator()(ast_manager & _m, clause * cls) override {
m.del_clause_eh(cls);
dealloc(this);

1
src/smt/proto_model/proto_model.h
View file

@ -59,7 +59,6 @@ class proto_model : public model_core {
public:
proto_model(ast_manager & m, params_ref const & p = params_ref());
~proto_model() override {}
void register_factory(value_factory * f) { m_factories.register_plugin(f); }

4
src/smt/smt_case_split_queue.cpp
View file

@ -150,8 +150,6 @@ namespace {
if (!first)
out << "\n";
}
~act_case_split_queue() override {};
};
/**
@ -1244,8 +1242,6 @@ namespace {
out << "\n";
}
~theory_aware_branching_queue() override {};
};
}

2
src/smt/smt_for_each_relevant_expr.h
View file

@ -92,7 +92,6 @@ namespace smt {
for_each_relevant_expr(ctx),
m_buffer(b) {
}
~collect_relevant_label_lits() override {}
void operator()(expr * n) override;
};
@ -103,7 +102,6 @@ namespace smt {
for_each_relevant_expr(ctx),
m_buffer(b) {
}
~collect_relevant_labels() override {}
void operator()(expr * n) override;
};

3
src/smt/smt_justification.h
View file

@ -239,7 +239,6 @@ namespace smt {
unsigned num_params, parameter* params):
simple_justification(r, num_lits, lits),
m_th_id(fid), m_params(num_params, params) {}
~simple_theory_justification() override {}
bool has_del_eh() const override { return !m_params.empty(); }
@ -323,8 +322,6 @@ namespace smt {
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params = 0, parameter* params = nullptr):
ext_simple_justification(r, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {}
~ext_theory_simple_justification() override {}
bool has_del_eh() const override { return !m_params.empty(); }

6
src/smt/smt_model_finder.cpp
View file

@ -1180,7 +1180,6 @@ namespace smt {
unsigned m_var_j;
public:
f_var(ast_manager& m, func_decl* f, unsigned i, unsigned j) : qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {}
~f_var() override {}
char const* get_kind() const override {
return "f_var";
@ -1261,7 +1260,6 @@ namespace smt {
f_var(m, f, i, j),
m_offset(offset, m) {
}
~f_var_plus_offset() override {}
char const* get_kind() const override {
return "f_var_plus_offset";
@ -1427,7 +1425,6 @@ namespace smt {
public:
select_var(ast_manager& m, app* s, unsigned i, unsigned j) :qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
~select_var() override {}
char const* get_kind() const override {
return "select_var";
@ -1497,8 +1494,6 @@ namespace smt {
std::swap(m_var_i, m_var_j);
}
~var_pair() override {}
bool is_equal(qinfo const* qi) const override {
if (qi->get_kind() != get_kind())
return false;
@ -1577,7 +1572,6 @@ namespace smt {
var_expr_pair(ast_manager& m, unsigned i, expr* t) :
qinfo(m),
m_var_i(i), m_t(t, m) {}
~var_expr_pair() override {}
bool is_equal(qinfo const* qi) const override {
if (qi->get_kind() != get_kind())

3
src/smt/smt_quantifier.cpp
View file

@ -606,9 +606,6 @@ namespace smt {
m_active(false) {
}
~default_qm_plugin() override {
}
void set_manager(quantifier_manager & qm) override {
SASSERT(m_qm == nullptr);
m_qm = &qm;

4
src/smt/smt_relevancy.cpp
View file

@ -52,7 +52,6 @@ namespace smt {
app * m_parent;
public:
and_relevancy_eh(app * p):m_parent(p) {}
~and_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -60,7 +59,6 @@ namespace smt {
app * m_parent;
public:
or_relevancy_eh(app * p):m_parent(p) {}
~or_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -68,7 +66,6 @@ namespace smt {
app * m_parent;
public:
ite_relevancy_eh(app * p):m_parent(p) {}
~ite_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -78,7 +75,6 @@ namespace smt {
app * m_else_eq;
public:
ite_term_relevancy_eh(app * p, app * then_eq, app * else_eq):m_parent(p), m_then_eq(then_eq), m_else_eq(else_eq) {}
~ite_term_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};

4
src/smt/theory_arith.h
View file

@ -319,7 +319,6 @@ namespace smt {
public:
atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind);
atom_kind get_atom_kind() const { return static_cast<atom_kind>(m_atom_kind); }
~atom() override {}
inline inf_numeral const & get_k() const { return m_k; }
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_is_true; }
@ -341,7 +340,6 @@ namespace smt {
m_rhs(rhs) {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
}
~eq_bound() override {}
bool has_justification() const override { return true; }
void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
@ -357,7 +355,6 @@ namespace smt {
friend class theory_arith;
public:
derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
~derived_bound() override {}
literal_vector const& lits() const { return m_lits; }
eq_vector const& eqs() const { return m_eqs; }
bool has_justification() const override { return true; }
@ -374,7 +371,6 @@ namespace smt {
friend class theory_arith;
public:
justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {}
~justified_derived_bound() override {}
bool has_justification() const override { return true; }
void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override;
void push_lit(literal l, numeral const& coeff) override;

1
src/smt/theory_array_bapa.cpp
View file

@ -450,7 +450,6 @@ namespace smt {
app* m_obj;
public:
remove_sz(ast_manager& m, obj_map<app, sz_info*>& tab, app* t): m(m), m_table(tab), m_obj(t) { }
~remove_sz() override {}
void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
};

2
src/smt/theory_array_base.cpp
View file

@ -890,8 +890,6 @@ namespace smt {
m_unspecified_else(true) {
}
~array_value_proc() override {}
void add_entry(unsigned num_args, enode * const * args, enode * value) {
SASSERT(num_args > 0);
SASSERT(m_dim == 0 || m_dim == num_args);

2
src/smt/theory_bv.h
View file

@ -56,7 +56,6 @@ namespace smt {
struct bit_atom : public atom {
var_pos_occ * m_occs;
bit_atom():m_occs(nullptr) {}
~bit_atom() override {}
bool is_bit() const override { return true; }
};
@ -64,7 +63,6 @@ namespace smt {
literal m_var;
literal m_def;
le_atom(literal v, literal d):m_var(v), m_def(d) {}
~le_atom() override {}
bool is_bit() const override { return false; }
};

1
src/smt/theory_datatype.cpp
View file

@ -823,7 +823,6 @@ namespace smt {
public:
datatype_value_proc(func_decl * d):m_constructor(d) {}
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
~datatype_value_proc() override {}
void get_dependencies(buffer<model_value_dependency> & result) override {
result.append(m_dependencies.size(), m_dependencies.data());
}

1
src/smt/theory_dummy.h
View file

@ -46,7 +46,6 @@ namespace smt {
public:
theory_dummy(context& ctx, family_id fid, char const * name);
~theory_dummy() override {}
theory * mk_fresh(context * new_ctx) override { return alloc(theory_dummy, *new_ctx, get_family_id(), m_name); }

3
src/smt/theory_fpa.h
View file

@ -47,8 +47,6 @@ namespace smt {
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
m_ebits(ebits), m_sbits(sbits) {}
~fpa_value_proc() override {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
void get_dependencies(buffer<model_value_dependency> & result) override {
@ -75,7 +73,6 @@ namespace smt {
result.append(m_deps);
}
~fpa_rm_value_proc() override {}
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
};

1
src/smt/theory_seq.cpp
View file

@ -1923,7 +1923,6 @@ public:
seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) {
(void)m_node;
}
~seq_value_proc() override {}
void add_unit(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
m_source.push_back(unit_source);

5
src/smt/theory_seq.h
View file

@ -230,7 +230,6 @@ namespace smt {
expr_ref m_e;
public:
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_length_coherence() override {}
void operator()(theory_seq& th) override {
th.check_length_coherence(m_e);
m_e.reset();
@ -241,7 +240,6 @@ namespace smt {
expr_ref m_e;
public:
replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_fixed_length() override {}
void operator()(theory_seq& th) override {
th.fixed_length(m_e, false, false);
m_e.reset();
@ -252,7 +250,6 @@ namespace smt {
expr_ref m_e;
public:
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_axiom() override {}
void operator()(theory_seq& th) override {
th.enque_axiom(m_e);
m_e.reset();
@ -264,7 +261,6 @@ namespace smt {
bool m_sign;
public:
replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {}
~replay_unit_literal() override {}
void operator()(theory_seq& th) override {
literal lit = th.mk_literal(m_e);
if (m_sign) lit.neg();
@ -278,7 +274,6 @@ namespace smt {
expr_ref m_e;
public:
replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_is_axiom() override {}
void operator()(theory_seq& th) override {
th.check_int_string(m_e);
m_e.reset();

2
src/smt/theory_str.h
View file

@ -51,7 +51,6 @@ public:
str_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
u(m), delim("!"), m_next(0) {}
~str_value_factory() override {}
expr * get_some_value(sort * s) override {
return u.str.mk_string("some value");
}
@ -93,7 +92,6 @@ class binary_search_trail : public trail {
public:
binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
target(target), entry(entry) {}
~binary_search_trail() override {}
void undo() override {
TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
if (target.contains(entry)) {

5
src/smt/theory_wmaxsat.h
View file

@ -74,10 +74,7 @@ namespace smt {
m_old_values(old) {
old.push_back(value);
}
~numeral_trail() override {
}
void undo() override {
m_value = m_old_values.back();
m_old_values.shrink(m_old_values.size() - 1);

1
src/solver/combined_solver.cpp
View file

@ -398,7 +398,6 @@ class combined_solver_factory : public solver_factory {
scoped_ptr<solver_factory> m_f2;
public:
combined_solver_factory(solver_factory * f1, solver_factory * f2):m_f1(f1), m_f2(f2) {}
~combined_solver_factory() override {}
solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),

1
src/solver/solver.h
View file

@ -53,7 +53,6 @@ class solver : public check_sat_result, public user_propagator::core {
symbol m_cancel_backup_file;
public:
solver() {}
~solver() override {}
/**
\brief Creates a clone of the solver.

4
src/solver/tactic2solver.cpp
View file

@ -357,9 +357,7 @@ class tactic2solver_factory : public solver_factory {
public:
tactic2solver_factory(tactic * t):m_tactic(t) {
}
~tactic2solver_factory() override {}
solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
}

Some files were not shown because too many files have changed in this diff Show more