package smtml

  1. Overview
  2. No Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Edit opam file Versions (25)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.30.0.tar.gz
md5=afedffddc52bc135ea1bd98b19ca0455
sha512=ed7d21125c7441de37c3326fb667822ccd97e5880449886ff6bcbdddcac39d0cd7821c86982e8b21fa97b308edf92b7c8b4de127a993d56360cef10b63c7c8fa

Description

Smt.ml is an SMT solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability.

Added to opam-repository:

Dependencies (22)

  1. zarith >= "1.5"
  2. yojson >= "1.6.0"
  3. mtime >= "2.0.0"
  4. scfg >= "0.5"
  5. prelude >= "0.5"
  6. ppx_enumerate
  7. ppx_deriving
  8. ocaml_intrinsics
  9. ocaml >= "4.14.0"
  10. menhir build & >= "20220210"
  11. hc >= "0.5"
  12. farith
  13. fpath
  14. fmt >= "0.8.7"
  15. dolmen_model >= "0.10"
  16. dolmen_type >= "0.10"
  17. dolmen >= "0.10"
  18. dune-site >= "3.20"
  19. dune-build-info >= "3.20"
  20. dune >= "3.20"
  21. cmdliner >= "1.3.0"
  22. bos

Dev Dependencies (16)

  1. tls-lwt with-dev-setup
  2. sexplib with-dev-setup
  3. re with-dev-setup
  4. mdx with-test
  5. lwt with-dev-setup
  6. dune-glob with-dev-setup
  7. extunix with-dev-setup
  8. cohttp-lwt-unix with-dev-setup
  9. cohttp with-dev-setup
  10. benchpress with-dev-setup & = "dev"
  11. ocaml-lsp-server with-dev-setup
  12. ocamlformat >= "0.29.0" & with-dev-setup
  13. bisect_ppx with-dev-setup & >= "2.5.0"
  14. alcotest with-test
  15. sherlodoc with-doc
  16. odoc with-doc

Used by (1)

  1. symex

Conflicts (6)

  1. z3 < "4.16.0"
  2. cvc5 < "1.3.0-2"
  3. colibrilib < "0.6.0"
  4. colibri2 < "0.6.0"
  5. bitwuzla-cxx < "0.6.0"
  6. alt-ergo-lib < "2.6.2"