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 if (j == size())
258 throw new NoSuchElementException();
259 }
260 // arraycopy is always faster than manual copy
261 System.arraycopy(this.myarray, j + 1, this.myarray, j, size() - j - 1);
262 this.myarray[--this.nbelem] = null;
263 }
264
265 /**
266 * Delete the ith element of the vector. The latest element of the vector
267 * replaces the removed element at the ith indexer.
268 *
269 * @param index
270 * the indexer of the element in the vector
271 * @return the former ith element of the vector that is now removed from the
272 * vector
273 */
274 public T delete(int index) {
275 // assert index >= 0 && index < nbelem;
276 T ith = this.myarray[index];
277 this.myarray[index] = this.myarray[--this.nbelem];
278 this.myarray[this.nbelem] = null;
279 return ith;
280 }
281
282 /**
283 * Ces operations devraient se faire en temps constant. Ce n'est pas le cas
284 * ici.
285 *
286 * @param copy
287 */
288 public void copyTo(IVec<T> copy) {
289 final Vec<T> ncopy = (Vec<T>) copy;
290 final int nsize = this.nbelem + ncopy.nbelem;
291 copy.ensure(nsize);
292 System.arraycopy(this.myarray, 0, ncopy.myarray, ncopy.nbelem,
293 this.nbelem);
294 ncopy.nbelem = nsize;
295 }
296
297 /**
298 * @param dest
299 */
300 public <E> void copyTo(E[] dest) {
301 // assert dest.length >= nbelem;
302 System.arraycopy(this.myarray, 0, dest, 0, this.nbelem);
303 }
304
305 /*
306 * Copy one vector to another (cleaning the first), in constant time.
307 */
308 public void moveTo(IVec<T> dest) {
309 copyTo(dest);
310 clear();
311 }
312
313 public void moveTo(int dest, int source) {
314 if (dest != source) {
315 this.myarray[dest] = this.myarray[source];
316 this.myarray[source] = null;
317 }
318 }
319
320 public T[] toArray() {
321 // DLB findbugs ok
322 return this.myarray;
323 }
324
325 private int nbelem;
326
327 private T[] myarray;
328
329 /*
330 * (non-Javadoc)
331 *
332 * @see java.lang.Object#toString()
333 */
334 @Override
335 public String toString() {
336 StringBuffer stb = new StringBuffer();
337 for (int i = 0; i < this.nbelem - 1; i++) {
338 stb.append(this.myarray[i]);
339 stb.append(","); //$NON-NLS-1$
340 }
341 if (this.nbelem > 0) {
342 stb.append(this.myarray[this.nbelem - 1]);
343 }
344 return stb.toString();
345 }
346
347 void selectionSort(int from, int to, Comparator<T> cmp) {
348 int i, j, besti;
349 T tmp;
350
351 for (i = from; i < to - 1; i++) {
352 besti = i;
353 for (j = i + 1; j < to; j++) {
354 if (cmp.compare(this.myarray[j], this.myarray[besti]) < 0) {
355 besti = j;
356 }
357 }
358 tmp = this.myarray[i];
359 this.myarray[i] = this.myarray[besti];
360 this.myarray[besti] = tmp;
361 }
362 }
363
364 void sort(int from, int to, Comparator<T> cmp) {
365 int width = to - from;
366 if (width <= 15) {
367 selectionSort(from, to, cmp);
368 } else {
369 T pivot = this.myarray[width / 2 + from];
370 T tmp;
371 int i = from - 1;
372 int j = to;
373
374 for (;;) {
375 do {
376 i++;
377 } while (cmp.compare(this.myarray[i], pivot) < 0);
378 do {
379 j--;
380 } while (cmp.compare(pivot, this.myarray[j]) < 0);
381
382 if (i >= j) {
383 break;
384 }
385
386 tmp = this.myarray[i];
387 this.myarray[i] = this.myarray[j];
388 this.myarray[j] = tmp;
389 }
390
391 sort(from, i, cmp);
392 sort(i, to, cmp);
393 }
394 }
395
396 /**
397 * @param comparator
398 */
399 public void sort(Comparator<T> comparator) {
400 sort(0, this.nbelem, comparator);
401 }
402
403 public void sortUnique(Comparator<T> cmp) {
404 int i, j;
405 T last;
406
407 if (this.nbelem == 0) {
408 return;
409 }
410
411 sort(0, this.nbelem, cmp);
412
413 i = 1;
414 last = this.myarray[0];
415 for (j = 1; j < this.nbelem; j++) {
416 if (cmp.compare(last, this.myarray[j]) < 0) {
417 last = this.myarray[i] = this.myarray[j];
418 i++;
419 }
420 }
421
422 this.nbelem = i;
423 }
424
425 /*
426 * (non-Javadoc)
427 *
428 * @see java.lang.Object#equals(java.lang.Object)
429 */
430 @Override
431 public boolean equals(Object obj) {
432 if (obj instanceof IVec<?>) {
433 IVec<?> v = (IVec<?>) obj;
434 if (v.size() != size()) {
435 return false;
436 }
437 for (int i = 0; i < size(); i++) {
438 if (!v.get(i).equals(get(i))) {
439 return false;
440 }
441 }
442 return true;
443 }
444 return false;
445 }
446
447 /*
448 * (non-Javadoc)
449 *
450 * @see java.lang.Object#hashCode()
451 */
452 @Override
453 public int hashCode() {
454 int sum = 0;
455 for (int i = 0; i < this.nbelem; i++) {
456 sum += this.myarray[i].hashCode() / this.nbelem;
457 }
458 return sum;
459 }
460
461 public Iterator<T> iterator() {
462 return new Iterator<T>() {
463 private int i = 0;
464
465 public boolean hasNext() {
466 return this.i < Vec.this.nbelem;
467 }
468
469 public T next() {
470 if (this.i == Vec.this.nbelem) {
471 throw new NoSuchElementException();
472 }
473 return Vec.this.myarray[this.i++];
474 }
475
476 public void remove() {
477 throw new UnsupportedOperationException();
478 }
479 };
480 }
481
482 public boolean isEmpty() {
483 return this.nbelem == 0;
484 }
485
486 /**
487 * @since 2.1
488 */
489 public boolean contains(T e) {
490 for (int i = 0; i < this.nbelem; i++) {
491 if (this.myarray[i].equals(e)) {
492 return true;
493 }
494 }
495 return false;
496 }
497
498 /**
499 * @since 2.2
500 */
501 public int indexOf(T element) {
502 for (int i = 0; i < this.nbelem; i++) {
503 if (this.myarray[i].equals(element)) {
504 return i;
505 }
506 }
507 return -1;
508 }
509 }