From 400e459397c3a678dcc67d9ed794e0c777cb0024 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 18 Jan 2022 16:01:38 +0100
Subject: [PATCH] [WP] improves the simplifier dedicated to eq_sequence
---
src/plugins/wp/Vlist.ml | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 827c189d43e..28e5a725862 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -369,14 +369,23 @@ let rewrite_eq a b =
match F.repr a , F.repr b with
| L.Fun(nil,[]) , _ when nil == f_nil -> rewrite_is_nil ~nil:a b
| _ , L.Fun(nil,[]) when nil == f_nil -> rewrite_is_nil ~nil:b a
+ | L.Fun(repeat_a, [x;n]), L.Fun(repeat_b, [y;m])
+ when repeat_a == f_repeat &&
+ repeat_b == f_repeat &&
+ F.decide (F.e_eq x y) ->
+ (* ( s *^ n == s *^ m <==> (s *^ n == [] && y *^ m == []) || (n == m) *)
+ let nil_a = v_nil (F.typeof a) in
+ let nil_b = v_nil (F.typeof b) in
+ F.p_or (F.p_equal n m)
+ (F.p_and (F.p_equal a nil_b) (F.p_equal nil_a b))
| L.Fun(repeat_a, [x;n]), L.Fun(repeat_b, [y;m])
when repeat_a == f_repeat &&
repeat_b == f_repeat &&
F.decide (
let nil_a = v_nil (F.typeof a) in
let nil_b = v_nil (F.typeof b) in
- F.e_or [ F.e_and [ F.e_eq x y; F.e_eq n m];
- F.e_and [F.e_eq a nil_b; F.e_eq nil_a b]]
+ F.e_or [ F.e_and [F.e_eq x y; F.e_eq n m];
+ F.e_and [F.e_eq a nil_b; F.e_eq nil_a b] ]
) ->
(* x *^ n == [] && y *^ m == []) || (x == y && n == m) ==> x *^ n == y *^ m *)
F.p_true
--
GitLab