either fix up or remove the constant-case multiplier #5512
Conversation
This code executes every time a bvmul is bit-blasted and has exactly one constant operand, but its output was always discarded because it unconditionally returns `false`. I'm trying to give this multiplier the best opportunity to show its value over straightforward long multiplication with three changes: - Try this variant even if some bits in both operands are not constant. If there are too many such bits it will still refuse to apply this potentially exponential-space transformation, though. - Use bool_rewriter's mk_ite simplifications, instead of calling ast_manager's mk_ite directly. - And, of course, return `true` if the transformation applied, so we can see what happens when it's actually used.
|
with the current branch I get
The trend seems to be very clearly in favor of this change. GIven that this has the clearest signal, I would merge this first. |
| @@ -1247,20 +1253,16 @@ void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsig | |||
|
|
|||
| 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) { | |||
| if (!m_use_bcm) { | |||
There was a problem hiding this comment.
I removed m_use_bcm. It would always be false, but my change almost for sure changes the behavior which I would have to revise or check.
| @@ -1212,7 +1216,7 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * | |||
| 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; | |||
There was a problem hiding this comment.
this looks like a terrible mistake
|
Since I introduced a bug in my previous push (a code path ignores that m_use_bcm is now false) I am porting your pull request directly and trying it out. There seems to be no longer a use for mk_const_multiplier either so this can be removed. |
Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work. In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier.
|
The changes from this pull request have now been integrated. |
|
|
|
One note about the version you merged: you only need to call the const case multiplier once. If calling it with the arguments one way around returns false, the other way will too. In the previous version it had to be called twice just because it was called only when its first argument was entirely constant, but that's not true in the current version. |
There's been a
mk_const_case_multiplierin the bit-blaster since 2015, but in all that time its output has never been used. With this PR I'm trying to give this multiplier the best opportunity to show its value over straightforward long multiplication. If it doesn't actually help, then instead of merging this PR I propose to remove the implementation.@NikolajBjorner, would you mind running a performance comparison of this patch versus master?