Add proper type for provers.

- Cmdline check for prover existance and exit with error in case no such a prover exist.
- User can now enter the name of a prover in a case-insensitive way.

caisar.opam

@@ -26,7 +26,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst" "--root" "."] {dev}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -34,8 +34,7 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files"
-    "false"
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

nnet.opam

@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst" "--root" "."] {dev}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -17,8 +17,7 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files"
-    "false"
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

onnx.opam

@@ -10,7 +10,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst" "--root" "."] {dev}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -18,8 +18,7 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files"
-    "false"
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

src/main.ml

@@ -71,7 +71,7 @@ let config detect () =
 let verify format loadpath memlimit timeout prover files =
   let debug = log_level_is_debug () in
   List.iter
-    ~f:(Verification.verify ~debug format loadpath ?memlimit ?timeout ~prover)
+    ~f:(Verification.verify ~debug format loadpath ?memlimit ?timeout prover)
     files
 
 let exec_cmd cmdname cmd =
@@ -141,7 +141,14 @@ let verify_cmd =
     Arg.(value & opt (some int) None & info [ "t"; "timeout" ] ~doc)
   in
   let prover =
-    let doc = "Prover to use." in
+    let available_provers =
+      Fmt.str "%a"
+        (Fmt.list ~sep:Fmt.comma Fmt.string)
+        (List.map ~f:Prover.to_string (Prover.list_available ()))
+    in
+    let doc =
+      Fmt.str "Prover to use. Available provers are: %s" available_provers
+    in
     Arg.(required & opt (some string) None & info [ "p"; "prover" ] ~doc)
   in
   let doc =
@@ -152,9 +159,13 @@ let verify_cmd =
   ( Term.(
       ret
         (const (fun format loadpath memlimit timeout prover files _ ->
-           `Ok
-             (exec_cmd cmdname (fun () ->
-                verify format loadpath memlimit timeout prover files)))
+           let error_msg = Fmt.str "No such prover %s" prover in
+           Option.value_map (Prover.of_string prover)
+             ~default:(`Error (true, error_msg))
+             ~f:(fun prover ->
+               `Ok
+                 (exec_cmd cmdname (fun () ->
+                    verify format loadpath memlimit timeout prover files))))
         $ format $ loadpath $ memlimit $ timeout $ prover $ files $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 

src/prover.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type t = Marabou | Pyrat | Saver
+
+let list_available () = [ Marabou; Pyrat; Saver ]
+
+let of_string prover =
+  let prover = String.lowercase_ascii prover in
+  match prover with
+  | "marabou" -> Some Marabou
+  | "pyrat" -> Some Pyrat
+  | "saver" -> Some Saver
+  | _ -> None
+
+let to_string = function
+  | Marabou -> "Marabou"
+  | Pyrat -> "PyRAT"
+  | Saver -> "SAVer"

src/prover.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type t
+
+val list_available : unit -> t list
+val of_string : string -> t option
+val to_string : t -> string

src/verification.ml

@@ -66,7 +66,7 @@ let call_prover ~limit config (prover : Whyconf.config_prover) driver task =
   Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
     Call_provers.print_prover_answer answer
 
-let verify ?(debug = false) format loadpath ?memlimit ?timeout ~prover file =
+let verify ?(debug = false) format loadpath ?memlimit ?timeout prover file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in
@@ -94,6 +94,7 @@ let verify ?(debug = false) format loadpath ?memlimit ?timeout ~prover file =
     (fun _ theory ->
       let tasks = Task.split_theory theory None None in
       let prover =
+        let prover = Prover.to_string prover in
         Whyconf.(filter_one_prover config (mk_filter_prover prover))
       in
       let driver =

src/verification.mli

@@ -10,7 +10,7 @@ val verify :
   string list ->
   ?memlimit:int ->
   ?timeout:int ->
-  prover:string ->
+  Prover.t ->
   string ->
   unit
 (** [verify debug format loadpath memlimit prover file] launches a verification