From c558828a6cf86dcb83dca86039654f67c7becfad Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 4 Oct 2022 15:21:19 +0200
Subject: [PATCH] Automatic application of actual_net_apply transform for CVC5.
---
src/prover.mli | 2 +-
src/transformations/actual_net_apply.mli | 4 ++++
src/verification.ml | 9 +++++----
3 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/src/prover.mli b/src/prover.mli
index 2d0dba9..cf4ff02 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-type t = private Marabou | Pyrat | Saver
+type t = private Marabou | Pyrat | Saver | CVC5
val list_available : unit -> t list
val of_string : string -> t option
diff --git a/src/transformations/actual_net_apply.mli b/src/transformations/actual_net_apply.mli
index f4c6a6b..e45ca3e 100644
--- a/src/transformations/actual_net_apply.mli
+++ b/src/transformations/actual_net_apply.mli
@@ -14,5 +14,9 @@
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 4e26a9a..d0e5f1a 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -93,13 +93,14 @@ 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 =
+let answer_generic limit config prover config_prover driver task env =
let task_prepared = Driver.prepare_task driver task in
let tasks =
- (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
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
@@ -128,8 +129,8 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
match prover with
| Prover.Saver ->
answer_saver limit config env config_prover dataset_csv task
- | Marabou | Pyrat ->
- answer_generic limit config prover config_prover driver task
+ | Marabou | Pyrat | CVC5 ->
+ answer_generic limit config prover config_prover driver task env
in
Logs.app (fun m ->
m "@[Goal %a:@ %a%a@]" Pretty.print_pr (Task.task_goal task)
--
GitLab