[SAVer] Added option for loading a CSV dataset for SAVer.

src/main.ml

@@ -16,7 +16,7 @@ let () =
 let () =
   Pyrat.init ();
   Marabou.init ();
-  Saver.init()
+  Saver.init ()
 
 (* -- Logs. *)
 
@@ -69,10 +69,12 @@ let config detect () =
            Whyconf.print_prover Pp.nothing)
         provers))
 
-let verify format loadpath memlimit timeout prover files =
+let verify format loadpath memlimit timeout prover dataset_csv 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
+         ~dataset_csv)
     files
 
 let exec_cmd cmdname cmd =
@@ -155,6 +157,13 @@ let verify_cmd =
     in
     Arg.(required & opt (some provers) None & info [ "p"; "prover" ] ~doc)
   in
+  let dataset_csv =
+    let doc =
+      "Dataset under .csv format to use for analyse.\n\
+      \    Currently only supported by SAVer."
+    in
+    Arg.(value & opt (some string) None & info [ "dataset-csv" ] ~doc)
+  in
   let doc =
     "Property verification of neural networks using external provers."
   in
@@ -162,11 +171,13 @@ let verify_cmd =
   let man = [ `S Manpage.s_description; `P doc ] in
   ( Term.(
       ret
-        (const (fun format loadpath memlimit timeout prover files _ ->
+        (const
+           (fun format loadpath memlimit timeout prover dataset_csv files _ ->
            `Ok
              (exec_cmd cmdname (fun () ->
-                verify format loadpath memlimit timeout prover files)))
-        $ format $ loadpath $ memlimit $ timeout $ prover $ files $ setup_logs)),
+                verify format loadpath memlimit timeout prover dataset_csv files)))
+        $ format $ loadpath $ memlimit $ timeout $ prover $ dataset_csv $ files
+        $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
 let default_cmd =

src/verification.ml

@@ -55,9 +55,13 @@ let combine_prover_answers answers =
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-let handle_task_saver task env command =
+let handle_task_saver task env dataset_csv command =
   let open Why3 in
-  let dataset_filename = "test_data.csv" in
+  let dataset_filename =
+    match dataset_csv with
+    | Some s -> s
+    | None -> failwith "Error, no dataset provided for SAVer."
+  in
   let goal = Task.task_goal_fmla task in
   let eps, svm_filename =
     match goal.t_node with
@@ -96,12 +100,12 @@ let handle_task_saver task env command =
   command
 
 let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
-  task =
+  dataset_csv task =
   let open Why3 in
   if String.equal prover.prover.prover_name "SAVer"
   then
     let command = Whyconf.get_complete_command ~with_steps:false prover in
-    let command = handle_task_saver task env command in
+    let command = handle_task_saver task env dataset_csv command in
     let res_parser =
       {
         Call_provers.prp_regexps =
@@ -174,7 +178,8 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
     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
+  ~dataset_csv file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in
@@ -217,6 +222,8 @@ let verify ?(debug = false) format loadpath ?memlimit ?timeout prover file =
           Driver.load_driver_absolute env file prover.extra_drivers
       in
       List.iter
-        ~f:(call_prover ~limit (Whyconf.get_main config) prover driver env)
+        ~f:
+          (call_prover ~limit (Whyconf.get_main config) prover driver env
+             dataset_csv)
         tasks)
     mstr_theory

src/verification.mli

@@ -18,6 +18,7 @@ val verify :
   ?memlimit:int ->
   ?timeout:int ->
   Prover.t ->
+  dataset_csv:string option ->
   File.t ->
   unit
 (** [verify debug format loadpath memlimit timeout prover file] launches a
@@ -28,4 +29,7 @@ val verify :
     @param loadpath is the additional loadpath.
     @param memlimit
       is the memory limit (in megabytes) granted to the verification.
-    @param timeout is the timeout (in seconds) granted to the verification. *)
+    @param timeout is the timeout (in seconds) granted to the verification.
+    @param dataset_csv
+      is the filepath of a dataset to analyze. Currently, it is only required
+      for SAVer. *)