From be1e8f0175bff88b413a77a888a849c6e93b50e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 13 Apr 2023 19:08:26 +0200
Subject: [PATCH] [wp] proof strategy
---
src/plugins/wp/ProofStrategy.ml | 9 ++++
src/plugins/wp/ProofStrategy.mli | 1 +
src/plugins/wp/ProverScript.ml | 84 +++++++++++++++++++++++++++++++-
3 files changed, 92 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 9112e292372..6498a2dae7c 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -301,6 +301,15 @@ let fallback = function
| Strategy s -> resolve s
| Tactic _ | Auto _ | Provers _ -> None
+let auto = function
+ | Strategy _ | Tactic _ | Provers _ -> None
+ | Auto s ->
+ match Strategy.lookup ~id:s.value with
+ | exception Not_found ->
+ Wp_parameters.error ~source:(fst s.loc) ~once:true
+ "Auto-Strategy '%s' not found (skipped)." s.value ; None
+ | h -> Some h
+
(* -------------------------------------------------------------------------- *)
(* --- Strategy Tactical Step --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofStrategy.mli b/src/plugins/wp/ProofStrategy.mli
index ea8b19ec6ac..c9d50c46ee4 100644
--- a/src/plugins/wp/ProofStrategy.mli
+++ b/src/plugins/wp/ProofStrategy.mli
@@ -35,6 +35,7 @@ val hints : WpPropId.prop_id -> strategy list
val alternatives : strategy -> alternative list
val provers : alternative -> VCS.prover list * float
+val auto : alternative -> Strategy.heuristic option
val fallback : alternative -> strategy option
val tactic : tree -> node -> strategy -> alternative -> node list option
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 623583773bc..a2696a88325 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -317,7 +317,87 @@ and autofork env ~depth fork =
(* --- Proof Strategy Alternatives --- *)
(* -------------------------------------------------------------------------- *)
-(*TODO*)
+type solver = ProofEngine.node -> bool Task.task
+
+let success = Task.return true
+let failed = Task.return false
+let unknown : solver = fun _ -> failed
+
+let (+>>) (a : solver) (b : solver) : solver =
+ fun node -> a node >>= fun ok -> if ok then success else b node
+
+let rec sequence (f : 'a -> solver) = function
+ | [] -> unknown
+ | x::xs -> f x +>> sequence f xs
+
+let rec explore_strategie env p s : solver =
+ sequence
+ (explore_alternative env p s)
+ (ProofStrategy.alternatives s)
+
+and explore_alternative env p s a : solver =
+ explore_provers env a +>>
+ explore_tactic env p s a +>>
+ explore_auto env p a +>>
+ explore_fallback env p a
+
+and explore_provers env a : solver =
+ let provers,timeout = ProofStrategy.provers a in
+ sequence (explore_prover env timeout) provers
+
+and explore_prover env timeout prover node =
+ let wpo = ProofEngine.goal node in
+ let result = Wpo.get_result wpo prover in
+ if VCS.is_valid result then success else
+ if VCS.is_verdict result then failed else
+ let config = { VCS.default with timeout = Some timeout } in
+ Env.prove env wpo ~config prover
+
+and explore_tactic env process s a node =
+ match ProofStrategy.tactic env.tree node s a with
+ | None -> failed
+ | Some nodes -> List.iter process nodes ; success
+
+and explore_auto env process a node =
+ match ProofStrategy.auto a with
+ | None -> failed
+ | Some h ->
+ match ProverSearch.search env.tree ~anchor:node [h] with
+ | None -> failed
+ | Some fork ->
+ List.iter (fun (_,node) -> process node) @@
+ snd @@ ProofEngine.commit fork ; success
+
+and explore_fallback env process a node =
+ match ProofStrategy.fallback a with
+ | None -> failed
+ | 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
+ | None -> failed
+ | Some s -> explore_strategie env process s node
+
+let explore_further env process strategy node =
+ let marked =
+ match ProofEngine.get_hint node with
+ | None -> false
+ | Some s -> ProofStrategy.name strategy = s
+ in if marked then failed else explore_strategie env process strategy node
+
+let explore_further_hints env process =
+ let wpo = ProofEngine.main env.Env.tree in
+ sequence (explore_further env process) (ProofStrategy.hints wpo.po_pid)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Automated Solving --- *)
+(* -------------------------------------------------------------------------- *)
+
+let automated env process : solver =
+ auto env +>> explore_hint env process +>> explore_further_hints env process
(* -------------------------------------------------------------------------- *)
(* --- Apply Script Tactic --- *)
@@ -342,7 +422,7 @@ let rec crawl env on_child node = function
| [] ->
let node = ProofEngine.anchor (Env.tree env) ?node () in
- auto env node >>= fun ok ->
+ automated env on_child node >>= fun ok ->
if ok then Env.validate env else Env.stuck env ;
Task.return ()
--
GitLab