package smtml
Install
Dune Dependency
Authors
Maintainers
Sources
md5=d05fc0acfe533234995c50c5264e20f1
sha512=63e057f40c8d5261493b5d7a03bcf073598dfa10c43b22b177fb24f8292e78753a051ae28e1d5a62d3c6725a7a32a9f1431f4c5f256f679d1a4b2b4c875f084b
CHANGES.md.html
v0.1.1
Improves interoperability with multiple solvers
Bug fixes for
colibri2
andz3
Adds preliminary support for cvc5
v0.1.0
Renames project to
Smt.ml
and library tosmtml
Minor fixes and typos
Adds preliminary support for the Bitwuzla solver
Completes concrete simplifications
Solver.check
now returns aSat | Unsat | Unknown
instead of abool
valueAdds owi's simplifications and smart op constructors
Moves theory annotation (
Ty.t
) only to necessary variants
v0.0.4
Adds Arthur's clz and ctz implementations for i64s
Completes missing
eval_numeric
operationsAdds more tests to increase code coverage
Adds
extend_ixx
to lexerAdds colibri2 mappings
Fixes hash-consing in 72eeb6f
Rename
declare-fun
tolet-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
andFloor
FPA operatorsStart 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
andtimeout
parametersImproves documentation
Relax ocaml compiler constraint to
>= 4.14.0
v0.0.1
Initial release