package alt-ergo-lib
Source file vec.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153(******************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) (* Copyright (C) 2013-2018 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of the license indicated *) (* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) (* present, please contact us to clarify licensing. *) (* *) (******************************************************************************) open Options type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int } let make capa d = {data = Array.make capa d; sz = 0; dummy = d} let init capa f d = {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} let from_array data sz d = {data = data; sz = sz; dummy = d} let from_list l sz d = let l = ref l in let f_init _ = match !l with [] -> assert false | e::r -> l := r; e in {data = Array.init sz f_init; sz = sz; dummy = d} let clear s = s.sz <- 0 let shrink t i fill_with_dummy = assert (i >= 0 && i<=t.sz); if fill_with_dummy then for i = t.sz - i to t.sz - 1 do t.data.(i) <- t.dummy done; t.sz <- t.sz - i let pop t = assert (t.sz >=1); t.sz <- t.sz - 1 let size t = t.sz let is_empty t = t.sz = 0 let grow_to t new_capa = let data = t.data in let capa = Array.length data in if new_capa > capa then t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy) let grow_to_double_size t = let n = max 1 (Array.length t.data) in grow_to t (2 * n) let grow_to_by_double t new_capa = let new_capa = max 1 new_capa in let data = t.data in let capa = ref (max 1 (Array.length data)) in while !capa < new_capa do capa := 2 * !capa done; grow_to t !capa let is_full t = Array.length t.data = t.sz let push t e = (*Format.eprintf "push; sz = %d et capa=%d@." t.sz (Array.length t.data);*) if is_full t then grow_to_double_size t; t.data.(t.sz) <- e; t.sz <- t.sz + 1 let push_none t = if is_full t then grow_to_double_size t; t.data.(t.sz) <- t.dummy; t.sz <- t.sz + 1 let last t = let e = t.data.(t.sz - 1) in assert (not (e == t.dummy)); e let get t i = assert (i < t.sz); let e = t.data.(i) in if e == t.dummy then raise Not_found else e let set t i v = t.data.(i) <- v; t.sz <- max t.sz (i + 1) let set_size t sz = t.sz <- sz let copy t = let data = t.data in let len = Array.length data in let data = Array.init len (fun i -> data.(i)) in { data=data; sz=t.sz; dummy = t.dummy } let move_to t t' = let data = t.data in let len = Array.length data in let data = Array.init len (fun i -> data.(i)) in t'.data <- data; t'.sz <- t.sz let remove t e = let j = ref 0 in while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; assert (!j < t.sz); for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done; pop t let fast_remove t e = let j = ref 0 in while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; assert (!j < t.sz); t.data.(!j) <- last t; pop t let sort t f = let sub_arr = Array.sub t.data 0 t.sz in Array.fast_sort f sub_arr; t.data <- sub_arr let iter vec f = for i = 0 to size vec - 1 do f (get vec i) done (* template<class V, class T> static inline void remove(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); assert(j < ts.size()); ts[j] = ts.last(); ts.pop(); } #endif template<class V, class T> static inline bool find(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); return j < ts.size(); } #endif *)