From 870596db0a9b4d148b944abb48489eb12ea45eee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 17 Apr 2023 16:24:50 +0200
Subject: [PATCH] [wp] limit strategy depth
---
src/plugins/wp/ProofEngine.ml | 5 +++++
src/plugins/wp/ProofEngine.mli | 1 +
src/plugins/wp/ProverScript.ml | 12 +++++++-----
3 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index ef36ce6af08..52c83f5c4e1 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -138,6 +138,11 @@ let iteri f tree =
let k = ref 0 in
walk (fun node -> f !k node ; incr k) r
+let rec depth node =
+ match node.parent with
+ | None -> 0
+ | Some p -> depth p
+
(* -------------------------------------------------------------------------- *)
(* --- Consolidating --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 81f682d62f6..33cb4ae786c 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -73,6 +73,7 @@ val proved : node -> bool
val pending : node -> int
val stats : node -> Stats.stats
val parent : node -> node option
+val depth : node -> int
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array (* current index *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index a2696a88325..e146dc0edfb 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -374,12 +374,14 @@ and explore_fallback env process a node =
| Some s -> explore_strategie env process s node
let explore_hint env process node =
- match ProofEngine.get_hint node with
- | None -> failed
- | Some s ->
- match ProofStrategy.find s with
+ if ProofEngine.depth node > env.Env.depth then failed
+ else
+ match ProofEngine.get_hint node with
| None -> failed
- | Some s -> explore_strategie env process s node
+ | Some s ->
+ match ProofStrategy.find s with
+ | None -> failed
+ | Some s -> explore_strategie env process s node
let explore_further env process strategy node =
let marked =
--
GitLab