[Marabou] Just a little rework.

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. *)

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

src/transformations/vars_on_lhs.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val init : unit -> unit
+(** Register the transformation. *)

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.+