mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
fix errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
61f99b242e
commit
6f610674fa
3 changed files with 14 additions and 17 deletions
|
@ -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 {
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -36,7 +36,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void display(std::ostream& out) {
|
||||
out << m_dep << "\n";
|
||||
out << m_dep.get() << "\n";
|
||||
}
|
||||
};
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue