1 /*-----------------------------------------------------------------------
2
3 File : clb_ddarrays.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Funktions realising the dynamic array type for doubles.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Sun Aug 8 22:49:36 GMT 1999
20 Copied from clb_pdarrays.c
21
22 -----------------------------------------------------------------------*/
23
24 #include "clb_ddarrays.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32
33 /*---------------------------------------------------------------------*/
34 /* Forward Declarations */
35 /*---------------------------------------------------------------------*/
36
37
38 /*---------------------------------------------------------------------*/
39 /* Internal Functions */
40 /*---------------------------------------------------------------------*/
41
42
43
44 /*---------------------------------------------------------------------*/
45 /* Exported Functions */
46 /*---------------------------------------------------------------------*/
47
48 /*-----------------------------------------------------------------------
49 //
50 // Function: DDArrayAlloc()
51 //
52 // Return an initialized dynamic array of size init_size where all
53 // elements are interpreted as pointers and initialized to NULL.
54 //
55 // Global Variables: -
56 //
57 // Side Effects : Memory Operations
58 //
59 /----------------------------------------------------------------------*/
60
DDArrayAlloc(long init_size,long grow)61 DDArray_p DDArrayAlloc(long init_size, long grow)
62 {
63 DDArray_p handle = DDArrayCellAlloc();
64 long i;
65
66 assert(init_size > 0);
67 assert(grow > 0);
68
69 handle->size = init_size;
70 handle->grow = grow;
71 handle->array = SizeMalloc(handle->size*sizeof(double));
72 for(i=0; i<handle->size; i++)
73 {
74 handle->array[i] = 0.0;
75 }
76 return handle;
77 }
78
79 /*-----------------------------------------------------------------------
80 //
81 // Function: DDArrayFree()
82 //
83 // Free a DDArray. Leaves elements untouched.
84 //
85 // Global Variables: -
86 //
87 // Side Effects : Memory Operations
88 //
89 /----------------------------------------------------------------------*/
90
DDArrayFree(DDArray_p junk)91 void DDArrayFree(DDArray_p junk)
92 {
93 assert(junk);
94 assert(junk->size > 0);
95 assert(junk->array);
96
97 SizeFree(junk->array, junk->size*sizeof(double));
98 DDArrayCellFree(junk);
99 }
100
101 /*-----------------------------------------------------------------------
102 //
103 // Function: DDArayEnlarge()
104 //
105 // Enlarge array enough to accomodate idx.
106 //
107 // Global Variables:
108 //
109 // Side Effects :
110 //
111 /----------------------------------------------------------------------*/
112
DDArayEnlarge(DDArray_p array,long idx)113 void DDArayEnlarge(DDArray_p array, long idx)
114 {
115 double *tmp;
116 long old_size, i;
117
118 old_size = array->size;
119 tmp = array->array;
120 array->size = ((idx/array->grow)+1)*array->grow;
121 array->array = SizeMalloc(array->size * sizeof(double));
122 memcpy(array->array, tmp, old_size*sizeof(double));
123 SizeFree(tmp, old_size * sizeof(double));
124 for(i=old_size; i<array->size; i++)
125 {
126 array->array[i] = 0.0;
127 }
128 }
129
130 /*-----------------------------------------------------------------------
131 //
132 // Function: DDArrayDebugPrint()
133 //
134 // Print the array, only for debugging.
135 //
136 // Global Variables:
137 //
138 // Side Effects :
139 //
140 /----------------------------------------------------------------------*/
141
DDArrayDebugPrint(FILE * out,DDArray_p array,long size)142 void DDArrayDebugPrint(FILE* out, DDArray_p array, long size)
143 {
144 long i;
145
146 for(i = 0; i<size; i++)
147 {
148 fprintf(out, " %5.3f ", DDArrayElement(array, i));
149 if(((i+1) % 10)==0)
150 {
151 fprintf(out, "\n");
152 }
153 }
154 fprintf(out, "\n");
155 }
156
157
158 /*-----------------------------------------------------------------------
159 //
160 // Function: DDArrayAdd()
161 //
162 // Add the first limit elements from new to the corresponding entries
163 // in collect. All entries are interpreted as numerical.
164 //
165 // Global Variables: -
166 //
167 // Side Effects : Changes collect.
168 //
169 /----------------------------------------------------------------------*/
170
DDArrayAdd(DDArray_p collect,DDArray_p data,long limit)171 void DDArrayAdd(DDArray_p collect, DDArray_p data, long limit)
172 {
173 long i;
174 double old, new;
175
176 assert(collect);
177 assert(data);
178
179 for(i=0; i<limit; i++)
180 {
181 old = DDArrayElement(collect, i);
182 new = DDArrayElement(data, i);
183 DDArrayAssign(collect, i, old+new);
184 }
185 }
186
187
188 /*-----------------------------------------------------------------------
189 //
190 // Function: DDArraySelectPart()
191 //
192 // Find a value d with at least part*(last+1) values >= d and
193 // (1-part)*(last+1) values <= d in array.
194 //
195 // Global Variables: -
196 //
197 // Side Effects : Changes order in array.
198 //
199 /----------------------------------------------------------------------*/
200
DDArraySelectPart(DDArray_p array,double part,long size)201 double DDArraySelectPart(DDArray_p array, double part, long size)
202 {
203 double pivot, tmp, *arr;
204 long i,j, start, end, rank1, rank2;
205
206 assert((0 <= part) && (part <= 1));
207 assert(size>0);
208
209 tmp = (size-1)*part; /* -1 due to C's indexing */
210
211 rank1 = ((long)tmp);
212 rank2 = ((long)(tmp+0.5));
213
214 start = 0;
215 end = size-1;
216
217 /* printf("# Rank1,2: %ld, %ld\n", rank1, rank2); */
218
219 assert(array->size >= size);
220 arr = array->array;
221 while(start!=end)
222 {
223 /* Pick a good pseudo-pivot to make worst case-behaviour less
224 likely */
225
226 pivot = (arr[start]+arr[(start+end)/2]+arr[end])/3.0;
227
228 /* printf("Pivot: %f\n", pivot); */
229 i=start;
230 j=end;
231
232 while(i != j)
233 {
234 /* printf("%ld, %ld\n", i, j); */
235 while((i<j) && (arr[i] <= pivot))
236 {
237 i++;
238 }
239 while((j>i) && (arr[j] > pivot))
240 {
241 j--;
242 }
243 tmp = arr[i];
244 arr[i] = arr[j];
245 arr[j] = tmp;
246 }
247 /* printf("Hier - i= %ld\n",i);
248 DDArrayDebugPrint(stdout, array, size); */
249 if(i > rank1)
250 {
251 end = i-1;
252 }
253 else
254 {
255 start = i;
256 }
257 }
258
259 if(rank2!=rank1)
260 {
261 /* Now find the second value. We know that all values with index
262 > rank1 are >= arr[rank1] and that all values >
263 arr[rank1] have index > rank1 -> we only need to search for
264 the minimum of the second part of the array */
265 assert(rank1!=size-1); /* Should be impossible, otherwise part =
266 1.0 and rank1==rank2 */
267 tmp = arr[start+1];
268 for(i=start+1; i<size; i++)
269 {
270 tmp = MIN(tmp, arr[i]);
271 }
272 }
273 else
274 {
275 tmp = arr[start];
276 }
277 return (arr[start]+tmp)/2;
278 }
279
280
281
282
283 /*---------------------------------------------------------------------*/
284 /* End of File */
285 /*---------------------------------------------------------------------*/
286
287
288