Adds is_available flag to know which solvers are installed

Author: filipeom

CHANGES.md

@@ -2,6 +2,8 @@
 
 ### Added
 
+- Adds `Solver_dispacher.{is_available|available_solvers|solver}` to check
+availability of installed solvers
 - Model generation for Bitwuzla
 
 ### Changed

lib/bitwuzla_mappings.default.ml

@@ -412,6 +412,9 @@ end
 include (
   Mappings.Make (struct
     module Make () = Fresh_bitwuzla (Bitwuzla_cxx.Make ())
+
+    let is_available = true
+
     include Fresh_bitwuzla (Bitwuzla_cxx)
   end) :
     S_with_fresh )

lib/colibri2_mappings.default.ml

@@ -1065,4 +1065,6 @@ module Fresh = struct
   end
 end
 
+let is_available = true
+
 include Fresh.Make ()

lib/cvc5_mappings.default.ml

@@ -426,6 +426,9 @@ end
 
 module Cvc5_with_make : Mappings_intf.M_with_make = struct
   module Make () = Fresh_cvc5 ()
+
+  let is_available = true
+
   include Fresh_cvc5 ()
 end
 

lib/mappings.ml

@@ -686,5 +686,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
     module Make () = Make_ (M_with_make.Make ())
   end
 
+  let is_available = M_with_make.is_available
+
   include Make_ (M_with_make)
 end

lib/mappings.nop.ml

@@ -349,6 +349,8 @@ module Nop = struct
     end
   end
 
+  let is_available = false
+
   include Make ()
 end
 

lib/mappings_intf.ml

@@ -367,6 +367,8 @@ end
 module type M_with_make = sig
   module Make () : M
 
+  val is_available : bool
+
   include M
 end
 
@@ -439,5 +441,7 @@ module type S_with_fresh = sig
     module Make () : S
   end
 
+  val is_available : bool
+
   include S
 end

lib/solver_dispatcher.ml

@@ -1,28 +1,45 @@
 (* TODO: put this in some other more appropriate module? *)
 type solver_type =
   | Z3_solver
-  | Cvc5_solver
-  | Colibri2_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)
-  | Cvc5_solver -> (module Cvc5_mappings)
-  | Colibri2_solver -> (module Colibri2_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
-  | "colibri2" -> Ok Colibri2_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"
-  | Cvc5_solver -> Format.fprintf fmt "CVC5"
-  | Colibri2_solver -> Format.fprintf fmt "Colibri2"
   | Bitwuzla_solver -> Format.fprintf fmt "Bitwuzla"
+  | Colibri2_solver -> Format.fprintf fmt "Colibri2"
+  | Cvc5_solver -> Format.fprintf fmt "cvc5"

lib/z3_mappings.default.ml

@@ -816,4 +816,6 @@ module Fresh = struct
   end
 end
 
+let is_available = true
+
 include Fresh.Make ()

lib/z3_mappings2.default.ml

@@ -472,6 +472,8 @@ module M = struct
     end
   end
 
+  let is_available = true
+
   include Make ()
 end
 

test/test_bitwuzla.ml

@@ -1,5 +1,8 @@
 open Smtml
 open Smtml_tests
+
+let () = assert Bitwuzla_mappings.is_available
+
 module Test_solver_params =
   Test_solver_params.Make (Bitwuzla_mappings.Fresh.Make ())
 module Test_bv = Test_bv.Make (Bitwuzla_mappings)

test/test_colibri2.ml

@@ -1,5 +1,8 @@
 open Smtml
 open Smtml_tests
+
+let () = assert Colibri2_mappings.is_available
+
 module Test_solver_params = Test_solver_params.Make (Colibri2_mappings)
 module Test_solver = Test_solver.Make (Colibri2_mappings)
 module Test_bv = Test_bv.Make (Colibri2_mappings)

test/test_z3.ml

@@ -1,5 +1,8 @@
 open Smtml
 open Smtml_tests
+
+let () = assert Z3_mappings.is_available
+
 module Test_solver_params = Test_solver_params.Make (Z3_mappings.Fresh.Make ())
 module Test_solver = Test_solver.Make (Z3_mappings.Fresh.Make ())
 module Test_bv = Test_bv.Make (Z3_mappings.Fresh.Make ())