Henrik Böving
Henrik Böving
Right now without the respective reverse chunks functions to check if this API design is fine before doing it wrong twice.
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....
Closes: #66 A few open problems remain: - the generation of the simp syntax is not pretty - it also doesn't necessarily generate correct simp syntax apparently - It generates...
https://github.com/arminbiere/lrat-trim can be useful for us in two ways: 1. It provides a high performance LRAT checker implementation. We can probably check their algorithm out and learn something for our...
https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf describes a series of optimizations for AIGs that we might be interested in applying. Some of the basic ones are already implemented. We should check whether the remainder is...
https://github.com/bitwuzla/bitwuzla is currently the best QF_BV solver out there. While it is capable of a lot of things that we cannot imitate it might be interesting to: - [x] check...
If we want to support features like if statements efficiently it is necessary to process theory terms that consist e.g. of some BV logic which contains a boolean term which...
Having this would make the `sat_decide` part of the project obsolete as we could just always run `bv_decide` (potentially under a `sat_decide` alias) and use its capabilities for reasoning over...
Similar to `sat_decide?` there should be a `bv_decide?` that allows us to point `bv_decide` directly at a LRAT file to avoid making installing a SAT solver a basic requirement for...