mirror of
https://github.com/Z3Prover/z3
synced 2026-03-01 19:26:53 +00:00
Rename bv1-blast2 to bv1-blast, remove old tactic source
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
033ea50a5d
commit
668dd7a0a1
2 changed files with 41 additions and 467 deletions
|
|
@ -7,13 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1.
|
||||
This rewriter only supports concat and extract operators.
|
||||
This transformation is useful for handling benchmarks that contain
|
||||
many BV equalities.
|
||||
|
||||
Remark: other operators can be mapped into concat/extract by using
|
||||
the simplifiers.
|
||||
Probe for checking if a goal is in the QF_BV fragment that uses only =, extract, and concat.
|
||||
|
||||
Author:
|
||||
|
||||
|
|
@ -22,469 +16,50 @@ Author:
|
|||
Notes:
|
||||
|
||||
--*/
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/bv/bit_blaster_model_converter.h"
|
||||
#include "tactic/bv/bv1_blaster_tactic.h"
|
||||
#include "tactic/tactic.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
#include "ast/rewriter/rewriter_def.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/rewriter/bv_rewriter.h"
|
||||
|
||||
class bv1_blaster_tactic : public tactic {
|
||||
|
||||
struct rw_cfg : public default_rewriter_cfg {
|
||||
ast_manager & m_manager;
|
||||
bv_util m_util;
|
||||
obj_map<func_decl, expr*> m_const2bits;
|
||||
ptr_vector<func_decl> m_newbits;
|
||||
ast_ref_vector m_saved;
|
||||
expr_ref m_bit1;
|
||||
expr_ref m_bit0;
|
||||
|
||||
unsigned long long m_max_memory; // in bytes
|
||||
unsigned m_max_steps;
|
||||
bool m_produce_models;
|
||||
|
||||
ast_manager & m() const { return m_manager; }
|
||||
bv_util & butil() { return m_util; }
|
||||
bv_util const & butil() const { return m_util; }
|
||||
|
||||
void cleanup_buffers() {
|
||||
m_saved.finalize();
|
||||
}
|
||||
|
||||
rw_cfg(ast_manager & m, params_ref const & p):
|
||||
m_manager(m),
|
||||
m_util(m),
|
||||
m_saved(m),
|
||||
m_bit1(m),
|
||||
m_bit0(m) {
|
||||
m_bit1 = butil().mk_numeral(rational(1), 1);
|
||||
m_bit0 = butil().mk_numeral(rational(0), 1);
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
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_produce_models = p.get_bool("produce_models", false);
|
||||
}
|
||||
|
||||
bool rewrite_patterns() const { UNREACHABLE(); return false; }
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
typedef ptr_buffer<expr, 128> bit_buffer;
|
||||
|
||||
void get_bits(expr * arg, bit_buffer & bits) {
|
||||
SASSERT(butil().is_concat(arg) || butil().get_bv_size(arg) == 1);
|
||||
if (butil().is_concat(arg))
|
||||
bits.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
|
||||
else
|
||||
bits.push_back(arg);
|
||||
}
|
||||
|
||||
void mk_const(func_decl * f, expr_ref & result) {
|
||||
SASSERT(f->get_family_id() == null_family_id);
|
||||
SASSERT(f->get_arity() == 0);
|
||||
expr * r;
|
||||
if (m_const2bits.find(f, r)) {
|
||||
result = r;
|
||||
return;
|
||||
}
|
||||
sort * s = f->get_range();
|
||||
SASSERT(butil().is_bv_sort(s));
|
||||
unsigned bv_size = butil().get_bv_size(s);
|
||||
if (bv_size == 1) {
|
||||
result = m().mk_const(f);
|
||||
return;
|
||||
}
|
||||
sort * b = butil().mk_sort(1);
|
||||
ptr_buffer<expr> bits;
|
||||
for (unsigned i = 0; i < bv_size; ++i) {
|
||||
bits.push_back(m().mk_fresh_const(nullptr, b));
|
||||
m_newbits.push_back(to_app(bits.back())->get_decl());
|
||||
m_saved.push_back(m_newbits.back());
|
||||
}
|
||||
r = butil().mk_concat(bits.size(), bits.data());
|
||||
m_saved.push_back(r);
|
||||
m_saved.push_back(f);
|
||||
m_const2bits.insert(f, r);
|
||||
result = r;
|
||||
}
|
||||
|
||||
void blast_bv_term(expr * t, expr_ref & result) {
|
||||
bit_buffer bits;
|
||||
unsigned bv_size = butil().get_bv_size(t);
|
||||
if (bv_size == 1) {
|
||||
result = t;
|
||||
return;
|
||||
}
|
||||
unsigned i = bv_size;
|
||||
while (i > 0) {
|
||||
--i;
|
||||
bits.push_back(butil().mk_extract(i, i, t));
|
||||
}
|
||||
result = butil().mk_concat(bits.size(), bits.data());
|
||||
}
|
||||
|
||||
void reduce_eq(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
bit_buffer bits1;
|
||||
bit_buffer bits2;
|
||||
get_bits(arg1, bits1);
|
||||
get_bits(arg2, bits2);
|
||||
SASSERT(bits1.size() == bits2.size());
|
||||
bit_buffer new_eqs;
|
||||
unsigned i = bits1.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
new_eqs.push_back(m().mk_eq(bits1[i], bits2[i]));
|
||||
}
|
||||
result = mk_and(m(), new_eqs.size(), new_eqs.data());
|
||||
}
|
||||
|
||||
void reduce_ite(expr * c, expr * t, expr * e, expr_ref & result) {
|
||||
bit_buffer t_bits;
|
||||
bit_buffer e_bits;
|
||||
get_bits(t, t_bits);
|
||||
get_bits(e, e_bits);
|
||||
SASSERT(t_bits.size() == e_bits.size());
|
||||
bit_buffer new_ites;
|
||||
unsigned num = t_bits.size();
|
||||
for (unsigned i = 0; i < num; ++i)
|
||||
new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i]));
|
||||
result = butil().mk_concat(new_ites.size(), new_ites.data());
|
||||
}
|
||||
|
||||
void reduce_num(func_decl * f, expr_ref & result) {
|
||||
SASSERT(f->get_num_parameters() == 2);
|
||||
SASSERT(f->get_parameter(0).is_rational());
|
||||
SASSERT(f->get_parameter(1).is_int());
|
||||
bit_buffer bits;
|
||||
rational v = f->get_parameter(0).get_rational();
|
||||
rational two(2);
|
||||
unsigned sz = f->get_parameter(1).get_int();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if ((v % two).is_zero())
|
||||
bits.push_back(m_bit0);
|
||||
else
|
||||
bits.push_back(m_bit1);
|
||||
v = div(v, two);
|
||||
}
|
||||
std::reverse(bits.begin(), bits.end());
|
||||
result = butil().mk_concat(bits.size(), bits.data());
|
||||
}
|
||||
|
||||
void reduce_extract(func_decl * f, expr * arg, expr_ref & result) {
|
||||
bit_buffer arg_bits;
|
||||
get_bits(arg, arg_bits);
|
||||
SASSERT(arg_bits.size() == butil().get_bv_size(arg));
|
||||
unsigned high = butil().get_extract_high(f);
|
||||
unsigned low = butil().get_extract_low(f);
|
||||
unsigned sz = arg_bits.size();
|
||||
unsigned start = sz - 1 - high;
|
||||
unsigned end = sz - 1 - low;
|
||||
bit_buffer bits;
|
||||
for (unsigned i = start; i <= end; ++i) {
|
||||
bits.push_back(arg_bits[i]);
|
||||
}
|
||||
result = butil().mk_concat(bits.size(), bits.data());
|
||||
}
|
||||
|
||||
void reduce_concat(unsigned num, expr * const * args, expr_ref & result) {
|
||||
bit_buffer bits;
|
||||
bit_buffer arg_bits;
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
expr * arg = args[i];
|
||||
arg_bits.reset();
|
||||
get_bits(arg, arg_bits);
|
||||
bits.append(arg_bits.size(), arg_bits.data());
|
||||
}
|
||||
result = butil().mk_concat(bits.size(), bits.data());
|
||||
}
|
||||
|
||||
void reduce_bin_xor(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
bit_buffer bits1;
|
||||
bit_buffer bits2;
|
||||
get_bits(arg1, bits1);
|
||||
get_bits(arg2, bits2);
|
||||
SASSERT(bits1.size() == bits2.size());
|
||||
bit_buffer new_bits;
|
||||
unsigned num = bits1.size();
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
new_bits.push_back(m().mk_ite(m().mk_eq(bits1[i], bits2[i]), m_bit0, m_bit1));
|
||||
}
|
||||
result = butil().mk_concat(new_bits.size(), new_bits.data());
|
||||
}
|
||||
|
||||
void reduce_xor(unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num_args > 0);
|
||||
#if 1
|
||||
if (num_args == 1) {
|
||||
result = args[0];
|
||||
return;
|
||||
}
|
||||
reduce_bin_xor(args[0], args[1], result);
|
||||
for (unsigned i = 2; i < num_args; ++i) {
|
||||
reduce_bin_xor(result, args[i], result);
|
||||
}
|
||||
#else
|
||||
ptr_buffer<bit_buffer> args_bits;
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
bit_buffer * buff_i = alloc(bit_buffer);
|
||||
get_bits(args[i], *buff_i);
|
||||
args_bits.push_back(buff_i);
|
||||
}
|
||||
bit_buffer new_bits;
|
||||
unsigned sz = butil().get_bv_size(args[0]);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
ptr_buffer<expr> eqs;
|
||||
for (unsigned j = 0; j < num_args; ++j) {
|
||||
bit_buffer * buff_j = args_bits[j];
|
||||
eqs.push_back(m().mk_eq(buff_j->get(i), m_bit1));
|
||||
}
|
||||
expr * cond = m().mk_xor(eqs.size(), eqs.c_ptr());
|
||||
new_bits.push_back(m().mk_ite(cond, m_bit1, m_bit0));
|
||||
}
|
||||
result = butil().mk_concat(new_bits.size(), new_bits.c_ptr());
|
||||
std::for_each(args_bits.begin(), args_bits.end(), delete_proc<bit_buffer>());
|
||||
#endif
|
||||
}
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = nullptr;
|
||||
if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
|
||||
mk_const(f, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (m().is_eq(f)) {
|
||||
SASSERT(num == 2);
|
||||
if (butil().is_bv(args[0])) {
|
||||
reduce_eq(args[0], args[1], result);
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
if (m().is_ite(f)) {
|
||||
SASSERT(num == 3);
|
||||
if (butil().is_bv(args[1])) {
|
||||
reduce_ite(args[0], args[1], args[2], result);
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
if (f->get_family_id() == butil().get_family_id()) {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_BV_NUM:
|
||||
reduce_num(f, result);
|
||||
return BR_DONE;
|
||||
case OP_EXTRACT:
|
||||
SASSERT(num == 1);
|
||||
reduce_extract(f, args[0], result);
|
||||
return BR_DONE;
|
||||
case OP_CONCAT:
|
||||
reduce_concat(num, args, result);
|
||||
return BR_DONE;
|
||||
case OP_BXOR:
|
||||
reduce_xor(num, args, result);
|
||||
return BR_DONE;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
|
||||
if (butil().is_bv_sort(f->get_range())) {
|
||||
blast_bv_term(m().mk_app(f, num, args), result);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
bool reduce_quantifier(quantifier * old_q,
|
||||
expr * new_body,
|
||||
expr * const * new_patterns,
|
||||
expr * const * new_no_patterns,
|
||||
expr_ref & result,
|
||||
proof_ref & result_pr) {
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
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 {
|
||||
rw m_rw;
|
||||
unsigned m_num_steps;
|
||||
|
||||
imp(ast_manager & m, params_ref const & p):
|
||||
m_rw(m, p) {
|
||||
}
|
||||
|
||||
struct not_target : public std::exception {};
|
||||
|
||||
struct visitor {
|
||||
family_id m_bv_fid;
|
||||
visitor(family_id bv_fid):m_bv_fid(bv_fid) {}
|
||||
void operator()(var const * n) { throw not_target(); }
|
||||
void operator()(app const * n) {
|
||||
if (n->get_family_id() == m_bv_fid) {
|
||||
switch (n->get_decl_kind()) {
|
||||
case OP_BV_NUM:
|
||||
case OP_EXTRACT:
|
||||
case OP_CONCAT:
|
||||
return;
|
||||
case OP_BXOR:
|
||||
// it doesn't payoff to do the reduction in this case.
|
||||
throw not_target();
|
||||
default:
|
||||
throw not_target();
|
||||
}
|
||||
}
|
||||
}
|
||||
void operator()(quantifier const * n) { throw not_target(); }
|
||||
};
|
||||
|
||||
bool is_target(goal const & g) const {
|
||||
expr_fast_mark1 visited;
|
||||
unsigned sz = g.size();
|
||||
visitor proc(m_rw.cfg().butil().get_family_id());
|
||||
try {
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr * f = g.form(i);
|
||||
for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, f);
|
||||
}
|
||||
}
|
||||
catch (const not_target &) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
ast_manager & m() const { return m_rw.m(); }
|
||||
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result) {
|
||||
|
||||
if (!is_target(*g))
|
||||
throw tactic_exception("bv1 blaster cannot be applied to goal");
|
||||
|
||||
tactic_report report("bv1-blaster", *g);
|
||||
m_num_steps = 0;
|
||||
|
||||
bool proofs_enabled = g->proofs_enabled();
|
||||
expr_ref new_curr(m());
|
||||
proof_ref new_pr(m());
|
||||
unsigned size = g->size();
|
||||
for (unsigned idx = 0; idx < size; ++idx) {
|
||||
if (g->inconsistent())
|
||||
break;
|
||||
expr * curr = g->form(idx);
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
m_num_steps += m_rw.get_num_steps();
|
||||
if (proofs_enabled) {
|
||||
proof * pr = g->pr(idx);
|
||||
new_pr = m().mk_modus_ponens(pr, new_pr);
|
||||
}
|
||||
g->update(idx, new_curr, new_pr, g->dep(idx));
|
||||
}
|
||||
|
||||
if (g->models_enabled())
|
||||
g->add(mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits, m_rw.cfg().m_newbits));
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
m_rw.cfg().cleanup();
|
||||
}
|
||||
|
||||
unsigned get_num_steps() const { return m_num_steps; }
|
||||
};
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref()):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) override {
|
||||
return alloc(bv1_blaster_tactic, m, m_params);
|
||||
}
|
||||
|
||||
~bv1_blaster_tactic() override {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
char const* name() const override { return "bv1_blaster"; }
|
||||
|
||||
void updt_params(params_ref const & p) override {
|
||||
m_params.append(p);
|
||||
m_imp->m_rw.cfg().updt_params(m_params);
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) override {
|
||||
insert_max_memory(r);
|
||||
insert_max_steps(r);
|
||||
}
|
||||
|
||||
bool is_target(goal const & g) const {
|
||||
return m_imp->is_target(g);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief "Blast" bit-vectors of size n in s into bit-vectors of size 1.
|
||||
If s contains other bit-vectors operators different from concat/extract, then this is method is a NO-OP.
|
||||
It also does not support quantifiers.
|
||||
Return a model_converter that converts any model for the updated set into a model for the old set.
|
||||
*/
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result) override {
|
||||
(*m_imp)(g, result);
|
||||
}
|
||||
|
||||
void cleanup() override {
|
||||
imp * d = alloc(imp, m_imp->m(), m_params);
|
||||
std::swap(d, m_imp);
|
||||
dealloc(d);
|
||||
}
|
||||
|
||||
unsigned get_num_steps() const {
|
||||
return m_imp->get_num_steps();
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(bv1_blaster_tactic, m, p));
|
||||
}
|
||||
|
||||
class is_qfbv_eq_probe : public probe {
|
||||
public:
|
||||
result operator()(goal const & g) override {
|
||||
bv1_blaster_tactic t(g.m());
|
||||
return t.is_target(g);
|
||||
struct not_target : public std::exception {};
|
||||
|
||||
struct visitor {
|
||||
family_id m_bv_fid;
|
||||
visitor(family_id bv_fid) : m_bv_fid(bv_fid) {}
|
||||
void operator()(var const* n) { throw not_target(); }
|
||||
void operator()(app const* n) {
|
||||
if (n->get_family_id() == m_bv_fid) {
|
||||
switch (n->get_decl_kind()) {
|
||||
case OP_BV_NUM:
|
||||
case OP_EXTRACT:
|
||||
case OP_CONCAT:
|
||||
return;
|
||||
default:
|
||||
throw not_target();
|
||||
}
|
||||
}
|
||||
}
|
||||
void operator()(quantifier const* n) { throw not_target(); }
|
||||
};
|
||||
|
||||
public:
|
||||
result operator()(goal const& g) override {
|
||||
bv_util util(g.m());
|
||||
expr_fast_mark1 visited;
|
||||
visitor proc(util.get_family_id());
|
||||
try {
|
||||
for (unsigned i = 0; i < g.size(); ++i)
|
||||
for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, g.form(i));
|
||||
}
|
||||
catch (const not_target&) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
probe * mk_is_qfbv_eq_probe() {
|
||||
probe* mk_is_qfbv_eq_probe() {
|
||||
return alloc(is_qfbv_eq_probe);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -42,13 +42,12 @@ the simplifiers.
|
|||
|
||||
#include "util/params.h"
|
||||
#include "tactic/dependent_expr_state_tactic.h"
|
||||
#include "tactic/probe.h"
|
||||
#include "ast/simplifiers/bv1_blaster.h"
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
|
||||
inline tactic * mk_bv1_blaster2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
inline tactic * mk_bv1_blaster_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(bv1_blaster_simplifier, m, p, s);
|
||||
|
|
@ -58,6 +57,6 @@ inline tactic * mk_bv1_blaster2_tactic(ast_manager & m, params_ref const & p = p
|
|||
probe * mk_is_qfbv_eq_probe();
|
||||
/*
|
||||
ADD_TACTIC("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "mk_bv1_blaster_tactic(m, p)")
|
||||
ADD_TACTIC("bv1-blast2", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "mk_bv1_blaster2_tactic(m, p)")
|
||||
ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", "mk_is_qfbv_eq_probe()")
|
||||
*/
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue