mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

fix compiler warnings

Browse source
This commit is contained in:
Nuno Lopes 2022-10-12 10:02:21 +01:00
parent 8ad480ab59
commit a7f018aa03
6 changed files with 4 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/arith_proof_checker.h
View file

@ -303,8 +303,6 @@ namespace arith {
m_implied_eq("implied-eq"), m_implied_eq("implied-eq"),
m_bound("bound") {} m_bound("bound") {}
~proof_checker() override {}
void reset() { void reset() {
m_ineq.reset(); m_ineq.reset();
m_conseq.reset(); m_conseq.reset();

8
src/sat/smt/euf_ackerman.h
View file

@ -29,12 +29,12 @@ namespace euf {
class ackerman { class ackerman {
struct inference : dll_base<inference>{ struct inference : dll_base<inference>{
bool is_cc;
expr* a, *b, *c; expr* a, *b, *c;
unsigned m_count{ 0 }; unsigned m_count{ 0 };
inference():is_cc(false), a(nullptr), b(nullptr), c(nullptr) {} bool is_cc;
inference(app* a, app* b):is_cc(true), a(a), b(b), c(nullptr) {} inference(): a(nullptr), b(nullptr), c(nullptr), is_cc(false) {}
inference(expr* a, expr* b, expr* c):is_cc(false), a(a), b(b), c(c) {} inference(app* a, app* b): a(a), b(b), c(nullptr), is_cc(true) {}
inference(expr* a, expr* b, expr* c): a(a), b(b), c(c), is_cc(false) {}
}; };
struct inference_eq { struct inference_eq {

5
src/sat/smt/euf_proof_checker.cpp
View file

@ -23,7 +23,6 @@ Author:
#include "sat/smt/arith_proof_checker.h" #include "sat/smt/arith_proof_checker.h"
#include "sat/smt/q_proof_checker.h" #include "sat/smt/q_proof_checker.h"
#include "sat/smt/tseitin_proof_checker.h" #include "sat/smt/tseitin_proof_checker.h"
#include <iostream>
namespace euf { namespace euf {
@ -121,8 +120,6 @@ namespace euf {
public: public:
eq_proof_checker(ast_manager& m): m(m) {} eq_proof_checker(ast_manager& m): m(m) {}
~eq_proof_checker() override {}
expr_ref_vector clause(app* jst) override { expr_ref_vector clause(app* jst) override {
expr_ref_vector result(m); expr_ref_vector result(m);
for (expr* arg : *jst) for (expr* arg : *jst)
@ -213,8 +210,6 @@ namespace euf {
public: public:
res_proof_checker(ast_manager& m, proof_checker& pc): m(m), pc(pc) {} res_proof_checker(ast_manager& m, proof_checker& pc): m(m), pc(pc) {}
~res_proof_checker() override {}
bool check(app* jst) override { bool check(app* jst) override {
if (jst->get_num_args() != 3) if (jst->get_num_args() != 3)

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

@ -60,7 +60,6 @@ namespace euf {
symbol m_rule; symbol m_rule;
public: public:
smt_proof_checker_plugin(ast_manager& m, symbol const& n): m(m), m_rule(n) {} smt_proof_checker_plugin(ast_manager& m, symbol const& n): m(m), m_rule(n) {}
~smt_proof_checker_plugin() override {}
bool check(app* jst) override { return false; } bool check(app* jst) override { return false; }
expr_ref_vector clause(app* jst) override; expr_ref_vector clause(app* jst) override;
void register_plugins(proof_checker& pc) override { pc.register_plugin(m_rule, this); } void register_plugins(proof_checker& pc) override { pc.register_plugin(m_rule, this); }

2
src/sat/smt/q_proof_checker.h
View file

@ -42,8 +42,6 @@ namespace q {
m_inst("inst"), m_inst("inst"),
m_bind("bind") { m_bind("bind") {
} }
~proof_checker() override {}
expr_ref_vector clause(app* jst) override; expr_ref_vector clause(app* jst) override;

2
src/sat/smt/tseitin_proof_checker.h
View file

@ -61,8 +61,6 @@ namespace tseitin {
m(m) { m(m) {
} }
~proof_checker() override {}
expr_ref_vector clause(app* jst) override; expr_ref_vector clause(app* jst) override;
bool check(app* jst) override; bool check(app* jst) override;