[NN_prover] Keep only used inputs

src/transformations/native_nn_prover.ml

@@ -276,35 +276,10 @@ let abstract_nn_term env =
         let output_vars, goal = create_output_vars goal in
         let pr = Why3.Decl.create_prsymbol (Why3.Ident.id_clone pr.pr_name) in
         let decl = Why3.Decl.create_prop_decl Pgoal pr goal in
-        (* Add default lower and upper bounds for each input variable. *)
-        let task =
-          Why3.Term.Mls.fold_left
-            (fun task ls _ ->
-              let task =
-                Why3.Task.add_prop_decl task Paxiom
-                  (Why3.Decl.create_prsymbol
-                     (Why3.Ident.id_fresh "default_lower_bound"))
-                  (Why3.Term.ps_app th_float64.le
-                     [
-                       Utils.term_of_float env (-.Float.max_finite_value);
-                       Why3.Term.fs_app ls [] th_float64.ty;
-                     ])
-              in
-              let task =
-                Why3.Task.add_prop_decl task Paxiom
-                  (Why3.Decl.create_prsymbol
-                     (Why3.Ident.id_fresh "default_upper_bound"))
-                  (Why3.Term.ps_app th_float64.le
-                     [
-                       Why3.Term.fs_app ls [] th_float64.ty;
-                       Utils.term_of_float env Float.max_finite_value;
-                     ])
-              in
-              task)
-            task input_vars
-        in
-        (* Add meta for outputs. Again, for each output variable, add the meta
-           first, then its actual declaration. *)
+
+        (* Again, for each output variable, add the meta first, then its actual
+           declaration. *)
+        (* Add meta for outputs *)
         let task =
           Why3.Term.Mterm.fold_left
             (fun task _ (index, output_var) ->
@@ -320,6 +295,16 @@ let abstract_nn_term env =
             (fun acc term (index, _) -> { index; term } :: acc)
             [] output_vars
         in
+        let used_ls =
+          List.fold
+            ~f:(fun acc out ->
+              Why3.Term.t_s_fold
+                (fun acc _ -> acc)
+                (fun acc ls -> Why3.Term.Sls.add ls acc)
+                acc out.term)
+            ~init:Why3.Term.Sls.empty output_vars
+        in
+        let input_vars = Why3.Term.Sls.inter input_vars used_ls in
         let _, input_vars =
           Why3.Term.Mls.mapi_fold (fun _ () i -> (i + 1, i)) input_vars 0
         in