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.NoSuchElementException;
31
32 import org.sat4j.specs.IVecInt;
33 import org.sat4j.specs.IteratorInt;
34
35 /*
36 * Created on 9 oct. 2003
37 */
38
39 /**
40 * A vector specific for primitive integers, widely used in the solver. Note
41 * that if the vector has a sort method, the operations on the vector DO NOT
42 * preserve sorting.
43 *
44 * @author leberre
45 */
46 public class VecInt implements IVecInt {
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 public static final IVecInt EMPTY = new VecInt() {
71
72 /**
73 *
74 */
75 private static final long serialVersionUID = 1L;
76
77 @Override
78 public int size() {
79 return 0;
80 }
81
82 @Override
83 public void shrink(int nofelems) {
84 }
85
86 @Override
87 public void shrinkTo(int newsize) {
88 }
89
90 @Override
91 public IVecInt pop() {
92 throw new UnsupportedOperationException();
93 }
94
95 @Override
96 public void growTo(int newsize, int pad) {
97 }
98
99 @Override
100 public void ensure(int nsize) {
101 }
102
103 @Override
104 public IVecInt push(int elem) {
105 throw new UnsupportedOperationException();
106 }
107
108 @Override
109 public void unsafePush(int elem) {
110 throw new UnsupportedOperationException();
111 }
112
113 @Override
114 public void clear() {
115 }
116
117 @Override
118 public int last() {
119 throw new UnsupportedOperationException();
120 }
121
122 @Override
123 public int get(int i) {
124 throw new UnsupportedOperationException();
125 }
126
127 @Override
128 public void set(int i, int o) {
129 throw new UnsupportedOperationException();
130 }
131
132 @Override
133 public boolean contains(int e) {
134 return false;
135 }
136
137 @Override
138 public void copyTo(IVecInt copy) {
139 }
140
141 @Override
142 public void copyTo(int[] is) {
143 }
144
145 @Override
146 public void moveTo(IVecInt dest) {
147 }
148
149 @Override
150 public void moveTo2(IVecInt dest) {
151 }
152
153 @Override
154 public void moveTo(int[] dest) {
155 }
156
157 @Override
158 public void insertFirst(int elem) {
159 throw new UnsupportedOperationException();
160 }
161
162 @Override
163 public void remove(int elem) {
164 throw new UnsupportedOperationException();
165 }
166
167 @Override
168 public int delete(int i) {
169 throw new UnsupportedOperationException();
170 }
171
172 @Override
173 public void sort() {
174 }
175
176 @Override
177 public void sortUnique() {
178 }
179 };
180
181 public VecInt() {
182 this(5);
183 }
184
185 public VecInt(int size) {
186 myarray = new int[size];
187 }
188
189 /**
190 * Adapter method to translate an array of int into an IVecInt.
191 *
192 * The array is used inside the VecInt, so the elements may be modified
193 * outside the VecInt. But it should not take much memory.The size of the
194 * created VecInt is the length of the array.
195 *
196 * @param lits
197 * a filled array of int.
198 */
199 public VecInt(int[] lits) {
200 myarray = lits;
201 nbelem = lits.length;
202 }
203
204 /**
205 * Build a vector of a given initial size filled with an integer.
206 *
207 * @param size
208 * the initial size of the vector
209 * @param pad
210 * the integer to fill the vector with
211 */
212 public VecInt(int size, int pad) {
213 myarray = new int[size];
214 for (int i = 0; i < size; i++) {
215 myarray[i] = pad;
216 }
217 nbelem = size;
218 }
219
220 public int size() {
221 return nbelem;
222 }
223
224 /**
225 * Remove the latest nofelems elements from the vector
226 *
227 * @param nofelems
228 */
229 public void shrink(int nofelems) {
230 // assert nofelems >= 0;
231 // assert nofelems <= size();
232 nbelem -= nofelems;
233 }
234
235 public void shrinkTo(int newsize) {
236 // assert newsize >= 0;
237 // assert newsize < nbelem;
238 nbelem = newsize;
239 }
240
241 /**
242 * depile le dernier element du vecteur. Si le vecteur est vide, ne
243 * fait rien.
244 */
245 public IVecInt pop() {
246 // assert size() != 0;
247 --nbelem;
248 return this;
249 }
250
251 public void growTo(int newsize, final int pad) {
252 // assert newsize > size();
253 ensure(newsize);
254 while (--newsize >= 0) {
255 myarray[nbelem++] = pad;
256 }
257 }
258
259 public void ensure(int nsize) {
260 if (nsize >= myarray.length) {
261 int[] narray = new int[Math.max(nsize, nbelem * 2)];
262 System.arraycopy(myarray, 0, narray, 0, nbelem);
263 myarray = narray;
264 }
265 }
266
267 public IVecInt push(int elem) {
268 ensure(nbelem + 1);
269 myarray[nbelem++] = elem;
270 return this;
271 }
272
273 public void unsafePush(int elem) {
274 myarray[nbelem++] = elem;
275 }
276
277 public void clear() {
278 nbelem = 0;
279 }
280
281 public int last() {
282 // assert nbelem > 0;
283 return myarray[nbelem - 1];
284 }
285
286 public int get(int i) {
287 // assert i >= 0 && i < nbelem;
288 return myarray[i];
289 }
290
291 public int unsafeGet(int i) {
292 return myarray[i];
293 }
294
295 public void set(int i, int o) {
296 assert i >= 0 && i < nbelem;
297 myarray[i] = o;
298 }
299
300 public boolean contains(int e) {
301 final int[] workArray = myarray; // dvh, faster access
302 for (int i = 0; i < nbelem; i++) {
303 if (workArray[i] == e)
304 return true;
305 }
306 return false;
307 }
308
309 public int containsAt(int e) {
310 return containsAt(e, -1);
311 }
312
313 public int containsAt(int e, int from) {
314 final int[] workArray = myarray; // dvh, faster access
315 for (int i = from+1; i < nbelem; i++) {
316 if (workArray[i] == e)
317 return i;
318 }
319 return -1;
320 }
321
322 /**
323 * Copy the content of this vector into another one.
324 * Non constant time operation.
325 *
326 * @param copy
327 */
328 public void copyTo(IVecInt copy) {
329 VecInt ncopy = (VecInt) copy;
330 int nsize = nbelem + ncopy.nbelem;
331 ncopy.ensure(nsize);
332 System.arraycopy(myarray, 0, ncopy.myarray, ncopy.nbelem, nbelem);
333 ncopy.nbelem = nsize;
334 }
335
336 /**
337 * Copy the content of this vector into an array of integer.
338 * Non constant time operation.
339 *
340 * @param is
341 */
342 public void copyTo(int[] is) {
343 // assert is.length >= nbelem;
344 System.arraycopy(myarray, 0, is, 0, nbelem);
345 }
346
347 public void moveTo(IVecInt dest) {
348 copyTo(dest);
349 nbelem = 0;
350 }
351
352 public void moveTo2(IVecInt dest) {
353 VecInt ndest = (VecInt) dest;
354 int s = ndest.nbelem;
355 int tmp[] = ndest.myarray;
356 ndest.myarray = myarray;
357 ndest.nbelem = nbelem;
358 myarray = tmp;
359 nbelem = s;
360 nbelem = 0;
361 }
362
363 public void moveTo(int dest, int source) {
364 myarray[dest] = myarray[source];
365 }
366
367 public void moveTo(int[] dest) {
368 System.arraycopy(myarray, 0, dest, 0, nbelem);
369 nbelem = 0;
370 }
371
372 /**
373 * Insert an element at the very begining of the vector. The former first
374 * element is appended to the end of the vector in order to have a constant
375 * time operation.
376 *
377 * @param elem
378 * the element to put first in the vector.
379 */
380 public void insertFirst(final int elem) {
381 if (nbelem > 0) {
382 push(myarray[0]);
383 myarray[0] = elem;
384 return;
385 }
386 push(elem);
387 }
388
389 /**
390 * Enleve un element qui se trouve dans le vecteur!!!
391 *
392 * @param elem
393 * un element du vecteur
394 */
395 public void remove(int elem) {
396 //assert size() > 0;
397 int j = 0;
398 for (; myarray[j] != elem; j++) {
399 assert j < size();
400 }
401 System.arraycopy(myarray, j + 1, myarray, j, size() - j);
402 pop();
403 }
404
405 /**
406 * Delete the ith element of the vector. The latest element of the vector
407 * replaces the removed element at the ith indexer.
408 *
409 * @param i
410 * the indexer of the element in the vector
411 * @return the former ith element of the vector that is now removed from the
412 * vector
413 */
414 public int delete(int i) {
415 // assert i >= 0 && i < nbelem;
416 int ith = myarray[i];
417 myarray[i] = myarray[--nbelem];
418 return ith;
419 }
420
421 private int nbelem;
422
423 private int[] myarray;
424
425 /*
426 * (non-Javadoc)
427 *
428 * @see java.lang.int#toString()
429 */
430 @Override
431 public String toString() {
432 StringBuffer stb = new StringBuffer();
433 for (int i = 0; i < nbelem - 1; i++) {
434 stb.append(myarray[i]);
435 stb.append(","); //$NON-NLS-1$
436 }
437 if (nbelem > 0) {
438 stb.append(myarray[nbelem - 1]);
439 }
440 return stb.toString();
441 }
442
443 void selectionSort(int from, int to) {
444 int i, j, best_i;
445 int tmp;
446
447 for (i = from; i < to - 1; i++) {
448 best_i = i;
449 for (j = i + 1; j < to; j++) {
450 if (myarray[j] < myarray[best_i])
451 best_i = j;
452 }
453 tmp = myarray[i];
454 myarray[i] = myarray[best_i];
455 myarray[best_i] = tmp;
456 }
457 }
458
459 void sort(int from, int to) {
460 int width = to - from;
461 if (width <= 15)
462 selectionSort(from, to);
463
464 else {
465 final int[] locarray = myarray;
466 int pivot = locarray[width/2 + from];
467 int tmp;
468 int i = from - 1;
469 int j = to;
470
471 for (;;) {
472 do
473 i++;
474 while (locarray[i] < pivot);
475 do
476 j--;
477 while (pivot < locarray[j]);
478
479 if (i >= j)
480 break;
481
482 tmp = locarray[i];
483 locarray[i] = locarray[j];
484 locarray[j] = tmp;
485 }
486
487 sort(from, i);
488 sort(i, to);
489 }
490 }
491
492 /**
493 * sort the vector using a custom quicksort.
494 */
495 public void sort() {
496 sort(0, nbelem);
497 }
498
499 public void sortUnique() {
500 int i, j;
501 int last;
502 if (nbelem == 0)
503 return;
504
505 sort(0, nbelem);
506 i = 1;
507 int[] locarray = myarray;
508 last = locarray[0];
509 for (j = 1; j < nbelem; j++) {
510 if (last < locarray[j]) {
511 last = locarray[i] = locarray[j];
512 i++;
513 }
514 }
515
516 nbelem = i;
517 }
518
519 /**
520 * Two vectors are equals iff they have the very same elements in the order.
521 *
522 * @param obj
523 * an object
524 * @return true iff obj is a VecInt and has the same elements as this vector
525 * at each index.
526 *
527 * @see java.lang.Object#equals(java.lang.Object)
528 */
529 @Override
530 public boolean equals(Object obj) {
531 if (obj instanceof VecInt) {
532 VecInt v = (VecInt) obj;
533 if (v.nbelem != nbelem)
534 return false;
535 for (int i = 0; i < nbelem; i++) {
536 if (v.myarray[i] != myarray[i]) {
537 return false;
538 }
539 }
540 return true;
541 }
542 return false;
543 }
544
545 /*
546 * (non-Javadoc)
547 *
548 * @see java.lang.Object#hashCode()
549 */
550 @Override
551 public int hashCode() {
552 long sum = 0;
553 for (int i = 0; i < nbelem; i++) {
554 sum += myarray[i];
555 }
556 return (int) sum / nbelem;
557 }
558
559 /*
560 * (non-Javadoc)
561 *
562 * @see org.sat4j.specs.IVecInt2#pushAll(org.sat4j.specs.IVecInt2)
563 */
564 public void pushAll(IVecInt vec) {
565 VecInt nvec = (VecInt) vec;
566 int nsize = nbelem + nvec.nbelem;
567 ensure(nsize);
568 System.arraycopy(nvec.myarray, 0, myarray, nbelem, nvec.nbelem);
569 nbelem = nsize;
570 }
571
572 /**
573 * to detect that the vector is a subset of another one. Note that the
574 * method assumes that the two vectors are sorted!
575 *
576 * @param vec
577 * a vector
578 * @return true iff the current vector is a subset of vec
579 */
580 public boolean isSubsetOf(VecInt vec) {
581 int i = 0;
582 int j = 0;
583 while ((i < this.nbelem) && (j < vec.nbelem)) {
584 while ((j < vec.nbelem) && (vec.myarray[j] < this.myarray[i])) {
585 j++;
586 }
587 if (j == vec.nbelem || this.myarray[i] != vec.myarray[j])
588 return false;
589 i++;
590 }
591 return true;
592 }
593
594 public IteratorInt iterator() {
595 return new IteratorInt() {
596 private int i = 0;
597
598 public boolean hasNext() {
599 return i < nbelem;
600 }
601
602 public int next() {
603 if (i == nbelem)
604 throw new NoSuchElementException();
605 return myarray[i++];
606 }
607 };
608 }
609
610 public boolean isEmpty() {
611 return nbelem == 0;
612 }
613
614 public int[] toArray() {
615 return myarray;
616 }
617 }