From 1d0efd9950b4b578b4a7d248b4c897cb35edf603 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 5 Jun 2023 12:44:00 +0200
Subject: [PATCH] [aimos] Do not log specification information for AIMOS.
---
src/aimos.ml | 3 ---
tests/aimos.t | 26 --------------------------
2 files changed, 29 deletions(-)
diff --git a/src/aimos.ml b/src/aimos.ml
index e6a8a1c..f51a3b1 100644
--- a/src/aimos.ml
+++ b/src/aimos.ml
@@ -94,9 +94,6 @@ let build_command config_prover
amplitude
in
let command = Whyconf.get_complete_command ~with_steps:false config_prover in
- Logs.info (fun m ->
- m "@[Specification to verify:\n%s@]"
- (Stdio.In_channel.read_all (Unix.realpath aimos_config)));
Re__Core.replace_string re_aimos_file ~by:aimos_config command
let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
diff --git a/tests/aimos.t b/tests/aimos.t
index 86a8fdc..1d53b28 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -23,29 +23,3 @@ Test verify
> end
> EOF
[caisar] Goal G: Valid
-
- $ cat >> test <<EOF
- > theory AIMOS_oracle
- > use TestNetwork.AsArray
- > use ieee_float.Float64
- > use caisar.DatasetClassification
- > use caisar.DatasetClassificationProps
- >
- > 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 --log-category=specification 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] Specification to verify:
- options:
- plot: false
- inputs_path: $TESTCASE_ROOT/test_data.csv
- transformations:
- - name: reluplex_rotation
- custom_t_path: config/custom_transformations.py
- models:
- - defaults:
- models_path: _build/default/tests/TestNetwork.nnet
- out_mode: classif_min
-
- [caisar][INFO] Verification results for theory 'AIMOS_oracle'
- [caisar] Goal G: Valid
--
GitLab