package smtml

Overview
No Docs

You can search for identifiers within the package.

in-package search v0.2.0

An SMT solver frontend for OCaml

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

Maintainers

F

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

Sources

v0.8.0.tar.gz

md5=f3384afc4c52ea0fcda2b434892f8412

sha512=47a70d32fae1c833b6a4765ab1152b241e1c60078a30c27b4669bb4a7fe499228d5c5783aca4462ed553408fa16488903924bad11b050bb22a985770796f56af

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.

Published: 05 Jul 2025

Dependencies (18)

zarith >= "1.5"
yojson >= "1.6.0"
scfg >= "0.5"
rusage
prelude >= "0.5"
patricia-tree >= "0.11.0"
ocaml_intrinsics
ocaml >= "4.14.0"
menhir build & >= "20220210"
hc >= "0.3"
fpath
fmt >= "0.8.7"
dolmen_model = "0.10"
dolmen_type = "0.10"
dolmen = "0.10"
dune >= "3.10"
cmdliner >= "1.3.0"
bos

Dev Dependencies (13)

tls-lwt with-dev-setup
sexplib with-dev-setup
mdx with-test
lwt with-dev-setup
dune-glob with-dev-setup
extunix with-dev-setup
cohttp-lwt-unix with-dev-setup
cohttp with-dev-setup
benchpress with-dev-setup & = "dev"
ounit2 with-test
bisect_ppx with-test & >= "2.5.0"
sherlodoc with-doc
odoc with-doc

Used by (1)

owi >= "0.2"

Conflicts (3)

z3 < "4.12.2" | >= "4.15"
alt-ergo-lib < "2.6.2"
bitwuzla-cxx < "0.6.0"

On This Page

Description
Dependencies (18)
Dev Dependencies (13)
Used by (1)
Conflicts (3)