diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index e889cc7d28636556e4bd95d472db3dbdd01da4f6..72a7467a5a38115973b22c0770461db1f062f5e2 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -90,4 +90,5 @@ val is_cint_simplifier: simplifier
val mask_simplifier: simplifier
+(* under approximation: [is_positive_or_null e] ==> [e] >= 0 *)
val is_positive_or_null: term -> bool
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index 3671cd67b73db65cf679ea358e3a6b56640dba10..ab689630267f2bfc69790deb410b7399075391ad 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -53,36 +53,59 @@ class sequence =
~descr:"Unroll repeat-sequence operator"
~params:[pmode]
- method select _feedback (s : Tactical.selection) =
+ method select feedback (s : Tactical.selection) =
let value = Tactical.selected s in
match F.repr value with
| Fun(f,[a;n]) when f == Vlist.f_repeat ->
let result = F.typeof value in
let at = Tactical.at s in
- Tactical.Applicable
- begin
- match self#get_field vmode with
- | `Sum ->
- let ns = sum n in
- let pos = F.p_all positive ns in
- let cat = concat ~result (List.map (repeat ~result a) ns) in
- Tactical.condition "Positive" pos @@
- Tactical.rewrite ?at [ "Unroll" , pos , value , cat ]
- | `Left ->
- let p = F.e_add n F.e_minus_one in
- let unroll = concat ~result [a ; repeat ~result a p] in
+ begin
+ match self#get_field vmode with
+ | `Sum ->
+ (* n1>=0 && n2>=0 && ... |- (a *^ (n1 + n2 + ...)) -+-> ((a *^ n1) ^ (a *^ n2) ^ ...) *)
+ begin
+ match sum n with
+ | [ s ] ->
+ feedback#set_descr
+ "Cannot unroll with selected option, '%a' is not a sum"
+ F.pp_term s ;
+ Tactical.Not_configured
+ | ns ->
+ (* NB. the term is rewriten in itself when the initial term is not a sum *)
+ let pos = F.p_all positive ns in
+ let cat =
+ concat ~result (List.map (repeat ~result a) ns) in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll sum" ;
+ Tactical.Applicable (
+ Tactical.condition "Positive" pos @@
+ Tactical.rewrite ?at [ "Unroll" , pos , value , cat ])
+ end
+ | `Left ->
+ (* n<=0 |- (a *^ n) -+-> [] *)
+ (* n-1>=0 |- (a *^ n) -+-> (a ^ (a *^ (n-1))) *)
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [a ; repeat ~result a p] in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll first element" ;
+ Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
"Unroll", positive p , value , unroll ;
- ]
- | `Right ->
- let p = F.e_add n F.e_minus_one in
- let unroll = concat ~result [repeat ~result a p ; a] in
+ ])
+ | `Right ->
+ (* n<=0 |- (a *^ n) -+-> [] *)
+ (* n-1>=0 |- (a *^ n) -+-> ((a *^ (n-1)) ^ a) *)
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [repeat ~result a p ; a] in
+ feedback#set_descr
+ "Unroll repeat-sequence: unroll last element" ;
+ Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
"Unroll", positive p , value , unroll ;
- ]
- end
+ ])
+ end
| _ -> Not_applicable
end
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index c46c6b226aef8d634e93f6df32fbecff73698184..76423f7fee8de99ce2a543a5d264bc5c18128ed5 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -23,6 +23,9 @@
(* -------------------------------------------------------------------------- *)
(* --- VList Builtins --- *)
(* -------------------------------------------------------------------------- *)
+let dkey = Wp_parameters.register_category "sequence"
+let debug fmt = Wp_parameters.debug ~dkey fmt
+let debugN level fmt = Wp_parameters.debug ~level ~dkey fmt
open Lang
open Lang.F
@@ -113,39 +116,75 @@ let () =
add_builtin "\\repeat" [A;Z] f_repeat ;
end
+let category e =
+ match F.repr e with
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_nil -> "Nil"
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_cons -> "Cons"
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_nth -> "Nth"
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_length -> "Length"
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_concat -> "Concat"
+ | Qed.Logic.Fun (f,_) when Fun.equal f f_repeat -> "Repeat"
+ | _ -> "_"
+
+let rec pp_pattern fmt e =
+ match F.repr e with
+ | Qed.Logic.Fun (f, args) when Fun.equal f f_nil ||
+ Fun.equal f f_cons ||
+ Fun.equal f f_nth ||
+ Fun.equal f f_length ||
+ Fun.equal f f_concat ||
+ Fun.equal f f_repeat -> Format.fprintf fmt "(%s %a)" (category e) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt " ") pp_pattern) args
+ | _ -> Format.pp_print_string fmt "_"
+
(*--- Smart Constructors ---*)
-let is_nil e =
+let is_nil e = (* under-approximation of e==[] *)
match F.repr e with
| Qed.Logic.Fun (f,_) -> Fun.equal f f_nil
| _ -> false
+
let v_nil t = F.e_fun ~result:t f_nil []
let v_elt e = F.e_fun f_elt [e]
let v_concat es tau = F.e_fun f_concat es ~result:tau
let v_length l = F.e_fun f_length [l]
-let v_repeat s n = F.e_fun f_repeat [s;n]
+let v_repeat s n tau = F.e_fun f_repeat [s;n] ~result:tau
(* -------------------------------------------------------------------------- *)
(* --- Rewriters --- *)
(* -------------------------------------------------------------------------- *)
-let rewrite_cons a w tau = v_concat [v_elt a ; w] (vlist_get_tau tau)
+let rewrite_cons a w tau = (* a::w == [a]^w *)
+ v_concat [v_elt a ; w] (vlist_get_tau tau)
let rewrite_length e =
match F.repr e with
- | L.Fun( nil , [] ) when nil == f_nil -> F.e_zero
- | L.Fun( elt , [_] ) when elt == f_elt -> F.e_one
- | L.Fun( concat , es ) when concat == f_concat ->
+ | L.Fun( nil , [] ) when nil == f_nil -> F.e_zero (* \length([]) == 0 *)
+ | L.Fun( elt , [_] ) when elt == f_elt -> F.e_one (* \length([x]) == 1 *)
+ | L.Fun( concat , es ) when concat == f_concat -> (* \length(\concat(...,x_i,...)) == \sum(...,\length(x_i),...) *)
F.e_sum (List.map v_length es)
- | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat &&
- Cint.is_positive_or_null n ->
- F.e_mul (v_length u) n
+ | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat ->
+ (* \length(u ^* n) == if 0<=n then n * \length(u) else 0 *)
+ F.e_if (F.e_leq e_zero n) (F.e_mul n (v_length u)) e_zero
+ | _ ->
+ (* NB. do not considers \Cons because they are removed *)
+ raise Not_found
+
+let match_natural k =
+ match F.repr k with
+ | L.Kint z ->
+ let k = try Integer.to_int_exn z with Z.Overflow -> raise Not_found in
+ if 0 <= k then k else raise Not_found
| _ -> raise Not_found
+(* Why3 definition: [\nth(e,k)] is undefined for [k<0 || k>=\length(e)].
+ So, the list cannot be destructured when the length is unknown *)
let rec get_nth k e =
match F.repr e with
| L.Fun( concat , list ) when concat == f_concat -> get_nth_list k list
- | L.Fun( elt , [x] ) when elt == f_elt && k = 0 -> x
+ | L.Fun( elt , [x] ) when elt == f_elt ->
+ get_nth_elt k x (fun _ -> raise Not_found)
+ | L.Fun( repeat , [x;n] ) when repeat == f_repeat ->
+ get_nth_repeat k x n (fun _ -> raise Not_found)
| _ -> raise Not_found
and get_nth_list k = function
@@ -153,37 +192,78 @@ and get_nth_list k = function
begin
match F.repr head with
| L.Fun( elt , [x] ) when elt == f_elt ->
- if k = 0 then x else get_nth_list (k-1) tail
+ get_nth_elt k x (fun k -> get_nth_list k tail)
+ | L.Fun( repeat , [x;n] ) when repeat == f_repeat ->
+ get_nth_repeat k x n (fun k -> get_nth_list k tail)
| _ -> raise Not_found
end
| [] -> raise Not_found
+and get_nth_elt k x f =
+ if k = 0 then x else (f (k-1))
+
+and get_nth_repeat k x n f =
+ let n = match_natural n in
+ if n = 0 then raise Not_found ;
+ let m = match_natural (rewrite_length x) in
+ if m = 0 then raise Not_found ;
+ let en = Integer.of_int n in
+ let em = Integer.of_int m in
+ let ek = Integer.of_int k in
+ if Integer.(ge ek (mul en em)) then f (k -(n*m))
+ else get_nth (k mod m) x
+
let rewrite_nth s k =
- match F.repr k with
- | L.Kint z ->
- let k = try Integer.to_int_exn z with Z.Overflow -> raise Not_found in
- if 0 <= k then get_nth k s else raise Not_found
- | _ -> raise Not_found
+ get_nth (match_natural k) s
let rewrite_repeat s n =
- if F.equal n e_zero then v_nil (F.typeof s) else
- if F.equal n e_one then s else
- if is_nil s then s else
+ if F.decide (F.e_leq n e_zero) then (* n <=0 ==> (s *^ n) == [] *)
+ v_nil (F.typeof s)
+ else if F.equal n e_one then (* (s *^ 1) == s *)
+ s
+ else if is_nil s then (* ([] *^ n) == [] ; even if [n] is negative *)
+ s
+ else
match F.repr s with
- | L.Fun( repeat , [s0 ; n0] )
+ | L.Fun( repeat , [s0 ; n0] ) (* n0>=0 && n>=0 ==> ((s0 *^ n0) *^ n) == (s0 *^ (n0 * n)) *)
when (repeat == f_repeat) &&
(Cint.is_positive_or_null n) &&
- (Cint.is_positive_or_null n0) -> v_repeat s0 (F.e_mul n0 n)
+ (Cint.is_positive_or_null n0) -> v_repeat s0 (F.e_mul n0 n) (F.typeof s)
| _ -> raise Not_found
let rec leftmost a ms =
match F.repr a with
| L.Fun( concat , e :: es ) when concat == f_concat ->
leftmost e (es@ms)
- | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat && Cint.is_positive_or_null n ->
- leftmost u (v_repeat u (F.e_sub n F.e_one) :: ms)
+ | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat -> begin
+ match (* tries to perform some rolling that do not depend on [n] *)
+ (match ms with
+ | b::ms ->
+ let b,ms = leftmost b ms in
+ let u,us = leftmost u [] in
+ if F.decide (F.e_eq u b) then
+ (* u=b ==> ((u^us)*^n) ^ b ^ ms == u ^ (us^b)*^n) ^ ms *)
+ Some (u, v_repeat (v_concat (us@[b]) (F.typeof a)) n (F.typeof a) :: ms)
+ else None
+ | _ -> None) with
+ | Some res -> res
+ | None ->
+ if F.decide (F.e_lt F.e_zero n) then
+ (* 0<n ==> (u*^n) ^ ms == u ^ (u*^(n-1)) ^ ms *)
+ leftmost u (v_repeat u (F.e_sub n F.e_one) (F.typeof a) :: ms)
+ else a , ms
+ end
| _ -> a , ms
+(* [leftmost a] returns [s,xs] such that [a = s ^ x1 ^ ... ^ xn] *)
+let leftmost a =
+ let r = leftmost a [] in
+ debugN 2 "Vlist.leftmost %a@ = %a (form: %s) ^ ... (%d more)@."
+ Lang.F.pp_term a
+ Lang.F.pp_term (fst r) (category (fst r))
+ (List.length (snd r)) ;
+ r
+
let rec rightmost ms a =
match F.repr a with
| L.Fun( concat , es ) when concat == f_concat ->
@@ -191,72 +271,182 @@ let rec rightmost ms a =
| [] -> ms , a
| e::es -> rightmost (ms @ List.rev es) e
end
- | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat && Cint.is_positive_or_null n ->
- rightmost (ms @ [v_repeat u (F.e_sub n F.e_one)]) u
+ | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat -> begin
+ match (* tries to perform some rolling that do not depend on [n] *)
+ (match List.rev ms with
+ | b::ms ->
+ let ms,b = rightmost (List.rev ms) b in
+ let us,u = rightmost [] u in
+ if F.decide (F.e_eq u b) then
+ (* u=b ==> (ms ^ b ^ (us^u)*^n) == ms ^ (b^us)*^n) ^ u *)
+ Some (ms @ [ v_repeat (v_concat (b::us) (F.typeof a)) n (F.typeof a)], u)
+ else None
+ | _ -> None) with
+ | Some res -> res
+ | None ->
+ if F.decide (F.e_lt F.e_zero n) then
+ (* 0<n ==> ms ^ (u*^n) == ms ^ (u*^(n-1)) ^ u *)
+ rightmost (ms @ [v_repeat u (F.e_sub n F.e_one) (F.typeof a)]) u
+ else ms , a
+ end
| _ -> ms , a
+(* [rightmost a] returns [s,xs] such that [a = x1 ^ ... ^ xn ^ s] *)
+let rightmost a =
+ let r = rightmost [] a in
+ debugN 2 "Vlist.rightmost %a@ = (%d more) ... ^ %a (form: %s)@."
+ Lang.F.pp_term a
+ (List.length (fst r))
+ Lang.F.pp_term (snd r) (category (snd r));
+ r
+
let leftmost_eq a b =
- let a , u = leftmost a [] in
- let b , v = leftmost b [] in
+ let a , u = leftmost a in
+ let b , v = leftmost b in
if u <> [] || v <> [] then
match F.is_equal a b with
- | L.Yes -> F.p_equal (v_concat u (F.typeof a)) (v_concat v (F.typeof a))
- | L.No -> F.p_false
- | L.Maybe -> raise Not_found
+ | L.Yes ->
+ (* s ^ u1 ^ ... = s ^ v1 ^ ... <=> u1 ^ ... = v1 ^ ... *)
+ F.p_equal (v_concat u (F.typeof a)) (v_concat v (F.typeof a))
+ | L.No when F.decide (F.e_eq (v_length a) (v_length b)) ->
+ (* a <> b && \length(a)=\length(b) ==> a ^ u1 ^ ... <> b ^ v1 ^ ... *)
+ F.p_false
+ | _ -> raise Not_found
else
raise Not_found
let rightmost_eq a b =
- let u , a = rightmost [] a in
- let v , b = rightmost [] b in
+ let u , a = rightmost a in
+ let v , b = rightmost b in
if u <> [] || v <> [] then
match F.is_equal a b with
- | L.Yes -> F.p_equal (v_concat u (F.typeof a)) (v_concat v (F.typeof a))
- | L.No -> F.p_false
- | L.Maybe -> raise Not_found
+ | L.Yes ->
+ (* u1 ^ ... ^ s = v1 ^ ... ^ s <=> u1 ^ ... = v1 ^ ... *)
+ F.p_equal (v_concat u (F.typeof a)) (v_concat v (F.typeof a))
+ | L.No when F.decide (F.e_eq (v_length a) (v_length b)) ->
+ (* a <> b && \length(a)=\length(b) ==> u1 ^ ... ^ a <> v1 ^ ... ^ b *)
+ F.p_false
+ | _ -> raise Not_found
else
raise Not_found
-let p_is_nil a = F.p_equal a (v_nil (F.typeof a))
-let rewrite_is_nil a =
+let rewrite_is_nil ~nil a =
+ let p_is_nil a = F.p_equal nil a in
match F.repr a with
- | L.Fun(concat,es) when concat == f_concat -> F.p_all p_is_nil es
- | L.Fun(elt,[_]) when elt == f_elt -> F.p_false
- | L.Fun(repeat,[u;n]) when repeat == f_repeat ->
- F.p_or (F.p_leq n F.e_zero) (p_is_nil u)
+ | L.Fun(concat,es) when concat == f_concat ->
+ (* \concat (s1,...,sn)==[] <==> (s1==[] && ... && sn==[]) *)
+ F.p_all p_is_nil es
+ | L.Fun(elt,[_]) when elt == f_elt -> F.p_false (* [x]==[] <==> false *)
+ | L.Fun(repeat,[s;n]) when repeat == f_repeat ->
+ (* (s *^ n)==[] <==> (s==[] || n<=0) *)
+ F.p_or (F.p_leq n F.e_zero) (p_is_nil s)
+ | _ ->
+ raise Not_found
+
+(* Ensures xs to be a sub-sequence of ys, otherwise raise Not_found
+ In such a case, (concat xs = concat ys) <==> (forall r in result, r = nil) *)
+let rec subsequence xs ys =
+ match xs , ys with
+ | [],ys -> ys
+ | x::rxs, y::rys ->
+ if (F.decide (e_eq x y)) then subsequence rxs rys else y :: subsequence xs rys
| _ -> raise Not_found
let elements a =
match F.repr a with
- | L.Fun( nil , [] ) when nil == f_nil -> []
- | L.Fun( concat , es ) when concat == f_concat -> es
- | _ -> [a]
-
-(* [omit rs x ys]: if ys = u.x.v returns (rs+u,v) with r in reverse order *)
-
-let rec omit rs x = function
- | [] -> raise Not_found
- | y::ys -> if x == y then rs,ys else omit (y::rs) x ys
-
-let rec subsequence xs rs ys =
- match xs with
- | [] -> List.rev_append rs ys
- | x::xs ->
- let rs,ys = omit rs x ys in
- subsequence xs rs ys
+ | L.Fun(concat,es) when concat == f_concat -> true, es
+ | _ -> false, [ a ]
+
+(* Ensures that [a] or [b] is a sub-sequence of the other, otherwise [raise Not_found]
+ In such a case, (concat xs = concat ys) <==> (forall r in result, r = nil) *)
+let subsequence a b =
+ let destruct_a, xs = elements a in
+ let destruct_b, ys = elements b in
+ if not (destruct_a || destruct_b) then raise Not_found;
+ let shortest,xs,ys = if List.length xs <= List.length ys then a,xs,ys else b,ys,xs in
+ let es = subsequence xs ys in
+ (* xs=ys <==> forall s in es ; s = nil *)
+ let nil = v_nil (F.typeof shortest) in
+ (* [s] are elements of [ys] (the longest sequence) and [nil] has the same type than the [shortest] sequence *)
+ let p_is_nil s = F.p_equal nil s in
+ F.p_all p_is_nil es
+
+let repeat_eq a x n b y m =
+ let e_eq_x_y = F.e_eq x y in
+ let e_eq_n_m = F.e_eq n m in
+ if F.decide e_eq_x_y then
+ (* s *^ n == s *^ m <==> ( n=m || (s *^ n == [] && s *^ m == []) ) *)
+ let nil_a = v_nil (F.typeof a) in
+ let nil_b = v_nil (F.typeof b) in
+ F.p_or (Lang.F.p_bool e_eq_n_m)
+ (F.p_and (F.p_equal a nil_b) (F.p_equal nil_a b))
+ else if F.decide e_eq_n_m then
+ (* x *^ n == y *^ n <==> ( x == y || n<=0 ) *)
+ F.p_or (F.p_leq n e_zero) (Lang.F.p_bool e_eq_x_y)
+ else if F.decide (e_eq (v_length x) (v_length y)) then
+ (* \length(x)=\length(y) ==> ( x *^ n == y *^ m <==> ( m == n && x == y) || (x *^ n == [] && y *^ m == [] ) *)
+ let nil_a = v_nil (F.typeof a) in
+ let nil_b = v_nil (F.typeof b) in
+ F.p_or (F.p_and (F.p_bool e_eq_n_m) (Lang.F.p_bool e_eq_x_y))
+ (F.p_and (F.p_equal a nil_b) (F.p_equal nil_a b))
+ else raise Not_found
+
+let rewrite_eq_sequence a b =
+ debug "Vlist.rewrite_eq_sequence: tries to rewrite %a@ = %a@.- left pattern: %a@.- right pattern: %a@."
+ Lang.F.pp_term a Lang.F.pp_term b
+ pp_pattern a pp_pattern 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
+ | _ -> try
+ match F.repr a , F.repr b with
+ | L.Fun(repeat_a, [x;n]), L.Fun(repeat_b, [y;m])
+ when repeat_a == f_repeat &&
+ repeat_b == f_repeat ->
+ repeat_eq a x n b y m
+ | _ ->
+ try leftmost_eq a b with Not_found ->
+ try rightmost_eq a b with Not_found ->
+ subsequence a b
+ with Not_found ->
+ if F.decide (F.e_neq (v_length a) (v_length b)) then
+ F.p_false
+ else raise Not_found
+
+let rewrite_eq_length a b =
+ match F.repr a , F.repr b with
+ | L.Fun(length_a,[_]), L.Fun(length_b,[_]) when length_a == f_length &&
+ length_b == f_length ->
+ (* N.B. cannot be simplified by the next patterns *)
+ raise Not_found
+ | _, L.Fun(length,[_]) when length == f_length &&
+ F.decide (e_lt a e_zero) ->
+ (* a < 0 ==> ( a=\length(b) <=> false ) *)
+ F.p_false
+ | L.Fun(length,[_]), _ when length == f_length &&
+ F.decide (e_lt b e_zero) ->
+ (* b < 0 ==> ( \length(a)<=b <=> false ) *)
+ F.p_false
+ | _ -> raise Not_found
-let rewrite_eq a b =
+let rewrite_leq_length a b =
match F.repr a , F.repr b with
- | L.Fun(nil,[]) , _ when nil == f_nil -> rewrite_is_nil b
- | _ , L.Fun(nil,[]) when nil == f_nil -> rewrite_is_nil a
- | _ ->
- try leftmost_eq a b with Not_found ->
- try rightmost_eq a b with Not_found ->
- let xs = elements a in
- let ys = elements b in
- if List.length xs < List.length ys
- then F.p_all p_is_nil (subsequence xs [] ys)
- else F.p_all p_is_nil (subsequence ys [] xs)
+ | L.Fun(length_a,[_]), L.Fun(length_b,[_]) when length_a == f_length &&
+ length_b == f_length ->
+ (* N.B. cannot be simplified by the next patterns *)
+ raise Not_found
+ | L.Fun(length,[_]), _ when length == f_length &&
+ F.decide (e_lt b e_zero) ->
+ (* b < 0 ==> ( \length(a)<=b <=> false ) *)
+ F.e_false
+ (* N.B. the next rule does not allow to split on the sign of \length(a) with TIP
+ | _, L.Fun(length,[_]) when length == f_length &&
+ F.decide (e_leq a e_zero) ->
+ (* a <= 0 ==> ( a<=\length(b) <=> true ) *)
+ F.e_true
+ *)
+ | _ -> raise Not_found
+
(* All Simplifications *)
@@ -267,8 +457,11 @@ let () =
F.set_builtin_2' f_cons rewrite_cons ;
F.set_builtin_2 f_repeat rewrite_repeat ;
F.set_builtin_1 f_length rewrite_length ;
- F.set_builtin_eqp f_repeat rewrite_eq ;
- F.set_builtin_eqp f_nil rewrite_eq ;
+ F.set_builtin_leq f_length rewrite_leq_length ;
+ F.set_builtin_eqp f_length rewrite_eq_length ;
+ F.set_builtin_eqp f_concat rewrite_eq_sequence ;
+ F.set_builtin_eqp f_repeat rewrite_eq_sequence ;
+ F.set_builtin_eqp f_nil rewrite_eq_sequence ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp_plugin/nth.i b/src/plugins/wp/tests/wp_plugin/nth.i
index 3e5a1d4e75d247e894c07d6e09395a0d3c7bdf92..0e444d63fe1e9d5f689f657eea8a81b7188fce9c 100644
--- a/src/plugins/wp/tests/wp_plugin/nth.i
+++ b/src/plugins/wp/tests/wp_plugin/nth.i
@@ -3,8 +3,85 @@
*/
/*@
- axiomatic Nth {
+ axiomatic Def {
+
logic integer f(integer a);
+ logic integer N;
+ logic integer M;
+ logic \list<integer> S;
+ logic \list<integer> A;
+ logic \list<integer> B;
+ logic \list<integer> C;
+
+ logic \list<integer> empty = \Nil;
+ predicate IsEmpty(\list<integer> s) = s == empty;
+
+ predicate P(\list<integer> s) reads \nothing;
+
+ }
+*/
+
+/*@
+ axiomatic MkRepeat {
+
+ check lemma negative_repeat: ok: P( A *^ 0 ) <==> P( S *^ (-1) ) ;
+ check lemma repeat_nil: ok: P( A *^ 0 ) <==> P( (S *^ 0) *^ N );
+ check lemma repeat_one: ok: P( S *^ 1 ) <==> P( S );
+ check lemma repeat_repeated: ok: P( (S *^ ((N&1)) *^ (M&2)) ) <==> P( S *^ ((N&1) * (M&2)) );
+
+ }
+*/
+
+/*@
+ axiomatic Equality {
+
+ check lemma constructor_elt: ok: [| 1 |] != [| 2 |] ;
+
+ check lemma not_nil_elt: ok: ([| 1 |] ^ A) != A ;
+
+
+ check lemma repeat1: ko: (S *^ N) == (S *^ M)
+ <==> ( N == M || ( ((S *^ N) ^ A) == A && ((S *^ M) ^ A) == A ) ) ;
+
+ check lemma repeat2: ok: ( ((S *^ N) ^ S) *^ M ) == ( ( S ^ (S *^ N)) *^ M ) ;
+
+ check lemma left_shift_repeat1: ok: ( ((S ^ A ^ B) *^ N) ^ S ^ A ) == (S ^ C)
+ <==> ( ( (A ^ B ^ S) *^ N) ^ A ) == ( C);
+ check lemma left_unfold_repeat1: ok: ( ((S ^ A ^ B) *^ 3) ^ A ^ S ) == (S ^ C)
+ <==> ( A ^ B ^ ((S ^ A ^ B) *^ 2) ^ A ^ S ) == ( C);
+
+ check lemma right_shift_repeat1: ko: ( A ^ S ^ ((B ^ A ^ S) *^ N) ) == (C ^ S)
+ <==> ( A ^ ((S ^ B ^ A ) *^ N) ) == (C );
+ check lemma right_unfold_repeat1: ko: ( S ^ A ^ ((B ^ A ^ S) *^ 3) ) == (C ^ S)
+ <==> ( S ^ A ^ ((B ^ A ^ S) *^ 2) ^ B ^ A) == (C );
+
+
+ check lemma left_shift_repeat2: ok: ( ((S ^ A ^ B) *^ N) ^ S ^ A ^ C) == (S ^ A)
+ <==> ( (C ^ S) == S && (N<=0 || (A ^ B ^ S ^ S) == S) );
+ check lemma left_unfold_repeat2: ok: ( ((S ^ A ^ B) *^ 3) ^ C) == (S ^ A)
+ <==> (A ^ A ^ B ^ C ^ S) == A ;
+
+ check lemma right_shift_repeat2: ko: ( C ^ A ^ S ^ ((B ^ A ^ S) *^ N) ) == (A ^ S)
+ <==> ( (C ^ S) == S && (N<=0 || (A ^ B ^ S ^ S) == S) );
+ check lemma right_unfold_repeat2: ko: ( C ^ ((B ^ A ^ S) *^ 3) ) == (A ^ S)
+ <==> (A ^ B ^ C ^ S ^ S) == S ;
+
+
+ check lemma subsequence1: ko: ( A ^ (S *^ N) ^ B ^ S ^ C ) == ( (S *^ N) ^ S )
+ <==> ( A ^ B ^ C ^ C ) == C ;
+
+ }
+*/
+
+/*@
+ axiomatic Nth {
+
+ check lemma nth_repeat_undefined_1: ko: \nth ( [| f(0), f(1), f(2), f(3) |] *^ 3, 12 ) == f(0);
+
+ check lemma nth_repeat_1: ok: \nth ( [| f(0), f(1), f(2), f(3) |] *^ 3, 0 ) == f(0);
+ check lemma nth_repeat_2: ok: \nth ( [| f(0), f(1), f(2), f(3) |] *^ 3, 11 ) == f(3);
+ check lemma nth_repeat_3: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12) |] , 12 ) == f(12);
+ check lemma nth_repeat_4: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12),f(13),f(14)|] ^ S, 13 ) == f(13);
lemma access_16_16: ok:
\forall integer k ; 0 <= k < 16 ==>
@@ -15,12 +92,12 @@
\forall integer k ; 0 <= k < 4 ==>
f(k)==\nth([| f(0), f(1), f(2), f(3) |], k);
- lemma eq_repeat_concat_3: ok:
- \forall \list<integer> x ; (x *^ 3) == (x ^ x ^ x) ;
+ lemma eq_repeat_concat_3: ok: (S *^ 3) == (S ^ S ^ S) ;
lemma access_repeat_concat_3: ok: lack:
- \forall \list<integer> x ;
- \forall integer k ; 0 <= k < 3*\length(x) ==> \nth(x *^ 3, k) == \nth(x ^ x ^ x, k) ;
+ \forall integer k ; 0 <= k < 3*\length(S) ==> \nth(S *^ 3, k) == \nth(S ^ S ^ S, k) ;
}
+
+
*/
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 908af494da9eac274fa2f4293aa6379dc9accb7c..c93629cbb62d4b5fa92e4144cc23d6e0c1089cf1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -1,6 +1,97 @@
# frama-c -wp [...]
[kernel] Parsing nth.i (no preprocessing)
[wp] Running WP plugin...
+------------------------------------------------------------
+ Axiomatic 'Equality'
+------------------------------------------------------------
+
+Lemma constructor_elt:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma left_shift_repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma left_shift_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma left_unfold_repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma left_unfold_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma not_nil_elt:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_shift_repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_shift_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_unfold_repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_unfold_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma subsequence1:
+Prove: true
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Axiomatic 'MkRepeat'
+------------------------------------------------------------
+
+Lemma negative_repeat:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_nil:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_one:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_repeated:
+Prove: true
+
+------------------------------------------------------------
------------------------------------------------------------
Axiomatic 'Nth'
------------------------------------------------------------
@@ -27,8 +118,8 @@ Prove: (0<=k_0) -> (k_0<=3)
Lemma access_repeat_concat_3:
Assume: 'eq_repeat_concat_3' 'access_4_4' 'access_16_16'
-Prove: (0<=k_0) -> (k_0<(3*(length x_0)))
- -> ((nth (concat x_0 x_0 x_0) k_0)=(nth (repeat x_0 3) k_0))
+Prove: (0<=k_0) -> (k_0<(3*(length L_S)))
+ -> ((nth (concat L_S L_S L_S) k_0)=(nth (repeat L_S 3) k_0))
------------------------------------------------------------
@@ -37,3 +128,31 @@ Assume: 'access_4_4' 'access_16_16'
Prove: true
------------------------------------------------------------
+
+Lemma nth_repeat_1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_3:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_4:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_undefined_1:
+Prove: let x_0 = (L_f 0) in
+ (nth
+ (repeat (concat (elt x_0) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3)))
+ 3) 12)=x_0
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index eaf6561ef18ecbc197623780c17af09faa1eb1ba..fedcdb66fb660ab5c85989b6c35ce166281fa5ba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -34,7 +34,7 @@ Assume {
(* Call 'f' *)
Have: L_call_obs(call_seq_3) = a_1.
}
-Prove: nth(a_1, 1 + length(a)) = z.
+Prove: nth(a_1, 1 + i) = z.
------------------------------------------------------------
@@ -181,30 +181,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition for 'g_called' 'ok,u1' in 'loops':
-Let a = ([ y ] *^ i).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
- is_sint32(z).
- (* Heap *)
- Type: is_sint32(call_seq_0).
- (* Pre-condition *)
- Have: L_call_obs(call_seq_0) = nil.
- (* Pre-condition for 'g_called' *)
- Have: 0 < n.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_1) = [ x ].
- (* Invariant 'ok,id_min' *)
- Have: 0 <= i.
- (* Invariant 'ok,id_max' *)
- Have: i <= n.
- (* Invariant 'ok,inv' *)
- Have: L_call_obs(call_seq_2) = [ x ] ^ a.
- (* Else *)
- Have: n <= i.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ z ].
-}
-Prove: length(a) = i.
+Prove: true.
------------------------------------------------------------
@@ -240,7 +217,7 @@ Assume {
(* Call 'f' *)
Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ z ].
}
-Prove: length(a) = 0.
+Prove: i = 0.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index 68fe97d6e4fa3fa66f330d8a0def5a8eab97d2f6..d276407bd64584ec645b8c0a7af2e28af3fb306d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
@@ -1,15 +1,39 @@
# frama-c -wp [...]
[kernel] Parsing nth.i (no preprocessing)
[wp] Running WP plugin...
-[wp] 4 goals scheduled
+[wp] 26 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
+[wp] [Qed] Goal typed_check_lemma_constructor_elt_ok : Valid
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
-[wp] Proved goals: 3 / 4
- Qed: 1
- Alt-Ergo: 2 (unsuccess: 1)
+[wp] [Qed] Goal typed_check_lemma_left_shift_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_shift_repeat2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_unfold_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_unfold_repeat2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_negative_repeat_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_not_nil_elt_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_3_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_4_ok : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_nth_repeat_undefined_1_ko : Unsuccess
+[wp] [Qed] Goal typed_check_lemma_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat_nil_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat_one_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat_repeated_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_right_shift_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_shift_repeat2_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_unfold_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_unfold_repeat2_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_subsequence1_ko : Valid
+[wp] Proved goals: 25 / 26
+ Qed: 22
+ Alt-Ergo: 3 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic Nth 1 2 4 75.0%
+ Axiomatic Equality 13 - 13 100%
+ Axiomatic MkRepeat 4 - 4 100%
+ Axiomatic Nth 5 3 9 88.9%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index 08751dc1962e76436108d5c150fb46acbffc110b..7602867d0780d45feb0ba2978880f36079220b2c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
@@ -38,16 +38,16 @@
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
+[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u2 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 39 / 39
- Qed: 25
- Alt-Ergo: 14
+ Qed: 26
+ Alt-Ergo: 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 5 5 10 100%
sequence 8 2 10 100%
- loops 12 7 19 100%
+ loops 13 6 19 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index d2806020044b634a1c493759069ee6fe5ebee4ee..fb728b9fa94a45d92d1f3cf5d409d84160adeadd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -33,16 +33,16 @@
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_caveat_loops_assigns_normal_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
+[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u1 : Valid
[wp] [Qed] Goal typed_caveat_loops_g_called_ensures_ok_u2 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 34 / 34
- Qed: 22
- Alt-Ergo: 12
+ Qed: 23
+ Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 2 3 5 100%
sequence 8 2 10 100%
- loops 12 7 19 100%
+ loops 13 6 19 100%
------------------------------------------------------------