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) {
86  		// DLB findbugs ok
87  		myarray = elts;
88  		nbelem = elts.length;
89  	}
90  
91  	/**
92  	 * Create a Vector with a given capacity.
93  	 * 
94  	 * @param size
95  	 * 		the capacity of the vector.
96  	 */
97  	@SuppressWarnings("unchecked")
98  	public Vec(int size) {
99  		myarray = (T[]) new Object[size];
100 	}
101 
102 	/**
103 	 * Construit un vecteur contenant de taille size rempli a l'aide de size
104 	 * pad.
105 	 * 
106 	 * @param size
107 	 * 		la taille du vecteur
108 	 * @param pad
109 	 * 		l'objet servant a remplir le vecteur
110 	 */
111 	@SuppressWarnings("unchecked")
112 	public Vec(int size, T pad) {
113 		myarray = (T[]) new Object[size];
114 		for (int i = 0; i < size; i++) {
115 			myarray[i] = pad;
116 		}
117 		nbelem = size;
118 	}
119 
120 	public int size() {
121 		return nbelem;
122 	}
123 
124 	/**
125 	 * Remove nofelems from the Vector. It is assumed that the number of
126 	 * elements to remove is smaller or equals to the current number of elements
127 	 * in the vector
128 	 * 
129 	 * @param nofelems
130 	 * 		the number of elements to remove.
131 	 */
132 	public void shrink(int nofelems) {
133 		// assert nofelems <= nbelem;
134 		while (nofelems-- > 0) {
135 			myarray[--nbelem] = null;
136 		}
137 	}
138 
139 	/**
140 	 * reduce the Vector to exactly newsize elements
141 	 * 
142 	 * @param newsize
143 	 * 		the new size of the vector.
144 	 */
145 	public void shrinkTo(final int newsize) {
146 		// assert newsize <= size();
147 		for (int i = nbelem; i > newsize; i--) {
148 			myarray[i - 1] = null;
149 		}
150 		nbelem = newsize;
151 		// assert size() == newsize;
152 	}
153 
154 	/**
155 	 * Pop the last element on the stack. It is assumed that the stack is not
156 	 * empty!
157 	 */
158 	public void pop() {
159 		// assert size() > 0;
160 		myarray[--nbelem] = null;
161 	}
162 
163 	public void growTo(final int newsize, final T pad) {
164 		// assert newsize >= size();
165 		ensure(newsize);
166 		for (int i = nbelem; i < newsize; i++) {
167 			myarray[i] = pad;
168 		}
169 		nbelem = newsize;
170 	}
171 
172 	@SuppressWarnings("unchecked")
173 	public void ensure(final int nsize) {
174 		if (nsize >= myarray.length) {
175 			T[] narray = (T[]) new Object[Math.max(nsize, nbelem * 2)];
176 			System.arraycopy(myarray, 0, narray, 0, nbelem);
177 			myarray = narray;
178 		}
179 	}
180 
181 	public IVec<T> push(final T elem) {
182 		ensure(nbelem + 1);
183 		myarray[nbelem++] = elem;
184 		return this;
185 	}
186 
187 	public void unsafePush(final T elem) {
188 		myarray[nbelem++] = elem;
189 	}
190 
191 	/**
192 	 * Insert an element at the very begining of the vector. The former first
193 	 * element is appended to the end of the vector in order to have a constant
194 	 * time operation.
195 	 * 
196 	 * @param elem
197 	 * 		the element to put first in the vector.
198 	 */
199 	public void insertFirst(final T elem) {
200 		if (nbelem > 0) {
201 			push(myarray[0]);
202 			myarray[0] = elem;
203 			return;
204 		}
205 		push(elem);
206 	}
207 
208 	public void insertFirstWithShifting(final T elem) {
209 		if (nbelem > 0) {
210 			ensure(nbelem + 1);
211 			for (int i = nbelem; i > 0; i--) {
212 				myarray[i] = myarray[i - 1];
213 			}
214 			myarray[0] = elem;
215 			nbelem++;
216 			return;
217 		}
218 		push(elem);
219 	}
220 
221 	public void clear() {
222 		Arrays.fill(myarray, 0, nbelem, null);
223 		nbelem = 0;
224 	}
225 
226 	/**
227 	 * return the latest element on the stack. It is assumed that the stack is
228 	 * not empty!
229 	 * 
230 	 * @return the last element on the stack (the one on the top)
231 	 */
232 	public T last() {
233 		// assert size() != 0;
234 		return myarray[nbelem - 1];
235 	}
236 
237 	public T get(final int index) {
238 		return myarray[index];
239 	}
240 
241 	public void set(int index, T elem) {
242 		myarray[index] = elem;
243 	}
244 
245 	/**
246 	 * Remove an element that belongs to the Vector. The method will break if
247 	 * the element does not belong to the vector.
248 	 * 
249 	 * @param elem
250 	 * 		an element from the vector.
251 	 */
252 	public void remove(T elem) {
253 		// assert size() > 0;
254 		int j = 0;
255 		for (; myarray[j] != elem; j++) {
256 			assert j < size();
257 		}
258 		// arraycopy is always faster than manual copy
259 		System.arraycopy(myarray, j + 1, myarray, j, size() - j - 1);
260 		myarray[--nbelem] = null;
261 	}
262 
263 	/**
264 	 * Delete the ith element of the vector. The latest element of the vector
265 	 * replaces the removed element at the ith indexer.
266 	 * 
267 	 * @param index
268 	 * 		the indexer of the element in the vector
269 	 * @return the former ith element of the vector that is now removed from the
270 	 * 	vector
271 	 */
272 	public T delete(int index) {
273 		// assert index >= 0 && index < nbelem;
274 		T ith = myarray[index];
275 		myarray[index] = myarray[--nbelem];
276 		myarray[nbelem] = null;
277 		return ith;
278 	}
279 
280 	/**
281 	 * Ces operations devraient se faire en temps constant. Ce n'est pas le cas
282 	 * ici.
283 	 * 
284 	 * @param copy
285 	 */
286 	public void copyTo(IVec<T> copy) {
287 		final Vec<T> ncopy = (Vec<T>) copy;
288 		final int nsize = nbelem + ncopy.nbelem;
289 		copy.ensure(nsize);
290 		System.arraycopy(myarray, 0, ncopy.myarray, ncopy.nbelem, nbelem);
291 		ncopy.nbelem = nsize;
292 	}
293 
294 	/**
295 	 * @param dest
296 	 */
297 	public <E> void copyTo(E[] dest) {
298 		// assert dest.length >= nbelem;
299 		System.arraycopy(myarray, 0, dest, 0, nbelem);
300 	}
301 
302 	/*
303 	 * Copy one vector to another (cleaning the first), in constant time.
304 	 */
305 	public void moveTo(IVec<T> dest) {
306 		copyTo(dest);
307 		clear();
308 	}
309 
310 	public void moveTo(int dest, int source) {
311 		if (dest != source) {
312 			myarray[dest] = myarray[source];
313 			myarray[source] = null;
314 		}
315 	}
316 
317 	public T[] toArray() {
318 		// DLB findbugs ok
319 		return myarray;
320 	}
321 
322 	private int nbelem;
323 
324 	private T[] myarray;
325 
326 	/*
327 	 * (non-Javadoc)
328 	 * 
329 	 * @see java.lang.Object#toString()
330 	 */
331 	@Override
332 	public String toString() {
333 		StringBuffer stb = new StringBuffer();
334 		for (int i = 0; i < nbelem - 1; i++) {
335 			stb.append(myarray[i]);
336 			stb.append(","); //$NON-NLS-1$
337 		}
338 		if (nbelem > 0) {
339 			stb.append(myarray[nbelem - 1]);
340 		}
341 		return stb.toString();
342 	}
343 
344 	void selectionSort(int from, int to, Comparator<T> cmp) {
345 		int i, j, best_i;
346 		T tmp;
347 
348 		for (i = from; i < to - 1; i++) {
349 			best_i = i;
350 			for (j = i + 1; j < to; j++) {
351 				if (cmp.compare(myarray[j], myarray[best_i]) < 0)
352 					best_i = j;
353 			}
354 			tmp = myarray[i];
355 			myarray[i] = myarray[best_i];
356 			myarray[best_i] = tmp;
357 		}
358 	}
359 
360 	void sort(int from, int to, Comparator<T> cmp) {
361 		int width = to - from;
362 		if (width <= 15)
363 			selectionSort(from, to, cmp);
364 
365 		else {
366 			T pivot = myarray[width / 2 + from];
367 			T tmp;
368 			int i = from - 1;
369 			int j = to;
370 
371 			for (;;) {
372 				do
373 					i++;
374 				while (cmp.compare(myarray[i], pivot) < 0);
375 				do
376 					j--;
377 				while (cmp.compare(pivot, myarray[j]) < 0);
378 
379 				if (i >= j)
380 					break;
381 
382 				tmp = myarray[i];
383 				myarray[i] = myarray[j];
384 				myarray[j] = tmp;
385 			}
386 
387 			sort(from, i, cmp);
388 			sort(i, to, cmp);
389 		}
390 	}
391 
392 	/**
393 	 * @param comparator
394 	 */
395 	public void sort(Comparator<T> comparator) {
396 		sort(0, nbelem, comparator);
397 	}
398 
399 	public void sortUnique(Comparator<T> cmp) {
400 		int i, j;
401 		T last;
402 
403 		if (nbelem == 0)
404 			return;
405 
406 		sort(0, nbelem, cmp);
407 
408 		i = 1;
409 		last = myarray[0];
410 		for (j = 1; j < nbelem; j++) {
411 			if (cmp.compare(last, myarray[j]) < 0) {
412 				last = myarray[i] = myarray[j];
413 				i++;
414 			}
415 		}
416 
417 		nbelem = i;
418 	}
419 
420 	/*
421 	 * (non-Javadoc)
422 	 * 
423 	 * @see java.lang.Object#equals(java.lang.Object)
424 	 */
425 	@Override
426 	public boolean equals(Object obj) {
427 		if (obj instanceof IVec) {
428 			IVec<?> v = (IVec<?>) obj;
429 			if (v.size() != size())
430 				return false;
431 			for (int i = 0; i < size(); i++) {
432 				if (!v.get(i).equals(get(i))) {
433 					return false;
434 				}
435 			}
436 			return true;
437 		}
438 		return false;
439 	}
440 
441 	/*
442 	 * (non-Javadoc)
443 	 * 
444 	 * @see java.lang.Object#hashCode()
445 	 */
446 	@Override
447 	public int hashCode() {
448 		int sum = 0;
449 		for (int i = 0; i < nbelem; i++) {
450 			sum += myarray[i].hashCode() / nbelem;
451 		}
452 		return sum;
453 	}
454 
455 	public Iterator<T> iterator() {
456 		return new Iterator<T>() {
457 			private int i = 0;
458 
459 			public boolean hasNext() {
460 				return i < nbelem;
461 			}
462 
463 			public T next() {
464 				if (i == nbelem)
465 					throw new NoSuchElementException();
466 				return myarray[i++];
467 			}
468 
469 			public void remove() {
470 				throw new UnsupportedOperationException();
471 			}
472 		};
473 	}
474 
475 	public boolean isEmpty() {
476 		return nbelem == 0;
477 	}
478 }