From 34ef77458c2135597a338f066d50e109c2977c53 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 23 Nov 2021 11:22:38 +0100
Subject: [PATCH] [Marabou] Introduce the used symbol in the initial task
---
src/transformations/vars_on_lhs.ml | 13 ++++++--
tests/marabout.t | 51 ++++++++++++++++++++++++++++++
2 files changed, 61 insertions(+), 3 deletions(-)
create mode 100644 tests/marabout.t
diff --git a/src/transformations/vars_on_lhs.ml b/src/transformations/vars_on_lhs.ml
index 021ac66a..b6cb6ae7 100644
--- a/src/transformations/vars_on_lhs.ml
+++ b/src/transformations/vars_on_lhs.ml
@@ -7,6 +7,7 @@
let make_rt env =
let open Why3 in
let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+ let t = Theory.ns_find_ts th.th_export [ "t" ] in
let le = Theory.ns_find_ls th.th_export [ "le" ] in
let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
let ge = Theory.ns_find_ls th.th_export [ "ge" ] in
@@ -32,11 +33,17 @@ let make_rt env =
else t
| _ -> t
in
- rt
+ let init = None in
+ let init = Task.add_ty_decl init t in
+ let init = Task.add_param_decl init le in
+ let init = Task.add_param_decl init lt in
+ let init = Task.add_param_decl init ge in
+ let init = Task.add_param_decl init gt in
+ (rt, init)
let vars_on_lhs env =
- let rt = make_rt env in
- Why3.Trans.rewrite rt None
+ let rt, init = make_rt env in
+ Why3.Trans.rewrite rt init
let init () =
Why3.Trans.register_env_transform
diff --git a/tests/marabout.t b/tests/marabout.t
new file mode 100644
index 00000000..f2db6c2f
--- /dev/null
+++ b/tests/marabout.t
@@ -0,0 +1,51 @@
+Test verify
+ $ cat - > bin/alt-ergo << EOF
+ > #!/bin/sh
+ > echo "2.4.0"
+ > EOF
+
+ $ cat - > bin/Marabou << EOF
+ > #!/bin/sh
+ > echo "1.0.+"
+ > EOF
+
+ $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+
+ $ bin/alt-ergo
+ 2.4.0
+
+ $ bin/pyrat.py --version
+ PyRAT 1.1
+
+ $ bin/Marabou
+ 1.0.+
+
+ $ PATH=$(pwd)/bin:$PATH
+
+ $ caisar verify -L . --format whyml --prover=Marabou - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+ > theory T
+ > use TestNetwork.AsTuple
+ > use ieee_float.Float64
+ > use caisar.NNet
+ >
+ > goal G: forall x1 x2 x3 x4 x5.
+ > (0.0:t) .< x1 .< (0.5:t) ->
+ > let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+ > (0.0:t) .< y1 .< (0.5:t)
+ > end
+ > EOF
+ <autodetect>0 prover(s) added
+ <autodetect>Generating strategies:
+ <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
+ <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+ <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
+ <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+ <autodetect>Found prover Marabou version 1.0.+, OK.
+ <autodetect>Found prover PyRAT version 1.1, OK.
+ <autodetect>3 prover(s) added
+ HERE: lt (0.0:t) x1!
+ HERE: lt (0.0:t) y!
+ Goal G: High failure
+ Output:
+ 1.0.+
+
--
GitLab