From 6f610674fa4a94675fe5b99f32b03c84c3fe1b57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Feb 2018 15:31:57 -0800 Subject: [PATCH] fix errors Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.h | 11 ++++------- src/tactic/core/elim_term_ite_tactic.cpp | 18 +++++++++--------- src/tactic/dependency_converter.cpp | 2 +- 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index e2fbe81fa..8ebbe9cb4 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -129,17 +129,14 @@ public: m_trail(m), m_args(m), m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {} - virtual ~dom_simplify_tactic(); - virtual tactic * translate(ast_manager & m); - virtual void updt_params(params_ref const & p) {} + tactic * translate(ast_manager & m) override; + void updt_params(params_ref const & p) override {} static void get_param_descrs(param_descrs & r) {} - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - + void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); } void operator()(goal_ref const & in, goal_ref_buffer & result) override; - - virtual void cleanup(); + void cleanup() override; }; class expr_substitution_simplifier : public dom_simplifier { diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 49815b6d1..c8591840d 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -136,33 +136,33 @@ public: m_params(p) { m_imp = alloc(imp, m, p); } - - virtual tactic * translate(ast_manager & m) { - return alloc(elim_term_ite_tactic, m, m_params); - } virtual ~elim_term_ite_tactic() { dealloc(m_imp); } - virtual void updt_params(params_ref const & p) { + tactic * translate(ast_manager & m) override { + return alloc(elim_term_ite_tactic, m, m_params); + } + + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { + void collect_param_descrs(param_descrs & r) override { insert_max_memory(r); insert_max_steps(r); r.insert("max_args", CPK_UINT, "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result) { + void operator()(goal_ref const & in, + goal_ref_buffer & result) override { (*m_imp)(in, result); } - virtual void cleanup() { + void cleanup() override { ast_manager & m = m_imp->m; m_imp->~imp(); m_imp = new (m_imp) imp(m, m_params); diff --git a/src/tactic/dependency_converter.cpp b/src/tactic/dependency_converter.cpp index fbd445d52..34c864526 100644 --- a/src/tactic/dependency_converter.cpp +++ b/src/tactic/dependency_converter.cpp @@ -36,7 +36,7 @@ public: } virtual void display(std::ostream& out) { - out << m_dep << "\n"; + out << m_dep.get() << "\n"; } };