From 3abe106080dd7bf14f1e9a6451139e9b17fb7218 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 1 Oct 2021 15:04:24 +0200
Subject: [PATCH] Some comments.
---
config/drivers/pyrat.drv | 1 -
src/transformations.ml | 10 +++++-----
2 files changed, 5 insertions(+), 6 deletions(-)
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index e0354858..8a88c457 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -26,7 +26,6 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "introduce_premises"
-
transformation "eliminate_builtin"
transformation "simplify_formula"
transformation "caisar_native_prover"
diff --git a/src/transformations.ml b/src/transformations.ml
index 762bd9d6..99dda35a 100644
--- a/src/transformations.ml
+++ b/src/transformations.ml
@@ -18,6 +18,8 @@ let meta_output =
~desc:"Indicates the position of the output in the neural network"
[ MTlsymbol; MTint ])
+(* Retrieves the (input) variables appearing, as arguments, after an
+ 'nnet_apply' symbol. *)
let get_input_variables =
let rec aux acc (term : Why3.Term.term) =
match term.t_node with
@@ -40,6 +42,8 @@ let get_input_variables =
(fun decl acc -> Why3.Decl.decl_fold aux acc decl)
Why3.Term.Mls.empty
+(* Creates logic symbols for output variables and simplifies the formula. *)
+(* TODO: [Reduction_engine] is probably an overkill and should be replaced. *)
let simplify_goal env input_variables =
let rec aux hls (term : Why3.Term.term) =
match term.t_node with
@@ -100,11 +104,7 @@ let simplify_goal env input_variables =
None
let caisar_native_prover env =
- Why3.Trans.seq
- [
- Why3.Trans.bind get_input_variables (simplify_goal env)
- (* Why3.Simplify_formula.simplify_; *);
- ]
+ Why3.Trans.seq [ Why3.Trans.bind get_input_variables (simplify_goal env) ]
let init () =
Why3.Trans.register_env_transform
--
GitLab