|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ S E T S --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
131
|
9 -- Copyright (C) 2010-2018, Free Software Foundation, Inc. --
|
|
111
|
10 -- --
|
|
|
11 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
12 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
|
|
|
17 -- --
|
|
|
18 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
19 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
20 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
21 -- --
|
|
|
22 -- You should have received a copy of the GNU General Public License and --
|
|
|
23 -- a copy of the GCC Runtime Library Exception along with this program; --
|
|
|
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
|
|
25 -- <http://www.gnu.org/licenses/>. --
|
|
|
26 ------------------------------------------------------------------------------
|
|
|
27
|
|
|
28 with Ada.Containers.Hash_Tables.Generic_Bounded_Operations;
|
|
|
29 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations);
|
|
|
30
|
|
|
31 with Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
|
|
|
32 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
|
|
|
33
|
|
|
34 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
|
|
|
35
|
|
|
36 with System; use type System.Address;
|
|
|
37
|
|
|
38 package body Ada.Containers.Formal_Hashed_Sets with
|
|
|
39 SPARK_Mode => Off
|
|
|
40 is
|
|
|
41 -----------------------
|
|
|
42 -- Local Subprograms --
|
|
|
43 -----------------------
|
|
|
44
|
|
|
45 -- All need comments ???
|
|
|
46
|
|
|
47 procedure Difference (Left : Set; Right : Set; Target : in out Set);
|
|
|
48
|
|
|
49 function Equivalent_Keys
|
|
|
50 (Key : Element_Type;
|
|
|
51 Node : Node_Type) return Boolean;
|
|
|
52 pragma Inline (Equivalent_Keys);
|
|
|
53
|
|
|
54 procedure Free
|
|
|
55 (HT : in out Set;
|
|
|
56 X : Count_Type);
|
|
|
57
|
|
|
58 generic
|
|
|
59 with procedure Set_Element (Node : in out Node_Type);
|
|
|
60 procedure Generic_Allocate
|
|
|
61 (HT : in out Set;
|
|
|
62 Node : out Count_Type);
|
|
|
63
|
|
|
64 function Hash_Node (Node : Node_Type) return Hash_Type;
|
|
|
65 pragma Inline (Hash_Node);
|
|
|
66
|
|
|
67 procedure Insert
|
|
|
68 (Container : in out Set;
|
|
|
69 New_Item : Element_Type;
|
|
|
70 Node : out Count_Type;
|
|
|
71 Inserted : out Boolean);
|
|
|
72
|
|
|
73 procedure Intersection
|
|
|
74 (Left : Set;
|
|
|
75 Right : Set;
|
|
|
76 Target : in out Set);
|
|
|
77
|
|
|
78 function Is_In
|
|
|
79 (HT : Set;
|
|
|
80 Key : Node_Type) return Boolean;
|
|
|
81 pragma Inline (Is_In);
|
|
|
82
|
|
|
83 procedure Set_Element (Node : in out Node_Type; Item : Element_Type);
|
|
|
84 pragma Inline (Set_Element);
|
|
|
85
|
|
|
86 function Next (Node : Node_Type) return Count_Type;
|
|
|
87 pragma Inline (Next);
|
|
|
88
|
|
|
89 procedure Set_Next (Node : in out Node_Type; Next : Count_Type);
|
|
|
90 pragma Inline (Set_Next);
|
|
|
91
|
|
|
92 function Vet (Container : Set; Position : Cursor) return Boolean;
|
|
|
93
|
|
|
94 --------------------------
|
|
|
95 -- Local Instantiations --
|
|
|
96 --------------------------
|
|
|
97
|
|
|
98 package HT_Ops is new Hash_Tables.Generic_Bounded_Operations
|
|
|
99 (HT_Types => HT_Types,
|
|
|
100 Hash_Node => Hash_Node,
|
|
|
101 Next => Next,
|
|
|
102 Set_Next => Set_Next);
|
|
|
103
|
|
|
104 package Element_Keys is new Hash_Tables.Generic_Bounded_Keys
|
|
|
105 (HT_Types => HT_Types,
|
|
|
106 Next => Next,
|
|
|
107 Set_Next => Set_Next,
|
|
|
108 Key_Type => Element_Type,
|
|
|
109 Hash => Hash,
|
|
|
110 Equivalent_Keys => Equivalent_Keys);
|
|
|
111
|
|
|
112 procedure Replace_Element is
|
|
|
113 new Element_Keys.Generic_Replace_Element (Hash_Node, Set_Element);
|
|
|
114
|
|
|
115 ---------
|
|
|
116 -- "=" --
|
|
|
117 ---------
|
|
|
118
|
|
|
119 function "=" (Left, Right : Set) return Boolean is
|
|
|
120 begin
|
|
|
121 if Length (Left) /= Length (Right) then
|
|
|
122 return False;
|
|
|
123 end if;
|
|
|
124
|
|
|
125 if Length (Left) = 0 then
|
|
|
126 return True;
|
|
|
127 end if;
|
|
|
128
|
|
|
129 declare
|
|
|
130 Node : Count_Type;
|
|
|
131 ENode : Count_Type;
|
|
|
132
|
|
|
133 begin
|
|
|
134 Node := First (Left).Node;
|
|
|
135 while Node /= 0 loop
|
|
|
136 ENode :=
|
|
|
137 Find
|
|
|
138 (Container => Right,
|
|
|
139 Item => Left.Nodes (Node).Element).Node;
|
|
|
140
|
|
|
141 if ENode = 0
|
|
|
142 or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
|
|
|
143 then
|
|
|
144 return False;
|
|
|
145 end if;
|
|
|
146
|
|
|
147 Node := HT_Ops.Next (Left, Node);
|
|
|
148 end loop;
|
|
|
149
|
|
|
150 return True;
|
|
|
151 end;
|
|
|
152 end "=";
|
|
|
153
|
|
|
154 ------------
|
|
|
155 -- Assign --
|
|
|
156 ------------
|
|
|
157
|
|
|
158 procedure Assign (Target : in out Set; Source : Set) is
|
|
|
159 procedure Insert_Element (Source_Node : Count_Type);
|
|
|
160
|
|
|
161 procedure Insert_Elements is
|
|
|
162 new HT_Ops.Generic_Iteration (Insert_Element);
|
|
|
163
|
|
|
164 --------------------
|
|
|
165 -- Insert_Element --
|
|
|
166 --------------------
|
|
|
167
|
|
|
168 procedure Insert_Element (Source_Node : Count_Type) is
|
|
|
169 N : Node_Type renames Source.Nodes (Source_Node);
|
|
|
170 X : Count_Type;
|
|
|
171 B : Boolean;
|
|
|
172
|
|
|
173 begin
|
|
|
174 Insert (Target, N.Element, X, B);
|
|
|
175 pragma Assert (B);
|
|
|
176 end Insert_Element;
|
|
|
177
|
|
|
178 -- Start of processing for Assign
|
|
|
179
|
|
|
180 begin
|
|
|
181 if Target'Address = Source'Address then
|
|
|
182 return;
|
|
|
183 end if;
|
|
|
184
|
|
|
185 if Target.Capacity < Length (Source) then
|
|
|
186 raise Storage_Error with "not enough capacity"; -- SE or CE? ???
|
|
|
187 end if;
|
|
|
188
|
|
|
189 HT_Ops.Clear (Target);
|
|
|
190 Insert_Elements (Source);
|
|
|
191 end Assign;
|
|
|
192
|
|
|
193 --------------
|
|
|
194 -- Capacity --
|
|
|
195 --------------
|
|
|
196
|
|
|
197 function Capacity (Container : Set) return Count_Type is
|
|
|
198 begin
|
|
|
199 return Container.Nodes'Length;
|
|
|
200 end Capacity;
|
|
|
201
|
|
|
202 -----------
|
|
|
203 -- Clear --
|
|
|
204 -----------
|
|
|
205
|
|
|
206 procedure Clear (Container : in out Set) is
|
|
|
207 begin
|
|
|
208 HT_Ops.Clear (Container);
|
|
|
209 end Clear;
|
|
|
210
|
|
|
211 --------------
|
|
|
212 -- Contains --
|
|
|
213 --------------
|
|
|
214
|
|
|
215 function Contains (Container : Set; Item : Element_Type) return Boolean is
|
|
|
216 begin
|
|
|
217 return Find (Container, Item) /= No_Element;
|
|
|
218 end Contains;
|
|
|
219
|
|
|
220 ----------
|
|
|
221 -- Copy --
|
|
|
222 ----------
|
|
|
223
|
|
|
224 function Copy
|
|
|
225 (Source : Set;
|
|
|
226 Capacity : Count_Type := 0) return Set
|
|
|
227 is
|
|
|
228 C : constant Count_Type :=
|
|
|
229 Count_Type'Max (Capacity, Source.Capacity);
|
|
|
230 Cu : Cursor;
|
|
|
231 H : Hash_Type;
|
|
|
232 N : Count_Type;
|
|
|
233 Target : Set (C, Source.Modulus);
|
|
|
234
|
|
|
235 begin
|
|
|
236 if 0 < Capacity and then Capacity < Source.Capacity then
|
|
|
237 raise Capacity_Error;
|
|
|
238 end if;
|
|
|
239
|
|
|
240 Target.Length := Source.Length;
|
|
|
241 Target.Free := Source.Free;
|
|
|
242
|
|
|
243 H := 1;
|
|
|
244 while H <= Source.Modulus loop
|
|
|
245 Target.Buckets (H) := Source.Buckets (H);
|
|
|
246 H := H + 1;
|
|
|
247 end loop;
|
|
|
248
|
|
|
249 N := 1;
|
|
|
250 while N <= Source.Capacity loop
|
|
|
251 Target.Nodes (N) := Source.Nodes (N);
|
|
|
252 N := N + 1;
|
|
|
253 end loop;
|
|
|
254
|
|
|
255 while N <= C loop
|
|
|
256 Cu := (Node => N);
|
|
|
257 Free (Target, Cu.Node);
|
|
|
258 N := N + 1;
|
|
|
259 end loop;
|
|
|
260
|
|
|
261 return Target;
|
|
|
262 end Copy;
|
|
|
263
|
|
|
264 ---------------------
|
|
|
265 -- Default_Modulus --
|
|
|
266 ---------------------
|
|
|
267
|
|
|
268 function Default_Modulus (Capacity : Count_Type) return Hash_Type is
|
|
|
269 begin
|
|
|
270 return To_Prime (Capacity);
|
|
|
271 end Default_Modulus;
|
|
|
272
|
|
|
273 ------------
|
|
|
274 -- Delete --
|
|
|
275 ------------
|
|
|
276
|
|
|
277 procedure Delete (Container : in out Set; Item : Element_Type) is
|
|
|
278 X : Count_Type;
|
|
|
279
|
|
|
280 begin
|
|
|
281 Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
|
|
|
282
|
|
|
283 if X = 0 then
|
|
|
284 raise Constraint_Error with "attempt to delete element not in set";
|
|
|
285 end if;
|
|
|
286
|
|
|
287 Free (Container, X);
|
|
|
288 end Delete;
|
|
|
289
|
|
|
290 procedure Delete (Container : in out Set; Position : in out Cursor) is
|
|
|
291 begin
|
|
|
292 if not Has_Element (Container, Position) then
|
|
|
293 raise Constraint_Error with "Position cursor has no element";
|
|
|
294 end if;
|
|
|
295
|
|
|
296 pragma Assert (Vet (Container, Position), "bad cursor in Delete");
|
|
|
297
|
|
|
298 HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
|
|
|
299 Free (Container, Position.Node);
|
|
|
300
|
|
|
301 Position := No_Element;
|
|
|
302 end Delete;
|
|
|
303
|
|
|
304 ----------------
|
|
|
305 -- Difference --
|
|
|
306 ----------------
|
|
|
307
|
|
|
308 procedure Difference (Target : in out Set; Source : Set) is
|
|
|
309 Src_Last : Count_Type;
|
|
|
310 Src_Length : Count_Type;
|
|
|
311 Src_Node : Count_Type;
|
|
|
312 Tgt_Node : Count_Type;
|
|
|
313
|
|
|
314 TN : Nodes_Type renames Target.Nodes;
|
|
|
315 SN : Nodes_Type renames Source.Nodes;
|
|
|
316
|
|
|
317 begin
|
|
|
318 if Target'Address = Source'Address then
|
|
|
319 Clear (Target);
|
|
|
320 return;
|
|
|
321 end if;
|
|
|
322
|
|
|
323 Src_Length := Source.Length;
|
|
|
324
|
|
|
325 if Src_Length = 0 then
|
|
|
326 return;
|
|
|
327 end if;
|
|
|
328
|
|
|
329 if Src_Length >= Target.Length then
|
|
|
330 Tgt_Node := HT_Ops.First (Target);
|
|
|
331 while Tgt_Node /= 0 loop
|
|
|
332 if Element_Keys.Find (Source, TN (Tgt_Node).Element) /= 0 then
|
|
|
333 declare
|
|
|
334 X : constant Count_Type := Tgt_Node;
|
|
|
335 begin
|
|
|
336 Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
|
|
|
337 HT_Ops.Delete_Node_Sans_Free (Target, X);
|
|
|
338 Free (Target, X);
|
|
|
339 end;
|
|
|
340
|
|
|
341 else
|
|
|
342 Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
|
|
|
343 end if;
|
|
|
344 end loop;
|
|
|
345
|
|
|
346 return;
|
|
|
347 else
|
|
|
348 Src_Node := HT_Ops.First (Source);
|
|
|
349 Src_Last := 0;
|
|
|
350 end if;
|
|
|
351
|
|
|
352 while Src_Node /= Src_Last loop
|
|
|
353 Tgt_Node := Element_Keys.Find (Target, SN (Src_Node).Element);
|
|
|
354
|
|
|
355 if Tgt_Node /= 0 then
|
|
|
356 HT_Ops.Delete_Node_Sans_Free (Target, Tgt_Node);
|
|
|
357 Free (Target, Tgt_Node);
|
|
|
358 end if;
|
|
|
359
|
|
|
360 Src_Node := HT_Ops.Next (Source, Src_Node);
|
|
|
361 end loop;
|
|
|
362 end Difference;
|
|
|
363
|
|
|
364 procedure Difference (Left : Set; Right : Set; Target : in out Set) is
|
|
|
365 procedure Process (L_Node : Count_Type);
|
|
|
366
|
|
|
367 procedure Iterate is
|
|
|
368 new HT_Ops.Generic_Iteration (Process);
|
|
|
369
|
|
|
370 -------------
|
|
|
371 -- Process --
|
|
|
372 -------------
|
|
|
373
|
|
|
374 procedure Process (L_Node : Count_Type) is
|
|
|
375 B : Boolean;
|
|
|
376 E : Element_Type renames Left.Nodes (L_Node).Element;
|
|
|
377 X : Count_Type;
|
|
|
378
|
|
|
379 begin
|
|
|
380 if Find (Right, E).Node = 0 then
|
|
|
381 Insert (Target, E, X, B);
|
|
|
382 pragma Assert (B);
|
|
|
383 end if;
|
|
|
384 end Process;
|
|
|
385
|
|
|
386 -- Start of processing for Difference
|
|
|
387
|
|
|
388 begin
|
|
|
389 Iterate (Left);
|
|
|
390 end Difference;
|
|
|
391
|
|
|
392 function Difference (Left : Set; Right : Set) return Set is
|
|
|
393 C : Count_Type;
|
|
|
394 H : Hash_Type;
|
|
|
395
|
|
|
396 begin
|
|
|
397 if Left'Address = Right'Address then
|
|
|
398 return Empty_Set;
|
|
|
399 end if;
|
|
|
400
|
|
|
401 if Length (Left) = 0 then
|
|
|
402 return Empty_Set;
|
|
|
403 end if;
|
|
|
404
|
|
|
405 if Length (Right) = 0 then
|
|
|
406 return Left.Copy;
|
|
|
407 end if;
|
|
|
408
|
|
|
409 C := Length (Left);
|
|
|
410 H := Default_Modulus (C);
|
|
|
411
|
|
|
412 return S : Set (C, H) do
|
|
|
413 Difference (Left, Right, Target => S);
|
|
|
414 end return;
|
|
|
415 end Difference;
|
|
|
416
|
|
|
417 -------------
|
|
|
418 -- Element --
|
|
|
419 -------------
|
|
|
420
|
|
|
421 function Element
|
|
|
422 (Container : Set;
|
|
|
423 Position : Cursor) return Element_Type
|
|
|
424 is
|
|
|
425 begin
|
|
|
426 if not Has_Element (Container, Position) then
|
|
|
427 raise Constraint_Error with "Position cursor equals No_Element";
|
|
|
428 end if;
|
|
|
429
|
|
|
430 pragma Assert
|
|
|
431 (Vet (Container, Position), "bad cursor in function Element");
|
|
|
432
|
|
|
433 return Container.Nodes (Position.Node).Element;
|
|
|
434 end Element;
|
|
|
435
|
|
|
436 ---------------------
|
|
|
437 -- Equivalent_Sets --
|
|
|
438 ---------------------
|
|
|
439
|
|
|
440 function Equivalent_Sets (Left, Right : Set) return Boolean is
|
|
|
441
|
|
|
442 function Find_Equivalent_Key
|
|
|
443 (R_HT : Hash_Table_Type'Class;
|
|
|
444 L_Node : Node_Type) return Boolean;
|
|
|
445 pragma Inline (Find_Equivalent_Key);
|
|
|
446
|
|
|
447 function Is_Equivalent is
|
|
|
448 new HT_Ops.Generic_Equal (Find_Equivalent_Key);
|
|
|
449
|
|
|
450 -------------------------
|
|
|
451 -- Find_Equivalent_Key --
|
|
|
452 -------------------------
|
|
|
453
|
|
|
454 function Find_Equivalent_Key
|
|
|
455 (R_HT : Hash_Table_Type'Class;
|
|
|
456 L_Node : Node_Type) return Boolean
|
|
|
457 is
|
|
|
458 R_Index : constant Hash_Type :=
|
|
|
459 Element_Keys.Index (R_HT, L_Node.Element);
|
|
|
460 R_Node : Count_Type := R_HT.Buckets (R_Index);
|
|
|
461 RN : Nodes_Type renames R_HT.Nodes;
|
|
|
462
|
|
|
463 begin
|
|
|
464 loop
|
|
|
465 if R_Node = 0 then
|
|
|
466 return False;
|
|
|
467 end if;
|
|
|
468
|
|
|
469 if Equivalent_Elements
|
|
|
470 (L_Node.Element, RN (R_Node).Element)
|
|
|
471 then
|
|
|
472 return True;
|
|
|
473 end if;
|
|
|
474
|
|
|
475 R_Node := HT_Ops.Next (R_HT, R_Node);
|
|
|
476 end loop;
|
|
|
477 end Find_Equivalent_Key;
|
|
|
478
|
|
|
479 -- Start of processing for Equivalent_Sets
|
|
|
480
|
|
|
481 begin
|
|
|
482 return Is_Equivalent (Left, Right);
|
|
|
483 end Equivalent_Sets;
|
|
|
484
|
|
|
485 ---------------------
|
|
|
486 -- Equivalent_Keys --
|
|
|
487 ---------------------
|
|
|
488
|
|
|
489 function Equivalent_Keys
|
|
|
490 (Key : Element_Type;
|
|
|
491 Node : Node_Type) return Boolean
|
|
|
492 is
|
|
|
493 begin
|
|
|
494 return Equivalent_Elements (Key, Node.Element);
|
|
|
495 end Equivalent_Keys;
|
|
|
496
|
|
|
497 -------------
|
|
|
498 -- Exclude --
|
|
|
499 -------------
|
|
|
500
|
|
|
501 procedure Exclude (Container : in out Set; Item : Element_Type) is
|
|
|
502 X : Count_Type;
|
|
|
503 begin
|
|
|
504 Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
|
|
|
505 Free (Container, X);
|
|
|
506 end Exclude;
|
|
|
507
|
|
|
508 ----------
|
|
|
509 -- Find --
|
|
|
510 ----------
|
|
|
511
|
|
|
512 function Find
|
|
|
513 (Container : Set;
|
|
|
514 Item : Element_Type) return Cursor
|
|
|
515 is
|
|
|
516 Node : constant Count_Type := Element_Keys.Find (Container, Item);
|
|
|
517
|
|
|
518 begin
|
|
|
519 if Node = 0 then
|
|
|
520 return No_Element;
|
|
|
521 end if;
|
|
|
522
|
|
|
523 return (Node => Node);
|
|
|
524 end Find;
|
|
|
525
|
|
|
526 -----------
|
|
|
527 -- First --
|
|
|
528 -----------
|
|
|
529
|
|
|
530 function First (Container : Set) return Cursor is
|
|
|
531 Node : constant Count_Type := HT_Ops.First (Container);
|
|
|
532
|
|
|
533 begin
|
|
|
534 if Node = 0 then
|
|
|
535 return No_Element;
|
|
|
536 end if;
|
|
|
537
|
|
|
538 return (Node => Node);
|
|
|
539 end First;
|
|
|
540
|
|
|
541 ------------------
|
|
|
542 -- Formal_Model --
|
|
|
543 ------------------
|
|
|
544
|
|
|
545 package body Formal_Model is
|
|
|
546
|
|
|
547 -------------------------
|
|
|
548 -- E_Elements_Included --
|
|
|
549 -------------------------
|
|
|
550
|
|
|
551 function E_Elements_Included
|
|
|
552 (Left : E.Sequence;
|
|
|
553 Right : E.Sequence) return Boolean
|
|
|
554 is
|
|
|
555 begin
|
|
|
556 for I in 1 .. E.Length (Left) loop
|
|
|
557 if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
|
|
|
558 then
|
|
|
559 return False;
|
|
|
560 end if;
|
|
|
561 end loop;
|
|
|
562
|
|
|
563 return True;
|
|
|
564 end E_Elements_Included;
|
|
|
565
|
|
|
566 function E_Elements_Included
|
|
|
567 (Left : E.Sequence;
|
|
|
568 Model : M.Set;
|
|
|
569 Right : E.Sequence) return Boolean
|
|
|
570 is
|
|
|
571 begin
|
|
|
572 for I in 1 .. E.Length (Left) loop
|
|
|
573 declare
|
|
|
574 Item : constant Element_Type := E.Get (Left, I);
|
|
|
575 begin
|
|
|
576 if M.Contains (Model, Item) then
|
|
|
577 if not E.Contains (Right, 1, E.Length (Right), Item) then
|
|
|
578 return False;
|
|
|
579 end if;
|
|
|
580 end if;
|
|
|
581 end;
|
|
|
582 end loop;
|
|
|
583
|
|
|
584 return True;
|
|
|
585 end E_Elements_Included;
|
|
|
586
|
|
|
587 function E_Elements_Included
|
|
|
588 (Container : E.Sequence;
|
|
|
589 Model : M.Set;
|
|
|
590 Left : E.Sequence;
|
|
|
591 Right : E.Sequence) return Boolean
|
|
|
592 is
|
|
|
593 begin
|
|
|
594 for I in 1 .. E.Length (Container) loop
|
|
|
595 declare
|
|
|
596 Item : constant Element_Type := E.Get (Container, I);
|
|
|
597 begin
|
|
|
598 if M.Contains (Model, Item) then
|
|
|
599 if not E.Contains (Left, 1, E.Length (Left), Item) then
|
|
|
600 return False;
|
|
|
601 end if;
|
|
|
602 else
|
|
|
603 if not E.Contains (Right, 1, E.Length (Right), Item) then
|
|
|
604 return False;
|
|
|
605 end if;
|
|
|
606 end if;
|
|
|
607 end;
|
|
|
608 end loop;
|
|
|
609
|
|
|
610 return True;
|
|
|
611 end E_Elements_Included;
|
|
|
612
|
|
|
613 ----------
|
|
|
614 -- Find --
|
|
|
615 ----------
|
|
|
616
|
|
|
617 function Find
|
|
|
618 (Container : E.Sequence;
|
|
|
619 Item : Element_Type) return Count_Type
|
|
|
620 is
|
|
|
621 begin
|
|
|
622 for I in 1 .. E.Length (Container) loop
|
|
|
623 if Equivalent_Elements (Item, E.Get (Container, I)) then
|
|
|
624 return I;
|
|
|
625 end if;
|
|
|
626 end loop;
|
|
|
627 return 0;
|
|
|
628 end Find;
|
|
|
629
|
|
|
630 --------------
|
|
|
631 -- Elements --
|
|
|
632 --------------
|
|
|
633
|
|
|
634 function Elements (Container : Set) return E.Sequence is
|
|
|
635 Position : Count_Type := HT_Ops.First (Container);
|
|
|
636 R : E.Sequence;
|
|
|
637
|
|
|
638 begin
|
|
|
639 -- Can't use First, Next or Element here, since they depend on models
|
|
|
640 -- for their postconditions.
|
|
|
641
|
|
|
642 while Position /= 0 loop
|
|
|
643 R := E.Add (R, Container.Nodes (Position).Element);
|
|
|
644 Position := HT_Ops.Next (Container, Position);
|
|
|
645 end loop;
|
|
|
646
|
|
|
647 return R;
|
|
|
648 end Elements;
|
|
|
649
|
|
|
650 ----------------------------
|
|
|
651 -- Lift_Abstraction_Level --
|
|
|
652 ----------------------------
|
|
|
653
|
|
|
654 procedure Lift_Abstraction_Level (Container : Set) is null;
|
|
|
655
|
|
|
656 -----------------------
|
|
|
657 -- Mapping_Preserved --
|
|
|
658 -----------------------
|
|
|
659
|
|
|
660 function Mapping_Preserved
|
|
|
661 (E_Left : E.Sequence;
|
|
|
662 E_Right : E.Sequence;
|
|
|
663 P_Left : P.Map;
|
|
|
664 P_Right : P.Map) return Boolean
|
|
|
665 is
|
|
|
666 begin
|
|
|
667 for C of P_Left loop
|
|
|
668 if not P.Has_Key (P_Right, C)
|
|
|
669 or else P.Get (P_Left, C) > E.Length (E_Left)
|
|
|
670 or else P.Get (P_Right, C) > E.Length (E_Right)
|
|
|
671 or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
|
|
672 E.Get (E_Right, P.Get (P_Right, C))
|
|
|
673 then
|
|
|
674 return False;
|
|
|
675 end if;
|
|
|
676 end loop;
|
|
|
677
|
|
|
678 return True;
|
|
|
679 end Mapping_Preserved;
|
|
|
680
|
|
|
681 ------------------------------
|
|
|
682 -- Mapping_Preserved_Except --
|
|
|
683 ------------------------------
|
|
|
684
|
|
|
685 function Mapping_Preserved_Except
|
|
|
686 (E_Left : E.Sequence;
|
|
|
687 E_Right : E.Sequence;
|
|
|
688 P_Left : P.Map;
|
|
|
689 P_Right : P.Map;
|
|
|
690 Position : Cursor) return Boolean
|
|
|
691 is
|
|
|
692 begin
|
|
|
693 for C of P_Left loop
|
|
|
694 if C /= Position
|
|
|
695 and (not P.Has_Key (P_Right, C)
|
|
|
696 or else P.Get (P_Left, C) > E.Length (E_Left)
|
|
|
697 or else P.Get (P_Right, C) > E.Length (E_Right)
|
|
|
698 or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
|
|
699 E.Get (E_Right, P.Get (P_Right, C)))
|
|
|
700 then
|
|
|
701 return False;
|
|
|
702 end if;
|
|
|
703 end loop;
|
|
|
704
|
|
|
705 return True;
|
|
|
706 end Mapping_Preserved_Except;
|
|
|
707
|
|
|
708 -----------
|
|
|
709 -- Model --
|
|
|
710 -----------
|
|
|
711
|
|
|
712 function Model (Container : Set) return M.Set is
|
|
|
713 Position : Count_Type := HT_Ops.First (Container);
|
|
|
714 R : M.Set;
|
|
|
715
|
|
|
716 begin
|
|
|
717 -- Can't use First, Next or Element here, since they depend on models
|
|
|
718 -- for their postconditions.
|
|
|
719
|
|
|
720 while Position /= 0 loop
|
|
|
721 R :=
|
|
|
722 M.Add
|
|
|
723 (Container => R,
|
|
|
724 Item => Container.Nodes (Position).Element);
|
|
|
725
|
|
|
726 Position := HT_Ops.Next (Container, Position);
|
|
|
727 end loop;
|
|
|
728
|
|
|
729 return R;
|
|
|
730 end Model;
|
|
|
731
|
|
|
732 ---------------
|
|
|
733 -- Positions --
|
|
|
734 ---------------
|
|
|
735
|
|
|
736 function Positions (Container : Set) return P.Map is
|
|
|
737 I : Count_Type := 1;
|
|
|
738 Position : Count_Type := HT_Ops.First (Container);
|
|
|
739 R : P.Map;
|
|
|
740
|
|
|
741 begin
|
|
|
742 -- Can't use First, Next or Element here, since they depend on models
|
|
|
743 -- for their postconditions.
|
|
|
744
|
|
|
745 while Position /= 0 loop
|
|
|
746 R := P.Add (R, (Node => Position), I);
|
|
|
747 pragma Assert (P.Length (R) = I);
|
|
|
748 Position := HT_Ops.Next (Container, Position);
|
|
|
749 I := I + 1;
|
|
|
750 end loop;
|
|
|
751
|
|
|
752 return R;
|
|
|
753 end Positions;
|
|
|
754
|
|
|
755 end Formal_Model;
|
|
|
756
|
|
|
757 ----------
|
|
|
758 -- Free --
|
|
|
759 ----------
|
|
|
760
|
|
|
761 procedure Free (HT : in out Set; X : Count_Type) is
|
|
|
762 begin
|
|
|
763 HT.Nodes (X).Has_Element := False;
|
|
|
764 HT_Ops.Free (HT, X);
|
|
|
765 end Free;
|
|
|
766
|
|
|
767 ----------------------
|
|
|
768 -- Generic_Allocate --
|
|
|
769 ----------------------
|
|
|
770
|
|
|
771 procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
|
|
|
772 procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
|
|
|
773 begin
|
|
|
774 Allocate (HT, Node);
|
|
|
775 HT.Nodes (Node).Has_Element := True;
|
|
|
776 end Generic_Allocate;
|
|
|
777
|
|
|
778 package body Generic_Keys with SPARK_Mode => Off is
|
|
|
779
|
|
|
780 -----------------------
|
|
|
781 -- Local Subprograms --
|
|
|
782 -----------------------
|
|
|
783
|
|
|
784 function Equivalent_Key_Node
|
|
|
785 (Key : Key_Type;
|
|
|
786 Node : Node_Type) return Boolean;
|
|
|
787 pragma Inline (Equivalent_Key_Node);
|
|
|
788
|
|
|
789 --------------------------
|
|
|
790 -- Local Instantiations --
|
|
|
791 --------------------------
|
|
|
792
|
|
|
793 package Key_Keys is new Hash_Tables.Generic_Bounded_Keys
|
|
|
794 (HT_Types => HT_Types,
|
|
|
795 Next => Next,
|
|
|
796 Set_Next => Set_Next,
|
|
|
797 Key_Type => Key_Type,
|
|
|
798 Hash => Hash,
|
|
|
799 Equivalent_Keys => Equivalent_Key_Node);
|
|
|
800
|
|
|
801 --------------
|
|
|
802 -- Contains --
|
|
|
803 --------------
|
|
|
804
|
|
|
805 function Contains
|
|
|
806 (Container : Set;
|
|
|
807 Key : Key_Type) return Boolean
|
|
|
808 is
|
|
|
809 begin
|
|
|
810 return Find (Container, Key) /= No_Element;
|
|
|
811 end Contains;
|
|
|
812
|
|
|
813 ------------
|
|
|
814 -- Delete --
|
|
|
815 ------------
|
|
|
816
|
|
|
817 procedure Delete (Container : in out Set; Key : Key_Type) is
|
|
|
818 X : Count_Type;
|
|
|
819
|
|
|
820 begin
|
|
|
821 Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
|
|
822
|
|
|
823 if X = 0 then
|
|
|
824 raise Constraint_Error with "attempt to delete key not in set";
|
|
|
825 end if;
|
|
|
826
|
|
|
827 Free (Container, X);
|
|
|
828 end Delete;
|
|
|
829
|
|
|
830 -------------
|
|
|
831 -- Element --
|
|
|
832 -------------
|
|
|
833
|
|
|
834 function Element
|
|
|
835 (Container : Set;
|
|
|
836 Key : Key_Type) return Element_Type
|
|
|
837 is
|
|
|
838 Node : constant Count_Type := Find (Container, Key).Node;
|
|
|
839
|
|
|
840 begin
|
|
|
841 if Node = 0 then
|
|
|
842 raise Constraint_Error with "key not in map";
|
|
|
843 end if;
|
|
|
844
|
|
|
845 return Container.Nodes (Node).Element;
|
|
|
846 end Element;
|
|
|
847
|
|
|
848 -------------------------
|
|
|
849 -- Equivalent_Key_Node --
|
|
|
850 -------------------------
|
|
|
851
|
|
|
852 function Equivalent_Key_Node
|
|
|
853 (Key : Key_Type;
|
|
|
854 Node : Node_Type) return Boolean
|
|
|
855 is
|
|
|
856 begin
|
|
|
857 return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element));
|
|
|
858 end Equivalent_Key_Node;
|
|
|
859
|
|
|
860 -------------
|
|
|
861 -- Exclude --
|
|
|
862 -------------
|
|
|
863
|
|
|
864 procedure Exclude (Container : in out Set; Key : Key_Type) is
|
|
|
865 X : Count_Type;
|
|
|
866 begin
|
|
|
867 Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
|
|
|
868 Free (Container, X);
|
|
|
869 end Exclude;
|
|
|
870
|
|
|
871 ----------
|
|
|
872 -- Find --
|
|
|
873 ----------
|
|
|
874
|
|
|
875 function Find
|
|
|
876 (Container : Set;
|
|
|
877 Key : Key_Type) return Cursor
|
|
|
878 is
|
|
|
879 Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
880 begin
|
|
|
881 return (if Node = 0 then No_Element else (Node => Node));
|
|
|
882 end Find;
|
|
|
883
|
|
|
884 ------------------
|
|
|
885 -- Formal_Model --
|
|
|
886 ------------------
|
|
|
887
|
|
|
888 package body Formal_Model is
|
|
|
889
|
|
|
890 -----------------------
|
|
|
891 -- M_Included_Except --
|
|
|
892 -----------------------
|
|
|
893
|
|
|
894 function M_Included_Except
|
|
|
895 (Left : M.Set;
|
|
|
896 Right : M.Set;
|
|
|
897 Key : Key_Type) return Boolean
|
|
|
898 is
|
|
|
899 begin
|
|
|
900 for E of Left loop
|
|
|
901 if not Contains (Right, E)
|
|
|
902 and not Equivalent_Keys (Generic_Keys.Key (E), Key)
|
|
|
903 then
|
|
|
904 return False;
|
|
|
905 end if;
|
|
|
906 end loop;
|
|
|
907
|
|
|
908 return True;
|
|
|
909 end M_Included_Except;
|
|
|
910
|
|
|
911 end Formal_Model;
|
|
|
912
|
|
|
913 ---------
|
|
|
914 -- Key --
|
|
|
915 ---------
|
|
|
916
|
|
|
917 function Key (Container : Set; Position : Cursor) return Key_Type is
|
|
|
918 begin
|
|
|
919 if not Has_Element (Container, Position) then
|
|
|
920 raise Constraint_Error with "Position cursor has no element";
|
|
|
921 end if;
|
|
|
922
|
|
|
923 pragma Assert
|
|
|
924 (Vet (Container, Position), "bad cursor in function Key");
|
|
|
925
|
|
|
926 declare
|
|
|
927 N : Node_Type renames Container.Nodes (Position.Node);
|
|
|
928 begin
|
|
|
929 return Key (N.Element);
|
|
|
930 end;
|
|
|
931 end Key;
|
|
|
932
|
|
|
933 -------------
|
|
|
934 -- Replace --
|
|
|
935 -------------
|
|
|
936
|
|
|
937 procedure Replace
|
|
|
938 (Container : in out Set;
|
|
|
939 Key : Key_Type;
|
|
|
940 New_Item : Element_Type)
|
|
|
941 is
|
|
|
942 Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
943
|
|
|
944 begin
|
|
|
945 if Node = 0 then
|
|
|
946 raise Constraint_Error with "attempt to replace key not in set";
|
|
|
947 end if;
|
|
|
948
|
|
|
949 Replace_Element (Container, Node, New_Item);
|
|
|
950 end Replace;
|
|
|
951
|
|
|
952 end Generic_Keys;
|
|
|
953
|
|
|
954 -----------------
|
|
|
955 -- Has_Element --
|
|
|
956 -----------------
|
|
|
957
|
|
|
958 function Has_Element (Container : Set; Position : Cursor) return Boolean is
|
|
|
959 begin
|
|
|
960 if Position.Node = 0
|
|
|
961 or else not Container.Nodes (Position.Node).Has_Element
|
|
|
962 then
|
|
|
963 return False;
|
|
|
964 end if;
|
|
|
965
|
|
|
966 return True;
|
|
|
967 end Has_Element;
|
|
|
968
|
|
|
969 ---------------
|
|
|
970 -- Hash_Node --
|
|
|
971 ---------------
|
|
|
972
|
|
|
973 function Hash_Node (Node : Node_Type) return Hash_Type is
|
|
|
974 begin
|
|
|
975 return Hash (Node.Element);
|
|
|
976 end Hash_Node;
|
|
|
977
|
|
|
978 -------------
|
|
|
979 -- Include --
|
|
|
980 -------------
|
|
|
981
|
|
|
982 procedure Include (Container : in out Set; New_Item : Element_Type) is
|
|
|
983 Inserted : Boolean;
|
|
|
984 Position : Cursor;
|
|
|
985
|
|
|
986 begin
|
|
|
987 Insert (Container, New_Item, Position, Inserted);
|
|
|
988
|
|
|
989 if not Inserted then
|
|
|
990 Container.Nodes (Position.Node).Element := New_Item;
|
|
|
991 end if;
|
|
|
992 end Include;
|
|
|
993
|
|
|
994 ------------
|
|
|
995 -- Insert --
|
|
|
996 ------------
|
|
|
997
|
|
|
998 procedure Insert
|
|
|
999 (Container : in out Set;
|
|
|
1000 New_Item : Element_Type;
|
|
|
1001 Position : out Cursor;
|
|
|
1002 Inserted : out Boolean)
|
|
|
1003 is
|
|
|
1004 begin
|
|
|
1005 Insert (Container, New_Item, Position.Node, Inserted);
|
|
|
1006 end Insert;
|
|
|
1007
|
|
|
1008 procedure Insert (Container : in out Set; New_Item : Element_Type) is
|
|
|
1009 Inserted : Boolean;
|
|
|
1010 Position : Cursor;
|
|
|
1011
|
|
|
1012 begin
|
|
|
1013 Insert (Container, New_Item, Position, Inserted);
|
|
|
1014
|
|
|
1015 if not Inserted then
|
|
|
1016 raise Constraint_Error with
|
|
|
1017 "attempt to insert element already in set";
|
|
|
1018 end if;
|
|
|
1019 end Insert;
|
|
|
1020
|
|
|
1021 procedure Insert
|
|
|
1022 (Container : in out Set;
|
|
|
1023 New_Item : Element_Type;
|
|
|
1024 Node : out Count_Type;
|
|
|
1025 Inserted : out Boolean)
|
|
|
1026 is
|
|
|
1027 procedure Allocate_Set_Element (Node : in out Node_Type);
|
|
|
1028 pragma Inline (Allocate_Set_Element);
|
|
|
1029
|
|
|
1030 function New_Node return Count_Type;
|
|
|
1031 pragma Inline (New_Node);
|
|
|
1032
|
|
|
1033 procedure Local_Insert is
|
|
|
1034 new Element_Keys.Generic_Conditional_Insert (New_Node);
|
|
|
1035
|
|
|
1036 procedure Allocate is
|
|
|
1037 new Generic_Allocate (Allocate_Set_Element);
|
|
|
1038
|
|
|
1039 ---------------------------
|
|
|
1040 -- Allocate_Set_Element --
|
|
|
1041 ---------------------------
|
|
|
1042
|
|
|
1043 procedure Allocate_Set_Element (Node : in out Node_Type) is
|
|
|
1044 begin
|
|
|
1045 Node.Element := New_Item;
|
|
|
1046 end Allocate_Set_Element;
|
|
|
1047
|
|
|
1048 --------------
|
|
|
1049 -- New_Node --
|
|
|
1050 --------------
|
|
|
1051
|
|
|
1052 function New_Node return Count_Type is
|
|
|
1053 Result : Count_Type;
|
|
|
1054 begin
|
|
|
1055 Allocate (Container, Result);
|
|
|
1056 return Result;
|
|
|
1057 end New_Node;
|
|
|
1058
|
|
|
1059 -- Start of processing for Insert
|
|
|
1060
|
|
|
1061 begin
|
|
|
1062 Local_Insert (Container, New_Item, Node, Inserted);
|
|
|
1063 end Insert;
|
|
|
1064
|
|
|
1065 ------------------
|
|
|
1066 -- Intersection --
|
|
|
1067 ------------------
|
|
|
1068
|
|
|
1069 procedure Intersection (Target : in out Set; Source : Set) is
|
|
|
1070 Tgt_Node : Count_Type;
|
|
|
1071 TN : Nodes_Type renames Target.Nodes;
|
|
|
1072
|
|
|
1073 begin
|
|
|
1074 if Target'Address = Source'Address then
|
|
|
1075 return;
|
|
|
1076 end if;
|
|
|
1077
|
|
|
1078 if Source.Length = 0 then
|
|
|
1079 Clear (Target);
|
|
|
1080 return;
|
|
|
1081 end if;
|
|
|
1082
|
|
|
1083 Tgt_Node := HT_Ops.First (Target);
|
|
|
1084 while Tgt_Node /= 0 loop
|
|
|
1085 if Find (Source, TN (Tgt_Node).Element).Node /= 0 then
|
|
|
1086 Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
|
|
|
1087
|
|
|
1088 else
|
|
|
1089 declare
|
|
|
1090 X : constant Count_Type := Tgt_Node;
|
|
|
1091 begin
|
|
|
1092 Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
|
|
|
1093 HT_Ops.Delete_Node_Sans_Free (Target, X);
|
|
|
1094 Free (Target, X);
|
|
|
1095 end;
|
|
|
1096 end if;
|
|
|
1097 end loop;
|
|
|
1098 end Intersection;
|
|
|
1099
|
|
|
1100 procedure Intersection (Left : Set; Right : Set; Target : in out Set) is
|
|
|
1101 procedure Process (L_Node : Count_Type);
|
|
|
1102
|
|
|
1103 procedure Iterate is
|
|
|
1104 new HT_Ops.Generic_Iteration (Process);
|
|
|
1105
|
|
|
1106 -------------
|
|
|
1107 -- Process --
|
|
|
1108 -------------
|
|
|
1109
|
|
|
1110 procedure Process (L_Node : Count_Type) is
|
|
|
1111 E : Element_Type renames Left.Nodes (L_Node).Element;
|
|
|
1112 X : Count_Type;
|
|
|
1113 B : Boolean;
|
|
|
1114
|
|
|
1115 begin
|
|
|
1116 if Find (Right, E).Node /= 0 then
|
|
|
1117 Insert (Target, E, X, B);
|
|
|
1118 pragma Assert (B);
|
|
|
1119 end if;
|
|
|
1120 end Process;
|
|
|
1121
|
|
|
1122 -- Start of processing for Intersection
|
|
|
1123
|
|
|
1124 begin
|
|
|
1125 Iterate (Left);
|
|
|
1126 end Intersection;
|
|
|
1127
|
|
|
1128 function Intersection (Left : Set; Right : Set) return Set is
|
|
|
1129 C : Count_Type;
|
|
|
1130 H : Hash_Type;
|
|
|
1131
|
|
|
1132 begin
|
|
|
1133 if Left'Address = Right'Address then
|
|
|
1134 return Left.Copy;
|
|
|
1135 end if;
|
|
|
1136
|
|
|
1137 C := Count_Type'Min (Length (Left), Length (Right)); -- ???
|
|
|
1138 H := Default_Modulus (C);
|
|
|
1139
|
|
|
1140 return S : Set (C, H) do
|
|
|
1141 if Length (Left) /= 0 and Length (Right) /= 0 then
|
|
|
1142 Intersection (Left, Right, Target => S);
|
|
|
1143 end if;
|
|
|
1144 end return;
|
|
|
1145 end Intersection;
|
|
|
1146
|
|
|
1147 --------------
|
|
|
1148 -- Is_Empty --
|
|
|
1149 --------------
|
|
|
1150
|
|
|
1151 function Is_Empty (Container : Set) return Boolean is
|
|
|
1152 begin
|
|
|
1153 return Length (Container) = 0;
|
|
|
1154 end Is_Empty;
|
|
|
1155
|
|
|
1156 -----------
|
|
|
1157 -- Is_In --
|
|
|
1158 -----------
|
|
|
1159
|
|
|
1160 function Is_In (HT : Set; Key : Node_Type) return Boolean is
|
|
|
1161 begin
|
|
|
1162 return Element_Keys.Find (HT, Key.Element) /= 0;
|
|
|
1163 end Is_In;
|
|
|
1164
|
|
|
1165 ---------------
|
|
|
1166 -- Is_Subset --
|
|
|
1167 ---------------
|
|
|
1168
|
|
|
1169 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
|
|
|
1170 Subset_Node : Count_Type;
|
|
|
1171 Subset_Nodes : Nodes_Type renames Subset.Nodes;
|
|
|
1172
|
|
|
1173 begin
|
|
|
1174 if Subset'Address = Of_Set'Address then
|
|
|
1175 return True;
|
|
|
1176 end if;
|
|
|
1177
|
|
|
1178 if Length (Subset) > Length (Of_Set) then
|
|
|
1179 return False;
|
|
|
1180 end if;
|
|
|
1181
|
|
|
1182 Subset_Node := First (Subset).Node;
|
|
|
1183 while Subset_Node /= 0 loop
|
|
|
1184 declare
|
|
|
1185 N : Node_Type renames Subset_Nodes (Subset_Node);
|
|
|
1186 E : Element_Type renames N.Element;
|
|
|
1187
|
|
|
1188 begin
|
|
|
1189 if Find (Of_Set, E).Node = 0 then
|
|
|
1190 return False;
|
|
|
1191 end if;
|
|
|
1192 end;
|
|
|
1193
|
|
|
1194 Subset_Node := HT_Ops.Next (Subset, Subset_Node);
|
|
|
1195 end loop;
|
|
|
1196
|
|
|
1197 return True;
|
|
|
1198 end Is_Subset;
|
|
|
1199
|
|
|
1200 ------------
|
|
|
1201 -- Length --
|
|
|
1202 ------------
|
|
|
1203
|
|
|
1204 function Length (Container : Set) return Count_Type is
|
|
|
1205 begin
|
|
|
1206 return Container.Length;
|
|
|
1207 end Length;
|
|
|
1208
|
|
|
1209 ----------
|
|
|
1210 -- Move --
|
|
|
1211 ----------
|
|
|
1212
|
|
|
1213 -- Comments???
|
|
|
1214
|
|
|
1215 procedure Move (Target : in out Set; Source : in out Set) is
|
|
|
1216 NN : HT_Types.Nodes_Type renames Source.Nodes;
|
|
|
1217 X, Y : Count_Type;
|
|
|
1218
|
|
|
1219 begin
|
|
|
1220 if Target'Address = Source'Address then
|
|
|
1221 return;
|
|
|
1222 end if;
|
|
|
1223
|
|
|
1224 if Target.Capacity < Length (Source) then
|
|
|
1225 raise Constraint_Error with -- ???
|
|
|
1226 "Source length exceeds Target capacity";
|
|
|
1227 end if;
|
|
|
1228
|
|
|
1229 Clear (Target);
|
|
|
1230
|
|
|
1231 if Source.Length = 0 then
|
|
|
1232 return;
|
|
|
1233 end if;
|
|
|
1234
|
|
|
1235 X := HT_Ops.First (Source);
|
|
|
1236 while X /= 0 loop
|
|
|
1237 Insert (Target, NN (X).Element); -- optimize???
|
|
|
1238
|
|
|
1239 Y := HT_Ops.Next (Source, X);
|
|
|
1240
|
|
|
1241 HT_Ops.Delete_Node_Sans_Free (Source, X);
|
|
|
1242 Free (Source, X);
|
|
|
1243
|
|
|
1244 X := Y;
|
|
|
1245 end loop;
|
|
|
1246 end Move;
|
|
|
1247
|
|
|
1248 ----------
|
|
|
1249 -- Next --
|
|
|
1250 ----------
|
|
|
1251
|
|
|
1252 function Next (Node : Node_Type) return Count_Type is
|
|
|
1253 begin
|
|
|
1254 return Node.Next;
|
|
|
1255 end Next;
|
|
|
1256
|
|
|
1257 function Next (Container : Set; Position : Cursor) return Cursor is
|
|
|
1258 begin
|
|
|
1259 if Position.Node = 0 then
|
|
|
1260 return No_Element;
|
|
|
1261 end if;
|
|
|
1262
|
|
|
1263 if not Has_Element (Container, Position) then
|
|
|
1264 raise Constraint_Error with "Position has no element";
|
|
|
1265 end if;
|
|
|
1266
|
|
|
1267 pragma Assert (Vet (Container, Position), "bad cursor in Next");
|
|
|
1268
|
|
|
1269 return (Node => HT_Ops.Next (Container, Position.Node));
|
|
|
1270 end Next;
|
|
|
1271
|
|
|
1272 procedure Next (Container : Set; Position : in out Cursor) is
|
|
|
1273 begin
|
|
|
1274 Position := Next (Container, Position);
|
|
|
1275 end Next;
|
|
|
1276
|
|
|
1277 -------------
|
|
|
1278 -- Overlap --
|
|
|
1279 -------------
|
|
|
1280
|
|
|
1281 function Overlap (Left, Right : Set) return Boolean is
|
|
|
1282 Left_Node : Count_Type;
|
|
|
1283 Left_Nodes : Nodes_Type renames Left.Nodes;
|
|
|
1284
|
|
|
1285 begin
|
|
|
1286 if Length (Right) = 0 or Length (Left) = 0 then
|
|
|
1287 return False;
|
|
|
1288 end if;
|
|
|
1289
|
|
|
1290 if Left'Address = Right'Address then
|
|
|
1291 return True;
|
|
|
1292 end if;
|
|
|
1293
|
|
|
1294 Left_Node := First (Left).Node;
|
|
|
1295 while Left_Node /= 0 loop
|
|
|
1296 declare
|
|
|
1297 N : Node_Type renames Left_Nodes (Left_Node);
|
|
|
1298 E : Element_Type renames N.Element;
|
|
|
1299 begin
|
|
|
1300 if Find (Right, E).Node /= 0 then
|
|
|
1301 return True;
|
|
|
1302 end if;
|
|
|
1303 end;
|
|
|
1304
|
|
|
1305 Left_Node := HT_Ops.Next (Left, Left_Node);
|
|
|
1306 end loop;
|
|
|
1307
|
|
|
1308 return False;
|
|
|
1309 end Overlap;
|
|
|
1310
|
|
|
1311 -------------
|
|
|
1312 -- Replace --
|
|
|
1313 -------------
|
|
|
1314
|
|
|
1315 procedure Replace (Container : in out Set; New_Item : Element_Type) is
|
|
|
1316 Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
|
|
|
1317
|
|
|
1318 begin
|
|
|
1319 if Node = 0 then
|
|
|
1320 raise Constraint_Error with "attempt to replace element not in set";
|
|
|
1321 end if;
|
|
|
1322
|
|
|
1323 Container.Nodes (Node).Element := New_Item;
|
|
|
1324 end Replace;
|
|
|
1325
|
|
|
1326 ---------------------
|
|
|
1327 -- Replace_Element --
|
|
|
1328 ---------------------
|
|
|
1329
|
|
|
1330 procedure Replace_Element
|
|
|
1331 (Container : in out Set;
|
|
|
1332 Position : Cursor;
|
|
|
1333 New_Item : Element_Type)
|
|
|
1334 is
|
|
|
1335 begin
|
|
|
1336 if not Has_Element (Container, Position) then
|
|
|
1337 raise Constraint_Error with "Position cursor equals No_Element";
|
|
|
1338 end if;
|
|
|
1339
|
|
|
1340 pragma Assert
|
|
|
1341 (Vet (Container, Position), "bad cursor in Replace_Element");
|
|
|
1342
|
|
|
1343 Replace_Element (Container, Position.Node, New_Item);
|
|
|
1344 end Replace_Element;
|
|
|
1345
|
|
|
1346 ----------------------
|
|
|
1347 -- Reserve_Capacity --
|
|
|
1348 ----------------------
|
|
|
1349
|
|
|
1350 procedure Reserve_Capacity
|
|
|
1351 (Container : in out Set;
|
|
|
1352 Capacity : Count_Type)
|
|
|
1353 is
|
|
|
1354 begin
|
|
|
1355 if Capacity > Container.Capacity then
|
|
|
1356 raise Constraint_Error with "requested capacity is too large";
|
|
|
1357 end if;
|
|
|
1358 end Reserve_Capacity;
|
|
|
1359
|
|
|
1360 ------------------
|
|
|
1361 -- Set_Element --
|
|
|
1362 ------------------
|
|
|
1363
|
|
|
1364 procedure Set_Element (Node : in out Node_Type; Item : Element_Type) is
|
|
|
1365 begin
|
|
|
1366 Node.Element := Item;
|
|
|
1367 end Set_Element;
|
|
|
1368
|
|
|
1369 --------------
|
|
|
1370 -- Set_Next --
|
|
|
1371 --------------
|
|
|
1372
|
|
|
1373 procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is
|
|
|
1374 begin
|
|
|
1375 Node.Next := Next;
|
|
|
1376 end Set_Next;
|
|
|
1377
|
|
|
1378 --------------------------
|
|
|
1379 -- Symmetric_Difference --
|
|
|
1380 --------------------------
|
|
|
1381
|
|
|
1382 procedure Symmetric_Difference (Target : in out Set; Source : Set) is
|
|
|
1383 procedure Process (Source_Node : Count_Type);
|
|
|
1384 pragma Inline (Process);
|
|
|
1385
|
|
|
1386 procedure Iterate is new HT_Ops.Generic_Iteration (Process);
|
|
|
1387
|
|
|
1388 -------------
|
|
|
1389 -- Process --
|
|
|
1390 -------------
|
|
|
1391
|
|
|
1392 procedure Process (Source_Node : Count_Type) is
|
|
|
1393 B : Boolean;
|
|
|
1394 N : Node_Type renames Source.Nodes (Source_Node);
|
|
|
1395 X : Count_Type;
|
|
|
1396
|
|
|
1397 begin
|
|
|
1398 if Is_In (Target, N) then
|
|
|
1399 Delete (Target, N.Element);
|
|
|
1400 else
|
|
|
1401 Insert (Target, N.Element, X, B);
|
|
|
1402 pragma Assert (B);
|
|
|
1403 end if;
|
|
|
1404 end Process;
|
|
|
1405
|
|
|
1406 -- Start of processing for Symmetric_Difference
|
|
|
1407
|
|
|
1408 begin
|
|
|
1409 if Target'Address = Source'Address then
|
|
|
1410 Clear (Target);
|
|
|
1411 return;
|
|
|
1412 end if;
|
|
|
1413
|
|
|
1414 if Length (Target) = 0 then
|
|
|
1415 Assign (Target, Source);
|
|
|
1416 return;
|
|
|
1417 end if;
|
|
|
1418
|
|
|
1419 Iterate (Source);
|
|
|
1420 end Symmetric_Difference;
|
|
|
1421
|
|
|
1422 function Symmetric_Difference (Left : Set; Right : Set) return Set is
|
|
|
1423 C : Count_Type;
|
|
|
1424 H : Hash_Type;
|
|
|
1425
|
|
|
1426 begin
|
|
|
1427 if Left'Address = Right'Address then
|
|
|
1428 return Empty_Set;
|
|
|
1429 end if;
|
|
|
1430
|
|
|
1431 if Length (Right) = 0 then
|
|
|
1432 return Left.Copy;
|
|
|
1433 end if;
|
|
|
1434
|
|
|
1435 if Length (Left) = 0 then
|
|
|
1436 return Right.Copy;
|
|
|
1437 end if;
|
|
|
1438
|
|
|
1439 C := Length (Left) + Length (Right);
|
|
|
1440 H := Default_Modulus (C);
|
|
|
1441
|
|
|
1442 return S : Set (C, H) do
|
|
|
1443 Difference (Left, Right, S);
|
|
|
1444 Difference (Right, Left, S);
|
|
|
1445 end return;
|
|
|
1446 end Symmetric_Difference;
|
|
|
1447
|
|
|
1448 ------------
|
|
|
1449 -- To_Set --
|
|
|
1450 ------------
|
|
|
1451
|
|
|
1452 function To_Set (New_Item : Element_Type) return Set is
|
|
|
1453 X : Count_Type;
|
|
|
1454 B : Boolean;
|
|
|
1455
|
|
|
1456 begin
|
|
|
1457 return S : Set (Capacity => 1, Modulus => 1) do
|
|
|
1458 Insert (S, New_Item, X, B);
|
|
|
1459 pragma Assert (B);
|
|
|
1460 end return;
|
|
|
1461 end To_Set;
|
|
|
1462
|
|
|
1463 -----------
|
|
|
1464 -- Union --
|
|
|
1465 -----------
|
|
|
1466
|
|
|
1467 procedure Union (Target : in out Set; Source : Set) is
|
|
|
1468 procedure Process (Src_Node : Count_Type);
|
|
|
1469
|
|
|
1470 procedure Iterate is
|
|
|
1471 new HT_Ops.Generic_Iteration (Process);
|
|
|
1472
|
|
|
1473 -------------
|
|
|
1474 -- Process --
|
|
|
1475 -------------
|
|
|
1476
|
|
|
1477 procedure Process (Src_Node : Count_Type) is
|
|
|
1478 N : Node_Type renames Source.Nodes (Src_Node);
|
|
|
1479 E : Element_Type renames N.Element;
|
|
|
1480
|
|
|
1481 X : Count_Type;
|
|
|
1482 B : Boolean;
|
|
|
1483
|
|
|
1484 begin
|
|
|
1485 Insert (Target, E, X, B);
|
|
|
1486 end Process;
|
|
|
1487
|
|
|
1488 -- Start of processing for Union
|
|
|
1489
|
|
|
1490 begin
|
|
|
1491 if Target'Address = Source'Address then
|
|
|
1492 return;
|
|
|
1493 end if;
|
|
|
1494
|
|
|
1495 Iterate (Source);
|
|
|
1496 end Union;
|
|
|
1497
|
|
|
1498 function Union (Left : Set; Right : Set) return Set is
|
|
|
1499 C : Count_Type;
|
|
|
1500 H : Hash_Type;
|
|
|
1501
|
|
|
1502 begin
|
|
|
1503 if Left'Address = Right'Address then
|
|
|
1504 return Left.Copy;
|
|
|
1505 end if;
|
|
|
1506
|
|
|
1507 if Length (Right) = 0 then
|
|
|
1508 return Left.Copy;
|
|
|
1509 end if;
|
|
|
1510
|
|
|
1511 if Length (Left) = 0 then
|
|
|
1512 return Right.Copy;
|
|
|
1513 end if;
|
|
|
1514
|
|
|
1515 C := Length (Left) + Length (Right);
|
|
|
1516 H := Default_Modulus (C);
|
|
|
1517 return S : Set (C, H) do
|
|
|
1518 Assign (Target => S, Source => Left);
|
|
|
1519 Union (Target => S, Source => Right);
|
|
|
1520 end return;
|
|
|
1521 end Union;
|
|
|
1522
|
|
|
1523 ---------
|
|
|
1524 -- Vet --
|
|
|
1525 ---------
|
|
|
1526
|
|
|
1527 function Vet (Container : Set; Position : Cursor) return Boolean is
|
|
|
1528 begin
|
|
|
1529 if Position.Node = 0 then
|
|
|
1530 return True;
|
|
|
1531 end if;
|
|
|
1532
|
|
|
1533 declare
|
|
|
1534 S : Set renames Container;
|
|
|
1535 N : Nodes_Type renames S.Nodes;
|
|
|
1536 X : Count_Type;
|
|
|
1537
|
|
|
1538 begin
|
|
|
1539 if S.Length = 0 then
|
|
|
1540 return False;
|
|
|
1541 end if;
|
|
|
1542
|
|
|
1543 if Position.Node > N'Last then
|
|
|
1544 return False;
|
|
|
1545 end if;
|
|
|
1546
|
|
|
1547 if N (Position.Node).Next = Position.Node then
|
|
|
1548 return False;
|
|
|
1549 end if;
|
|
|
1550
|
|
|
1551 X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element));
|
|
|
1552
|
|
|
1553 for J in 1 .. S.Length loop
|
|
|
1554 if X = Position.Node then
|
|
|
1555 return True;
|
|
|
1556 end if;
|
|
|
1557
|
|
|
1558 if X = 0 then
|
|
|
1559 return False;
|
|
|
1560 end if;
|
|
|
1561
|
|
|
1562 if X = N (X).Next then -- to prevent unnecessary looping
|
|
|
1563 return False;
|
|
|
1564 end if;
|
|
|
1565
|
|
|
1566 X := N (X).Next;
|
|
|
1567 end loop;
|
|
|
1568
|
|
|
1569 return False;
|
|
|
1570 end;
|
|
|
1571 end Vet;
|
|
|
1572
|
|
|
1573 end Ada.Containers.Formal_Hashed_Sets;
|
