package cvc5

  1. Overview
  2. Docs
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, and CAMLreturn 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:

Added

Stubs with support for the following cvc5 API classes:

  • Solver
  • TermManager
  • Term
  • Op
  • Result
  • Sort

Changed

Fixed

OCaml

Innovation. Community. Security.