[NN_prover] use the same output for the same term

src/transformations/native_nn_prover.ml

@@ -177,12 +177,10 @@ let create_new_nn env input_vars outputs : string =
         m "Why3 term to IR (impossible?): %a" Why3.Pretty.print_term term)
   in
 
-  let r = ref (List.length outputs) in
   let outputs =
-    List.rev_map outputs ~f:(fun o ->
-      Int.decr r;
-      assert (!r = o.index);
-      convert_term o.term)
+    List.rev_map outputs ~f:(fun { index; term } -> (index, convert_term term))
+    |> List.sort ~compare:(fun (i, _) (j, _) -> Int.compare i j)
+    |> List.map ~f:snd
   in
   let output = IR.Node.create (Concat { inputs = outputs; axis = 0 }) in
   assert (
@@ -230,15 +228,22 @@ let abstract_nn_term env =
   let th_model = Symbols.Model.create env in
   let th_nn = Symbols.NN.create env in
   let th_float64 = Symbols.Float64.create env in
-  let rec do_simplify (new_index, output_vars) term =
+  let rec do_simplify ((new_index, output_vars) as acc) term =
     if heuristic th_model th_nn term
     then
-      let ls =
-        Why3.(Term.create_fsymbol (Ident.id_fresh "y") [] th_float64.ty)
+      let acc, ls =
+        match Why3.Term.Mterm.find_opt term output_vars with
+        | None ->
+          let ls =
+            Why3.(Term.create_fsymbol (Ident.id_fresh "y") [] th_float64.ty)
+          in
+          ( (new_index + 1, Why3.Term.Mterm.add term (new_index, ls) output_vars),
+            ls )
+        | Some (_, ls) -> (acc, ls)
       in
       let term' = Why3.Term.fs_app ls [] th_float64.ty in
-      ((new_index + 1, ({ index = new_index; term }, ls) :: output_vars), term')
-    else Why3.Term.t_map_fold do_simplify (new_index, output_vars) term
+      (acc, term')
+    else Why3.Term.t_map_fold do_simplify acc term
   in
   Why3.Trans.fold_map
     (fun task_hd (((index, input_vars) as acc), task) ->
@@ -275,7 +280,9 @@ let abstract_nn_term env =
         let input_vars = Why3.Term.Mls.add ls index input_vars in
         ((index, input_vars), task)
       | Decl { d_node = Dprop (Pgoal, pr, goal); _ } ->
-        let (_, output_vars), goal = do_simplify (0, []) goal in
+        let (_, output_vars), goal =
+          do_simplify (0, Why3.Term.Mterm.empty) 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
 
@@ -288,17 +295,21 @@ let abstract_nn_term env =
 
         (* Add meta for outputs *)
         let task =
-          List.fold output_vars ~init:task
-            ~f:(fun task ({ index; _ }, output_var) ->
-            let task =
-              Why3.Task.add_meta task Meta.meta_output
-                [ MAls output_var; MAint index ]
-            in
-            Why3.Task.add_param_decl task output_var)
+          Why3.Term.Mterm.fold_left
+            (fun task _ (index, output_var) ->
+              let task =
+                Why3.Task.add_meta task Meta.meta_output
+                  [ MAls output_var; MAint index ]
+              in
+              Why3.Task.add_param_decl task output_var)
+            task output_vars
         in
-        let nn_filename =
-          create_new_nn env input_vars (List.map ~f:fst output_vars)
+        let output_vars =
+          Why3.Term.Mterm.fold_left
+            (fun acc term (index, _) -> { index; term } :: acc)
+            [] output_vars
         in
+        let nn_filename = create_new_nn env input_vars output_vars in
         let task =
           Why3.Task.add_meta task Meta.meta_nn_filename [ MAstr nn_filename ]
         in

tests/acasxu.t

@@ -269,7 +269,7 @@ Test verify on acasxu
   55947.6909999999988940544426441192626953125 <= x1
   1145.0 <= x4
   x5 <= 60.0
-  y0 <= y1 and y2 <= y3
+  y0 <= y1 and y1 <= y0
   
   [DEBUG]{InterpretGoal} Interpreted formula for goal 'run3'vc':
   forall x:t, x1:t, x2:t, x3:t, x4:t, eps:t.
@@ -345,7 +345,7 @@ Test verify on acasxu
   x5 <= 60.0
   -1.0 <= x6
   x6 <= 1.0
-  y0 <= y1 and y2 <= y3
+  y0 <= y1 and y1 <= y0
   
   [DEBUG]{InterpretGoal} Interpreted formula for goal 'test'vc':
   forall x:t, x1:t, x2:t, x3:t, x4:t.
@@ -565,12 +565,6 @@ Test verify on acasxu
   (assert (>= X_4 1145.0))
   (assert (<= X_5 60.0))
   
-  ;; Y_3
-  (declare-const Y_3 Real)
-  
-  ;; Y_2
-  (declare-const Y_2 Real)
-  
   ;; Y_1
   (declare-const Y_1 Real)
   
@@ -579,7 +573,7 @@ Test verify on acasxu
   
   ;; Goal run2'vc
   (assert (or (and (>= Y_0 Y_1))
-              (and (>= Y_2 Y_3))
+              (and (>= Y_1 Y_0))
               ))
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
@@ -629,21 +623,15 @@ Test verify on acasxu
   ;; H
   (assert (<= X_6 1.0))
   
-  ;; Y_3
-  (declare-const Y_3 Real)
-  
-  ;; Y_2
-  (declare-const Y_2 Real)
+  ;; Y_0
+  (declare-const Y_0 Real)
   
   ;; Y_1
   (declare-const Y_1 Real)
   
-  ;; Y_0
-  (declare-const Y_0 Real)
-  
   ;; Goal run3'vc
   (assert (or (and (>= Y_0 Y_1))
-              (and (>= Y_2 Y_3))
+              (and (>= Y_1 Y_0))
               ))
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
@@ -833,7 +821,7 @@ Test verify on acasxu
   x1 >= 55947.6909999999988940544426441192626953125
   x4 >= 1145.0
   x5 <= 60.0
-  +y2 -y3 >= 0
+  +y1 -y0 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x1 >= 0.0
@@ -869,7 +857,7 @@ Test verify on acasxu
   x5 <= 60.0
   x6 >= -1.0
   x6 <= 1.0
-  +y2 -y3 >= 0
+  +y1 -y0 >= 0
   
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x1 >= 0.0