package smtml

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

Install 

dune-project
 Dependency

github.com Readme Changelog 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.25.0.tar.gz
md5=9ef240b636d7059d48bb54e6b8f0a4c4
sha512=2c73a5baa2e4f8a496f575087597510edae58a4416959108e7a4b063fb9a35ae7461227c679868d82cd324865a563bd2a0df6da1fa3a88d416f76be32ea07809

doc/src/smtml/solver_type.ml.html

Source file solver_type.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by the Smtml programmers *)

type t =
  | Z3_solver
  | Bitwuzla_solver
  | Colibri2_solver
  | Cvc5_solver
  | Altergo_solver
  | Smtzilla_solver
[@@deriving enumerate]

let supported_solvers = all

let of_string s =
  match String.map Char.lowercase_ascii s with
  | "z3" -> Ok Z3_solver
  | "bitwuzla" -> Ok Bitwuzla_solver
  | "colibri2" -> Ok Colibri2_solver
  | "cvc5" -> Ok Cvc5_solver
  | "alt-ergo" -> Ok Altergo_solver
  | "smtzilla" -> Ok Smtzilla_solver
  | s -> Error (`Msg (Fmt.str "unknown solver %s" s))

let pp fmt = function
  | Z3_solver -> Fmt.string fmt "Z3"
  | Bitwuzla_solver -> Fmt.string fmt "Bitwuzla"
  | Colibri2_solver -> Fmt.string fmt "Colibri2"
  | Cvc5_solver -> Fmt.string fmt "cvc5"
  | Altergo_solver -> Fmt.string fmt "Alt-Ergo"
  | Smtzilla_solver -> Fmt.string fmt "SMTZilla"

let conv = Cmdliner.Arg.conv (of_string, pp)

let is_available = function
  | Z3_solver -> Z3_mappings.is_available
  | Bitwuzla_solver -> Bitwuzla_mappings.is_available
  | Colibri2_solver -> Colibri2_mappings.is_available
  | Cvc5_solver -> Cvc5_mappings.is_available
  | Altergo_solver -> Altergo_mappings.is_available
  | Smtzilla_solver ->
    Z3_mappings.is_available || Bitwuzla_mappings.is_available

let to_mappings : t -> (module Mappings.S_with_fresh) = function
  | Z3_solver -> (module Z3_mappings)
  | Bitwuzla_solver -> (module Bitwuzla_mappings)
  | Colibri2_solver -> (module Colibri2_mappings)
  | Cvc5_solver -> (module Cvc5_mappings)
  | Altergo_solver -> (module Altergo_mappings)
  | Smtzilla_solver -> (module Smtzilla)