mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

lazy multiplier experiment

Browse source 
this update provides a use case for and allows testing incremental multiplier compilation.
This commit is contained in:
Nikolaj Bjorner 2022-09-05 03:09:18 -07:00
parent 616fc2cbd5
commit 8dc8de8ccd
2 changed files with 63 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/sat/smt/bv_delay_internalize.cpp
View file

@ -72,6 +72,55 @@ namespace bv {
return expr_ref(bv.mk_numeral(val, get_bv_size(v)), m);
}
/**
\brief expose the multiplication circuit lazily.
It adds clauses for multiplier output one by one to enforce
the semantics of multiplier semantics.
*/
bool solver::check_lazy_mul(app* e, expr* arg_value, expr* mul_value) {
SASSERT(e->get_num_args() >= 2);
expr_ref_vector args(m), new_args(m), new_out(m);
lazy_mul* lz = nullptr;
rational v0, v1;
unsigned sz, diff = 0;
VERIFY(bv.is_numeral(arg_value, v0, sz));
VERIFY(bv.is_numeral(mul_value, v1));
for (diff = 0; diff < sz; ++diff)
if (v0.get_bit(diff) != v1.get_bit(diff))
break;
SASSERT(diff < sz);
auto set_bits = [&](unsigned j, expr_ref_vector& bits) {
bits.reset();
for (unsigned i = 0; i < sz; ++i)
bits.push_back(bv.mk_bit2bool(e->get_arg(0), j));
};
if (!m_lazymul.find(e, lz)) {
set_bits(0, args);
for (unsigned j = 1; j < e->get_num_args(); ++j) {
new_out.reset();
set_bits(j, new_args);
m_bb.mk_multiplier(sz, args.data(), new_args.data(), new_out);
new_out.swap(args);
}
lz = alloc(lazy_mul, e, args);
m_lazymul.insert(e, lz);
ctx.push(new_obj_trail(lz));
ctx.push(insert_obj_map(m_lazymul, e));
}
if (lz->m_out.size() == lz->m_bits)
return false;
for (unsigned i = lz->m_bits; i <= diff; ++i) {
sat::literal bit1 = mk_literal(lz->m_out.get(i));
sat::literal bit2 = mk_literal(bv.mk_bit2bool(e, i));
add_equiv(bit1, bit2);
}
ctx.push(value_trail(lz->m_bits));
IF_VERBOSE(1, verbose_stream() << "expand lazy mul " << mk_pp(e, m) << " to " << diff << "\n");
lz->m_bits = diff;
return false;
}
bool solver::check_mul(app* e) {
SASSERT(e->get_num_args() >= 2);
expr_ref_vector args(m);
@ -96,6 +145,9 @@ namespace bv {
if (!check_mul_invertibility(e, args, r1))
return false;
if (!check_lazy_mul(e, r1, r2))
return false;
// Some other possible approaches:
// algebraic rules:
// x*(y+z), and there are nodes for x*y or x*z -> x*(y+z) = x*y + x*z

11
src/sat/smt/bv_solver.h
View file

@ -26,6 +26,15 @@ namespace euf {
namespace bv {
struct lazy_mul {
expr_ref_vector m_out;
unsigned m_bits;
lazy_mul(app* a, expr_ref_vector& out):
m_out(out),
m_bits(0) {
}
};
class solver : public euf::th_euf_solver {
typedef rational numeral;
typedef euf::theory_var theory_var;
@ -215,6 +224,7 @@ namespace bv {
unsigned m_prop_queue_head = 0;
sat::literal m_true = sat::null_literal;
euf::enode_vector m_bv2ints;
obj_map<app, lazy_mul*> m_lazymul;
// internalize
void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
@ -280,6 +290,7 @@ namespace bv {
bool m_cheap_axioms{ true };
bool should_bit_blast(app * n);
bool check_delay_internalized(expr* e);
bool check_lazy_mul(app* e, expr* mul_value, expr* arg_value);
bool check_mul(app* e);
bool check_mul_invertibility(app* n, expr_ref_vector const& arg_values, expr* value);
bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);