mirror of
https://github.com/Z3Prover/z3
synced 2026-02-28 19:01:29 +00:00
Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
7390a9b856
commit
ff7cc0f59e
3 changed files with 23 additions and 202 deletions
|
|
@ -15,6 +15,7 @@ Author:
|
|||
|
||||
#include "ast/simplifiers/dependent_expr_state.h"
|
||||
#include "ast/rewriter/rewriter_def.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
|
||||
|
|
@ -116,4 +117,22 @@ public:
|
|||
m_fmls.update(idx, dependent_expr(m, new_fml, mp(d.pr(), new_pr), d.dep()));
|
||||
}
|
||||
}
|
||||
|
||||
static void blast_term_ite(expr_ref& fml, unsigned max_inflation) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
scoped_no_proof _sp(m);
|
||||
params_ref p;
|
||||
rw ite_rw(m, p);
|
||||
ite_rw.m_cfg.m_max_inflation = max_inflation;
|
||||
if (max_inflation < UINT_MAX)
|
||||
ite_rw.m_cfg.m_init_term_size = get_num_exprs(fml);
|
||||
try {
|
||||
expr_ref tmp(m);
|
||||
ite_rw(fml, tmp);
|
||||
fml = tmp;
|
||||
}
|
||||
catch (z3_exception &) {
|
||||
// max steps exceeded.
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -14,203 +14,9 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner) 2013-11-4
|
||||
|
||||
--*/
|
||||
#include "ast/normal_forms/defined_names.h"
|
||||
#include "ast/rewriter/rewriter_def.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
|
||||
|
||||
//
|
||||
// (f (if c1 (if c2 e1 e2) e3) b c) ->
|
||||
// (if c1 (if c2 (f e1 b c)
|
||||
//
|
||||
|
||||
|
||||
class blast_term_ite_tactic : public tactic {
|
||||
|
||||
struct rw_cfg : public default_rewriter_cfg {
|
||||
ast_manager& m;
|
||||
unsigned long long m_max_memory; // in bytes
|
||||
unsigned m_num_fresh; // number of expansions
|
||||
unsigned m_max_steps;
|
||||
unsigned m_max_inflation;
|
||||
unsigned m_init_term_size;
|
||||
|
||||
rw_cfg(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_num_fresh(0),
|
||||
m_max_steps(UINT_MAX),
|
||||
m_max_inflation(UINT_MAX),
|
||||
m_init_term_size(0) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
tactic_params tp(p);
|
||||
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
|
||||
m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps());
|
||||
m_max_inflation = p.get_uint("max_inflation", tp.blast_term_ite_max_inflation()); // multiplicative factor of initial term size.
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool max_steps_exceeded(unsigned num_steps) const {
|
||||
// if (memory::get_allocation_size() > m_max_memory)
|
||||
// throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
|
||||
return num_steps >= m_max_steps;
|
||||
}
|
||||
|
||||
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
|
||||
if (m.is_ite(f)) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
if (m_max_inflation < UINT_MAX &&
|
||||
m_init_term_size > 0 &&
|
||||
m_max_inflation * m_init_term_size < m_num_fresh)
|
||||
return BR_FAILED;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr* c, *t, *e;
|
||||
if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
|
||||
TRACE(blast_term_ite, result = m.mk_app(f, num_args, args); tout << result << "\n";);
|
||||
expr_ref e1(m), e2(m);
|
||||
ptr_vector<expr> args1(num_args, args);
|
||||
args1[i] = t;
|
||||
e1 = m.mk_app(f, num_args, args1.data());
|
||||
if (m.are_equal(t, e)) {
|
||||
result = e1;
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
else {
|
||||
args1[i] = e;
|
||||
e2 = m.mk_app(f, num_args, args1.data());
|
||||
result = m.mk_ite(c, e1, e2);
|
||||
++m_num_fresh;
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
bool rewrite_patterns() const { return false; }
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
return mk_app_core(f, num, args, result);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
struct rw : public rewriter_tpl<rw_cfg> {
|
||||
rw_cfg m_cfg;
|
||||
|
||||
rw(ast_manager & m, params_ref const & p):
|
||||
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
|
||||
m_cfg(m, p) {
|
||||
}
|
||||
};
|
||||
|
||||
struct imp {
|
||||
ast_manager & m;
|
||||
rw m_rw;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_rw(m, p) {
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_rw.m_cfg.updt_params(p);
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g, goal_ref_buffer & result) {
|
||||
tactic_report report("blast-term-ite", *g);
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned num_fresh = 0;
|
||||
unsigned idx = 0;
|
||||
for (auto [curr, dep, pr] : *g) {
|
||||
if (m_rw.m_cfg.m_max_inflation < UINT_MAX) {
|
||||
m_rw.m_cfg.m_init_term_size = get_num_exprs(curr);
|
||||
num_fresh += m_rw.m_cfg.m_num_fresh;
|
||||
m_rw.m_cfg.m_num_fresh = 0;
|
||||
}
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
g->update(idx++, new_curr, new_pr, dep);
|
||||
}
|
||||
|
||||
report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh + num_fresh);
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
}
|
||||
};
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
blast_term_ite_tactic(ast_manager & m, params_ref const & p):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) override {
|
||||
return alloc(blast_term_ite_tactic, m, m_params);
|
||||
}
|
||||
|
||||
~blast_term_ite_tactic() override {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
char const* name() const override { return "blast_term_ite"; }
|
||||
|
||||
void updt_params(params_ref const & p) override {
|
||||
m_params.append(p);
|
||||
m_imp->m_rw.m_cfg.updt_params(m_params);
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) override {
|
||||
insert_max_memory(r);
|
||||
insert_max_steps(r);
|
||||
r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.", "4294967295");
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
|
||||
(*m_imp)(in, result);
|
||||
}
|
||||
|
||||
void cleanup() override {
|
||||
ast_manager & m = m_imp->m;
|
||||
dealloc(m_imp);
|
||||
m_imp = alloc(imp, m, m_params);
|
||||
}
|
||||
|
||||
static void blast_term_ite(expr_ref& fml, unsigned max_inflation) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
scoped_no_proof _sp(m);
|
||||
params_ref p;
|
||||
rw ite_rw(m, p);
|
||||
ite_rw.m_cfg.m_max_inflation = max_inflation;
|
||||
if (max_inflation < UINT_MAX) {
|
||||
ite_rw.m_cfg.m_init_term_size = get_num_exprs(fml);
|
||||
}
|
||||
try {
|
||||
expr_ref tmp(m);
|
||||
ite_rw(fml, tmp);
|
||||
fml = tmp;
|
||||
}
|
||||
catch (z3_exception &) {
|
||||
// max steps exceeded.
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(blast_term_ite_tactic, m, p));
|
||||
}
|
||||
#include "tactic/core/blast_term_ite_tactic.h"
|
||||
|
||||
void blast_term_ite(expr_ref& fml, unsigned max_inflation) {
|
||||
blast_term_ite_tactic::blast_term_ite(fml, max_inflation);
|
||||
blast_term_ite_simplifier::blast_term_ite(fml, max_inflation);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -48,11 +48,8 @@ Use `elim-term-ite` elsewhere when possible.
|
|||
#include "tactic/tactic.h"
|
||||
#include "tactic/dependent_expr_state_tactic.h"
|
||||
#include "ast/simplifiers/blast_term_ite_simplifier.h"
|
||||
class ast_manager;
|
||||
|
||||
tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
|
||||
inline tactic * mk_blast_term_ite2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
inline tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
return alloc(dependent_expr_state_tactic, m, p,
|
||||
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
|
||||
return alloc(blast_term_ite_simplifier, m, p, s);
|
||||
|
|
@ -61,7 +58,6 @@ inline tactic * mk_blast_term_ite2_tactic(ast_manager & m, params_ref const & p
|
|||
|
||||
/*
|
||||
ADD_TACTIC("blast-term-ite", "blast term if-then-else by hoisting them.", "mk_blast_term_ite_tactic(m, p)")
|
||||
ADD_TACTIC("blast-term-ite2", "blast term if-then-else by hoisting them.", "mk_blast_term_ite2_tactic(m, p)")
|
||||
ADD_SIMPLIFIER("blast-term-ite", "blast term if-then-else by hoisting them.", "alloc(blast_term_ite_simplifier, m, p, s)")
|
||||
*/
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue