issues
search
leanprover
/
leansat
This package provides an interface and foundation for verified SAT reasoning
Apache License 2.0
48
stars
6
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
refactor: remove AIG optimizations
#87
hargoniX
closed
3 months ago
1
perf: Optimize the LRAT parser as far as I can
#86
hargoniX
closed
3 months ago
0
perf: Improve the performance of the LRAT parser.
#85
hargoniX
closed
3 months ago
0
feat: bv_decide?
#84
hargoniX
closed
3 months ago
0
feat: BitVec.slt
#83
hargoniX
closed
3 months ago
0
Investigate Local Two-Level And-Inverter Graph Minimization without Blowup
#82
hargoniX
opened
3 months ago
0
Investigate Bitwuzla
#81
hargoniX
opened
3 months ago
0
Investigate `lrat-trim`
#80
hargoniX
closed
2 months ago
1
feat: Counterexample extraction
#79
hargoniX
closed
3 months ago
0
test: consolidate the BV and AIG test framework
#78
hargoniX
closed
3 months ago
0
feat: BitVec.extract
#77
hargoniX
closed
3 months ago
0
feat: use rewriters if possible
#76
hargoniX
closed
3 months ago
0
chore: update to nightly
#75
hargoniX
closed
3 months ago
0
feat: BitVec.append
#74
hargoniX
closed
3 months ago
0
feat: normalize Nat.cast
#73
hargoniX
closed
3 months ago
0
feat: BitVec.ult/BitVec.ule
#72
hargoniX
closed
3 months ago
0
WIP: hitlist
#71
hargoniX
closed
3 months ago
0
feat: add ternary operator to AIG framework
#70
hargoniX
closed
3 months ago
0
feat: getLsb
#69
hargoniX
closed
3 months ago
0
Add support for mutual recursion between the BV and the boolean fragment
#68
hargoniX
opened
3 months ago
1
Add support for boolean variables in the `bv_decide` structure
#67
hargoniX
closed
2 months ago
0
`bv_decide?`
#66
hargoniX
closed
3 months ago
0
Get to the expressiveness of QF_BV
#65
hargoniX
opened
3 months ago
0
feat: increase constant folding capabilities of bv_normalize
#64
hargoniX
closed
3 months ago
0
feat: bitblast sub
#63
hargoniX
closed
4 months ago
0
feat: bitblast negation
#62
hargoniX
closed
4 months ago
0
chore: upgrade toolchain
#61
hargoniX
closed
4 months ago
0
feat: CITATION.cff
#60
hargoniX
closed
2 months ago
0
feat: Boolean sub structure for bit vector problems
#59
hargoniX
closed
4 months ago
0
chore: fix unused variables lint
#58
hargoniX
closed
4 months ago
0
chore: general cleanups of the proofs
#57
hargoniX
closed
4 months ago
0
chore: upgrade toolchain
#56
hargoniX
closed
4 months ago
0
feat: zeroExtend
#55
hargoniX
closed
4 months ago
0
feat: shift right const
#54
hargoniX
closed
4 months ago
0
chore: shift left rename
#53
hargoniX
closed
4 months ago
0
test: Eval framework
#52
hargoniX
closed
4 months ago
0
chore: upgrade toolchain
#51
hargoniX
closed
4 months ago
0
feat: add simple script to track successful builds
#50
Daniel1854
closed
4 months ago
0
refactor: switch to a different linearity ensuring style
#49
hargoniX
closed
4 months ago
0
test: add popcount example from galois
#48
hargoniX
closed
4 months ago
0
test: add the blog post I read today as a test
#47
hargoniX
closed
4 months ago
0
refactor: make some use of those cores!
#46
hargoniX
closed
4 months ago
0
feat: add BitVec.shiftLeft
#45
hargoniX
closed
4 months ago
0
refactor: Pull out shared code in reflecting binary ops
#44
hargoniX
closed
4 months ago
0
feat: BitVec.add
#43
hargoniX
closed
4 months ago
0
feat: Add BitVec.xor
#42
hargoniX
closed
4 months ago
0
feat: add BitVec.or support to bv_decide
#41
hargoniX
closed
4 months ago
0
refactor: always bitblast entire expressions at once instead of single bits
#40
hargoniX
closed
4 months ago
0
refactor: use AIG.Ref in AIG.Entrypoint
#39
hargoniX
closed
4 months ago
0
chore: update toolchain
#38
hargoniX
closed
5 months ago
0
Previous
Next