diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 988c1ba3b..356944281 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -33,6 +33,7 @@ z3_add_component(simplifiers TACTIC_HEADERS bit_blaster.h bit2int.h + blast_term_ite_simplifier.h elim_bounds.h elim_term_ite.h pull_nested_quantifiers.h diff --git a/src/ast/simplifiers/blast_term_ite_simplifier.h b/src/ast/simplifiers/blast_term_ite_simplifier.h new file mode 100644 index 000000000..977b6c586 --- /dev/null +++ b/src/ast/simplifiers/blast_term_ite_simplifier.h @@ -0,0 +1,138 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + blast_term_ite_simplifier.h + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-4 + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/rewriter_def.h" +#include "ast/scoped_proof.h" +#include "params/tactic_params.hpp" + + +class blast_term_ite_simplifier : public dependent_expr_simplifier { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager& m; + unsigned m_num_fresh; + 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_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()); + } + + bool max_steps_exceeded(unsigned num_steps) const { + 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 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 m_cfg; + + rw(ast_manager& m, params_ref const& p): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + }; + + rw m_rw; + +public: + blast_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s): + dependent_expr_simplifier(m, s), m_rw(m, p) {} + + char const* name() const override { return "blast-term-ite"; } + + void reduce() override { + expr_ref new_fml(m); + proof_ref new_pr(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + if (m_rw.m_cfg.m_max_inflation < UINT_MAX) { + m_rw.m_cfg.m_init_term_size = get_num_exprs(d.fml()); + m_rw.m_cfg.m_num_fresh = 0; + } + m_rw(d.fml(), new_fml, new_pr); + if (d.fml() != new_fml) + 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. + } + } +}; diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 45ea00045..f35a12668 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -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 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 m_cfg; - - rw(ast_manager & m, params_ref const & p): - rewriter_tpl(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); } + diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h index a322b8e11..c1233953a 100644 --- a/src/tactic/core/blast_term_ite_tactic.h +++ b/src/tactic/core/blast_term_ite_tactic.h @@ -45,13 +45,20 @@ Use `elim-term-ite` elsewhere when possible. #pragma once #include "util/params.h" -class ast_manager; -class tactic; +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/blast_term_ite_simplifier.h" -tactic * mk_blast_term_ite_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); + }); +} /* ADD_TACTIC("blast-term-ite", "blast term if-then-else by hoisting them.", "mk_blast_term_ite_tactic(m, p)") + ADD_SIMPLIFIER("blast-term-ite", "blast term if-then-else by hoisting them.", "alloc(blast_term_ite_simplifier, m, p, s)") */ void blast_term_ite(expr_ref& fml, unsigned max_inflation);