leansat
leansat copied to clipboard
leanprover
This package provides an interface and foundation for verified SAT reasoning
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...
We want the `bv_decide` tactic to be able to solve things at the expressiveness of QF_BV (https://smt-lib.org/theories-FixedSizeBitVectors.shtml). This requires adding a lot of primitive operations to the bitblaster still. It...
Metadata
Owner
Metadata
This package provides an interface and foundation for verified SAT reasoning