diff --git a/src/interpretation.ml b/src/interpretation.ml
index d5092e664ae7909df7a2f5369a358ed4a0206bff..fdbea6338da805e7dde38df603616b39c66cee9e 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -105,6 +105,8 @@ let print_caisar_op fmt caisar_env =
Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
fmt caisar_env.caisar_op_of_ls
+let _ = print_caisar_op
+
let const_real_of_float value =
let neg = Float.is_negative value in
let value = Fmt.str "%.64f" (Float.abs value) in
@@ -532,21 +534,7 @@ let interpret_task ~cwd env task =
caisar_env.caisar_op_of_ls task
in
let task = Task.(add_prop_decl task Pgoal g f) in
- Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
- f print_caisar_op caisar_env
-
-let interpret ?debug ?format ~loadpath file =
- let cwd =
- match file with
- | Verification.File.Stdin -> Unix.getcwd ()
- | File s -> Caml.Filename.dirname s
- | JSON _ -> Unix.getcwd () (*todo *)
- in
- let env, _config, mstr_theory =
- Verification.open_file ?debug ?format ~loadpath file
- in
- Wstdlib.Mstr.iter
- (fun _ theory ->
- List.iter (Task.split_theory theory None None) ~f:(fun task ->
- interpret_task ~cwd env task))
- mstr_theory
+ (* Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task)
+ Pretty.print_term *)
+ (* f print_caisar_op caisar_env; *)
+ task
diff --git a/src/interpretation.mli b/src/interpretation.mli
index 68649f274c7cb2c8bd730daad025bff68d8fb658..6252724c03c5cc06c5991f8837e27ae85ef02ccd 100644
--- a/src/interpretation.mli
+++ b/src/interpretation.mli
@@ -20,11 +20,6 @@
(* *)
(**************************************************************************)
-open Base
+open Why3
-val interpret :
- ?debug:bool ->
- ?format:string ->
- loadpath:string list ->
- Verification.File.t ->
- unit
+val interpret_task : cwd:string -> Env.env -> Task.task -> Task.task
diff --git a/src/main.ml b/src/main.ml
index 993fac062a68b99df72eea009dfcd847bf3bf907..9a5e2ed237800d781a9580a82b69e6ef50cd47f0 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -202,10 +202,6 @@ let verify_json ?memlimit ?timelimit ?outfile json =
~f:(record_verification_result jin.id verification_result)
| _ -> failwith "Unexpected more than one theory from a JSON file"
-let interpret format loadpath files =
- let debug = log_level_is_debug () in
- List.iter ~f:(Interpretation.interpret ~debug ?format ~loadpath) files
-
let verify_xgboost ?memlimit ?timelimit xgboost dataset prover =
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -362,24 +358,6 @@ let verify_json_cmd =
in
Cmd.v info term
-let interpret_cmd =
- let cmdname = "interpret" in
- let doc =
- "Interpret the goal and print the strategy that will be executed."
- in
- let info =
- Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
- ~doc
- ~man:[ `S Manpage.s_description; `P doc ]
- in
- let term =
- Term.(
- const (fun format loadpath files _ ->
- exec_cmd cmdname (fun () -> interpret format loadpath files))
- $ format $ loadpath $ files $ setup_logs)
- in
- Cmd.v info term
-
let verify_xgboost_cmd =
let cmdname = "verify-xgboost" in
let info =
@@ -456,13 +434,7 @@ let () =
let () =
try
Cmd.group ~default:default_cmd default_info
- [
- config_cmd;
- verify_cmd;
- verify_json_cmd;
- interpret_cmd;
- verify_xgboost_cmd;
- ]
+ [ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
with exn when not (log_level_is_debug ()) ->
Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/verification.ml b/src/verification.ml
index 280c22d7d2ff094147a2a1b936bbb260ffaa6e62..4e60bf6109a1c85d0aa3498f4dbc3576047ac1f9 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -247,7 +247,8 @@ let answer_generic limit config prover config_prover driver task =
let additional_info = Generic None in
(prover_answer, additional_info)
-let call_prover ?dataset ~limit config env prover config_prover driver task =
+let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
+ =
let prover_answer, additional_info =
match prover with
| Prover.Saver -> answer_saver limit config env config_prover dataset task
@@ -256,6 +257,7 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
let dataset = Unix.realpath (Option.value_exn dataset) in
answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | Nnenum ->
+ let task = Interpretation.interpret_task ~cwd env task in
let task = Proof_strategy.apply_native_nn_prover env task in
answer_generic limit config prover config_prover driver task
| CVC5 ->
@@ -265,25 +267,22 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
let id = Task.task_goal task in
{ id; prover_answer; additional_info }
-let open_file ?(debug = false) ?format ~loadpath file =
+let open_file ?format env file =
+ match file with
+ | File.Stdin ->
+ ( Unix.getcwd (),
+ Env.(read_channel ?format base_language env "stdin" Caml.stdin) )
+ | File file ->
+ let mlw_files, _ = Env.(read_file ?format base_language env file) in
+ (Caml.Filename.dirname file, mlw_files)
+ | JSON jin ->
+ let th = Json.theory_of_input env jin in
+ (Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th)
+
+let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
+ prover ?prover_altern file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env ~debug loadpath in
- let mstr_theory =
- match file with
- | File.Stdin ->
- Env.(read_channel ?format base_language env "stdin" Caml.stdin)
- | File file ->
- let mlw_files, _ = Env.(read_file ?format base_language env file) in
- mlw_files
- | JSON jin ->
- let th = Json.theory_of_input env jin in
- Wstdlib.Mstr.singleton th.th_name.id_string th
- in
- (env, config, mstr_theory)
-
-let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
- ?prover_altern file =
- let env, config, mstr_theory = open_file ?debug ?format ~loadpath file in
let main = Whyconf.get_main config in
let limit =
let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
@@ -338,10 +337,12 @@ let verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover
Driver.load_driver_file_and_extras main env file
config_prover.extra_drivers
in
+ let cwd, mstr_theory = open_file ?format env file in
Wstdlib.Mstr.map
(fun theory ->
let tasks = Task.split_theory theory None None in
List.map
- ~f:(call_prover ?dataset ~limit main env prover config_prover driver)
+ ~f:
+ (call_prover ~cwd ~limit main env prover config_prover driver ?dataset)
tasks)
mstr_theory
diff --git a/src/verification.mli b/src/verification.mli
index 82a575f331515156abf0d1a7e3445557ce42c6fc..645834243a14eae1befe979ff7e0083f3fc8656a 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -75,17 +75,5 @@ val verify :
for each theory, an [answer] for each goal of the theory, respecting the
order of appearance. *)
-val open_file :
- ?debug:bool ->
- ?format:string ->
- loadpath:string list ->
- File.t ->
- Env.env * Whyconf.config * Theory.theory Wstdlib.Mstr.t
-(** [open_file ?debug ?format ~loadpath file] just opens the given file.
-
- @param debug when set, enables debug information.
- @param format is the [file] format.
- @param loadpath is the additional loadpath. *)
-
val create_env :
?debug:bool -> string list -> Why3.Env.env * Why3.Whyconf.config