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

Use 'override' where possible.

Browse source
This commit is contained in:
Bruce Mitchener 2018-10-02 10:26:38 +07:00
parent b0dac346dc
commit 373b691709
19 changed files with 123 additions and 123 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_generalizers.cpp
View file

@ -50,7 +50,7 @@ namespace{
contains_array_op_proc(ast_manager &manager) :
m(manager), m_array_fid(m.mk_family_id("array"))
{}
virtual bool operator()(expr *e) {
bool operator()(expr *e) override {
return is_app(e) && to_app(e)->get_family_id() == m_array_fid;
}
};

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

@ -117,11 +117,11 @@ class lemma_quantifier_generalizer : public lemma_generalizer {
int m_offset;
public:
lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true);
virtual ~lemma_quantifier_generalizer() {}
virtual void operator()(lemma_ref &lemma);
~lemma_quantifier_generalizer() override {}
void operator()(lemma_ref &lemma) override;
virtual void collect_statistics(statistics& st) const;
virtual void reset_statistics() {m_st.reset();}
void collect_statistics(statistics& st) const override;
void reset_statistics() override {m_st.reset();}
private:
bool generalize(lemma_ref &lemma, app *term);

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

@ -126,7 +126,7 @@ namespace datalog {
*/
mk_synchronize(context & ctx, unsigned priority = 22500);
rule_set * operator()(rule_set const & source);
rule_set * operator()(rule_set const & source) override;
};
};

10
src/opt/maxres.cpp
View file

@ -144,7 +144,7 @@ public:
}
}
virtual ~maxres() {}
~maxres() override {}
bool is_literal(expr* l) {
return
@ -332,7 +332,7 @@ public:
}
virtual lbool operator()() {
lbool operator()() override {
m_defs.reset();
switch(m_st) {
case s_primal:
@ -343,7 +343,7 @@ public:
return l_undef;
}
virtual void collect_statistics(statistics& st) const {
void collect_statistics(statistics& st) const override {
st.update("maxres-cores", m_stats.m_num_cores);
st.update("maxres-correction-sets", m_stats.m_num_cs);
}
@ -781,7 +781,7 @@ public:
TRACE("opt", tout << "after remove: " << asms << "\n";);
}
virtual void updt_params(params_ref& _p) {
void updt_params(params_ref& _p) override {
maxsmt_solver_base::updt_params(_p);
opt_params p(_p);
m_hill_climb = p.maxres_hill_climb();
@ -816,7 +816,7 @@ public:
return l_true;
}
virtual void commit_assignment() {
void commit_assignment() override {
if (m_found_feasible_optimum) {
TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;);
s().assert_expr(m_defs);

54
src/opt/opt_cmds.cpp
View file

@ -56,33 +56,33 @@ public:
m_opt(opt)
{}
virtual ~assert_soft_cmd() {
~assert_soft_cmd() override {
}
virtual void reset(cmd_context & ctx) {
void reset(cmd_context & ctx) override {
m_idx = 0;
m_formula = nullptr;
}
virtual char const * get_usage() const { return "<formula> [:weight <rational-weight>] [:id <symbol>]"; }
virtual char const * get_main_descr() const { return "assert soft constraint with optional weight and identifier"; }
char const * get_usage() const override { return "<formula> [:weight <rational-weight>] [:id <symbol>]"; }
char const * get_main_descr() const override { return "assert soft constraint with optional weight and identifier"; }
// command invocation
virtual void prepare(cmd_context & ctx) {
void prepare(cmd_context & ctx) override {
reset(ctx);
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
if (m_idx == 0) return CPK_EXPR;
return parametric_cmd::next_arg_kind(ctx);
}
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
p.insert("weight", CPK_NUMERAL, "(default: 1) penalty of not satisfying constraint.");
p.insert("id", CPK_SYMBOL, "(default: null) partition identifier for soft constraints.");
}
virtual void set_next_arg(cmd_context & ctx, expr * t) {
void set_next_arg(cmd_context & ctx, expr * t) override {
SASSERT(m_idx == 0);
if (!ctx.m().is_bool(t)) {
throw cmd_exception("Invalid type for expression. Expected Boolean type.");
@ -91,11 +91,11 @@ public:
++m_idx;
}
virtual void failure_cleanup(cmd_context & ctx) {
void failure_cleanup(cmd_context & ctx) override {
reset(ctx);
}
virtual void execute(cmd_context & ctx) {
void execute(cmd_context & ctx) override {
if (!m_formula) {
throw cmd_exception("assert-soft requires a formulas as argument.");
}
@ -107,7 +107,7 @@ public:
reset(ctx);
}
virtual void finalize(cmd_context & ctx) {
void finalize(cmd_context & ctx) override {
}
};
@ -123,14 +123,14 @@ public:
m_opt(opt)
{}
virtual void reset(cmd_context & ctx) { }
virtual char const * get_usage() const { return "<term>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
virtual unsigned get_arity() const { return 1; }
virtual void prepare(cmd_context & ctx) {}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
void reset(cmd_context & ctx) override { }
char const * get_usage() const override { return "<term>"; }
char const * get_descr(cmd_context & ctx) const override { return "check sat modulo objective function";}
unsigned get_arity() const override { return 1; }
void prepare(cmd_context & ctx) override {}
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }
virtual void set_next_arg(cmd_context & ctx, expr * t) {
void set_next_arg(cmd_context & ctx, expr * t) override {
if (!is_app(t)) {
throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
}
@ -138,11 +138,11 @@ public:
ctx.print_success();
}
virtual void failure_cleanup(cmd_context & ctx) {
void failure_cleanup(cmd_context & ctx) override {
reset(ctx);
}
virtual void execute(cmd_context & ctx) {
void execute(cmd_context & ctx) override {
}
};
@ -154,18 +154,18 @@ public:
m_opt(opt)
{}
virtual void reset(cmd_context & ctx) { }
virtual char const * get_usage() const { return "(get-objectives)"; }
virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; }
virtual unsigned get_arity() const { return 0; }
virtual void prepare(cmd_context & ctx) {}
void reset(cmd_context & ctx) override { }
char const * get_usage() const override { return "(get-objectives)"; }
char const * get_descr(cmd_context & ctx) const override { return "retrieve the objective values (after optimization)"; }
unsigned get_arity() const override { return 0; }
void prepare(cmd_context & ctx) override {}
virtual void failure_cleanup(cmd_context & ctx) {
void failure_cleanup(cmd_context & ctx) override {
reset(ctx);
}
virtual void execute(cmd_context & ctx) {
void execute(cmd_context & ctx) override {
if (!ctx.ignore_check()) {
get_opt(ctx, m_opt).display_assignment(ctx.regular_stream());
}

4
src/opt/sortmax.cpp
View file

@ -39,9 +39,9 @@ namespace opt {
sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {}
virtual ~sortmax() {}
~sortmax() override {}
lbool operator()() {
lbool operator()() override {
obj_map<expr, rational> soft;
if (!init()) {
return l_false;

4
src/opt/wmax.cpp
View file

@ -49,9 +49,9 @@ namespace opt {
m_trail(m),
m_defs(m) {}
virtual ~wmax() {}
~wmax() override {}
lbool operator()() {
lbool operator()() override {
TRACE("opt", tout << "weighted maxsat\n";);
scoped_ensure_theory wth(*this);
obj_map<expr, rational> soft;

106
src/sat/ba_solver.h
View file

@ -128,7 +128,7 @@ namespace sat {
virtual void set_k(unsigned k) { VERIFY(k < 4000000000); m_k = k; }
virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; }
unsigned k() const { return m_k; }
virtual bool well_formed() const;
bool well_formed() const override;
};
class card : public pb_base {
@ -140,13 +140,13 @@ namespace sat {
literal& operator[](unsigned i) { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
virtual void negate();
virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
virtual literal_vector literals() const { return literal_vector(m_size, m_lits); }
virtual bool is_watching(literal l) const;
virtual literal get_lit(unsigned i) const { return m_lits[i]; }
virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; }
virtual unsigned get_coeff(unsigned i) const { return 1; }
void negate() override;
void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
literal_vector literals() const override { return literal_vector(m_size, m_lits); }
bool is_watching(literal l) const override;
literal get_lit(unsigned i) const override { return m_lits[i]; }
void set_lit(unsigned i, literal l) override { m_lits[i] = l; }
unsigned get_coeff(unsigned i) const override { return 1; }
};
@ -173,14 +173,14 @@ namespace sat {
void update_max_sum();
void set_num_watch(unsigned s) { m_num_watch = s; }
bool is_cardinality() const;
virtual void negate();
virtual void set_k(unsigned k) { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
virtual bool is_watching(literal l) const;
virtual literal get_lit(unsigned i) const { return m_wlits[i].second; }
virtual void set_lit(unsigned i, literal l) { m_wlits[i].second = l; }
virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
void negate() override;
void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); }
literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
bool is_watching(literal l) const override;
literal get_lit(unsigned i) const override { return m_wlits[i].second; }
void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; }
unsigned get_coeff(unsigned i) const override { return m_wlits[i].first; }
};
class xr : public constraint {
@ -191,13 +191,13 @@ namespace sat {
literal operator[](unsigned i) const { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return begin() + m_size; }
virtual void negate() { m_lits[0].neg(); }
virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
virtual bool is_watching(literal l) const;
virtual literal_vector literals() const { return literal_vector(size(), begin()); }
virtual literal get_lit(unsigned i) const { return m_lits[i]; }
virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; }
virtual bool well_formed() const;
void negate() override { m_lits[0].neg(); }
void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
bool is_watching(literal l) const override;
literal_vector literals() const override { return literal_vector(size(), begin()); }
literal get_lit(unsigned i) const override { return m_lits[i]; }
void set_lit(unsigned i, literal l) override { m_lits[i] = l; }
bool well_formed() const override;
};
@ -484,44 +484,44 @@ namespace sat {
public:
ba_solver();
virtual ~ba_solver();
virtual void set_solver(solver* s) { m_solver = s; }
virtual void set_lookahead(lookahead* l) { m_lookahead = l; }
virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; }
~ba_solver() override;
void set_solver(solver* s) override { m_solver = s; }
void set_lookahead(lookahead* l) override { m_lookahead = l; }
void set_unit_walk(unit_walk* u) override { m_unit_walk = u; }
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
void add_xr(literal_vector const& lits);
virtual bool propagate(literal l, ext_constraint_idx idx);
virtual lbool resolve_conflict();
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
virtual void asserted(literal l);
virtual check_result check();
virtual void push();
virtual void pop(unsigned n);
virtual void simplify();
virtual void clauses_modifed();
virtual lbool get_phase(bool_var v);
virtual bool set_root(literal l, literal r);
virtual void flush_roots();
virtual std::ostream& display(std::ostream& out) const;
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const;
virtual void collect_statistics(statistics& st) const;
virtual extension* copy(solver* s);
virtual extension* copy(lookahead* s, bool learned);
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes);
virtual void pop_reinit();
virtual void gc();
virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const;
virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r);
virtual void init_use_list(ext_use_list& ul);
virtual bool is_blocked(literal l, ext_constraint_idx idx);
virtual bool check_model(model const& m) const;
bool propagate(literal l, ext_constraint_idx idx) override;
lbool resolve_conflict() override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
void asserted(literal l) override;
check_result check() override;
void push() override;
void pop(unsigned n) override;
void simplify() override;
void clauses_modifed() override;
lbool get_phase(bool_var v) override;
bool set_root(literal l, literal r) override;
void flush_roots() override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
void collect_statistics(statistics& st) const override;
extension* copy(solver* s) override;
extension* copy(lookahead* s, bool learned) override;
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
void pop_reinit() override;
void gc() override;
double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const override;
bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override;
void init_use_list(ext_use_list& ul) override;
bool is_blocked(literal l, ext_constraint_idx idx) override;
bool check_model(model const& m) const override;
ptr_vector<constraint> const & constraints() const { return m_constraints; }
void display(std::ostream& out, constraint const& c, bool values) const;
virtual bool validate();
bool validate() override;
};

2
src/sat/sat_lookahead.cpp
View file

@ -1217,7 +1217,7 @@ namespace sat {
lookahead& lh;
public:
lookahead_literal_occs_fun(lookahead& lh): lh(lh) {}
double operator()(literal l) { return lh.literal_occs(l); }
double operator()(literal l) override { return lh.literal_occs(l); }
};
// Ternary clause managagement:

2
src/sat/tactic/goal2sat.h
View file

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

2
src/smt/theory_lra.cpp
View file

@ -147,7 +147,7 @@ class theory_lra::imp {
imp& m_imp;
public:
resource_limit(imp& i): m_imp(i) { }
virtual bool get_cancel_flag() { return m_imp.m.canceled(); }
bool get_cancel_flag() override { return m_imp.m.canceled(); }
};

6
src/smt/theory_pb.cpp
View file

@ -759,18 +759,18 @@ namespace smt {
card& get_card() { return m_card; }
virtual void get_antecedents(conflict_resolution& cr) {
void get_antecedents(conflict_resolution& cr) override {
cr.mark_literal(m_card.lit());
for (unsigned i = m_card.k(); i < m_card.size(); ++i) {
cr.mark_literal(~m_card.lit(i));
}
}
virtual theory_id get_from_theory() const {
theory_id get_from_theory() const override {
return m_fid;
}
virtual proof* mk_proof(smt::conflict_resolution& cr) {
proof* mk_proof(smt::conflict_resolution& cr) override {
ptr_buffer<proof> prs;
ast_manager& m = cr.get_context().get_manager();
expr_ref fact(m);

2
src/smt/theory_str.cpp
View file

@ -110,7 +110,7 @@ namespace smt {
public:
seq_expr_solver(ast_manager& m, smt_params& fp):
m_kernel(m, fp) {}
virtual lbool check_sat(expr* e) {
lbool check_sat(expr* e) override {
m_kernel.push();
m_kernel.assert_expr(e);
lbool r = m_kernel.check();

12
src/solver/parallel_tactic.cpp
View file

@ -672,7 +672,7 @@ public:
init();
}
void operator ()(const goal_ref & g,goal_ref_buffer & result) {
void operator ()(const goal_ref & g,goal_ref_buffer & result) override {
fail_if_proof_generation("parallel-tactic", g);
ast_manager& m = g->m();
solver* s = m_solver->translate(m, m_params);
@ -719,29 +719,29 @@ public:
return pp.conquer_batch_size();
}
void cleanup() {
void cleanup() override {
m_queue.reset();
}
tactic* translate(ast_manager& m) {
tactic* translate(ast_manager& m) override {
solver* s = m_solver->translate(m, m_params);
return alloc(parallel_tactic, s, m_params);
}
virtual void updt_params(params_ref const & p) {
void updt_params(params_ref const & p) override {
m_params.copy(p);
parallel_params pp(p);
m_conquer_delay = pp.conquer_delay();
}
virtual void collect_statistics(statistics & st) const {
void collect_statistics(statistics & st) const override {
st.copy(m_stats);
st.update("par unsat", m_num_unsat);
st.update("par models", m_models.size());
st.update("par progress", m_progress);
}
virtual void reset_statistics() {
void reset_statistics() override {
m_stats.reset();
}
};

2
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -40,7 +40,7 @@ public:
void operator()(goal_ref const & g,
goal_ref_buffer & result) override;
virtual void cleanup() override;
void cleanup() override;
};
class ac_rewriter {

18
src/tactic/dependency_converter.cpp
View file

@ -27,15 +27,15 @@ public:
unit_dependency_converter(expr_dependency_ref& d) : m_dep(d) {}
virtual expr_dependency_ref operator()() { return m_dep; }
expr_dependency_ref operator()() override { return m_dep; }
virtual dependency_converter * translate(ast_translation & translator) {
dependency_converter * translate(ast_translation & translator) override {
expr_dependency_translation tr(translator);
expr_dependency_ref d(tr(m_dep), translator.to());
return alloc(unit_dependency_converter, d);
}
virtual void display(std::ostream& out) {
void display(std::ostream& out) override {
out << m_dep.get() << "\n";
}
};
@ -47,18 +47,18 @@ public:
concat_dependency_converter(dependency_converter* c1, dependency_converter* c2) : m_dc1(c1), m_dc2(c2) {}
virtual expr_dependency_ref operator()() {
expr_dependency_ref operator()() override {
expr_dependency_ref d1 = (*m_dc1)();
expr_dependency_ref d2 = (*m_dc2)();
ast_manager& m = d1.get_manager();
return expr_dependency_ref(m.mk_join(d1, d2), m);
}
virtual dependency_converter * translate(ast_translation & translator) {
dependency_converter * translate(ast_translation & translator) override {
return alloc(concat_dependency_converter, m_dc1->translate(translator), m_dc2->translate(translator));
}
virtual void display(std::ostream& out) {
void display(std::ostream& out) override {
m_dc1->display(out);
m_dc2->display(out);
}
@ -73,7 +73,7 @@ public:
for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]);
}
virtual expr_dependency_ref operator()() {
expr_dependency_ref operator()() override {
expr_dependency_ref result(m.mk_empty_dependencies(), m);
for (goal_ref g : m_goals) {
dependency_converter_ref dc = g->dc();
@ -81,13 +81,13 @@ public:
}
return result;
}
virtual dependency_converter * translate(ast_translation & translator) {
dependency_converter * translate(ast_translation & translator) override {
goal_ref_buffer goals;
for (goal_ref g : m_goals) goals.push_back(g->translate(translator));
return alloc(goal_dependency_converter, goals.size(), goals.c_ptr());
}
virtual void display(std::ostream& out) { out << "goal-dep\n"; }
void display(std::ostream& out) override { out << "goal-dep\n"; }
};

2
src/tactic/generic_model_converter.h
View file

@ -41,7 +41,7 @@ class generic_model_converter : public model_converter {
public:
generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
virtual ~generic_model_converter();
~generic_model_converter() override;
void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }

6
src/tactic/tactical.cpp
View file

@ -744,7 +744,7 @@ public:
SASSERT(t);
}
virtual ~unary_tactical() { }
~unary_tactical() override { }
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
m_t->operator()(in, result);
@ -1003,7 +1003,7 @@ public:
SASSERT(m_p);
}
virtual ~cond_tactical() {}
~cond_tactical() override {}
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
if (m_p->operator()(*(in.get())).is_true())
@ -1035,7 +1035,7 @@ public:
SASSERT(m_p);
}
virtual ~fail_if_tactic() {}
~fail_if_tactic() override {}
void cleanup() override {}

2
src/util/lp/lar_solver.h
View file

@ -397,7 +397,7 @@ public:
column_type get_column_type(unsigned j) const;
std::string get_column_name(unsigned j) const;
std::string get_column_name(unsigned j) const override;
bool all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side);