package mc2
A mcsat-based SMT solver in pure OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/src/mc2.core/Vec.ml.html
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
type 'a t = { mutable data : 'a array; mutable sz : int; } let make n x = {data=Array.make n x; sz=0} let[@inline] create () = {data = [||]; sz = 0} let[@inline] clear s = s.sz <- 0 let[@inline] shrink t i = assert (i >= 0); assert (i<=t.sz); t.sz <- i let[@inline] pop t = if t.sz = 0 then invalid_arg "vec.pop"; let x = Array.unsafe_get t.data (t.sz - 1) in t.sz <- t.sz - 1; x let[@inline] size t = t.sz let[@inline] is_empty t = t.sz = 0 let[@inline] is_full t = Array.length t.data = t.sz let[@inline] copy t : _ t = let data = Array.copy t.data in {t with data} (* grow the array *) let[@inline never] grow_to_double_size t x : unit = if Array.length t.data = Sys.max_array_length then ( failwith "vec: cannot resize"; ); let size = min Sys.max_array_length (max 4 (2 * Array.length t.data)) in let arr' = Array.make size x in Array.blit t.data 0 arr' 0 (Array.length t.data); t.data <- arr'; assert (Array.length t.data > t.sz); () let[@inline] push t x : unit = if is_full t then grow_to_double_size t x; Array.unsafe_set t.data t.sz x; t.sz <- t.sz + 1 let[@inline] get t i = if i < 0 || i >= t.sz then invalid_arg "vec.get"; Array.unsafe_get t.data i let[@inline] set t i v = if i < 0 || i > t.sz then invalid_arg "vec.set"; if i = t.sz then ( push t v ) else ( Array.unsafe_set t.data i v ) let[@inline] fast_remove t i = assert (i>= 0 && i < t.sz); Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1); t.sz <- t.sz - 1 let filter_in_place f vec = let i = ref 0 in while !i < size vec do if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i done let sort t f : unit = let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in Array.fast_sort f sub_arr; t.data <- sub_arr let[@inline] iter f t = for i = 0 to size t - 1 do f (Array.unsafe_get t.data i) done let append a b = iter (push a) b let[@inline] iteri f t = for i = 0 to size t - 1 do f i (Array.unsafe_get t.data i) done let[@inline] to_iter a k = iter k a let exists p t = Iter.exists p @@ to_iter t let for_all p t = Iter.for_all p @@ to_iter t let fold f acc a = Iter.fold f acc @@ to_iter a let to_list a = Iter.to_list @@ to_iter a let to_array a = Array.sub a.data 0 a.sz let of_list l : _ t = match l with | [] -> create() | x :: tl -> let v = make (List.length tl+1) x in List.iter (push v) l; v let pp ?(sep=", ") pp out v = let first = ref true in iter (fun x -> if !first then first := false else Format.fprintf out "%s@," sep; pp out x) v
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>