mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-05 19:00:33 -05:00
remove useless dir
This commit is contained in:
parent
875efa33c6
commit
4aed7762a7
4 changed files with 0 additions and 164 deletions
|
|
@ -1,24 +0,0 @@
|
|||
|
||||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
(** {1 Utils for Arrays} *)
|
||||
|
||||
let exists p a =
|
||||
let n = Array.length a in
|
||||
let rec loop i =
|
||||
if i = n then false
|
||||
else if p (Array.unsafe_get a i) then true
|
||||
else loop (succ i) in
|
||||
loop 0
|
||||
|
||||
let for_all p a =
|
||||
let n = Array.length a in
|
||||
let rec loop i =
|
||||
if i = n then true
|
||||
else if p (Array.unsafe_get a i) then loop (succ i)
|
||||
else false in
|
||||
loop 0
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
|
||||
module type ARG = sig
|
||||
type t
|
||||
val equal : t -> t -> bool
|
||||
val hash : t -> int
|
||||
val set_id : t -> int -> unit
|
||||
end
|
||||
|
||||
module Make(A : ARG): sig
|
||||
val hashcons : A.t -> A.t
|
||||
val iter : (A.t -> unit) -> unit
|
||||
end = struct
|
||||
module W = Weak.Make(A)
|
||||
|
||||
let tbl_ = W.create 1024
|
||||
let n_ = ref 0
|
||||
|
||||
(* hashcons terms *)
|
||||
let hashcons t =
|
||||
let t' = W.merge tbl_ t in
|
||||
if t == t' then (
|
||||
incr n_;
|
||||
A.set_id t' !n_;
|
||||
);
|
||||
t'
|
||||
|
||||
let iter yield = W.iter yield tbl_
|
||||
end
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
|
||||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
(** {1 Sparse vector, filled with default value} *)
|
||||
|
||||
let _size_too_big()=
|
||||
failwith "Sparse_vec: capacity exceeds maximum array size"
|
||||
|
||||
type 'a t = { default : 'a; mutable data : 'a array; mutable sz : int }
|
||||
|
||||
let make sz default =
|
||||
if sz > Sys.max_array_length then _size_too_big();
|
||||
{ default; sz; data=Array.make sz default; }
|
||||
|
||||
let init sz f default =
|
||||
if sz > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init sz (fun i -> f i); sz ; default}
|
||||
|
||||
let length {sz} = sz
|
||||
|
||||
let grow_to t new_capa =
|
||||
assert (new_capa >= Array.length t.data);
|
||||
let data = t.data in
|
||||
let capa = Array.length data in
|
||||
t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.default)
|
||||
|
||||
let grow_to_by_double t new_capa =
|
||||
if new_capa > Sys.max_array_length then _size_too_big ();
|
||||
let data = t.data in
|
||||
let capa = ref (Array.length data + 1) in
|
||||
while !capa < new_capa do
|
||||
capa := min (2 * !capa) Sys.max_array_length;
|
||||
done;
|
||||
grow_to t !capa
|
||||
|
||||
let resize v len =
|
||||
assert (len >= 0);
|
||||
if len <= v.sz
|
||||
then v.sz <- len
|
||||
else (
|
||||
grow_to_by_double v len;
|
||||
v.sz <- len
|
||||
)
|
||||
|
||||
let incr v = resize v (v.sz + 1)
|
||||
|
||||
let decr v =
|
||||
if v.sz = 0 then invalid_arg "Sparse_vec.decr";
|
||||
resize v (v.sz - 1)
|
||||
|
||||
let is_empty {sz} = sz=0
|
||||
|
||||
let clear v = v.sz <- 0
|
||||
|
||||
let get t i =
|
||||
if i < 0 || i >= t.sz then invalid_arg "Sparse_vec.get";
|
||||
Array.unsafe_get t.data i
|
||||
|
||||
let set t i v =
|
||||
if i < 0 || i >= t.sz then invalid_arg "Sparse_vec.set";
|
||||
t.sz <- max t.sz i;
|
||||
Array.unsafe_set t.data i v
|
||||
|
||||
|
|
@ -1,45 +0,0 @@
|
|||
|
||||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
(** {1 Sparse vector, filled with default value} *)
|
||||
|
||||
type 'a t
|
||||
(** Abstract type of sparse vectors of 'a *)
|
||||
|
||||
val make : int -> 'a -> 'a t
|
||||
(** [make cap default] creates a new vector filled with [default]. The vector's
|
||||
initial length is [cap] *)
|
||||
|
||||
val init : int -> (int -> 'a) -> 'a -> 'a t
|
||||
(** Same as {!Array.init}, but also with a default element *)
|
||||
|
||||
val length : 'a t -> int
|
||||
(** Range of valid indices *)
|
||||
|
||||
val resize : 'a t -> int -> unit
|
||||
(** Set the length of the array to [i] *)
|
||||
|
||||
val incr : 'a t -> unit
|
||||
(** Increment length size by one *)
|
||||
|
||||
val decr : 'a t -> unit
|
||||
(** Decrement length by one *)
|
||||
|
||||
val is_empty : 'a t -> bool
|
||||
(** Check whether length=0 *)
|
||||
|
||||
val clear : 'a t -> unit
|
||||
(** Set length to 0 *)
|
||||
|
||||
val get : 'a t -> int -> 'a
|
||||
(** get the element at the given index, or
|
||||
@raise Invalid_argument if the index is not valid *)
|
||||
|
||||
val set : 'a t -> int -> 'a -> unit
|
||||
(** set the element at the given index, either already set or the first
|
||||
free slot if [not (is_full vec)], or
|
||||
@raise Invalid_argument if the index is not valid *)
|
||||
Loading…
Add table
Reference in a new issue