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

internalize the reduce_args_tactic to reduce the number of heap allocations

Browse source
This commit is contained in:
Nuno Lopes 2024-11-27 12:35:40 +00:00
parent 1ccfba6a91
commit ab1be5c06e
1 changed files with 44 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

116
src/tactic/core/reduce_args_tactic.cpp
View file

@ -62,45 +62,14 @@ Notes:
where f_1_2, f_1_3 and f_2_3 are new function symbols. where f_1_2, f_1_3 and f_2_3 are new function symbols.
Using the new map, we can replace the occurrences of f. Using the new map, we can replace the occurrences of f.
*/ */
namespace {
class reduce_args_tactic : public tactic { class reduce_args_tactic : public tactic {
struct imp; expr_ref_vector m_vars;
imp * m_imp;
public:
reduce_args_tactic(ast_manager & m);
tactic * translate(ast_manager & m) override {
return alloc(reduce_args_tactic, m);
}
~reduce_args_tactic() override;
char const* name() const override { return "reduce_args"; }
void operator()(goal_ref const & g, goal_ref_buffer & result) override;
void cleanup() override;
void user_propagate_register_expr(expr* e) override;
void user_propagate_clear() override;
};
tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(reduce_args_tactic, m));
}
struct reduce_args_tactic::imp {
expr_ref_vector m_vars;
ast_manager & m; ast_manager & m;
bv_util m_bv; bv_util m_bv;
array_util m_ar; array_util m_ar;
imp(ast_manager & m):
m_vars(m),
m(m),
m_bv(m),
m_ar(m) {
}
static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) { static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
expr *lhs, *rhs; expr *lhs, *rhs;
if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) {
@ -325,14 +294,17 @@ struct reduce_args_tactic::imp {
} }
} }
}; };
friend struct reduce_args_rw_cfg;
friend struct reduce_args_rw;
struct reduce_args_rw_cfg : public default_rewriter_cfg { struct reduce_args_rw_cfg : public default_rewriter_cfg {
ast_manager & m; ast_manager & m;
imp & m_owner; reduce_args_tactic & m_owner;
obj_map<func_decl, bit_vector> & m_decl2args; obj_map<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs; decl2arg2func_map & m_decl2arg2funcs;
reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs): reduce_args_rw_cfg(reduce_args_tactic & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
m(owner.m), m(owner.m),
m_owner(owner), m_owner(owner),
m_decl2args(decl2args), m_decl2args(decl2args),
@ -388,7 +360,7 @@ struct reduce_args_tactic::imp {
struct reduce_args_rw : rewriter_tpl<reduce_args_rw_cfg> { struct reduce_args_rw : rewriter_tpl<reduce_args_rw_cfg> {
reduce_args_rw_cfg m_cfg; reduce_args_rw_cfg m_cfg;
public: public:
reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs): reduce_args_rw(reduce_args_tactic & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
rewriter_tpl<reduce_args_rw_cfg>(owner.m, false, m_cfg), rewriter_tpl<reduce_args_rw_cfg>(owner.m, false, m_cfg),
m_cfg(owner, decl2args, decl2arg2funcs) { m_cfg(owner, decl2args, decl2arg2funcs) {
} }
@ -470,43 +442,43 @@ struct reduce_args_tactic::imp {
TRACE("reduce_args", g.display(tout); if (g.mc()) g.mc()->display(tout);); TRACE("reduce_args", g.display(tout); if (g.mc()) g.mc()->display(tout););
} }
};
reduce_args_tactic::reduce_args_tactic(ast_manager & m) { public:
expr_ref_vector vars(m); reduce_args_tactic(ast_manager & m) :
m_imp = alloc(imp, m); m_vars(m),
} m(m),
m_bv(m),
reduce_args_tactic::~reduce_args_tactic() { m_ar(m) {
dealloc(m_imp);
}
void reduce_args_tactic::operator()(goal_ref const & g,
goal_ref_buffer & result) {
fail_if_unsat_core_generation("reduce-args", g);
result.reset();
if (!m_imp->m.proofs_enabled()) {
m_imp->operator()(*(g.get()));
} }
g->inc_depth();
result.push_back(g.get()); tactic * translate(ast_manager & m) override {
return alloc(reduce_args_tactic, m);
}
char const* name() const override { return "reduce_args"; }
void operator()(goal_ref const & g, goal_ref_buffer & result) override {
fail_if_unsat_core_generation("reduce-args", g);
result.reset();
if (!m.proofs_enabled()) {
operator()(*(g.get()));
}
g->inc_depth();
result.push_back(g.get());
}
void cleanup() override {}
void user_propagate_register_expr(expr* e) override {
m_vars.push_back(e);
}
void user_propagate_clear() override {
m_vars.reset();
}
};
} }
void reduce_args_tactic::cleanup() { tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
ast_manager & m = m_imp->m; return clean(alloc(reduce_args_tactic, m));
expr_ref_vector vars = m_imp->m_vars;
m_imp->~imp();
m_imp = new (m_imp) imp(m);
m_imp->m_vars.append(vars);
} }
void reduce_args_tactic::user_propagate_register_expr(expr* e) {
m_imp->m_vars.push_back(e);
}
void reduce_args_tactic::user_propagate_clear() {
m_imp->m_vars.reset();
}