Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

src/utils/utils.ml
41 41
module IMap = struct
42 42
  include Map.Make (IdentModule)
43 43

  
44
  let union_l m1 m2 =
44
  let diff m1 m2 =
45 45
    merge
46 46
      (fun _ o1 o2 ->
47 47
        match o1, o2 with
48
        | None, None ->
49
          None
50
        | Some _, _ ->
51
          o1
52
        | _, Some _ ->
53
          o2)
48
        | Some v1, Some v2 ->
49
          if v1 = v2 then None else o1
50
        | _ ->
51
          o1)
54 52
      m1 m2
53

  
54
  let of_list l = List.fold_left (fun m (x, v) -> add x v m) empty l
55 55
end
56 56

  
57 57
module ISet = Set.Make (IdentModule)
......
123 123
    | t :: q ->
124 124
      if p t then t :: filter_upto p (n - 1) q else filter_upto p n q
125 125

  
126
(* Warning: bad complexity *)
127
let list_of_imap imap =
128
  IMap.fold (fun i v (il, vl) -> i :: il, v :: vl) imap ([], [])
129

  
130 126
(** [gcd a b] returns the greatest common divisor of [a] and [b]. *)
131 127
let rec gcd a b = if b = 0 then a else gcd b (a mod b)
132 128

  

Also available in: Unified diff