From 32cdffef2d9ec9113379c2e256c903bd3983aa02 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 25 May 2023 17:45:59 +0200
Subject: [PATCH] [tests] Relative model paths for AIMOS oracle
---
src/verification.ml | 10 +++++-----
tests/aimos.t | 5 +++--
tests/pyrat_onnx.t | 2 +-
3 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 415a0f2..1600b75 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -162,7 +162,12 @@ let build_command config_prover ~nn_filename =
in
Re__Core.replace_string re_config ~by:config_site command
+let log_prover_task driver task =
+ let print fm = ignore (Driver.print_task_prepared driver fm task) in
+ Logs.info (fun m -> m "@[Task sent to prover:\n%t@]" print)
+
let call_prover_on_task limit config command driver task =
+ log_prover_task driver task;
let prover_call =
Driver.prove_task_prepared ~command ~config ~limit driver task
in
@@ -175,10 +180,6 @@ let combine_prover_answers answers =
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
-let print_prover_task driver task =
- let print fm = ignore (Driver.print_task_prepared driver fm task) in
- Logs.info (fun m -> m "@[Task sent to prover:\n%t@]" print)
-
(* TODO: does printing the task means printing the csv here?*)
let answer_dataset limit config env prover config_prover driver dataset task =
let dataset_predicate =
@@ -261,7 +262,6 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
List.map tasks ~f:(call_prover_on_task limit config command driver))
in
let prover_answer = combine_prover_answers answers in
- List.iter ~f:(fun t -> print_prover_task driver t) tasks;
let additional_info = Generic None in
(prover_answer, additional_info)
diff --git a/tests/aimos.t b/tests/aimos.t
index 5d318b9..fd7f573 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -24,7 +24,7 @@ Test verify
> EOF
[caisar] Goal G: Valid
- $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv --verbosity=info - 2>&1 <<EOF
+ $ cat >> test <<EOF
> theory AIMOS_oracle
> use TestNetwork.AsArray
> use ieee_float.Float64
@@ -34,6 +34,7 @@ Test verify
> goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
> end
> EOF
+ $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv --verbosity=info test 2>&1 | awk '{if ($1 =="models_path:") {n=split ($2,a,"/");print " "$1" "a[n-3]"/"a[n-2]"/"a[n-1]"/"a[n];} else print $0}'
[caisar][INFO] Task sent to prover:
options:
plot: false
@@ -43,7 +44,7 @@ Test verify
custom_t_path: config/custom_transformations.py
models:
- defaults:
- models_path: /home/julien/LAISER/CAISAR/caisar/_build/default/tests/TestNetwork.nnet
+ models_path: _build/default/tests/TestNetwork.nnet
out_mode: classif_min
[caisar][INFO] Verification results for theory 'AIMOS_oracle'
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 280fd97..8b65e02 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -27,5 +27,5 @@ Test verify
0.0 < x0
x0 < 0.5
0.0 < y0 and y0 < 0.5
- [caisar][INFO] Verification results for theory 'T'
+ [caisar][INFO] Verification results for theory 'PyRAT_ONNX'
[caisar] Goal G: Unknown ()
--
GitLab