From d8218ba6484bed152696ed17bcd9c09b572b2178 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 23 Nov 2021 11:52:48 +0100
Subject: [PATCH] [Marabou] Just a little rework.
---
src/transformations/native_nn_prover.mli | 2 +-
src/transformations/vars_on_lhs.ml | 28 ++++++++++++------------
src/transformations/vars_on_lhs.mli | 8 +++++++
tests/marabout.t | 2 --
4 files changed, 23 insertions(+), 17 deletions(-)
create mode 100644 src/transformations/vars_on_lhs.mli
diff --git a/src/transformations/native_nn_prover.mli b/src/transformations/native_nn_prover.mli
index 65b43a80..d8ad4b12 100644
--- a/src/transformations/native_nn_prover.mli
+++ b/src/transformations/native_nn_prover.mli
@@ -5,7 +5,7 @@
(**************************************************************************)
val init : unit -> unit
-(** Register the transformations. *)
+(** Register the transformation. *)
val meta_input : Why3.Theory.meta
(** Indicate the input position. *)
diff --git a/src/transformations/vars_on_lhs.ml b/src/transformations/vars_on_lhs.ml
index b6cb6ae7..a1ac31d6 100644
--- a/src/transformations/vars_on_lhs.ml
+++ b/src/transformations/vars_on_lhs.ml
@@ -4,6 +4,8 @@
(* *)
(**************************************************************************)
+open Base
+
let make_rt env =
let open Why3 in
let th = Env.read_theory env [ "ieee_float" ] "Float64" in
@@ -21,29 +23,27 @@ let make_rt env =
({ t_node = Tconst _; _ } as const);
({ t_node = Tapp (_, []); _ } as var);
] ) ->
- Fmt.pr "HERE: %a!@." Pretty.print_term t;
+ let tt = [ var; const ] in
if Term.ls_equal ls le
- then Term.ps_app ge [ var; const ]
+ then Term.ps_app ge tt
else if Term.ls_equal ls ge
- then Term.ps_app le [ var; const ]
+ then Term.ps_app le tt
else if Term.ls_equal ls lt
- then Term.ps_app gt [ var; const ]
+ then Term.ps_app gt tt
else if Term.ls_equal ls gt
- then Term.ps_app lt [ var; const ]
+ then Term.ps_app lt tt
else t
| _ -> t
in
- 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 task =
+ List.fold [ le; lt; ge; gt ] ~init:(Task.add_ty_decl None t)
+ ~f:Task.add_param_decl
+ in
+ (rt, task)
let vars_on_lhs env =
- let rt, init = make_rt env in
- Why3.Trans.rewrite rt init
+ let rt, task = make_rt env in
+ Why3.Trans.rewrite rt task
let init () =
Why3.Trans.register_env_transform
diff --git a/src/transformations/vars_on_lhs.mli b/src/transformations/vars_on_lhs.mli
new file mode 100644
index 00000000..7914140e
--- /dev/null
+++ b/src/transformations/vars_on_lhs.mli
@@ -0,0 +1,8 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(**************************************************************************)
+
+val init : unit -> unit
+(** Register the transformation. *)
diff --git a/tests/marabout.t b/tests/marabout.t
index f2db6c2f..b05012d8 100644
--- a/tests/marabout.t
+++ b/tests/marabout.t
@@ -43,8 +43,6 @@ Test verify
<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