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

(* TODO: put this in some other more appropriate module? *)
type solver_type =
  | Z3_solver
  | Bitwuzla_solver
  | Colibri2_solver
  | Cvc5_solver

let mappings_of_solver : solver_type -> (module Mappings_intf.S_with_fresh) =
  function
  | Z3_solver -> (module Z3_mappings)
  | Bitwuzla_solver -> (module Bitwuzla_mappings)
  | Colibri2_solver -> (module Colibri2_mappings)
  | Cvc5_solver -> (module Cvc5_mappings)

let solver_type_of_string (s : string) :
  (solver_type, [> `Msg of string ]) result =
  match String.map Char.lowercase_ascii s with
  | "z3" -> Ok Z3_solver
  | "bitwuzla" -> Ok Bitwuzla_solver
  | "colibri2" -> Ok Colibri2_solver
  | "cvc5" -> Ok Cvc5_solver
  | s -> Error (`Msg (Format.sprintf "unknown solver %s" s))

let is_available : solver_type -> bool = 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

(** List of all available solvers *)
let available_solvers : solver_type list =
  List.filter is_available
    [ Z3_solver; Bitwuzla_solver; Colibri2_solver; Cvc5_solver ]

(** Returns first available solver or errors when none exist *)
let solver : ((module Mappings_intf.S_with_fresh), [> `Msg of string ]) result =
  match available_solvers with
  | [] -> Error (`Msg "no available solver")
  | solver :: _ -> Ok (mappings_of_solver solver)

let pp_solver_type fmt = function
  | Z3_solver -> Format.fprintf fmt "Z3"
  | Bitwuzla_solver -> Format.fprintf fmt "Bitwuzla"
  | Colibri2_solver -> Format.fprintf fmt "Colibri2"
  | Cvc5_solver -> Format.fprintf fmt "cvc5"