Symbolic Bit Vectors#763
Conversation
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #763 +/- ##
=============================================
- Coverage 97.039% 96.681% -0.358%
=============================================
Files 99 101 +2
Lines 7295 7442 +147
=============================================
+ Hits 7079 7195 +116
- Misses 216 247 +31 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
🟡 Regression Test (12-Queens)'ssoelvsten/adiar/bvec' is a change in performance of -0.39% (stdev: 0.31%).
Number of samples: 3 |
🟡 Regression Test (Picotrav 'arbiter')'ssoelvsten/adiar/bvec' is a change in performance of 0.58% (stdev: 0.48%).
Number of samples: 3 |
🟡 Regression Test (QBF 'httt/4x4_9_tippy_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of 0.28% (stdev: 0.60%).
Number of samples: 3 |
🟡 Regression Test (QBF 'connect4/6x6_11_connect4_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of 0.57% (stdev: 1.52%).
Number of samples: 3 |
🟡 Regression Test (QBF 'breakthrough_dual/3x6_10_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of -0.72% (stdev: 1.18%).
Number of samples: 3 |
🟡 Regression Test (QBF 'breakthrough/3x4_19_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of -0.37% (stdev: 0.36%).
Number of samples: 3 |
🟡 Regression Test (Picotrav 'adder')'ssoelvsten/adiar/bvec' is a change in performance of 0.34% (stdev: 3.14%).
Number of samples: 3 |
🟡 Regression Test (QBF 'domineering/5x5_13_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of -0.13% (stdev: 0.36%).
Number of samples: 3 |
🟡 Regression Test (QBF 'ep_dual/8x8_6_e-8-1_p-2-3_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of 2.24% (stdev: 4.71%).
Number of samples: 3 |
🟡 Regression Test (QBF 'hex/hein_08_5x5-11_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of -0.31% (stdev: 0.69%).
Number of samples: 3 |
🟡 Regression Test (QBF 'ep/8x8_7_e-8-1_p-3-4_bwnib')'ssoelvsten/adiar/bvec' is a change in performance of -0.52% (stdev: 1.00%).
Number of samples: 3 |
🟡 Regression Test (14-Queens)'ssoelvsten/adiar/bvec' is a change in performance of 0.60% (stdev: 1.35%).
Number of samples: 3 |
🟡 Regression Test (Picotrav 'mem_ctrl')'ssoelvsten/adiar/bvec' is a change in performance of -0.03% (stdev: 0.37%).
Number of samples: 3 |
While the other thing was cool, we have multiple issues: - It seems more likely, that the end user wants to do a `bvec x = 42` than to specify the bit length as `bvec x(32)`. If anything, we should investigate whether one can move the `bitlen` into a template parameter. - By changing the above, we have an implicit conversion of constants to bit vectors. This removes the need to have `template <typename Integer>` overloads for each operator. - To make this not have any unforseen consequences, the bit length derived is as conservative as possible, i.e. it is only the number of bits needed to represent the number. Alternatively, we could have set the bit length to its default size which is used in other operations. Yet, if you do so then `x + 42` where `x` is an 8-bit integer would suddenly be extended to 64 by mistake. - To make sure that the default is both 0 and makes all operations have no side-effects, its length is also 0.
This also fixes the issue that 'bvec_sub' does not properly deal with variable length bit vectors.
2 participants
First major step towards #436 . This work was done by Palle H. Petersen (@pallehpetersen) on their fork with a little bit of a clean-up by me.