mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
Added elim_small_bv_tactic.
This commit is contained in:
Christoph M. Wintersteiger
parent
faace0e6a3
commit
746689904d
332
src/tactic/bv/elim_small_bv_tactic.cpp
Normal file
332
src/tactic/bv/elim_small_bv_tactic.cpp
Normal file
|
|
@ -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<filter_model_converter> 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> {
|
||||
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 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));
|
||||
}
|
||||
|
||||
32
src/tactic/bv/elim_small_bv_tactic.h
Normal file
32
src/tactic/bv/elim_small_bv_tactic.h
Normal file
|
|
@ -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
|
||||
Loading…
Reference in a new issue