From a4fbc543e5216d8e35e529e23fc5bb5e4e3068ab Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 4 Feb 2021 16:14:42 +0100
Subject: [PATCH] Consider raw options as a string list rather than a mere
string.
---
main.ml | 5 +++--
solver.ml | 56 ++++++++++++++++++++++++++----------------------------
solver.mli | 4 ++--
3 files changed, 32 insertions(+), 33 deletions(-)
diff --git a/main.ml b/main.ml
index 1384273..c4f1cb2 100644
--- a/main.ml
+++ b/main.ml
@@ -67,7 +67,7 @@ let verify cmd raw_options config_file model property solver () =
Model.build ~filename:model >>= fun model ->
Property.build ~filename:property >>= fun property ->
Solver.get_config solver ~file:config_file >>= fun config ->
- Solver.exec ?raw_options config model property
+ Solver.exec ~raw_options config model property
in
match do_verify () with
| Ok () -> Logs.app (fun m -> m "Done.")
@@ -144,7 +144,8 @@ let verify_cmd =
in
let solver_raw_options =
let doc = "Additional options provided to the solver." in
- Arg.(value & opt (some string) None & info ["raw"; "raw-options"] ~doc)
+ Arg.(value & opt (list ~sep:' ' string) []
+ & info ["raw"; "raw-options"] ~doc)
in
let config_filename =
let doc = "$(b,FILE) to read the configuration from." in
diff --git a/solver.ml b/solver.ml
index 5078ddb..e5c03ae 100644
--- a/solver.ml
+++ b/solver.ml
@@ -286,7 +286,7 @@ let check_compatibility config model =
| _ ->
Ok ()
-let build_command ?raw_options confg_solver property model =
+let build_command ~raw_options confg_solver property model =
let module Filename = Caml.Filename in
let open Result in
let solver = confg_solver.solver in
@@ -307,46 +307,44 @@ let build_command ?raw_options confg_solver property model =
(* Build actual command-line. *)
try
let cmd =
- let raw_options = Option.to_list raw_options in
let exe = confg_solver.exe in
- match solver with
- | Pyrat ->
- let verbose =
- match Logs.level () with
- | None | Some (App | Error | Warning) -> false
- | Some (Info | Debug) -> true
- in
- Filename.quote_command
- exe
- (model.Model.filename ::
- prop ::
- if verbose then "--verbose" :: raw_options else raw_options)
- | Marabou ->
- let verbosity_level =
- match Logs.level () with
- | None | Some (App | Error | Warning) -> 0
- | Some Info -> 1
- | Some Debug -> 2
- in
- Filename.quote_command
- exe
- ("--property" :: prop ::
- "--input" :: model.Model.filename ::
- "--verbosity" :: Int.to_string verbosity_level ::
- raw_options)
+ let args =
+ match solver with
+ | Pyrat ->
+ let verbose =
+ match Logs.level () with
+ | None | Some (App | Error | Warning) -> false
+ | Some (Info | Debug) -> true
+ in
+ model.Model.filename ::
+ prop ::
+ if verbose then "--verbose" :: raw_options else raw_options
+ | Marabou ->
+ let verbosity_level =
+ match Logs.level () with
+ | None | Some (App | Error | Warning) -> 0
+ | Some Info -> 1
+ | Some Debug -> 2
+ in
+ "--property" :: prop ::
+ "--input" :: model.Model.filename ::
+ "--verbosity" :: Int.to_string verbosity_level ::
+ raw_options
+ in
+ Filename.quote_command exe args
in
Ok (prop, cmd)
with Failure e ->
Error (Format.sprintf "Unexpected failure@ `%s'." e)
-let exec ?raw_options config model property =
+let exec ~raw_options config model property =
let open Result in
(* Check solver availability. *)
check_availability config >>= fun () ->
(* Check solver and model compatibility. *)
check_compatibility config model >>= fun () ->
(* Build the required command-line. *)
- build_command ?raw_options config property model >>= fun (tmp, cmd) ->
+ build_command ~raw_options config property model >>= fun (tmp, cmd) ->
(* Execute the command. *)
begin
try
diff --git a/solver.mli b/solver.mli
index cc4aaae..6a70c6a 100644
--- a/solver.mli
+++ b/solver.mli
@@ -23,9 +23,9 @@ type config
the given [file]. *)
val get_config: file:string -> solver -> (config, string) Result.t
-(** [exec ?raw_options config model property] runs a solver wrt the given
+(** [exec ~raw_options config model property] runs a solver wrt the given
[config] on [property] for [model] with the provided [raw_options], if any.
*)
val exec:
- ?raw_options:string ->
+ raw_options:string list ->
config -> Model.t -> Property.t -> (unit, string) Result.t
--
GitLab