From 3a59305418c90ff59183ecc7469cbbfd5ff9f5dd Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 2 Jun 2023 11:28:30 +0200
Subject: [PATCH] [verification] Factor out code for building the prover
command.
---
src/verification.ml | 27 +++++++++++++++------------
1 file changed, 15 insertions(+), 12 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index f7c4914..77f6e2b 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -149,10 +149,19 @@ let answer_aimos limit config env config_prover dataset task =
let additional_info = Generic None in
(answer, additional_info)
-let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
-let config_re = Re__Core.(compile (str "%{config}"))
+let re_nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let re_config = Re__Core.(compile (str "%{config}"))
let config_site = List.hd_exn Dirs.Sites.config
+let build_command config_prover ~nn_filename =
+ let command = Whyconf.get_complete_command ~with_steps:false config_prover in
+ let command =
+ Re__Core.replace_string re_nnet_or_onnx
+ ~by:(Unix.realpath nn_filename)
+ command
+ in
+ Re__Core.replace_string re_config ~by:config_site command
+
let call_prover_on_task limit config command driver task =
let prover_call =
Driver.prove_task_prepared ~command ~config ~limit driver task
@@ -193,10 +202,8 @@ let answer_dataset limit config env prover config_prover driver dataset task =
Dataset.tasks_of_nn_csv_predicate env dataset_predicate
|> List.map ~f:(Driver.prepare_task driver)
in
- let command = Whyconf.get_complete_command ~with_steps:false config_prover in
let command =
- let nn_file = Unix.realpath dataset_predicate.model.filename in
- Re__Core.replace_string nnet_or_onnx ~by:nn_file command
+ build_command config_prover ~nn_filename:dataset_predicate.model.filename
in
let dataset_answers =
match prover with
@@ -231,9 +238,9 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
let answers =
List.concat_map tasks ~f:(fun task ->
let task = Driver.prepare_task driver task in
- let nn_file =
+ let nn_filename =
match Task.on_meta_excl Utils.meta_nn_filename task with
- | Some [ MAstr nn_file ] -> Unix.realpath nn_file
+ | Some [ MAstr nn_filename ] -> nn_filename
| Some _ -> assert false (* By construction of the meta. *)
| None -> invalid_arg "No neural network model found in task"
in
@@ -245,11 +252,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
| Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
| _ -> [ task ]
in
- let command =
- Whyconf.get_complete_command ~with_steps:false config_prover
- in
- let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
- let command = Re__Core.replace_string config_re ~by:config_site command in
+ let command = build_command config_prover ~nn_filename in
List.map tasks ~f:(call_prover_on_task limit config command driver))
in
let prover_answer = combine_prover_answers answers in
--
GitLab