From 5f9852f86fce293c63b90fef6a28e83464ad84fc Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 10 Oct 2022 16:44:57 +0200
Subject: [PATCH] Remove manually applied transformation for inlining net_apply
as not actually useful.
The driver seems to do the job already.
---
src/transformations/actual_net_apply.mli | 4 ----
src/verification.ml | 6 ++----
2 files changed, 2 insertions(+), 8 deletions(-)
diff --git a/src/transformations/actual_net_apply.mli b/src/transformations/actual_net_apply.mli
index e45ca3e..f4c6a6b 100644
--- a/src/transformations/actual_net_apply.mli
+++ b/src/transformations/actual_net_apply.mli
@@ -14,9 +14,5 @@
are stored inside of an environment, their shape being either provided by
the NIER or inferred with the expected result of ONNX operations. *)
-open Why3
-
-val actual_net_apply : Env.env -> Task.task Trans.trans
-
val init : unit -> unit
(** Register the transformation. *)
diff --git a/src/verification.ml b/src/verification.ml
index d0e5f1a..2541404 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -93,14 +93,12 @@ let answer_saver limit config env config_prover dataset_csv task =
let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in
(prover_answer, Some additional_info)
-let answer_generic limit config prover config_prover driver task env =
+let answer_generic limit config prover config_prover driver task =
let task_prepared = Driver.prepare_task driver task in
let tasks =
match prover with
| Prover.Marabou -> Trans.apply Split.split_all task_prepared
| Pyrat -> Trans.apply Split.split_premises task_prepared
- | Prover.CVC5 ->
- [ Trans.apply (Actual_net_apply.actual_net_apply env) task_prepared ]
| _ -> [ task_prepared ]
in
let command = Whyconf.get_complete_command ~with_steps:false config_prover in
@@ -130,7 +128,7 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
| Prover.Saver ->
answer_saver limit config env config_prover dataset_csv task
| Marabou | Pyrat | CVC5 ->
- answer_generic limit config prover config_prover driver task env
+ answer_generic limit config prover config_prover driver task
in
Logs.app (fun m ->
m "@[Goal %a:@ %a%a@]" Pretty.print_pr (Task.task_goal task)
--
GitLab