package msat
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
Library containing a SAT solver that can be parametrized by a theory
Install
dune-project
Dependency
Authors
Maintainers
Sources
v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99
doc/src/msat/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 113type '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[@inline] iteri f t = for i = 0 to size t - 1 do f i (Array.unsafe_get t.data i) done let[@inline] to_seq a k = iter k a let exists p t = Iter.exists p @@ to_seq t let for_all p t = Iter.for_all p @@ to_seq t let fold f acc a = Iter.fold f acc @@ to_seq a let to_list a = Iter.to_list @@ to_seq 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)"
>