From e24db71afbd7608bd35df809f9b952cc3439ad0c Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 12 Jan 2022 17:57:07 +0100
Subject: [PATCH] [WP] adds an improvement of the simplifier for eq_sequence
---
src/plugins/wp/Vlist.ml | 9 ++++++++-
src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle | 2 +-
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 3bc7f2de47a..157732e62ae 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -195,7 +195,14 @@ let rec leftmost a ms =
| L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat -> begin
let exception RetryOnUnfold in
try (* tries to perform some rolling that do not depend on [n] *)
- raise RetryOnUnfold
+ match ms with
+ | b::ms ->
+ let b,ms = leftmost b ms in
+ let u,us = leftmost u [] in
+ if not (F.decide (F.e_eq u b)) then raise RetryOnUnfold;
+ (* u=b ==> ((u^us)*^n) ^ b ^ ms == u ^ (us^b)*^n) ^ ms *)
+ u, v_repeat (v_concat (us@[b]) (F.typeof a)) n :: ms
+ | _ -> raise RetryOnUnfold
with RetryOnUnfold ->
if F.decide (F.e_lt F.e_zero n) then
(* 0<n ==> (u*^n) ^ ms == u ^ (u*^(n-1)) ^ ms *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
index 1a8f5dc954a..44d15eeb682 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -33,7 +33,7 @@ Prove: (0<=k_0) -> (k_0<(3*(length x_0)))
------------------------------------------------------------
Lemma concat_repeat_swap:
-Prove: let a_0 = (repeat x_0 k_0) in (concat a_0 x_0)=(concat x_0 a_0)
+Prove: (repeat x_0 k_0)=(repeat x_0 k_0)
------------------------------------------------------------
--
GitLab