diff --git a/src/dataset.ml b/src/dataset.ml
index b7929720a04da2d26c5b965a97125f6b0aead0b8..81544a9f8e33f19fd1c985bb310c2e329f5145a1 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -68,7 +68,7 @@ let clip = function
fun x -> if clip then do_clip ~min ~max x else x
| Znorm _ -> Fn.id
-let apply_normalization (dataset : Csv.t) normalization =
+let apply_normalization dataset normalization =
let normalize =
match normalization with
| MinMax { clip; min; max } ->
diff --git a/src/main.ml b/src/main.ml
index e5f656ddeb05c85965669c6fe44ac19740a4a9cc..d2dd830e37ede69b9a78c392ae969f91795dd90c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -119,22 +119,22 @@ let timelimit_of_string s =
| [ v ], [ "h" ] -> Int.of_string v * 3600
| _ -> invalid_arg "Unrecognized time limit"
-let verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv files =
+let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files =
let debug = log_level_is_debug () in
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
List.iter
~f:
- (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit prover
- ?dataset_csv)
+ (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit
+ ?dataset prover)
files
let verify_json ?memlimit ?timelimit file =
let jc = Result.ok_exn (Verification.JSON.of_string file) in
let prover = jc.Verification.JSON.prover in
- let dataset_csv = jc.Verification.JSON.property.dataset in
+ let dataset = jc.Verification.JSON.property.dataset in
let file = Result.ok_or_failwith (Verification.File.of_json_config jc) in
- verify ~loadpath:[] ?memlimit ?timelimit prover ~dataset_csv [ file ]
+ verify ~loadpath:[] ?memlimit ?timelimit ~dataset prover [ file ]
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Command `%s'" cmdname);
@@ -215,26 +215,27 @@ let verify_cmd =
let all_provers = Prover.list_available () in
let doc =
Fmt.str
- "Prover to use. Support is provided for the following provers: %a."
+ "Prover to use. Support is provided for the following $(docv)s: %a."
(Fmt.list ~sep:Fmt.comma Fmt.string)
(List.map ~f:Prover.to_string all_provers)
in
let provers =
Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
in
- Arg.(required & opt (some provers) None & info [ "p"; "prover" ] ~doc)
+ Arg.(
+ required
+ & opt (some provers) None
+ & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
in
- let dataset_csv =
- let doc = "Dataset in CSV format." in
- Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
+ let dataset =
+ let doc = "Dataset $(docv) (CSV format only)." in
+ Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
in
Term.(
- const
- (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
+ const (fun format loadpath memlimit timelimit prover dataset files _ ->
exec_cmd cmdname (fun () ->
- verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv
- files))
- $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
+ verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files))
+ $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset $ files
$ setup_logs)
in
Cmd.v info term
diff --git a/src/verification.ml b/src/verification.ml
index 67d5630f6e52d1ac4769a4b241a687b957c1f2b5..2b5eed3642877f40ef08ca8b372a36e3279056c9 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -145,7 +145,13 @@ module File = struct
if Caml.Sys.file_exists jc.JSON.model
then
if Caml.Sys.file_exists jc.JSON.property.dataset
- then Ok (Json jc)
+ then
+ if String.is_suffix jc.JSON.property.dataset ~suffix:".csv"
+ then Ok (Json jc)
+ else
+ Error
+ (Fmt.str "file '%s' has an unsupported extension"
+ jc.property.dataset)
else Error (Fmt.str "no '%s' file or directory" jc.property.dataset)
else Error (Fmt.str "no '%s' file or directory" jc.model)
@@ -183,16 +189,21 @@ let create_env ?(debug = false) loadpath =
(loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
config )
-let answer_saver limit config env config_prover dataset_csv task =
+let answer_saver limit config env config_prover dataset task =
let dataset_predicate =
let on_model ls =
let message = Fmt.str "No SVM model found as %a" Pretty.print_ls ls in
Option.value_exn ~message (Language.lookup_loaded_svms ls)
in
let on_dataset _ls =
- match dataset_csv with
+ match dataset with
| None -> invalid_arg "No dataset provided"
- | Some filename -> filename
+ | Some filename ->
+ if String.is_suffix filename ~suffix:".csv"
+ then filename
+ else
+ invalid_arg
+ (Fmt.str "File '%s' has an unsupported extension" filename)
in
Dataset.interpret_predicate env ~on_model ~on_dataset task
in
@@ -223,8 +234,7 @@ let combine_prover_answers answers =
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
-let answer_on_dataset limit config env prover config_prover driver dataset_csv
- task =
+let answer_dataset limit config env prover config_prover driver dataset task =
let dataset_predicate =
let on_model ls =
let message =
@@ -233,10 +243,14 @@ let answer_on_dataset limit config env prover config_prover driver dataset_csv
Option.value_exn ~message (Language.lookup_loaded_nets ls)
in
let on_dataset _ls =
- let csv_in_channel = Csv.of_channel (Stdlib.open_in dataset_csv) in
- let dataset = Csv.input_all csv_in_channel in
- Csv.close_in csv_in_channel;
- dataset
+ if String.is_suffix dataset ~suffix:".csv"
+ then (
+ let csv_in_channel = Csv.of_channel (Stdlib.open_in dataset) in
+ let dataset = Csv.input_all csv_in_channel in
+ Csv.close_in csv_in_channel;
+ dataset)
+ else
+ invalid_arg (Fmt.str "File '%s' has an unsupported extension" dataset)
in
Dataset.interpret_predicate env ~on_model ~on_dataset task
in
@@ -292,15 +306,13 @@ let answer_generic limit config env prover config_prover driver task =
let prover_answer = combine_prover_answers answers in
(prover_answer, None)
-let call_prover ~limit config env prover config_prover driver dataset_csv task =
+let call_prover ?dataset ~limit config env prover config_prover driver task =
let prover_answer, additional_info =
match prover with
- | Prover.Saver ->
- answer_saver limit config env config_prover dataset_csv task
- | (Marabou | Pyrat | Nnenum) when Option.is_some dataset_csv ->
- let dataset_csv = Option.value_exn dataset_csv in
- answer_on_dataset limit config env prover config_prover driver dataset_csv
- task
+ | Prover.Saver -> answer_saver limit config env config_prover dataset task
+ | (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
+ let dataset = Option.value_exn dataset in
+ answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | CVC5 | Nnenum ->
answer_generic limit config env prover config_prover driver task
in
@@ -310,8 +322,8 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
Fmt.(option ~none:nop (any " " ++ string))
additional_info)
-let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
- ?dataset_csv file =
+let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
+ prover file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env ~debug loadpath in
let main = Whyconf.get_main config in
@@ -339,7 +351,7 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
let tasks = Task.split_theory theory None None in
let config_prover =
let altern =
- if Prover.has_vnnlib_support prover && Option.is_some dataset_csv
+ if Prover.has_vnnlib_support prover && Option.is_some dataset
then "VNNLIB"
else ""
in
@@ -360,6 +372,6 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
Driver.load_driver_absolute env file config_prover.extra_drivers
in
List.iter
- ~f:(call_prover ~limit main env prover config_prover driver dataset_csv)
+ ~f:(call_prover ?dataset ~limit main env prover config_prover driver)
tasks)
mstr_theory
diff --git a/src/verification.mli b/src/verification.mli
index 5572343a325c553d6cfcc4bfc52a63fc4cfeb585..dbe28f1e67f8c852d25fad35d32afe13666bd196 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -53,13 +53,12 @@ val verify :
loadpath:string list ->
?memlimit:int ->
?timelimit:int ->
+ ?dataset:string ->
Prover.t ->
- ?dataset_csv:string ->
File.t ->
unit
-(** [verify debug format loadpath memlimit timeout prover dataset_csv file]
- launches a verification of the given [file] with the provided [prover] and
- [dataset_csv].
+(** [verify debug format loadpath memlimit timeout dataset prover file] launches
+ a verification of the given [file] with the provided [prover] and [dataset].
@param debug when set, enables debug information.
@param format is the [file] format.
@@ -67,5 +66,6 @@ val verify :
@param memlimit
is the memory limit (in megabytes) granted to the verification.
@param timeout is the timeout (in seconds) granted to the verification.
- @param dataset_csv
- is the filepath of a dataset, in CSV format, possibly appearing in [file]. *)
+ @param dataset
+ is the filepath of a dataset (eg, in CSV format) possibly appearing in
+ [file]. *)
diff --git a/tests/dataset.t b/tests/dataset.t
index 8253dc6a32e228f035ebaea00fde0a0bd593fdd1..6f05063743d0de5e3bc175e7cf99e62f81b1da5d 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -14,7 +14,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=PyRAT --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
> use ieee_float.Float64
@@ -31,7 +31,7 @@ Test verify
[caisar] Goal G: Unknown ()
[caisar] Goal H: Unknown ()
- $ caisar verify -L . --format whyml --prover=Marabou --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
> use ieee_float.Float64
diff --git a/tests/saver.t b/tests/saver.t
index 0204152bb426908c6f58f546c22374e67788cd74..ea252a3128ecccb2549d089ba0370dda592bfd4e 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -11,7 +11,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=SAVer --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestSVM.AsArray
> use ieee_float.Float64