Implement evaluation for integers and bitvectors

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic

MIT License

5 stars 0 forks source link

Implement evaluation for integers and bitvectors #137

Closed ryandancy closed 1 month ago

ryandancy commented 1 month ago

This expands Evaluator and DefinitionJit to evaluate integers, bitvectors, and builtin functions of the two. BvSignedRem and BvSignedMod aren't yet implemented since I wasn't sure what the difference between them is.

On 4-bit-adder.als, the evaluator reduces the time on my machine from ~6s to ~2s!

nancyday commented 1 month ago

Looks good to me. I will leave @otzzila to look at the bit vector code. Interesting bug in the typechecker for sorts.