package cvc5
OCaml bindings for the cvc5 SMT solver
Install
Dune Dependency
Authors
Maintainers
Sources
ocaml-cvc5-v1.3.0.tar.gz
md5=51a6d3810d142adc3364f130f2dd5472
sha512=25d939c6e44898b25ac05a1837fdfdc4e6bc7819e8542e5c3daa80e2371c963256318c1df58c030d8731ff97a27d2967071c249128a2f866546e004016b37dc6
doc/CHANGES.html
1.3.0
Added
- Stub to create RegExp sort
Changed
- Updated cvc5's version to v1.3.0
- Updated CaDiCaL's version to v2.1.3
- Updated LibPoly's version to v0.2.0
- Changed LICENSE to MIT
Fixed
1.2.0
Added
- Stub-side reference counting to deal with GC collection order
- Refactor stubs to include
CAMLparam
,CAMLlocal
, andCAMLreturn
directives to safeguard GC interactions - Documentation for module interfaces
Changed
- Updated the version of cvc5 supported to v1.2.0
Fixed
- Changed number of Opam jobs used during compilation to avoid excessive memory use
1.1.3
Initial release.
Vendor submodules:
- cvc5 commit:27e8c50 (v1.1.3-unreleased)
- CaDiCaL commit:2df7b7f
- LibPoly commit:7a4dedc
- SymFPU commit:c3acaf6
Added
Stubs with support for the following cvc5 API classes:
- Solver
- TermManager
- Term
- Op
- Result
- Sort