df74c80973
This PR adds a bitblasting circuit for `BitVec.cpop` with a divide-and-conquer for a parallel-prefix-sum. This is the [most efficient circuit we could fine](https://docs.google.com/spreadsheets/d/1dJ5uUY4-eWIQmMjIui3H4U-wBxBxy-qYuqJZFZD1xvA/edit?usp=sharing), after comparing with Kernighan's algorithm and with the intuitive addition circuit. --------- Co-authored-by: Henrik Böving <hargonix@gmail.com>
2 lines
142 B
Text
2 lines
142 B
Text
bv_decide_rewriter.lean:696:0-696:7: warning: declaration uses `sorry`
|
|
bv_decide_rewriter.lean:709:0-709:7: warning: declaration uses `sorry`
|