3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

tuning bit-vector operations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-21 13:09:03 +02:00
parent 1eebab355c
commit 8e26c97782
9 changed files with 271 additions and 94 deletions

View file

@ -277,7 +277,9 @@ extern "C" {
RESET_ERROR_CODE();
CHECK_NON_NULL(f, 0);
expr * e = to_func_interp_ref(f)->get_else();
mk_c(c)->save_ast_trail(e);
if (e) {
mk_c(c)->save_ast_trail(e);
}
RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(0);
}

View file

@ -121,8 +121,11 @@ public:
void mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
void mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
bool mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); }
void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits);
};

View file

@ -38,7 +38,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
template<typename Cfg>
bool bit_blaster_tpl<Cfg>::is_numeral(unsigned sz, expr * const * bits) const {
for (unsigned i = 0; i < sz; i++)
if (!m().is_true(bits[i]) && !m().is_false(bits[i]))
if (!is_bool_const(bits[i]))
return false;
return true;
}
@ -158,30 +158,24 @@ void bit_blaster_tpl<Cfg>::mk_subtracter(unsigned sz, expr * const * a_bits, exp
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
SASSERT(sz > 0);
if (!m_use_bcm) {
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_b))
std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) {
mk_neg(sz, a_bits, out_bits);
return;
}
if (is_numeral(sz, a_bits, n_a)) {
n_a *= n_b;
num2bits(n_a, sz, out_bits);
return;
}
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_b))
std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) {
mk_neg(sz, a_bits, out_bits);
return;
}
else {
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_a)) {
mk_const_multiplier(sz, a_bits, b_bits, out_bits);
return;
} else if (is_numeral(sz, b_bits, n_b)) {
mk_const_multiplier(sz, b_bits, a_bits, out_bits);
return;
}
if (is_numeral(sz, a_bits, n_a)) {
n_a *= n_b;
num2bits(n_a, sz, out_bits);
return;
}
if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
return;
}
if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
return;
}
if (!m_use_wtm) {
@ -1171,13 +1165,74 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
}
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
DEBUG_CODE({
numeral x;
SASSERT(is_numeral(sz, a_bits, x));
SASSERT(out_bits.empty());
});
bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
unsigned nb = 0;
unsigned case_size = 1;
unsigned circuit_size = sz*sz*5;
for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
if (!is_bool_const(a_bits[i])) {
case_size *= 2;
}
if (!is_bool_const(b_bits[i])) {
case_size *= 2;
}
}
if (case_size >= circuit_size) {
return false;
}
SASSERT(out_bits.empty());
ptr_buffer<expr, 128> na_bits;
na_bits.append(sz, a_bits);
ptr_buffer<expr, 128> nb_bits;
nb_bits.append(sz, b_bits);
mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits);
return false;
}
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;
if (is_a && i == sz) { is_a = false; i = 0; }
while (!is_a && i < sz && is_bool_const(b_bits[i])) ++i;
if (i < sz) {
expr_ref_vector out1(m()), out2(m());
expr_ref x(m());
x = is_a?a_bits[i]:b_bits[i];
if (is_a) a_bits[i] = m().mk_true(); else b_bits[i] = m().mk_true();
mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out1);
if (is_a) a_bits[i] = m().mk_false(); else b_bits[i] = m().mk_false();
mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);
if (is_a) a_bits[i] = x; else b_bits[i] = x;
SASSERT(out_bits.empty());
for (unsigned j = 0; j < sz; ++j) {
out_bits.push_back(m().mk_ite(x, out1[j].get(), out2[j].get()));
}
}
else {
numeral n_a, n_b;
SASSERT(i == sz && !is_a);
VERIFY(is_numeral(sz, a_bits.c_ptr(), n_a));
VERIFY(is_numeral(sz, b_bits.c_ptr(), n_b));
n_a *= n_b;
num2bits(n_a, sz, out_bits);
}
}
template<typename Cfg>
bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
numeral n_a;
if (!is_numeral(sz, a_bits, n_a)) {
return false;
}
SASSERT(out_bits.empty());
if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
return true;
}
if (!m_use_bcm) {
return false;
}
expr_ref_vector minus_b_bits(m()), tmp(m());
mk_neg(sz, b_bits, minus_b_bits);
@ -1255,4 +1310,6 @@ void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
return true;
}

View file

@ -1968,7 +1968,63 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
}
#include "ast_pp.h"
bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
std::swap(lhs, rhs);
}
if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
return false;
}
unsigned sz = to_app(rhs)->get_num_args();
expr_ref t1(m()), t2(m());
t1 = to_app(rhs)->get_arg(0);
if (sz > 2) {
t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
}
else {
SASSERT(sz == 2);
t2 = to_app(rhs)->get_arg(1);
}
mk_t1_add_t2_eq_c(t1, t2, lhs, result);
return true;
}
bool bv_rewriter::is_add_mul_const(expr* e) const {
if (!m_util.is_bv_add(e)) {
return false;
}
unsigned num = to_app(e)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(e)->get_arg(i);
expr * c2, * x2;
if (m_util.is_numeral(arg))
continue;
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
continue;
return false;
}
return true;
}
bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
return
m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs))) ||
m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)));
}
bool bv_rewriter::has_numeral(app* a) const {
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (is_numeral(a->get_arg(i))) {
return true;
}
}
return false;
}
br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
expr * c, * x;
numeral c_val, c_inv_val;
unsigned sz;
@ -2001,24 +2057,30 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
// c * x = t_1 + ... + t_n
// and t_i's have non-unary coefficients (this condition is used to make sure we are actually reducing the number of multipliers).
if (m_util.is_bv_add(rhs)) {
if (is_add_mul_const(rhs)) {
// Potential problem: this simplification may increase the number of adders by reducing the amount of sharing.
unsigned num = to_app(rhs)->get_num_args();
unsigned i;
for (i = 0; i < num; i++) {
expr * arg = to_app(rhs)->get_arg(i);
expr * c2, * x2;
if (m_util.is_numeral(arg))
continue;
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
continue;
break;
}
if (i == num) {
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
return BR_REWRITE2;
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
return BR_REWRITE2;
}
}
if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
unsigned sz = to_app(rhs)->get_num_args();
unsigned i = 0;
expr* c2, *x2;
numeral c2_val, c2_inv_val;
bool found = false;
for (; !found && i < sz; ++i) {
expr* arg = to_app(rhs)->get_arg(i);
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
m_util.mult_inverse(c2_val, sz, c2_inv_val)) {
found = true;
}
}
if (found) {
result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
return BR_REWRITE3;
}
}
return BR_FAILED;
}
@ -2065,9 +2127,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return st;
}
expr_ref new_lhs(m());
expr_ref new_rhs(m());
if (m_util.is_bv_add(lhs) || m_util.is_bv_mul(lhs) || m_util.is_bv_add(rhs) || m_util.is_bv_mul(rhs)) {
expr_ref new_lhs(m());
expr_ref new_rhs(m());
st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
if (st != BR_FAILED) {
if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
@ -2080,28 +2143,27 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
new_rhs = rhs;
}
lhs = new_lhs;
rhs = new_rhs;
// Try to rewrite t1 + t2 = c --> t1 = c - t2
// Reason: it is much cheaper to bit-blast.
expr * t1, * t2;
if (m_util.is_bv_add(new_lhs, t1, t2) && is_numeral(new_rhs)) {
mk_t1_add_t2_eq_c(t1, t2, new_rhs, result);
if (isolate_term(lhs, rhs, result)) {
return BR_REWRITE2;
}
if (m_util.is_bv_add(new_rhs, t1, t2) && is_numeral(new_lhs)) {
mk_t1_add_t2_eq_c(t1, t2, new_lhs, result);
return BR_REWRITE2;
if (is_concat_target(lhs, rhs)) {
return mk_eq_concat(lhs, rhs, result);
}
if (st != BR_FAILED) {
result = m().mk_eq(new_lhs, new_rhs);
result = m().mk_eq(lhs, rhs);
return BR_DONE;
}
}
if ((m_util.is_concat(lhs) && is_concat_split_target(rhs)) ||
(m_util.is_concat(rhs) && is_concat_split_target(lhs)))
if (is_concat_target(lhs, rhs)) {
return mk_eq_concat(lhs, rhs, result);
}
if (swapped) {
result = m().mk_eq(lhs, rhs);
return BR_DONE;

View file

@ -137,6 +137,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool is_concat_split_target(expr * t) const;
br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result);
bool is_add_mul_const(expr* e) const;
bool isolate_term(expr* lhs, expr* rhs, expr_ref & result);
bool has_numeral(app* e) const;
bool is_concat_target(expr* lhs, expr* rhs) const;
void updt_local_params(params_ref const & p);

View file

@ -424,6 +424,39 @@ namespace smt {
};
void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
++m_stats.m_num_eq_dynamic;
if (v1 > v2) {
std::swap(v1, v2);
}
unsigned sz = get_bv_size(v1);
ast_manager& m = get_manager();
context & ctx = get_context();
app* o1 = get_enode(v1)->get_owner();
app* o2 = get_enode(v2)->get_owner();
literal oeq = mk_eq(o1, o2, true);
TRACE("bv",
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
<< ctx.get_scope_level() << "\n";);
literal_vector eqs;
for (unsigned i = 0; i < sz; ++i) {
literal l1 = m_bits[v1][i];
literal l2 = m_bits[v2][i];
expr_ref e1(m), e2(m);
e1 = mk_bit2bool(o1, i);
e2 = mk_bit2bool(o2, i);
literal eq = mk_eq(e1, e2, true);
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
ctx.mk_th_axiom(get_id(), l1, l2, eq);
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
ctx.mk_th_axiom(get_id(), eq, ~oeq);
eqs.push_back(~eq);
}
eqs.push_back(oeq);
ctx.mk_th_axiom(get_id(), eqs.size(), eqs.c_ptr());
}
void theory_bv::fixed_var_eh(theory_var v) {
numeral val;
bool r = get_fixed_value(v, val);
@ -443,7 +476,9 @@ namespace smt {
display_var(tout, v);
display_var(tout, v2););
m_stats.m_num_th2core_eq++;
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
add_fixed_eq(v, v2);
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
m_fixed_var_table.insert(key, v2);
}
}
else {
@ -1177,6 +1212,7 @@ namespace smt {
}
void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
m_stats.m_num_bit2core++;
context & ctx = get_context();
SASSERT(ctx.get_assignment(antecedent) == l_true);
@ -1192,6 +1228,12 @@ namespace smt {
}
else {
ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
literal_vector lits;
lits.push_back(~consequent);
lits.push_back(antecedent);
lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (m_wpos[v2] == idx)
find_wpos(v2);
// REMARK: bit_eq_justification is marked as a theory_bv justification.
@ -1601,6 +1643,7 @@ namespace smt {
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
st.update("bv bit2core", m_stats.m_num_bit2core);
st.update("bv->core eq", m_stats.m_num_th2core_eq);
st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
}
#ifdef Z3DEBUG

View file

@ -34,6 +34,7 @@ namespace smt {
struct theory_bv_stats {
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
unsigned m_num_eq_dynamic;
void reset() { memset(this, 0, sizeof(theory_bv_stats)); }
theory_bv_stats() { reset(); }
};
@ -124,8 +125,9 @@ namespace smt {
typedef std::pair<numeral, unsigned> value_sort_pair;
typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
value2var m_fixed_var_table;
value2var m_fixed_var_table;
literal_vector m_tmp_literals;
svector<var_pos> m_prop_queue;
bool m_approximates_large_bvs;
@ -166,6 +168,7 @@ namespace smt {
void find_wpos(theory_var v);
friend class fixed_eq_justification;
void fixed_var_eh(theory_var v);
void add_fixed_eq(theory_var v1, theory_var v2);
bool get_fixed_value(theory_var v, numeral & result) const;
void internalize_num(app * n);
void internalize_add(app * n);

View file

@ -1,32 +1,33 @@
/*++
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
bit_blaster_tactic.h
Abstract:
Abstract:
Apply bit-blasting to a given goal.
Author:
Author:
Leonardo (leonardo) 2011-10-25
Notes:
--*/
Notes:
--*/
#ifndef BIT_BLASTER_TACTIC_H_
#define BIT_BLASTER_TACTIC_H_
#include"params.h"
#include"bit_blaster_rewriter.h"
class ast_manager;
class tactic;
#include"params.h"
#include"bit_blaster_rewriter.h"
class ast_manager;
class tactic;
tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p = params_ref());
/*
/*
ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
*/
#endif
*/
#endif

View file

@ -22,7 +22,7 @@ Revision History:
#include"occurs.h"
#include"cooperate.h"
#include"goal_shared_occs.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
class solve_eqs_tactic : public tactic {
struct imp {
@ -92,21 +92,23 @@ class solve_eqs_tactic : public tactic {
}
// Use: (= x def) and (= def x)
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
bool trivial_solve1(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
var = to_app(lhs);
def = rhs;
pr = 0;
return true;
}
else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) {
var = to_app(rhs);
def = lhs;
if (m_produce_proofs)
pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
return true;
else {
return false;
}
return false;
}
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
return
trivial_solve1(lhs, rhs, var, def, pr) ||
trivial_solve1(rhs, lhs, var, def, pr);
}
// (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))