1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
29 *******************************************************************************/
30 package org.sat4j.core;
31
32 import java.util.Arrays;
33 import java.util.Comparator;
34 import java.util.Iterator;
35 import java.util.NoSuchElementException;
36
37 import org.sat4j.specs.IVec;
38
39 /**
40 * Simple but efficient vector implementation, based on the vector
41 * implementation available in MiniSAT. Note that the elements are compared
42 * using their references, not using the equals method.
43 *
44 * @author leberre
45 */
46 public final class Vec<T> implements IVec<T> {
47 // MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
48 //
49 // Permission is hereby granted, free of charge, to any person obtaining a
50 // copy of this software and associated documentation files (the
51 // "Software"), to deal in the Software without restriction, including
52 // without limitation the rights to use, copy, modify, merge, publish,
53 // distribute, sublicense, and/or sell copies of the Software, and to
54 // permit persons to whom the Software is furnished to do so, subject to
55 // the following conditions:
56 //
57 // The above copyright notice and this permission notice shall be included
58 // in all copies or substantial portions of the Software.
59 //
60 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
61 // OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
62 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
63 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
64 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
65 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
66 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
67
68 private static final long serialVersionUID = 1L;
69
70 /**
71 * Create a Vector with an initial capacity of 5 elements.
72 */
73 public Vec() {
74 this(5);
75 }
76
77 /**
78 * Adapter method to translate an array of int into an IVec.
79 *
80 * The array is used inside the Vec, so the elements may be modified outside
81 * the Vec. But it should not take much memory. The size of the created Vec
82 * is the length of the array.
83 *
84 * @param elts
85 * a filled array of T.
86 */
87 public Vec(T[] elts) { // NOPMD
88 this.myarray = elts;
89 this.nbelem = elts.length;
90 }
91
92 /**
93 * Create a Vector with a given capacity.
94 *
95 * @param size
96 * the capacity of the vector.
97 */
98 @SuppressWarnings("unchecked")
99 public Vec(int size) {
100 this.myarray = (T[]) new Object[size];
101 }
102
103 /**
104 * Construit un vecteur contenant de taille size rempli a l'aide de size
105 * pad.
106 *
107 * @param size
108 * la taille du vecteur
109 * @param pad
110 * l'objet servant a remplir le vecteur
111 */
112 @SuppressWarnings("unchecked")
113 public Vec(int size, T pad) {
114 this.myarray = (T[]) new Object[size];
115 for (int i = 0; i < size; i++) {
116 this.myarray[i] = pad;
117 }
118 this.nbelem = size;
119 }
120
121 public int size() {
122 return this.nbelem;
123 }
124
125 /**
126 * Remove nofelems from the Vector. It is assumed that the number of
127 * elements to remove is smaller or equals to the current number of elements
128 * in the vector
129 *
130 * @param nofelems
131 * the number of elements to remove.
132 */
133 public void shrink(int nofelems) {
134 // assert nofelems <= nbelem;
135 while (nofelems-- > 0) {
136 this.myarray[--this.nbelem] = null;
137 }
138 }
139
140 /**
141 * reduce the Vector to exactly newsize elements
142 *
143 * @param newsize
144 * the new size of the vector.
145 */
146 public void shrinkTo(final int newsize) {
147 // assert newsize <= size();
148 for (int i = this.nbelem; i > newsize; i--) {
149 this.myarray[i - 1] = null;
150 }
151 this.nbelem = newsize;
152 // assert size() == newsize;
153 }
154
155 /**
156 * Pop the last element on the stack. It is assumed that the stack is not
157 * empty!
158 */
159 public void pop() {
160 // assert size() > 0;
161 this.myarray[--this.nbelem] = null;
162 }
163
164 public void growTo(final int newsize, final T pad) {
165 // assert newsize >= size();
166 ensure(newsize);
167 for (int i = this.nbelem; i < newsize; i++) {
168 this.myarray[i] = pad;
169 }
170 this.nbelem = newsize;
171 }
172
173 @SuppressWarnings("unchecked")
174 public void ensure(final int nsize) {
175 if (nsize >= this.myarray.length) {
176 T[] narray = (T[]) new Object[Math.max(nsize, this.nbelem * 2)];
177 System.arraycopy(this.myarray, 0, narray, 0, this.nbelem);
178 this.myarray = narray;
179 }
180 }
181
182 public IVec<T> push(final T elem) {
183 ensure(this.nbelem + 1);
184 this.myarray[this.nbelem++] = elem;
185 return this;
186 }
187
188 public void unsafePush(final T elem) {
189 this.myarray[this.nbelem++] = elem;
190 }
191
192 /**
193 * Insert an element at the very beginning of the vector. The former first
194 * element is appended to the end of the vector in order to have a constant
195 * time operation.
196 *
197 * @param elem
198 * the element to put first in the vector.
199 */
200 public void insertFirst(final T elem) {
201 if (this.nbelem > 0) {
202 push(this.myarray[0]);
203 this.myarray[0] = elem;
204 return;
205 }
206 push(elem);
207 }
208
209 public void insertFirstWithShifting(final T elem) {
210 if (this.nbelem > 0) {
211 ensure(this.nbelem + 1);
212 for (int i = this.nbelem; i > 0; i--) {
213 this.myarray[i] = this.myarray[i - 1];
214 }
215 this.myarray[0] = elem;
216 this.nbelem++;
217 return;
218 }
219 push(elem);
220 }
221
222 public void clear() {
223 Arrays.fill(this.myarray, 0, this.nbelem, null);
224 this.nbelem = 0;
225 }
226
227 /**
228 * return the latest element on the stack. It is assumed that the stack is
229 * not empty!
230 *
231 * @return the last element on the stack (the one on the top)
232 */
233 public T last() {
234 // assert size() != 0;
235 return this.myarray[this.nbelem - 1];
236 }
237
238 public T get(final int index) {
239 return this.myarray[index];
240 }
241
242 public void set(int index, T elem) {
243 this.myarray[index] = elem;
244 }
245
246 /**
247 * Remove an element that belongs to the Vector. The method will break if
248 * the element does not belong to the vector.
249 *
250 * @param elem
251 * an element from the vector.
252 */
253 public void remove(T elem) {
254 // assert size() > 0;
255 int j = 0;
256 for (; this.myarray[j] != elem; j++) {
257 assert j < size();
258 }
259 // arraycopy is always faster than manual copy
260 System.arraycopy(this.myarray, j + 1, this.myarray, j, size() - j - 1);
261 this.myarray[--this.nbelem] = null;
262 }
263
264 /**
265 * Delete the ith element of the vector. The latest element of the vector
266 * replaces the removed element at the ith indexer.
267 *
268 * @param index
269 * the indexer of the element in the vector
270 * @return the former ith element of the vector that is now removed from the
271 * vector
272 */
273 public T delete(int index) {
274 // assert index >= 0 && index < nbelem;
275 T ith = this.myarray[index];
276 this.myarray[index] = this.myarray[--this.nbelem];
277 this.myarray[this.nbelem] = null;
278 return ith;
279 }
280
281 /**
282 * Ces operations devraient se faire en temps constant. Ce n'est pas le cas
283 * ici.
284 *
285 * @param copy
286 */
287 public void copyTo(IVec<T> copy) {
288 final Vec<T> ncopy = (Vec<T>) copy;
289 final int nsize = this.nbelem + ncopy.nbelem;
290 copy.ensure(nsize);
291 System.arraycopy(this.myarray, 0, ncopy.myarray, ncopy.nbelem,
292 this.nbelem);
293 ncopy.nbelem = nsize;
294 }
295
296 /**
297 * @param dest
298 */
299 public <E> void copyTo(E[] dest) {
300 // assert dest.length >= nbelem;
301 System.arraycopy(this.myarray, 0, dest, 0, this.nbelem);
302 }
303
304 /*
305 * Copy one vector to another (cleaning the first), in constant time.
306 */
307 public void moveTo(IVec<T> dest) {
308 copyTo(dest);
309 clear();
310 }
311
312 public void moveTo(int dest, int source) {
313 if (dest != source) {
314 this.myarray[dest] = this.myarray[source];
315 this.myarray[source] = null;
316 }
317 }
318
319 public T[] toArray() {
320 // DLB findbugs ok
321 return this.myarray;
322 }
323
324 private int nbelem;
325
326 private T[] myarray;
327
328 /*
329 * (non-Javadoc)
330 *
331 * @see java.lang.Object#toString()
332 */
333 @Override
334 public String toString() {
335 StringBuffer stb = new StringBuffer();
336 for (int i = 0; i < this.nbelem - 1; i++) {
337 stb.append(this.myarray[i]);
338 stb.append(","); //$NON-NLS-1$
339 }
340 if (this.nbelem > 0) {
341 stb.append(this.myarray[this.nbelem - 1]);
342 }
343 return stb.toString();
344 }
345
346 void selectionSort(int from, int to, Comparator<T> cmp) {
347 int i, j, best_i;
348 T tmp;
349
350 for (i = from; i < to - 1; i++) {
351 best_i = i;
352 for (j = i + 1; j < to; j++) {
353 if (cmp.compare(this.myarray[j], this.myarray[best_i]) < 0) {
354 best_i = j;
355 }
356 }
357 tmp = this.myarray[i];
358 this.myarray[i] = this.myarray[best_i];
359 this.myarray[best_i] = tmp;
360 }
361 }
362
363 void sort(int from, int to, Comparator<T> cmp) {
364 int width = to - from;
365 if (width <= 15) {
366 selectionSort(from, to, cmp);
367 } else {
368 T pivot = this.myarray[width / 2 + from];
369 T tmp;
370 int i = from - 1;
371 int j = to;
372
373 for (;;) {
374 do {
375 i++;
376 } while (cmp.compare(this.myarray[i], pivot) < 0);
377 do {
378 j--;
379 } while (cmp.compare(pivot, this.myarray[j]) < 0);
380
381 if (i >= j) {
382 break;
383 }
384
385 tmp = this.myarray[i];
386 this.myarray[i] = this.myarray[j];
387 this.myarray[j] = tmp;
388 }
389
390 sort(from, i, cmp);
391 sort(i, to, cmp);
392 }
393 }
394
395 /**
396 * @param comparator
397 */
398 public void sort(Comparator<T> comparator) {
399 sort(0, this.nbelem, comparator);
400 }
401
402 public void sortUnique(Comparator<T> cmp) {
403 int i, j;
404 T last;
405
406 if (this.nbelem == 0) {
407 return;
408 }
409
410 sort(0, this.nbelem, cmp);
411
412 i = 1;
413 last = this.myarray[0];
414 for (j = 1; j < this.nbelem; j++) {
415 if (cmp.compare(last, this.myarray[j]) < 0) {
416 last = this.myarray[i] = this.myarray[j];
417 i++;
418 }
419 }
420
421 this.nbelem = i;
422 }
423
424 /*
425 * (non-Javadoc)
426 *
427 * @see java.lang.Object#equals(java.lang.Object)
428 */
429 @Override
430 public boolean equals(Object obj) {
431 if (obj instanceof IVec<?>) {
432 IVec<?> v = (IVec<?>) obj;
433 if (v.size() != size()) {
434 return false;
435 }
436 for (int i = 0; i < size(); i++) {
437 if (!v.get(i).equals(get(i))) {
438 return false;
439 }
440 }
441 return true;
442 }
443 return false;
444 }
445
446 /*
447 * (non-Javadoc)
448 *
449 * @see java.lang.Object#hashCode()
450 */
451 @Override
452 public int hashCode() {
453 int sum = 0;
454 for (int i = 0; i < this.nbelem; i++) {
455 sum += this.myarray[i].hashCode() / this.nbelem;
456 }
457 return sum;
458 }
459
460 public Iterator<T> iterator() {
461 return new Iterator<T>() {
462 private int i = 0;
463
464 public boolean hasNext() {
465 return this.i < Vec.this.nbelem;
466 }
467
468 public T next() {
469 if (this.i == Vec.this.nbelem) {
470 throw new NoSuchElementException();
471 }
472 return Vec.this.myarray[this.i++];
473 }
474
475 public void remove() {
476 throw new UnsupportedOperationException();
477 }
478 };
479 }
480
481 public boolean isEmpty() {
482 return this.nbelem == 0;
483 }
484
485 /**
486 * @since 2.1
487 */
488 public boolean contains(T e) {
489 for (int i = 0; i < this.nbelem; i++) {
490 if (this.myarray[i].equals(e)) {
491 return true;
492 }
493 }
494 return false;
495 }
496
497 /**
498 * @since 2.2
499 */
500 public int indexOf(T element) {
501 for (int i = 0; i < this.nbelem; i++) {
502 if (this.myarray[i].equals(element)) {
503 return i;
504 }
505 }
506 return -1;
507 }
508 }