This repository has been archived by the owner on Apr 22, 2024. It is now read-only.

v0.0.4

Adds Arthur's clz and ctz implementations for i64s
Completes missing eval_numeric operations
Adds more tests to increase code coverage
Adds extend_ixx to lexer
Adds colibri2 mappings
Fixes hash-consing in 72eeb6f
Rename declare-fun to let-const
Rotate_left and rotate_right operators
Print floats in OCaml syntax (Closes #49)

v0.0.3

Improve bitv creation interface
Add naive hash-consing of expressions
Add Ceil and Floor FPA operators
Start migrating inline tests to standard tests
No simplifier on batch solver

v0.0.2

Support for bv8
Refactor optimizer interface
Fixes batch solver in e061344
Adds default simplifier in z3 leading to great performance gains
Adds logic configuration option to mk_solver
Fixes pp function in 11476fb
Adds ematching and timeout parameters
Improves documentation
Relax ocaml compiler constraint to >= 4.14.0

v0.0.1

Initial release