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

elim_uncnstr_tactic: remove m_imp idiom to reduce mem alloc

Browse source
This commit is contained in:
Nuno Lopes 2018-12-21 19:48:18 +00:00
parent e1dc553228
commit 52f960a7c8
2 changed files with 806 additions and 832 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -28,9 +28,9 @@ Notes:
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
namespace {
class elim_uncnstr_tactic : public tactic { class elim_uncnstr_tactic : public tactic {
struct imp {
// unconstrained vars collector // unconstrained vars collector
typedef generic_model_converter mc; typedef generic_model_converter mc;
@ -786,21 +786,10 @@ class elim_uncnstr_tactic : public tactic {
ref<mc> m_mc; ref<mc> m_mc;
obj_hashtable<expr> m_vars; obj_hashtable<expr> m_vars;
scoped_ptr<rw> m_rw; scoped_ptr<rw> m_rw;
unsigned m_num_elim_apps; unsigned m_num_elim_apps = 0;
unsigned long long m_max_memory; unsigned long long m_max_memory;
unsigned m_max_steps; unsigned m_max_steps;
imp(ast_manager & m, params_ref const & p):
m_manager(m),
m_num_elim_apps(0) {
updt_params(p);
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
}
ast_manager & m() { return m_manager; } ast_manager & m() { return m_manager; }
void init_mc(bool produce_models) { void init_mc(bool produce_models) {
@ -814,7 +803,7 @@ class elim_uncnstr_tactic : public tactic {
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps); m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
} }
void operator()(goal_ref const & g, goal_ref_buffer & result) { void run(goal_ref const & g, goal_ref_buffer & result) {
bool produce_proofs = g->proofs_enabled(); bool produce_proofs = g->proofs_enabled();
TRACE("elim_uncnstr_bug", g->display(tout);); TRACE("elim_uncnstr_bug", g->display(tout););
@ -882,27 +871,21 @@ class elim_uncnstr_tactic : public tactic {
} }
} }
};
imp * m_imp;
params_ref m_params; params_ref m_params;
public: public:
elim_uncnstr_tactic(ast_manager & m, params_ref const & p): elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
m_params(p) { m_manager(m), m_params(p) {
m_imp = alloc(imp, m, p); updt_params(p);
} }
tactic * translate(ast_manager & m) override { tactic * translate(ast_manager & m) override {
return alloc(elim_uncnstr_tactic, m, m_params); return alloc(elim_uncnstr_tactic, m, m_params);
} }
~elim_uncnstr_tactic() override {
dealloc(m_imp);
}
void updt_params(params_ref const & p) override { void updt_params(params_ref const & p) override {
m_params = p; m_params = p;
m_imp->updt_params(p); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
} }
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
@ -912,32 +895,26 @@ public:
void operator()(goal_ref const & g, void operator()(goal_ref const & g,
goal_ref_buffer & result) override { goal_ref_buffer & result) override {
(*m_imp)(g, result); run(g, result);
report_tactic_progress(":num-elim-apps", get_num_elim_apps()); report_tactic_progress(":num-elim-apps", m_num_elim_apps);
} }
void cleanup() override { void cleanup() override {
unsigned num_elim_apps = get_num_elim_apps(); m_mc = nullptr;
ast_manager & m = m_imp->m_manager; m_rw = nullptr;
imp * d = alloc(imp, m, m_params); m_vars.reset();
std::swap(d, m_imp);
dealloc(d);
m_imp->m_num_elim_apps = num_elim_apps;
}
unsigned get_num_elim_apps() const {
return m_imp->m_num_elim_apps;
} }
void collect_statistics(statistics & st) const override { void collect_statistics(statistics & st) const override {
st.update("eliminated applications", get_num_elim_apps()); st.update("eliminated applications", m_num_elim_apps);
} }
void reset_statistics() override { void reset_statistics() override {
m_imp->m_num_elim_apps = 0; m_num_elim_apps = 0;
} }
}; };
}
tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) { tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(elim_uncnstr_tactic, m, p)); return clean(alloc(elim_uncnstr_tactic, m, p));

5
src/tactic/core/elim_uncnstr_tactic.h
View file

@ -16,8 +16,7 @@ Author:
Notes: Notes:
--*/ --*/
#ifndef ELIM_UNCNSTR_TACTIC_H_ #pragma once
#define ELIM_UNCNSTR_TACTIC_H_
#include "util/params.h" #include "util/params.h"
@ -29,5 +28,3 @@ tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p = params_r
/* /*
ADD_TACTIC("elim-uncnstr", "eliminate application containing unconstrained variables.", "mk_elim_uncnstr_tactic(m, p)") ADD_TACTIC("elim-uncnstr", "eliminate application containing unconstrained variables.", "mk_elim_uncnstr_tactic(m, p)")
*/ */
#endif