Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / HashConsing.ml @ 40a714df

History | View | Annotate | Download (8.64 KB)

1 4fd28192 Thorsten WiƟmann
(** This module implements hash-consing with an emphasis on using it for formulae.
2
    It is inspired by the paper "Type-Safe Modular Hash-Consing"
3
    and by the OCaml implementation of hash tables.
4
    @author Florian Widmann
5
 *)
6
7
8
(** The elements of this type represent elements of another structure.
9
    However, it is guaranteed that structural equality and physical equality coincide.
10
    Hence the elements can only be constructed by smart constructors.
11
    An element e has the following information.
12
    (a) the first level of the original structure of e;
13
    (b) the hash value of e which is also the hash value of node;
14
    (c) the unique tag corresponding to e;
15
    (d) some data associated with e (e.g. the original structure corresponding to e);
16
    (e) the "negation" of e if "negation" is defined, or e itself otherwise;
17
    the "negation" must be a bijection such that no element is mapped onto itself,
18
    and the "negation" of the "negation" of an element is the element itself.
19
    An element and its negation are always created at the same time.
20
 *)
21
type ('a, 'b) hash_consed =
22
    { node : 'a; hkey : int; tag : int; fml : 'b; mutable neg : ('a, 'b) hash_consed }
23
24
25
(** The input signature of the functor Make.
26
 *)
27
module type HashedTyped =
28
  sig
29
    (** This type represents the first level of the original structure.
30
        Its elements are called nodes to distinguish them from the final elements.
31
     *)
32
    type nde
33
34
    (** Some data associated with elements of type nde.
35
     *)
36
    type fml
37
    
38
    (** Determines whether two nodes are structurally equal.
39
        Structural equality must be an equivalence relation.
40
        @param The first node.
41
        @param The second node.
42
        @return True iff both nodes are structurally equal.
43
     *)
44
    val equal : nde -> nde -> bool
45
46
    (** Computes the hash value of a node.
47
        Elements which are structurally equal must have the same hash value.
48
        @param A node.
49
        @return The hash value of the node.
50
     *)
51
    val hash : nde -> int
52
53
    (** Computes the data which is associated to a node.
54
        @param A node.
55
        @return The data associated with the node.
56
     *)
57
    val toFml : nde -> fml
58
59
    (** Determines the "negation" of a node.
60
        For ever node n it must hold that "negNde (negNde n)" is structurally equal to n,
61
        that "negNde n" is not structurally equal to n, 
62
        and that structural equivalence is a congruence w.r.t. negation.
63
        If there is no meaningful concept of "negation",
64
        this can be a dummy function (e.g. throwing an exception).
65
        @param A node.
66
        @return The negation of the node.
67
     *)
68
    val negNde : nde -> nde
69
  end
70
71
72
(** The output signature of the functor Make.
73
    See functor Make for further information.
74
 *)
75
module type S =
76
  sig
77
    type t
78
    type nde
79
    type fml
80
    val create : ?size:int -> bool -> t
81
    val hashcons : t -> nde -> (nde, fml) hash_consed
82
    val length : t -> int
83
    val iter : ((nde, fml) hash_consed -> unit) -> t -> unit
84
    val fold : ('a -> (nde, fml) hash_consed -> 'a) -> 'a -> t -> 'a
85
  end
86
87
module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
88
  struct
89
    (** This type represents the first level of the original structure.
90
        Its elements are called nodes to distinguish them from the final elements.
91
        Each element basically represents its node
92
        and all nodes which are structurally equal.
93
     *)
94
    type nde = H.nde
95
96
    (** Some data associated with the elements (their corresponding nodes).
97
     *)
98
    type fml = H.fml
99
100
    (** Basically a degenerated hash table (i.e. only keys, no data)
101
        which stores all elements so that structurally uniqueness can be enforced.
102
        (a) the number of elements in the hash table;
103
        (b) the hash table.
104
     *)
105
    type t = { useNeg : bool; mutable size: int; mutable data: (nde, fml) hash_consed list array }
106
107
    (** Computes a non-negative hash value for an element.
108
        It is indirectly computed via the corresponding node,
109
        which has the same hash value.
110
        @param nde A node.
111
        @return The non-negative hash value for nde.
112
     *)
113
    let realhash nde = (H.hash nde) land max_int
114
115
    (** Creates a hash-cons table.
116
        @param hasNeg True iff the nodes have "negations".
117
        @param size The initial size of the hash-cons table.
118
        @return A hash-cons table.
119
     *)
120
    let create ?(size = 1) hasNeg =
121
      let ds =
122
        if size < 1 then 1
123
        else
124
          let maxds = Sys.max_array_length in
125
          if size >= maxds then maxds else size
126
      in
127
      { useNeg = hasNeg; size = 0; data = Array.make ds [] }
128
129
    (** Resizes a hash-cons table.
130
        @param hc A hash-cons table.
131
     *)
132
    let resize hc =
133
      let odata = hc.data in
134
      let ods = Array.length odata in
135
      let nds1 = 2 * ods + 1 in
136
      let maxds = Sys.max_array_length in
137
      let nds = if nds1 < ods || nds1 > maxds then maxds else nds1 in
138
      if nds > ods then
139
        let ndata = Array.make nds [] in
140
        let iter_bucket d =
141
          let nidx = d.hkey mod nds in
142
          ndata.(nidx) <- d :: ndata.(nidx)
143
        in
144
        for i = 0 to pred ods do
145
          List.iter iter_bucket odata.(i)
146
        done;
147
        hc.data <- ndata
148
      else ()
149
150
    (** Recursively searches for an element in a bucket.
151
        @param nde A node.
152
        @param bucket The remaining bucket.
153
        @return The element whose node is structurally equal to nde.
154
        @raise Not_found if such an element does not exist (yet).
155
     *)
156
    let rec find_rec nde bucket =
157
      match bucket with
158
      | [] -> raise Not_found
159
      | d::rest ->
160
          if H.equal nde d.node then d else find_rec nde rest
161
162
    (** Searches for an element in a bucket.
163
        @param nde A node.
164
        @param bucket A bucket.
165
        @return The element whose node is structurally equal to nde.
166
        @raise Not_found if such an element does not exist (yet).
167
     *)
168
    let find nde bucket =
169
      match bucket with
170
      | [] -> raise Not_found
171
      | d1::rest1 ->
172
          if H.equal nde d1.node then d1 else
173
            match rest1 with
174
            | [] -> raise Not_found
175
            | d2::rest2 ->
176
                if H.equal nde d2.node then d2 else
177
                  match rest2 with
178
                  | [] -> raise Not_found
179
                  | d3::rest3 ->
180
                      if H.equal nde d3.node then d3 else find_rec nde rest3
181
182
    (** Retrieves the element in a hash-cons table
183
        whose node is structurally equal to nde.
184
        If such an element e does not exist yet, it will be created.
185
        If the concept of "negation" is used,
186
        the negation of e will also be inserted in this case.
187
        It is guaranteed that the tag values of both new elements are consecutive,
188
        that the smaller tag is even,
189
        and that the smaller element (according to lessThanNeg) has the smaller tag.
190
        @param hc A hash-cons table.
191
        @param nde A node.
192
        @return An element in hc whose node is structurally equal to nde.
193
     *)
194
    let hashcons hc nde =
195
      let data = hc.data in
196
      let ds = Array.length data in
197
      let hkey = realhash nde in
198
      let idx = hkey mod ds in
199
      let bucket = data.(idx) in
200
      try
201
        find nde bucket
202
      with Not_found ->
203
        let fml = H.toFml nde in
204
        let osize = hc.size in
205
        let rec nd = { node = nde; hkey = hkey; tag = osize; fml = fml; neg = nd } in
206
        data.(idx) <- nd::bucket;
207
        if hc.useNeg then
208
          let ndeN = H.negNde nde in
209
          let hkeyN = realhash ndeN in
210
          let fmlN = H.toFml ndeN in
211
          let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
212
          nd.neg <- ndN;
213
          let idxN = hkeyN mod ds in
214
          data.(idxN) <- ndN :: data.(idxN);
215
          hc.size <- osize + 2;
216
        else hc.size <- succ osize;
217
        if hc.size > ds lsl 1 then resize hc else ();
218
        nd
219
   
220
    (** Returns the number of (structurally different) elements in a hash-cons table.
221
        @param hc A hash-cons table.
222
        @return The number of elements in hc.
223
     *)
224
    let length hc = hc.size
225
226
    (** Iterates through all elements in a hash-cons table
227
        and applies a given function to them.
228
        @param fkt A function which takes an element of hc and returns void.
229
        @param hc A hash-cons table.
230
     *)
231
    let iter fkt hc = Array.iter (List.iter fkt) hc.data
232
233
    (** Iterates through all elements in a hash-cons table
234
        and applies a given function to them.
235
        @param fkt A function which takes an element of hc and returns void.
236
        @param hc A hash-cons table.
237
     *)
238
    let fold fkt init hc =
239
      Array.fold_left (fun i l -> List.fold_left fkt i l) init hc.data
240
  end