intervals.ml 9.93 KB
Newer Older
1 2
open Big_int

3 4
module V = struct

5 6 7 8
(* Hack to compute hash value for bigints *)
let hash_nat x = Nat.nth_digit_nat x 0
let hash_bigint (sign,nat) = sign * 17 + hash_nat nat

9 10 11 12 13 14 15 16 17
type t = big_int
let print ppf i = Format.fprintf ppf "%s" (string_of_big_int i)
let dump = print
let compare = compare_big_int
let hash x = hash_bigint (Obj.magic x)
let equal = eq_big_int

let check i = ()

18
let from_int i = big_int_of_int i
19
let from_bigint i = i
20

21
let mk = big_int_of_string
22
let to_string = string_of_big_int
23
let get_int = int_of_big_int
24
let get_bigint i = i
25
let is_int = is_int_big_int
26 27 28 29 30
let add = add_big_int
let mult = mult_big_int
let sub = sub_big_int
let div = div_big_int
let modulo  = mod_big_int
31 32
let succ = succ_big_int
let pred = pred_big_int
33
let negat t = sub_big_int zero_big_int t
34 35 36

let lt = lt_big_int
let gt = gt_big_int
37

38 39 40
let zero = big_int_of_int 0
let one = big_int_of_int 1
let minus_one = big_int_of_int (-1)
41
let is_zero = equal zero
42 43 44 45 46

let from_int32 i = mk (Int32.to_string i)
let from_int64 i = mk (Int64.to_string i)
let to_int32 i = Int32.of_string (to_string i)
let to_int64 i = Int64.of_string (to_string i)
47
end
48

49
type interval =
50 51 52 53 54 55
  | Bounded of big_int * big_int
  | Left of big_int
  | Right of big_int
  | Any

type t = interval list
56 57 58 59 60

let dump ppf _ = Format.fprintf ppf "<Intervals.t>"

let rec check = function
  | []
61
  | [ Any ] | [ Right _ ] | [ Left _ ] | [ Bounded _ ] -> ()
62 63 64 65
  | (Left i | Bounded (_,i)) :: ((Bounded (j,_) | (Right j)) :: _ as rem) ->
      assert (V.compare i j < 0);
      check rem
  | _ -> assert false
66

67 68 69 70 71 72
let rec compare l1 l2 =
  match (l1,l2) with
    | [], [] -> 0
    | [],_ -> -1
    | _,[] -> 1
    | Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2 ->
73
	let c = V.compare a1 a2 in if c <> 0 then c
74
	else let c = V.compare b1 b2 in if c <> 0 then c
75 76 77 78 79
	else compare l1 l2
    | Bounded (_,_) :: _, _ -> -1
    | _, Bounded (_,_) :: _ -> 1

    | Left a1 :: l1, Left a2 :: l2 ->
80
	let c = V.compare a1 a2 in if c <> 0 then c
81 82 83 84 85
	else compare l1 l2
    | Left _ :: _, _ -> -1
    | _, Left _ :: _ -> 1

    | Right a1 :: l1, Right a2 :: l2 ->
86
	let c = V.compare a1 a2 in if c <> 0 then c
87 88 89 90 91 92
	else compare l1 l2
    | Right _ :: _, _ -> -1
    | _, Right _ :: _ -> 1

    | Any :: _, Any :: _ -> 0

93

94
let rec equal l1 l2 =
95
  (l1 == l2) ||
96 97 98 99 100 101 102 103 104 105 106 107
  match (l1,l2) with
    | (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) ->
	(eq_big_int a1 a2) &&
	(eq_big_int b1 b2) &&
	(equal l1 l2)
    | (Left b1 :: l1, Left b2 :: l2) ->
	(eq_big_int b1 b2) &&
	(equal l1 l2)
    | (Right a1 :: l1, Right a2 :: l2) ->
	(eq_big_int a1 a2) &&
	(equal l1 l2)
    | (Any :: _, Any :: _) -> true
108
    | ([], []) -> true
109 110
    | _ -> false

111 112
let rec hash accu = function
  | Bounded (a,b) :: rem  ->
113
      hash (1 + 2 * (V.hash a) + 3 * (V.hash b) + 17 * accu) rem
114
  | Left b :: rem ->
115
      hash (3 * V.hash b + 17 * accu) rem
116
  | Right a :: _ ->
117
      2 * (V.hash a) + 17 * accu
118 119
  | Any :: _ -> 17 * accu + 1234
  | [] -> accu + 3
120

121 122
let hash = hash 0

123
let empty = []
124 125
let any = [Any]

Pietro Abate's avatar
Pietro Abate committed
126 127 128 129
(* this is to have a uniform signature of all basic types *)
type elem = V.t
let full = any

130
let bounded a b =
131
  if le_big_int a b then [Bounded (a,b)] else empty
132

133 134 135 136
let left a = [Left a]
let right a = [Right a]
let atom a = bounded a a

137

138
let rec iadd_left l b = match l with
139 140
  | [] -> [Left b]
  | (Bounded (a1,_) | Right a1) :: _
141
      when (lt_big_int b (pred_big_int a1)) ->
142
      Left b :: l
143
  | Bounded (_,b1) :: l' ->
144
      iadd_left l' (max_big_int b b1)
145 146
  | Left b1 :: _ when le_big_int b b1-> l
  | Left _ :: l' ->
147
      iadd_left l' b
148
  | _ -> any
149

150
let rec iadd_bounded l a b = match l with
151
  | [] ->
152 153
      [Bounded (a,b)]
  | (Bounded (a1,_) | Right a1) :: _
154
      when (lt_big_int b (pred_big_int a1)) ->
155
      Bounded (a,b) :: l
156 157
  | ((Bounded (_,b1) | Left b1) as i') :: l'
      when (lt_big_int (succ_big_int b1) a) ->
158
      i'::(iadd_bounded l' a b)
159
  | Bounded (a1,b1) :: l' ->
160
      iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
161
  | Left b1 :: l' ->
162
      iadd_left l' (max_big_int b b1)
163
  | Right a1 :: _ -> [Right (min_big_int a a1)]
164 165
  | Any :: _ -> any

166
let rec iadd_right l a = match l with
167
  | [] -> [Right a]
168 169
  | ((Bounded (_,b1) | Left b1) as i') :: l'
      when (lt_big_int (succ_big_int b1) a) ->
170
      i'::(iadd_right l' a)
171
  | (Bounded (a1,_) | Right a1) :: _ ->
172 173 174
      [Right (min_big_int a a1)]
  | _ -> any

175 176 177 178
let iadd l = function
  | Bounded (a,b) -> iadd_bounded l a b
  | Left b -> iadd_left l b
  | Right a -> iadd_right l a
179 180 181 182
  | Any -> any

let rec neg' start l = match l with
  | [] -> [Right start]
183
  | Bounded (a,b) :: l' ->
184 185 186 187 188 189 190 191 192 193 194
      Bounded (start, pred_big_int a) :: (neg' (succ_big_int b) l')
  | Right a :: l' ->
      [Bounded (start, pred_big_int a)]
  | _ -> assert false

let neg = function
  | Any :: _ -> []
  | [] -> any
  | Left b :: l -> neg' (succ_big_int b) l
  | Right a :: _ -> [Left (pred_big_int a)]
  | Bounded (a,b) :: l -> Left (pred_big_int a) :: neg' (succ_big_int b) l
195 196

let cup i1 i2 =
197
  List.fold_left iadd i1 i2
198 199 200 201 202 203 204

let cap i1 i2 =
  neg (cup (neg i1) (neg i2))

let diff i1 i2 =
  neg (cup (neg i1) i2)

205
let is_empty = function [] -> true | _ -> false
206

207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225
let rec disjoint a b =
  match (a,b) with
    | [],_ | _,[] -> true
    | Any::_,_ | _,Any::_ -> false
    | Left _::_, Left _::_ -> false
    | Right _::_, Right _::_ -> false
    | Left x :: a, Bounded (y,_) :: _ -> (lt_big_int x y) && (disjoint a b)
    | Bounded (y,_) :: _, Left x :: b -> (lt_big_int x y) && (disjoint a b)
    | Left x :: _, Right y :: _ -> lt_big_int x y
    | Right y :: _, Left x :: _ -> lt_big_int x y
    | Right y :: _, Bounded (_,x) :: _ -> lt_big_int x y
    | Bounded (_,x) :: _, Right y :: _ -> lt_big_int x y
    | Bounded (xa,ya) :: a', Bounded (xb,yb) :: b' ->
	let c = compare_big_int xa xb in
	if c = 0 then false
	else
	  if c < 0 then (lt_big_int ya xb) && (disjoint a' b)
	  else (lt_big_int yb xa) && (disjoint a b')

226

227
(* TODO: can optimize this to stop running through the list earlier *)
228
let contains n =
229 230 231 232 233 234
  List.exists (function
		 | Any -> true
		 | Left b -> le_big_int n b
		 | Right a -> le_big_int a n
		 | Bounded (a,b) -> (le_big_int a n) && (le_big_int n b)
	      )
235 236

let sample = function
237 238 239
  | (Left x | Right x | Bounded (x,_)) :: _ -> x
  | Any :: _ -> zero_big_int
  | [] -> raise Not_found
240

241 242 243 244
let single = function
  | [ Bounded (x,y) ] when eq_big_int x y -> x
  | [] -> raise Not_found
  | _ -> raise Exit
245

246
let print l =
247
  List.map
248 249 250
    (fun x ppf -> match x with
       | Any ->
	   Format.fprintf ppf "Int"
251 252
       | Left b ->
	   Format.fprintf ppf "*--%s"
253
	     (string_of_big_int b)
254 255
       | Right a ->
	   Format.fprintf ppf "%s--*"
256
	     (string_of_big_int a)
257 258
       | Bounded (a,b) when eq_big_int a b ->
	   Format.fprintf ppf "%s"
259 260
	     (string_of_big_int a)
       | Bounded (a,b) ->
261 262
	   Format.fprintf ppf "%s--%s"
	     (string_of_big_int a)
263
	     (string_of_big_int b)
264
    )
265
    l
266

267 268
let ( + ) = add_big_int
let ( * ) = mult_big_int
269

270 271 272
let is_bounded l =
  List.for_all (function Left _ | Any -> false | _ -> true) l,
  List.for_all (function Right _ | Any -> false | _ -> true) l
273

274
let add_inter i1 i2 =
275 276
  match (i1,i2) with
    | Bounded (a1,b1), Bounded (a2,b2) -> Bounded (a1+a2, b1+b2)
277
    | Bounded (_,b1), Left b2
278 279
    | Left b1, Bounded (_,b2)
    | Left b1, Left b2 -> Left (b1+b2)
280
    | Bounded (a1,_), Right a2
281 282 283 284 285 286 287
    | Right a1, Bounded (a2,_)
    | Right a1, Right a2 -> Right (a1+a2)
    | _ -> Any


(* Optimize this ... *)
let add l1 l2 =
288
  List.fold_left
289 290 291 292
    (fun accu i1 ->
       List.fold_left
	 (fun accu i2 -> iadd accu (add_inter i1 i2))
	 accu l2
293

294
    ) empty l1
295

296 297
let negat =
  List.rev_map
298 299 300 301 302 303 304 305 306
    (function
       | Bounded (i,j) -> Bounded (minus_big_int j, minus_big_int i)
       | Left i -> Right (minus_big_int i)
       | Right j -> Left (minus_big_int j)
       | Any -> Any
    )

let sub l1 l2 =
  add l1 (negat l2)
307

308 309
type i = PlusInf | MinusInf | Int of V.t

310
let ( * ) x y =
311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
  match (x,y) with
    | PlusInf,PlusInf | MinusInf,MinusInf -> PlusInf
    | PlusInf,MinusInf | MinusInf,PlusInf -> MinusInf
    | Int x, Int y -> Int (x * y)
    | i,(Int x as ix) | (Int x as ix), i ->
	(match i, sign_big_int x with
	   | PlusInf,1 | MinusInf,-1 -> PlusInf
	   | PlusInf,-1 | MinusInf,1 -> MinusInf
	   | _ -> ix)

let min a b =
  match (a,b) with
    | MinusInf,_ | _,PlusInf -> a
    | PlusInf,_ | _,MinusInf -> b
    | Int x, Int y -> if le_big_int x y then a else b

let max a b =
  match (a,b) with
    | MinusInf,_ | _,PlusInf -> b
    | PlusInf,_ | _,MinusInf -> a
    | Int x, Int y -> if le_big_int x y then b else a

let max4 a b c d = max a (max b (max c d))
let min4 a b c d = min a (min b (min c d))

let ival = function
  | Bounded (a,b) -> (Int a,Int b)
  | Left a -> (MinusInf,Int a)
  | Right a -> (Int a,PlusInf)
  | Any -> (MinusInf,PlusInf)

let vali = function
  | (Int a, Int b) -> Bounded (a,b)
  | (MinusInf, Int a) -> Left a
  | (Int a, PlusInf) -> Right a
  | (MinusInf, PlusInf) -> Any
  | _ -> assert false

let mul_inter i1 i2 =
  let (a1,b1) = ival i1 and (a2,b2) = ival i2 in
  let a = a1 * a2 and b = b1 * b2 and c = a1 * b2 and d = a2 * b1 in
  vali (min4 a b c d, max4 a b c d)

let mul l1 l2 =
355
  List.fold_left
356 357 358 359
    (fun accu i1 ->
       List.fold_left
	 (fun accu i2 -> iadd accu (mul_inter i1 i2))
	 accu l2
360

361 362
    ) empty l1

363

364 365 366
let div i1 i2 = any
let modulo i1 i2 = any

367
let dmp s i =
368 369
  let ppf = Format.std_formatter in
  Format.fprintf ppf "%s = [ " s;
370
  List.iter (fun x -> x ppf; Format.fprintf ppf " ") (print i);
371 372
  Format.fprintf ppf "] "

373
(*
374 375
let diff i1 i2 =
  let ppf = Format.std_formatter in
376
  Format.fprintf ppf "Intervals.diff:";
377
  dump "i1" i1;
378 379
  dump "i2" i2;
  dump "i1-i2" (diff i1 i2);
380 381
  Format.fprintf ppf "@\n";
  diff i1 i2
382 383 384 385 386 387
*)
(*
let cap i1 i2 =
  let ppf = Format.std_formatter in
  Format.fprintf ppf "Intervals.cap:";
  dmp "i1" i1;
388 389
  dmp "i2" i2;
  dmp "i1*i2" (cap i1 i2);
390 391
  Format.fprintf ppf "@.";
  cap i1 i2
392

393
*)
394 395 396

let int32 = bounded (V.from_int32 Int32.min_int) (V.from_int32 Int32.max_int)
let int64 = bounded (V.from_int64 Int64.min_int) (V.from_int64 Int64.max_int)
397 398 399 400 401 402 403


let trivially_disjoint = disjoint

let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false