diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp new file mode 100644 index 000000000..d2c7ff5f4 --- /dev/null +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -0,0 +1,332 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + elim_small_bv.h + +Abstract: + + Tactic that eliminates small, quantified bit-vectors. + +Author: + + Christoph (cwinter) 2015-11-09 + +Revision History: + +--*/ +#include"tactical.h" +#include"rewriter_def.h" +#include"filter_model_converter.h" +#include"cooperate.h" +#include"bv_decl_plugin.h" +#include"used_vars.h" +#include"well_sorted.h" +#include"var_subst.h" +#include"simplifier.h" +#include"basic_simplifier_plugin.h" +#include"bv_simplifier_plugin.h" + +#include"elim_small_bv_tactic.h" + +class elim_small_bv_tactic : public tactic { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager & m; + bv_util m_util; + simplifier m_simp; + ref m_mc; + goal * m_goal; + unsigned m_max_bits; + unsigned long long m_max_steps; + unsigned long long m_max_memory; // in bytes + bool m_produce_models; + sort_ref_vector m_bindings; + unsigned long m_num_eliminated; + + rw_cfg(ast_manager & _m, params_ref const & p) : + m(_m), + m_util(_m), + m_simp(_m), + m_bindings(_m), + m_num_eliminated(0) { + updt_params(p); + m_goal = 0; + m_max_steps = UINT_MAX; + + basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m); + // bsimp->set_eliminate_and(true); + m_simp.register_plugin(bsimp); + + bv_simplifier_params bv_params; + bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, bv_params); + m_simp.register_plugin(bvsimp); + } + + bool max_steps_exceeded(unsigned long long num_steps) const { + cooperate("elim-small-bv"); + if (num_steps > m_max_steps) + return true; + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + return false; + } + + bool is_small_bv(sort * s) { + return m_util.is_bv_sort(s) && m_util.get_bv_size(s) <= m_max_bits; + } + + expr_ref replace_var(used_vars & uv, + unsigned num_decls, unsigned max_var_idx_p1, + unsigned idx, sort * s, expr * e, expr * replacement) { + TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) << + " in " << mk_ismt2_pp(e, m) << std::endl;); + expr_ref res(m); + expr_ref_vector substitution(m); + + substitution.resize(num_decls, 0); + substitution[num_decls - idx - 1] = replacement; + + // (VAR 0) is in the first position of substitution; (VAR num_decls-1) is in the last position. + + for (unsigned i = 0; i < max_var_idx_p1; i++) { + sort * s = uv.get(i); + substitution.push_back(0); + } + + // (VAR num_decls) ... (VAR num_decls+sz-1); are in positions num_decls .. num_decls+sz-1 + + std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); + + // (VAR 0) should be in the last position of substitution. + + TRACE("elim_small_bv", tout << "substitution: " << std::endl; + for (unsigned k = 0; k < substitution.size(); k++) { + expr * se = substitution[k].get(); + tout << k << " = "; + if (se == 0) tout << "0"; + else tout << mk_ismt2_pp(se, m); + tout << std::endl; + }); + + var_subst vsbst(m); + vsbst(e, substitution.size(), substitution.c_ptr(), res); + SASSERT(is_well_sorted(m, res)); + + proof_ref pr(m); + m_simp(res, res, pr); + TRACE("elim_small_bv", tout << "replace done: " << mk_ismt2_pp(res, m) << std::endl;); + + return res; + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result = m.mk_app(f, num, args); + TRACE("elim_small_bv_app", tout << "reduce " << mk_ismt2_pp(result, m) << std::endl; ); + return BR_FAILED; + } + + bool reduce_quantifier( + quantifier * q, + expr * old_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + TRACE("elim_small_bv", tout << "reduce_quantifier " << mk_ismt2_pp(q, m) << std::endl; ); + unsigned long long num_steps = 0; + unsigned curr_sz = m_bindings.size(); + SASSERT(q->get_num_decls() <= curr_sz); + unsigned num_decls = q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + + used_vars uv; + uv(q); + SASSERT(is_well_sorted(m, q)); + unsigned max_var_idx_p1 = uv.get_max_found_var_idx_plus_1(); + + expr_ref body(old_body, m); + for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) { + sort * s = q->get_decl_sort(i); + symbol const & name = q->get_decl_name(i); + unsigned bv_sz = m_util.get_bv_size(s); + + if (is_small_bv(s) && !max_steps_exceeded(num_steps)) { + TRACE("elim_small_bv", tout << "eliminating " << name << + "; sort = " << mk_ismt2_pp(s, m) << + "; body = " << mk_ismt2_pp(body, m) << std::endl;); + + expr_ref_vector new_bodies(m); + for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) { + expr_ref n(m_util.mk_numeral(j, bv_sz), m); + expr_ref nb(m); + nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n); + new_bodies.push_back(nb); + num_steps++; + } + + TRACE("elim_small_bv", tout << "new bodies: " << std::endl; + for (unsigned k = 0; k < new_bodies.size(); k++) + tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; ); + + body = q->is_forall() ? m.mk_and(new_bodies.size(), new_bodies.c_ptr()) : + m.mk_or(new_bodies.size(), new_bodies.c_ptr()); + SASSERT(is_well_sorted(m, body)); + + proof_ref pr(m); + m_simp(body, body, pr); + m_num_eliminated++; + } + } + + quantifier_ref new_q(m); + new_q = m.update_quantifier(q, body); + unused_vars_eliminator el(m); + el(new_q, result); + + TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; ); + + result_pr = 0; // proofs NIY + m_bindings.shrink(old_sz); + return true; + } + + bool pre_visit(expr * t) { + TRACE("elim_small_bv_pre", tout << "pre_visit: " << mk_ismt2_pp(t, m) << std::endl;); + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("elim_small_bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m) << std::endl;); + sort_ref_vector new_bindings(m); + for (unsigned i = 0; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; + } + + 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); + m_max_bits = p.get_uint("max_bits", 4); + } + }; + + 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 set_cancel(bool f) { + m_rw.set_cancel(f); + } + + void updt_params(params_ref const & p) { + m_rw.cfg().updt_params(p); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("elim-small-bv", *g); + bool produce_proofs = g->proofs_enabled(); + fail_if_proof_generation("elim-small-bv", g); + fail_if_unsat_core_generation("elim-small-bv", g); + m_rw.cfg().m_produce_models = g->models_enabled(); + + m_rw.m_cfg.m_goal = g.get(); + expr_ref new_curr(m); + proof_ref new_pr(m); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + if (produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + mc = m_rw.m_cfg.m_mc.get(); + + report_tactic_progress(":elim-small-bv-num-eliminated", m_rw.m_cfg.m_num_eliminated); + g->inc_depth(); + result.push_back(g.get()); + TRACE("elim-small-bv", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + }; + + imp * m_imp; + params_ref m_params; +public: + elim_small_bv_tactic(ast_manager & m, params_ref const & p) : + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(elim_small_bv_tactic, m, m_params); + } + + virtual ~elim_small_bv_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->m_rw.cfg().updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_max_steps(r); + r.insert("max_bits", CPK_UINT, "(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated."); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m; + imp * d = alloc(imp, m, m_params); +#pragma omp critical (tactic_cancel) + { + std::swap(d, m_imp); + } + dealloc(d); + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } +}; + +tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(elim_small_bv_tactic, m, p)); +} + diff --git a/src/tactic/bv/elim_small_bv_tactic.h b/src/tactic/bv/elim_small_bv_tactic.h new file mode 100644 index 000000000..bcdd8aad6 --- /dev/null +++ b/src/tactic/bv/elim_small_bv_tactic.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + elim_small_bv.h + +Abstract: + + Tactic that eliminates small, quantified bit-vectors. + +Author: + + Christoph (cwinter) 2015-11-09 + +Revision History: + +--*/ +#ifndef ELIM_SMALL_BV_H_ +#define ELIM_SMALL_BV_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_elim_small_bv_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("elim-small-bv", "eliminate small, quantified bit-vectors by expansion.", "mk_elim_small_bv_tactic(m, p)") +*/ + +#endif