Commit 2ba31cc1 authored by MARCHE Claude's avatar MARCHE Claude

LCP: restructuration

parent 17988c1a
......@@ -73,17 +73,12 @@ that it does so correctly.
*)
module SuffixArray
module LCP
use import int.Int
use import array.Array
type suffixArray = {
values : array int;
suffixes : array int;
}
(* TODO: dire plus precisement que c'est une permutation de 0..b-1 *)
predicate array_bounded (a:array int) (b:int) =
forall i:int. 0 <= i < a.length -> 0 <= a[i] < b
......@@ -96,16 +91,6 @@ predicate array_bounded (a:array int) (b:int) =
forall a1 a2:array int, n:int.
permut a1 a2 /\ array_bounded a1 n -> array_bounded a2 n
predicate inv(s:suffixArray) =
s.values.length = s.suffixes.length /\
array_bounded s.suffixes s.values.length
let select (s:suffixArray) (i:int) : int
requires { inv s /\ 0 <= i < s.values.length }
ensures { result = s.suffixes[i] }
= s.suffixes[i]
use import ref.Refint
predicate is_common_prefix (a:array int) (x y:int) (l:int) =
0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
......@@ -124,6 +109,9 @@ axiom lcp_spec:
(l = longest_common_prefix a x y <->
is_common_prefix a x y l /\ not is_common_prefix a x y (l+1))
use import ref.Refint
let lcp (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
......@@ -206,6 +194,29 @@ let compare (a:array int) (x y:int) : int
done
done
end
module SuffixArray
use import int.Int
use import array.Array
use import LCP
type suffixArray = {
values : array int;
suffixes : array int;
}
predicate inv(s:suffixArray) =
s.values.length = s.suffixes.length /\
array_bounded s.suffixes s.values.length
let select (s:suffixArray) (i:int) : int
requires { inv s /\ 0 <= i < s.values.length }
ensures { result = s.suffixes[i] }
= s.suffixes[i]
let create (a:array int) : suffixArray
requires { a.length >= 0 }
ensures { result.values.length = a.length /\ inv result }
......@@ -218,41 +229,41 @@ let create (a:array int) : suffixArray
sort a suf;
{ values = a; suffixes = suf }
let lcp2 (s:suffixArray) (i:int) : int
let lcp (s:suffixArray) (i:int) : int
requires { inv s }
requires { 0 < i < s.values.length }
=
lcp s.values s.suffixes[i] s.suffixes[i-1]
LCP.lcp s.values s.suffixes[i] s.suffixes[i-1]
let test2 () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let sa = create arr in
let x = lcp2 sa 1 in
let x = lcp sa 1 in
check {x = -1 (* TODO *)};
(* int[] brr = {1,2,3,5}; *)
let brr = Array.make 4 0 in
brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
let sa = create brr in
let x = lcp2 sa 1 in
let x = lcp sa 1 in
check {x = -1 (* TODO *)};
(* int[] crr = {1,2,3,5}; *)
let crr = Array.make 4 0 in
crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
let sa = create crr in
let x = lcp2 sa 2 in
let x = lcp sa 2 in
check {x = -1 (* TODO *)};
(* int[] drr = {1,2,3,3}; *)
let drr = Array.make 4 0 in
drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
let sa = create drr in
let x = lcp2 sa 2 in
let x = lcp sa 2 in
check {x = -1 (* TODO *)}
end
module LRS
module LRS "longest repeated substring"
use import int.Int
use import ref.Ref
......@@ -269,7 +280,7 @@ module LRS
solStart := 0;
solLength := 0;
for i=1 to a.length - 1 do
let l = SuffixArray.lcp2 sa i in
let l = SuffixArray.lcp sa i in
if l > !solLength then begin
solStart := SuffixArray.select sa i;
solLength := l
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment