mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Fix inconsistent missing override warnings.

Browse source
This commit is contained in:
Bruce Mitchener 2018-02-06 11:23:08 +07:00
parent b2bd4dd3b4
commit 5911f810ed
1 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/qe/qe.cpp
View file

@ -1536,19 +1536,19 @@ namespace qe {
pop(*model_eval); pop(*model_eval);
} }
ast_manager& get_manager() { return m; } ast_manager& get_manager() override { return m; }
atom_set const& pos_atoms() const { return m_current->pos_atoms(); } atom_set const& pos_atoms() const override { return m_current->pos_atoms(); }
atom_set const& neg_atoms() const { return m_current->neg_atoms(); } atom_set const& neg_atoms() const override { return m_current->neg_atoms(); }
unsigned get_num_vars() const { return m_current->num_free_vars(); } unsigned get_num_vars() const override { return m_current->num_free_vars(); }
app* get_var(unsigned idx) const { return m_current->free_var(idx); } app* get_var(unsigned idx) const override { return m_current->free_var(idx); }
app_ref_vector const& get_vars() const { return m_current->free_vars(); } app_ref_vector const& get_vars() const override { return m_current->free_vars(); }
contains_app& contains(unsigned idx) { return contains(get_var(idx)); } contains_app& contains(unsigned idx) override { return contains(get_var(idx)); }
// //
// The variable at idx is eliminated (without branching). // The variable at idx is eliminated (without branching).
@ -1564,7 +1564,7 @@ namespace qe {
normalize(*m_current); normalize(*m_current);
} }
void add_var(app* x) { void add_var(app* x) override {
m_new_vars.push_back(x); m_new_vars.push_back(x);
if (m_var2branch.contains(x)) { if (m_var2branch.contains(x)) {
return; return;
@ -1583,7 +1583,7 @@ namespace qe {
m_var2branch.insert(x, bv); m_var2branch.insert(x, bv);
} }
virtual void add_constraint(bool use_current_val, expr* l1 = 0, expr* l2 = 0, expr* l3 = 0) { void add_constraint(bool use_current_val, expr* l1 = 0, expr* l2 = 0, expr* l3 = 0) override {
search_tree* node = m_current; search_tree* node = m_current;
if (!use_current_val) { if (!use_current_val) {
node = m_current->parent(); node = m_current->parent();
@ -1602,7 +1602,7 @@ namespace qe {
m_solver.assert_expr(fml); m_solver.assert_expr(fml);
} }
void blast_or(app* var, expr_ref& fml) { void blast_or(app* var, expr_ref& fml) override {
m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, 0); m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, 0);
} }