Added meta nn filename for compatibility.

src/transformations/actual_net_apply.ml

@@ -6,6 +6,7 @@
 
 open Why3
 open Base
+open Utils
 module IR = Ir.Nier_cfg
 module G = Onnx.G
 
@@ -307,12 +308,13 @@ let terms_of_nier g ty_inputs env ~net_output_vars ~net_input_vars =
 (* Create logic symbols for input variables and replace
  * nnet_apply by control flow terms. *)
 let actual_nn_flow env =
-  let rec substitute_net_apply (term : Term.term) =
+  let rec substitute_net_apply meta (term : Term.term) =
     match term.t_node with
     | Term.Tapp (ls, args) -> (
       match Language.lookup_loaded_nets ls with
-      | None -> Term.t_map substitute_net_apply term
+      | None -> Term.t_map (substitute_net_apply meta) term
       | Some nn ->
+        meta := nn.filename :: !meta;
         let g =
           match nn.nier with
           | Some g -> g
@@ -333,24 +335,26 @@ let actual_nn_flow env =
               ]
             ~net_input_vars
         in
-        Stdio.printf "\nObtained term: \n%!";
-        Pretty.print_term Fmt.stdout cfg_term;
-        Stdio.printf "\n%!";
         cfg_term)
-    | _ -> Term.t_map substitute_net_apply term
+    | _ -> Term.t_map (substitute_net_apply meta) term
   in
   Trans.fold
     (fun task_hd task ->
       match task_hd.task_decl.td_node with
       | Use _ | Clone _ | Meta _ -> Task.add_tdecl task task_hd.task_decl
       | Decl decl ->
+        let meta = ref [] in
         let decl =
           Decl.decl_map
             (fun term ->
-              let term = substitute_net_apply term in
+              let term = substitute_net_apply meta term in
               term)
             decl
         in
+        let task =
+          List.fold !meta ~init:task ~f:(fun task s ->
+            Task.add_meta task meta_nn_filename [ MAstr s ])
+        in
         Task.add_decl task decl)
     None