package smtml
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5db378d398a6ef1a166955e66d2695f8
sha512=e17831796ffdcff0cecc7456a02dbfcd7c6f9c5cccdc1dc728948060e03161c4b96d9d567ff6ad732f93b11cd346f080e831969ddf2562748e6eb5f69c56d0da
CHANGES.md.html
Unreleased
v0.2.0
Added
Added
List
andApp
values (@joaomhmpereira)Added
Naryop
toExpr
(@joaomhmpereira)Added
val Expr.ptr : int32 -> t -> t
constructor (@filipeom)Added missing concrete simplification to
Eval
(@joaomhmpereira)
Changed
Renamed
Seq_
operators toString_
(@joaomhmpereira)String.concat
is now a nary operator (@joaomhmpereira)Made
Eval.TypeError
more explicit on which operator triggered the error. (@joaomhmpereira)Made
Expr.Ptr
a record (@filipeom)
Fixed
Missing bitwuzla operators
to_fp
andof_ieee_bv
.
v0.1.3
Changed
Changed
Num.( = )
toNum.equal
to be more consistent with other modules
Fixed
Fixed comparison of boolean values
v0.1.2
Added
Adds
Solver_dispacher.{is_available|available_solvers|solver}
to check availability of installed solversModel generation for Bitwuzla
Changed
Exposes
Optimizer.Make
to allow for parametric optimizersMakes Z3 optional
Fixed
Parametric mappings should only create sorts once
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