From 0d77531b3edf95120cf9d412f2d2b0793912558d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 29 May 2019 14:04:16 +0200
Subject: [PATCH] [qed] cache acceleration and pruning
---
src/plugins/qed/logic.ml | 2 ++
src/plugins/qed/term.ml | 16 +++++++++++-----
src/plugins/wp/Lang.ml | 3 +--
src/plugins/wp/wpo.ml | 19 +++++++------------
4 files changed, 21 insertions(+), 19 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 5a29bdd6166..94ce3aa7a62 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -323,6 +323,8 @@ sig
sig
type t = sigma
val create : ?pool:pool -> unit -> t
+
+ val cache : sigma -> term cache
val fresh : t -> tau -> var
val get : t -> term -> term
val filter : t -> term -> bool
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index f7e80b8320e..c3df0e1d46e 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2087,6 +2087,11 @@ struct
filter = [] ;
}
+ let cache sigma =
+ ref begin
+ match sigma.shared with MAP( m , _ ) -> m | _ -> Tmap.empty
+ end
+
let fresh sigma t = fresh sigma.pool t
let rec compute e = function
@@ -2124,15 +2129,16 @@ struct
let sigma = Subst.create
+ let filter sigma e =
+ Subst.filter sigma e || not (Bvars.is_empty e.bind)
+
let rec subst sigma alpha e =
- if Subst.filter sigma e then
- let mu = cache () in
- let v = compute mu sigma alpha e in
- set mu e v ; v
+ if filter sigma e then
+ incache (Subst.cache sigma) sigma alpha e
else e
and incache mu sigma alpha e =
- if Subst.filter sigma e then
+ if filter sigma e then
get mu (compute mu sigma alpha) e
else e
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index b0a2fcc1801..21e9a0e9e71 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -922,8 +922,7 @@ let alpha () =
match F.repr e with
| Fvar x -> lookup e x
| _ -> raise Not_found in
- F.Subst.add_fun sigma compute ;
- sigma
+ F.Subst.add_fun sigma compute ; sigma
let subst xs vs =
let bind w x v = Tmap.add (e_var x) v w in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index fedd25bd69d..9516c35ee35 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -227,18 +227,13 @@ struct
let safecompute g =
begin
- try
- g.simplified <- true ;
- let timer = ref 0.0 in
- Wp_parameters.debug ~dkey "Simplify goal" ;
- Command.time ~rmax:timer preprocess g ;
- Wp_parameters.debug ~dkey "Simplification time: %a"
- Rformat.pp_time !timer ;
- g.time <- !timer ;
- with e ->
- Format.eprintf "PREPROCESS ERROR(%s)@."
- (Printexc.to_string e) ;
- assert false
+ g.simplified <- true ;
+ let timer = ref 0.0 in
+ Wp_parameters.debug ~dkey "Simplify goal" ;
+ Command.time ~rmax:timer preprocess g ;
+ Wp_parameters.debug ~dkey "Simplification time: %a"
+ Rformat.pp_time !timer ;
+ g.time <- !timer ;
end
let compute g =
--
GitLab