View Javadoc

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