6 ms·
I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean (https://github.com/leanprover/lean4/pulls?q=+i
by bollu 2y ago
I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean (https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%3Abollu+ https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%...), and it's genius --- the algorithms, the reductions, the heuristics, it's all so deep.
- zero_k 2y agoWow, nice work [1] ! I used to work on CryptoMiniSat a lot. Nowadays I'm doing model counting and maybe synthesis, if all goes well [2] [1] https://github.com/leanprover/lean4/pulls/bollu https://github.com/leanprover/lean4/pulls/bollu [2] https://x.com/SoosMate/status/1827308967208317241 https://x.com/SoosMate/status/1827308967208317241