From 1ca1654688b44bc72a569ef51a7ca260797a874c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 9 Apr 2024 17:46:10 +0200
Subject: [PATCH] [NN_solver] Add metas for input just before goal
---
src/transformations/native_nn_prover.ml | 27 ++++++++++++++++---------
1 file changed, 17 insertions(+), 10 deletions(-)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 2164500..f8e4730 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -246,7 +246,7 @@ let abstract_nn_term env =
(output_vars, term)
in
Why3.Trans.fold_map
- (fun task_hd (((index, input_vars) as acc), task) ->
+ (fun task_hd ((input_vars as acc), task) ->
let tdecl = task_hd.task_decl in
match tdecl.td_node with
| Decl { d_node = Dparam ls; _ } when Language.mem_nn ls ->
@@ -269,15 +269,9 @@ let abstract_nn_term env =
_;
}
when Why3.Ty.ty_equal ty th_float64.ty ->
- (* Add meta for input variable declarations. Each meta needs to appear
- before the corresponding declaration in order to be leveraged by
- prover printers. *)
- let task =
- Why3.Task.add_meta task Meta.meta_input [ MAls ls; MAint index ]
- in
let task = Why3.Task.add_tdecl task tdecl in
- let input_vars = Why3.Term.Mls.add ls index input_vars in
- ((index + 1, input_vars), task)
+ let input_vars = Why3.Term.Sls.add ls input_vars in
+ (input_vars, task)
| Decl { d_node = Dprop (Pgoal, pr, goal); _ } ->
let output_vars, goal = create_output_vars goal in
let pr = Why3.Decl.create_prsymbol (Why3.Ident.id_clone pr.pr_name) in
@@ -326,6 +320,19 @@ let abstract_nn_term env =
(fun acc term (index, _) -> { index; term } :: acc)
[] output_vars
in
+ let _, input_vars =
+ Why3.Term.Mls.mapi_fold (fun _ () i -> (i + 1, i)) input_vars 0
+ in
+ (* Add meta for input variable declarations. Each meta needs to appear
+ before the corresponding declaration in order to be leveraged by
+ prover printers. *)
+ let task =
+ Why3.Term.Mls.fold_left
+ (fun task ls index ->
+ Why3.Task.add_meta task Meta.meta_input [ MAls ls; MAint index ])
+ task input_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 ]
@@ -335,7 +342,7 @@ let abstract_nn_term env =
(* TODO: check no nn applications *)
(acc, Why3.Task.add_tdecl task tdecl)
| _ -> (acc, Why3.Task.add_tdecl task tdecl))
- (0, Why3.Term.Mls.empty) None
+ Why3.Term.Sls.empty None
(** {2 Old way} *)
--
GitLab