mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

final

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-31 22:09:29 +02:00
parent 88c982ff0b
commit ee216b5274
3 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -1169,7 +1169,7 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
if (!m().is_true(a_bits[i]))
continue;
ptr_buffer<expr, 128> one, sbits;
ptr_buffer<expr, 128> kbits, ibits;
expr_ref_vector out_bits1(m());
unsigned k = 0;
@ -1189,8 +1189,8 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
// shift by k+1, subtract x
out_bits.reset();
mul2_i(k + 1, sbits);
mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
mul2_i(k + 1, kbits);
mk_adder(sz, out_bits.data(), kbits.data(), out_bits1);
out_bits.reset();
out_bits.append(out_bits1);
out_bits1.reset();
@ -1201,18 +1201,25 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
out_bits.append(out_bits1);
out_bits1.reset();
}
else if (i == k) {
mul2_i(i, sbits);
mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
else if (i <= k && k <= i + 1) {
mul2_i(i, ibits);
mk_adder(sz, out_bits.data(), ibits.data(), out_bits1);
out_bits.reset();
out_bits.append(out_bits1);
out_bits1.reset();
if (i + 1 == k) {
mul2_i(k, kbits);
mk_adder(sz, out_bits.data(), kbits.data(), out_bits1);
out_bits.reset();
out_bits.append(out_bits1);
out_bits1.reset();
}
}
else if (k == sz - 1) {
// 2^sz - 2^i = - 2^i
// -= x*2^i
mul2_i(i, sbits);
mk_subtracter(sz, out_bits.data(), sbits.data(), out_bits1, cout);
mul2_i(i, ibits);
mk_subtracter(sz, out_bits.data(), ibits.data(), out_bits1, cout);
out_bits.reset();
out_bits.append(out_bits1);
}

2
src/smt/theory_lra.cpp
View file

@ -1943,7 +1943,7 @@ public:
final_check_status final_check_eh() {
verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
// verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
//ctx().display(verbose_stream());
//exit(0);

9
src/test/bit_blaster.cpp
View file

@ -195,12 +195,6 @@ void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) {
expr_ref_vector c(m), out1(m), out2(m);
for (unsigned j = 0; j < sz; ++j)
c.push_back((i & (1ul << j)) ? m.mk_true() : m.mk_false());
for (auto xi : x)
verbose_stream() << mk_pp(xi, m);
verbose_stream() << " ";
for (auto ci : c)
verbose_stream() << mk_pp(ci, m);
verbose_stream() << "\n";
blaster.mk_const_case1_multiplier(sz, c.data(), x.data(), out1);
blaster.mk_generic_multiplier(sz, c.data(), x.data(), out2);
@ -211,7 +205,6 @@ void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) {
smt::kernel solver(m, fp);
solver.assert_expr(m.mk_not(fml));
auto r = solver.check();
verbose_stream() << r << "\n";
VERIFY(r == l_false);
expr_mark vis1, vis2;
unsigned sz1 = 0, sz2 = 0;
@ -272,7 +265,7 @@ void tst_bit_blaster() {
bit_blaster_params params;
bit_blaster blaster(m, params);
tst_const_multiplier(m, blaster, 7);
tst_const_multiplier(m, blaster, 8);
tst_adder(m, blaster);
tst_multiplier(m, blaster);
tst_le(m, 4);