From 599a59dda9c235c21975ab62e7530c65a8ac6943 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 7 Jul 2016 14:55:48 +0200 Subject: [PATCH] Removed unused modules --- util/hashcons.ml | 97 ----------------------------------------- util/hashcons.mli | 109 ---------------------------------------------- util/hstring.ml | 91 -------------------------------------- util/hstring.mli | 78 --------------------------------- 4 files changed, 375 deletions(-) delete mode 100644 util/hashcons.ml delete mode 100644 util/hashcons.mli delete mode 100644 util/hstring.ml delete mode 100644 util/hstring.mli diff --git a/util/hashcons.ml b/util/hashcons.ml deleted file mode 100644 index c16e9e2c..00000000 --- a/util/hashcons.ml +++ /dev/null @@ -1,97 +0,0 @@ -(**************************************************************************) -(* *) -(* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) -(* Andrei Paskevich *) -(* *) -(* This software is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Library General Public *) -(* License version 2.1, with the special exception on linking *) -(* described in file LICENSE. *) -(* *) -(* This software is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) -(* *) -(**************************************************************************) - -(*s Hash tables for hash-consing. (Some code is borrowed from the ocaml - standard library, which is copyright 1996 INRIA.) *) - -module type HashedType = -sig - type t - val equal : t -> t -> bool - val hash : t -> int - val tag : int -> t -> t -end - -module type S = -sig - type t - val hashcons : t -> t - val iter : (t -> unit) -> unit - val stats : unit -> int * int * int * int * int * int -end - -module Make(H : HashedType) : (S with type t = H.t) = -struct - type t = H.t - - module WH = Weak.Make (H) - - let next_tag = ref 0 - - let htable = WH.create 5003 - - let hashcons d = - let d = H.tag !next_tag d in - let o = WH.merge htable d in - if o == d then incr next_tag; - o - - let iter f = WH.iter f htable - - let stats () = WH.stats htable -end - -let combine acc n = n * 65599 + acc -let combine2 acc n1 n2 = combine acc (combine n1 n2) -let combine3 acc n1 n2 n3 = combine acc (combine n1 (combine n2 n3)) -let combine_list f = List.fold_left (fun acc x -> combine acc (f x)) -let combine_option h = function None -> 0 | Some s -> (h s) + 1 -let combine_pair h1 h2 (a1,a2) = combine (h1 a1) (h2 a2) - -type 'a hash_consed = { - tag : int; - node : 'a } - -module type HashedType_consed = -sig - type t - val equal : t -> t -> bool - val hash : t -> int -end - -module type S_consed = -sig - type key - val hashcons : key -> key hash_consed - val iter : (key hash_consed -> unit) -> unit - val stats : unit -> int * int * int * int * int * int -end - -module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) = -struct - module M = Make(struct - type t = H.t hash_consed - let hash x = H.hash x.node - let equal x y = H.equal x.node y.node - let tag i x = {x with tag = i} - end) - include M - type key = H.t - let hashcons x = M.hashcons {tag = -1; node = x} -end diff --git a/util/hashcons.mli b/util/hashcons.mli deleted file mode 100644 index 485b4086..00000000 --- a/util/hashcons.mli +++ /dev/null @@ -1,109 +0,0 @@ -(**************************************************************************) -(* *) -(* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) -(* Andrei Paskevich *) -(* *) -(* This software is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Library General Public *) -(* License version 2.1, with the special exception on linking *) -(* described in file LICENSE. *) -(* *) -(* This software is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) -(* *) -(**************************************************************************) - -(** Hash tables for hash consing *) - -(*s Hash tables for hash consing. - - Hash consed values are of the - following type [hash_consed]. The field [tag] contains a unique - integer (for values hash consed with the same table). The field - [hkey] contains the hash key of the value (without modulo) for - possible use in other hash tables (and internally when hash - consing tables are resized). The field [node] contains the value - itself. - - Hash consing tables are using weak pointers, so that values that are no - more referenced from anywhere else can be erased by the GC. *) - -module type HashedType = -sig - type t - val equal : t -> t -> bool - val hash : t -> int - val tag : int -> t -> t -end - -module type S = -sig - type t - - val hashcons : t -> t - (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns - any existing value in the table equal to [n], if any; - otherwise, creates a new value with function [f], stores it - in the table and returns it. Function [f] is passed - the node [n] as first argument and the unique id as second argument. - *) - - val iter : (t -> unit) -> unit - (** [iter f] iterates [f] over all elements of the table . *) - val stats : unit -> int * int * int * int * int * int - (** Return statistics on the table. The numbers are, in order: - table length, number of entries, sum of bucket lengths, - smallest bucket length, median bucket length, biggest - bucket length. *) -end - -module Make(H : HashedType) : (S with type t = H.t) - - -(* helpers *) - -val combine : int -> int -> int -val combine2 : int -> int -> int -> int -val combine3 : int -> int -> int -> int -> int -val combine_list : ('a -> int) -> int -> 'a list -> int -val combine_option : ('a -> int) -> 'a option -> int -val combine_pair : ('a -> int) -> ('b -> int) -> 'a * 'b -> int - -(* For simple use *) -type 'a hash_consed = private { - tag : int; - node : 'a } - -module type HashedType_consed = -sig - type t - val equal : t -> t -> bool - val hash : t -> int -end - -module type S_consed = -sig - type key - - val hashcons : key -> key hash_consed - (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns - any existing value in the table equal to [n], if any; - otherwise, creates a new value with function [f], stores it - in the table and returns it. Function [f] is passed - the node [n] as first argument and the unique id as second argument. - *) - - val iter : (key hash_consed -> unit) -> unit - (** [iter f] iterates [f] over all elements of the table . *) - val stats : unit -> int * int * int * int * int * int - (** Return statistics on the table. The numbers are, in order: - table length, number of entries, sum of bucket lengths, - smallest bucket length, median bucket length, biggest - bucket length. *) -end - -module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) diff --git a/util/hstring.ml b/util/hstring.ml deleted file mode 100644 index 4a0004bf..00000000 --- a/util/hstring.ml +++ /dev/null @@ -1,91 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Hashcons - -module S = - Hashcons.Make_consed(struct include String - let hash = Hashtbl.hash - let equal = (=) end) - -module HS = struct - - type t = string Hashcons.hash_consed - - let make s = S.hashcons s - - let view s = s.node - - let equal s1 s2 = s1.tag = s2.tag - - let compare s1 s2 = compare s1.tag s2.tag - - let hash s = s.tag - - let empty = make "" - - let rec list_assoc x = function - | [] -> raise Not_found - | (y, v) :: l -> if equal x y then v else list_assoc x l - - let rec list_mem_assoc x = function - | [] -> false - | (y, _) :: l -> compare x y = 0 || list_mem_assoc x l - - let rec list_mem x = function - | [] -> false - | y :: l -> compare x y = 0 || list_mem x l - - let compare_couple (x1,y1) (x2,y2) = - let c = compare x1 x2 in - if c <> 0 then c - else compare y1 y2 - - let rec compare_list l1 l2 = - match l1, l2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::r1, y::r2 -> - let c = compare x y in - if c <> 0 then c - else compare_list r1 r2 - - let rec list_mem_couple c = function - | [] -> false - | d :: l -> compare_couple c d = 0 || list_mem_couple c l - - let print fmt s = - Format.fprintf fmt "%s" (view s) - -end - -include HS - -module H = Hashtbl.Make(HS) - -module HSet = Set.Make(HS) - -module HMap = Map.Make(HS) - -(* struct *) -(* include Hashtbl.Make(HS) *) - -(* let find x h = *) -(* TimeHS.start (); *) -(* try *) -(* let r = find x h in *) -(* TimeHS.pause (); *) -(* r *) -(* with Not_found -> TimeHS.pause (); raise Not_found *) -(* end *) diff --git a/util/hstring.mli b/util/hstring.mli deleted file mode 100644 index 33a39652..00000000 --- a/util/hstring.mli +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -(** {b Hash-consed strings} - - Hash-consing is a technique to share values that are structurally - equal. More details on - {{:http://en.wikipedia.org/wiki/Hash_consing} Wikipedia} and - {{:http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf} here}. - - This module provides an easy way to use hash-consing for strings. -*) - -open Hashcons - -type t = string hash_consed -(** The type of Hash-consed string *) - -val make : string -> t -(** [make s] builds ans returns a hash-consed string from [s].*) - -val view : t -> string -(** [view hs] returns the string corresponding to [hs].*) - -val equal : t -> t -> bool -(** [equal x y] returns [true] if [x] and [y] are the same hash-consed string - (constant time).*) - -val compare : t -> t -> int -(** [compares x y] returns [0] if [x] and [y] are equal, and is unspecified - otherwise but provides a total ordering on hash-consed strings.*) - -val hash : t -> int -(** [hash x] returns the integer (hash) associated to [x].*) - -val empty : t -(** the empty ([""]) hash-consed string.*) - -val list_assoc : t -> (t * 'a) list -> 'a -(** [list_assoc x l] returns the element associated with [x] in the list of - pairs [l]. - @raise Not_found if there is no value associated with [x] in the list [l].*) - -val list_mem_assoc : t -> (t * 'a) list -> bool -(** Same as {! list_assoc}, but simply returns [true] if a binding exists, and - [false] if no bindings exist for the given key.*) - -val list_mem : t -> t list -> bool -(** [list_mem x l] is [true] if and only if [x] is equal to an element of [l].*) - -val list_mem_couple : t * t -> (t * t) list -> bool -(** [list_mem_couple (x,y) l] is [true] if and only if [(x,y)] is equal to an - element of [l].*) - -val compare_list : t list -> t list -> int -(** [compare_list l1 l2] returns [0] if and only if [l1] is equal to [l2].*) - -val print : Format.formatter -> t -> unit -(** Prints a list of hash-consed strings on a formatter. *) - -module H : Hashtbl.S with type key = t -(** Hash-tables indexed by hash-consed strings *) - -module HSet : Set.S with type elt = t -(** Sets of hash-consed strings *) - -module HMap : Map.S with type key = t -(** Maps indexed by hash-consed strings *)