Changes in directory llvm-test/MultiSource/Benchmarks/minisat:
Alg.h added (r1.1) BasicHeap.h added (r1.1) BoxedVec.h added (r1.1) Heap.h added (r1.1) Map.h added (r1.1) Queue.h added (r1.1) SolverTypes.h added (r1.1) Sort.h added (r1.1) Vec.h added (r1.1) Makefile updated: 1.3 -> 1.4 --- Log message: Flatten minisat's directory structure, and default to the shorter test case. --- Diffs of the changes: (+1098 -1) Alg.h | 57 ++++++++++++++++ BasicHeap.h | 98 ++++++++++++++++++++++++++++ BoxedVec.h | 147 +++++++++++++++++++++++++++++++++++++++++++ Heap.h | 169 +++++++++++++++++++++++++++++++++++++++++++++++++ Makefile | 5 + Map.h | 118 ++++++++++++++++++++++++++++++++++ Queue.h | 82 ++++++++++++++++++++++++ SolverTypes.h | 197 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Sort.h | 93 +++++++++++++++++++++++++++ Vec.h | 133 +++++++++++++++++++++++++++++++++++++++ 10 files changed, 1098 insertions(+), 1 deletion(-) Index: llvm-test/MultiSource/Benchmarks/minisat/Alg.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Alg.h:1.1 *** /dev/null Thu Feb 8 11:52:03 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Alg.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,57 ---- + /*******************************************************************************************[Alg.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Alg_h + #define Alg_h + + //================================================================================================= + // Useful functions on vectors + + + #if 1 + template<class V, class T> + static inline void remove(V& ts, const T& t) + { + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; + ts.pop(); + } + #else + template<class V, class T> + static inline void remove(V& ts, const T& t) + { + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + assert(j < ts.size()); + ts[j] = ts.last(); + ts.pop(); + } + #endif + + template<class V, class T> + static inline bool find(V& ts, const T& t) + { + int j = 0; + for (; j < ts.size() && ts[j] != t; j++); + return j < ts.size(); + } + + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/BasicHeap.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/BasicHeap.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/BasicHeap.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,98 ---- + /******************************************************************************************[Heap.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef BasicHeap_h + #define BasicHeap_h + + #include "Vec.h" + + //================================================================================================= + // A heap implementation with support for decrease/increase key. + + + template<class Comp> + class BasicHeap { + Comp lt; + vec<int> heap; // heap of ints + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + i = parent(i); + } + heap [i] = x; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + i = child; + } + heap[i] = x; + } + + + bool heapProperty(int i) { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + BasicHeap(const C& c) : comp(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + int operator[](int index) const { return heap[index+1]; } + void clear (bool dealloc = false) { heap.clear(dealloc); } + void insert (int n) { heap.push(n); percolateUp(heap.size()-1); } + + + int removeMin() { + int r = heap[0]; + heap[0] = heap.last(); + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return r; + } + + + // DEBUG: consistency checking + bool heapProperty() { + return heapProperty(1); } + + + // COMPAT: should be removed + int getmin () { return removeMin(); } + }; + + + //================================================================================================= + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/BoxedVec.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/BoxedVec.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/BoxedVec.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,147 ---- + /*******************************************************************************************[Vec.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef BoxedVec_h + #define BoxedVec_h + + #include <cstdlib> + #include <cassert> + #include <new> + + //================================================================================================= + // Automatically resizable arrays + // + // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + + template<class T> + class bvec { + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + struct Vec_t { + int sz; + int cap; + T data[0]; + + static Vec_t* alloc(Vec_t* x, int size){ + x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size); + x->cap = size; + return x; + } + + }; + + Vec_t* ref; + + static const int init_size = 2; + static int nextSize (int current) { return (current * 3 + 1) >> 1; } + static int fitSize (int needed) { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; } + + void fill (int size) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(); + } + + void fill (int size, const T& pad) { + assert(ref != NULL); + for (T* i = ref->data; i < ref->data + size; i++) + new (i) T(pad); + } + + // Don't allow copying (error prone): + altvec<T>& operator = (altvec<T>& other) { assert(0); } + altvec (altvec<T>& other) { assert(0); } + + public: + void clear (bool dealloc = false) { + if (ref != NULL){ + for (int i = 0; i < ref->sz; i++) + (*ref).data[i].~T(); + + if (dealloc) { + free(ref); ref = NULL; + }else + ref->sz = 0; + } + } + + // Constructors: + altvec(void) : ref (NULL) { } + altvec(int size) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size); ref->sz = size; } + altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; } + ~altvec(void) { clear(true); } + + // Ownership of underlying array: + operator T* (void) { return ref->data; } // (unsafe but convenient) + operator const T* (void) const { return ref->data; } + + // Size operations: + int size (void) const { return ref != NULL ? ref->sz : 0; } + + void pop (void) { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); } + void push (const T& elem) { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; + } + + void push () { + int size = ref != NULL ? ref->sz : 0; + int cap = ref != NULL ? ref->cap : 0; + if (size == cap){ + cap = cap != 0 ? nextSize(cap) : init_size; + ref = Vec_t::alloc(ref, cap); + } + new (&ref->data[size]) T(); + ref->sz = size+1; + } + + void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void shrink_(int nelems) { for (int i = 0; i < nelems; i++) pop(); } + void growTo (int size) { while (this->size() < size) push(); } + void growTo (int size, const T& pad) { while (this->size() < size) push(pad); } + void capacity (int size) { growTo(size); } + + const T& last (void) const { return ref->data[ref->sz-1]; } + T& last (void) { return ref->data[ref->sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return ref->data[index]; } + T& operator [] (int index) { return ref->data[index]; } + + void copyTo(altvec<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); } + void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; } + + }; + + + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Heap.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Heap.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Heap.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,169 ---- + /******************************************************************************************[Heap.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Heap_h + #define Heap_h + + #include "Vec.h" + + //================================================================================================= + // A heap implementation with support for decrease/increase key. + + + template<class Comp> + class Heap { + Comp lt; + vec<int> heap; // heap of ints + vec<int> indices; // int -> index in heap + + // Index "traversal" functions + static inline int left (int i) { return i*2+1; } + static inline int right (int i) { return (i+1)*2; } + static inline int parent(int i) { return (i-1) >> 1; } + + + inline void percolateUp(int i) + { + int x = heap[i]; + while (i != 0 && lt(x, heap[parent(i)])){ + heap[i] = heap[parent(i)]; + indices[heap[i]] = i; + i = parent(i); + } + heap [i] = x; + indices[x] = i; + } + + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); + if (!lt(heap[child], x)) break; + heap[i] = heap[child]; + indices[heap[i]] = i; + i = child; + } + heap [i] = x; + indices[x] = i; + } + + + bool heapProperty (int i) const { + return i >= heap.size() + || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } + + + public: + Heap(const Comp& c) : lt(c) { } + + int size () const { return heap.size(); } + bool empty () const { return heap.size() == 0; } + bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } + int operator[](int index) const { assert(index < heap.size()); return heap[index]; } + + void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); } + + // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED. + void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + + + void insert(int n) + { + indices.growTo(n+1, -1); + assert(!inHeap(n)); + + indices[n] = heap.size(); + heap.push(n); + percolateUp(indices[n]); + } + + + int removeMin() + { + int x = heap[0]; + heap[0] = heap.last(); + indices[heap[0]] = 0; + indices[x] = -1; + heap.pop(); + if (heap.size() > 1) percolateDown(0); + return x; + } + + + void clear(bool dealloc = false) + { + for (int i = 0; i < heap.size(); i++) + indices[heap[i]] = -1; + #ifdef NDEBUG + for (int i = 0; i < indices.size(); i++) + assert(indices[i] == -1); + #endif + heap.clear(dealloc); + } + + + // Fool proof variant of insert/decrease/increase + void update (int n) + { + if (!inHeap(n)) + insert(n); + else { + percolateUp(indices[n]); + percolateDown(indices[n]); + } + } + + + // Delete elements from the heap using a given filter function (-object). + // *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method *** + template <class F> + void filter(const F& filt) { + int i,j; + for (i = j = 0; i < heap.size(); i++) + if (filt(heap[i])){ + heap[j] = heap[i]; + indices[heap[i]] = j++; + }else + indices[heap[i]] = -1; + + heap.shrink(i - j); + for (int i = heap.size() / 2 - 1; i >= 0; i--) + percolateDown(i); + + assert(heapProperty()); + } + + + // DEBUG: consistency checking + bool heapProperty() const { + return heapProperty(1); } + + + // COMPAT: should be removed + void setBounds (int n) { } + void increase (int n) { decrease(n); } + int getmin () { return removeMin(); } + + }; + + + //================================================================================================= + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Map.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Map.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Map.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,118 ---- + /*******************************************************************************************[Map.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Map_h + #define Map_h + + #include <stdint.h> + + #include "Vec.h" + + //================================================================================================= + // Default hash/equals functions + // + + template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; + template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; + + template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; + template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; + + //================================================================================================= + // Some primes + // + + static const int nprimes = 25; + static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; + + //================================================================================================= + // Hash table implementation of Maps + // + + template<class K, class D, class H = Hash<K>, class E = Equal<K> > + class Map { + struct Pair { K key; D data; }; + + H hash; + E equals; + + vec<Pair>* table; + int cap; + int size; + + // Don't allow copying (error prone): + Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); } + Map (Map<K,D,H,E>& other) { assert(0); } + + int32_t index (const K& k) const { return hash(k) % cap; } + void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } + void rehash () { + const vec<Pair>* old = table; + + int newsize = primes[0]; + for (int i = 1; newsize <= cap && i < nprimes; i++) + newsize = primes[i]; + + table = new vec<Pair>[newsize]; + + for (int i = 0; i < cap; i++){ + for (int j = 0; j < old[i].size(); j++){ + _insert(old[i][j].key, old[i][j].data); }} + + delete [] old; + + cap = newsize; + } + + + public: + + Map () : table(NULL), cap(0), size(0) {} + Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} + ~Map () { delete [] table; } + + void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } + bool peek (const K& k, D& d) { + if (size == 0) return false; + const vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)){ + d = ps[i].data; + return true; } + return false; + } + + void remove (const K& k) { + assert(table != NULL); + vec<Pair>& ps = table[index(k)]; + int j = 0; + for (; j < ps.size() && !equals(ps[j].key, k); j++); + assert(j < ps.size()); + ps[j] = ps.last(); + ps.pop(); + } + + void clear () { + cap = size = 0; + delete [] table; + table = NULL; + } + }; + + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Queue.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Queue.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Queue.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,82 ---- + /*****************************************************************************************[Queue.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Queue_h + #define Queue_h + + #include "Vec.h" + + //================================================================================================= + + + template <class T> + class Queue { + vec<T> elems; + int first; + + public: + Queue(void) : first(0) { } + + void insert(T x) { elems.push(x); } + T peek () const { return elems[first]; } + void pop () { first++; } + + void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } + int size(void) { return elems.size() - first; } + + //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } + + const T& operator [] (int index) const { return elems[first + index]; } + + }; + + //template<class T> + //class Queue { + // vec<T> buf; + // int first; + // int end; + // + //public: + // typedef T Key; + // + // Queue() : buf(1), first(0), end(0) {} + // + // void clear () { buf.shrinkTo(1); first = end = 0; } + // int size () { return (end >= first) ? end - first : end - first + buf.size(); } + // + // T peek () { assert(first != end); return buf[first]; } + // void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } + // void insert(T elem) { // INVARIANT: buf[end] is always unused + // buf[end++] = elem; + // if (end == buf.size()) end = 0; + // if (first == end){ // Resize: + // vec<T> tmp((buf.size()*3 + 1) >> 1); + // //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); + // int i = 0; + // for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; + // for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; + // first = 0; + // end = buf.size(); + // tmp.moveTo(buf); + // } + // } + //}; + + //================================================================================================= + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/SolverTypes.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/SolverTypes.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/SolverTypes.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,197 ---- + /***********************************************************************************[SolverTypes.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + + #ifndef SolverTypes_h + #define SolverTypes_h + + #include <cassert> + #include <stdint.h> + + //================================================================================================= + // Variables, literals, lifted booleans, clauses: + + + // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, + // so that they can be used as array indices. + + typedef int Var; + #define var_Undef (-1) + + + class Lit { + int x; + public: + Lit() : x(2*var_Undef) { } // (lit_Undef) + explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } + + // Don't use these for constructing/deconstructing literals. Use the normal constructors instead. + friend int toInt (Lit p); // Guarantees small, positive integers suitable for array indexing. + friend Lit toLit (int i); // Inverse of 'toInt()' + friend Lit operator ~(Lit p); + friend bool sign (Lit p); + friend int var (Lit p); + friend Lit unsign (Lit p); + friend Lit id (Lit p, bool sgn); + + bool operator == (Lit p) const { return x == p.x; } + bool operator != (Lit p) const { return x != p.x; } + bool operator < (Lit p) const { return x < p.x; } // '<' guarantees that p, ~p are adjacent in the ordering. + }; + + inline int toInt (Lit p) { return p.x; } + inline Lit toLit (int i) { Lit p; p.x = i; return p; } + inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } + inline bool sign (Lit p) { return p.x & 1; } + inline int var (Lit p) { return p.x >> 1; } + inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; } + inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } + + const Lit lit_Undef(var_Undef, false); // }- Useful special constants. + const Lit lit_Error(var_Undef, true ); // } + + + //================================================================================================= + // Lifted booleans: + + + class lbool { + char value; + explicit lbool(int v) : value(v) { } + + public: + lbool() : value(0) { } + lbool(bool x) : value((int)x*2-1) { } + int toInt(void) const { return value; } + + bool operator == (lbool b) const { return value == b.value; } + bool operator != (lbool b) const { return value != b.value; } + lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); } + + friend int toInt (lbool l); + friend lbool toLbool(int v); + }; + inline int toInt (lbool l) { return l.toInt(); } + inline lbool toLbool(int v) { return lbool(v); } + + const lbool l_True = toLbool( 1); + const lbool l_False = toLbool(-1); + const lbool l_Undef = toLbool( 0); + + //================================================================================================= + // Clause -- a simple class for representing a clause: + + + class Clause { + uint32_t size_etc; + union { float act; uint32_t abst; } extra; + Lit data[0]; + + public: + void calcAbstraction() { + uint32_t abstraction = 0; + for (int i = 0; i < size(); i++) + abstraction |= 1 << (var(data[i]) & 31); + extra.abst = abstraction; } + + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). + template<class V> + Clause(const V& ps, bool learnt) { + size_etc = (ps.size() << 3) | (uint32_t)learnt; + for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) extra.act = 0; else calcAbstraction(); } + + // -- use this function instead: + template<class V> + friend Clause* Clause_new(const V& ps, bool learnt = false) { + assert(sizeof(Lit) == sizeof(uint32_t)); + assert(sizeof(float) == sizeof(uint32_t)); + void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size())); + return new (mem) Clause(ps, learnt); } + + int size () const { return size_etc >> 3; } + void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } + void pop () { shrink(1); } + bool learnt () const { return size_etc & 1; } + uint32_t mark () const { return (size_etc >> 1) & 3; } + void mark (uint32_t m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); } + const Lit& last () const { return data[size()-1]; } + + // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for + // subsumption operations to behave correctly. + Lit& operator [] (int i) { return data[i]; } + Lit operator [] (int i) const { return data[i]; } + operator const Lit* (void) const { return data; } + + float& activity () { return extra.act; } + uint32_t abstraction () const { return extra.abst; } + + Lit subsumes (const Clause& other) const; + void strengthen (Lit p); + }; + + + /*_________________________________________________________________________________________________ + | + | subsumes : (other : const Clause&) -> Lit + | + | Description: + | Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' + | by subsumption resolution. + | + | Result: + | lit_Error - No subsumption or simplification + | lit_Undef - Clause subsumes 'other' + | p - The literal p can be deleted from 'other' + |[EMAIL PROTECTED]/ + inline Lit Clause::subsumes(const Clause& other) const + { + if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) + return lit_Error; + + Lit ret = lit_Undef; + const Lit* c = (const Lit*)(*this); + const Lit* d = (const Lit*)other; + + for (int i = 0; i < size(); i++) { + // search for c[i] or ~c[i] + for (int j = 0; j < other.size(); j++) + if (c[i] == d[j]) + goto ok; + else if (ret == lit_Undef && c[i] == ~d[j]){ + ret = c[i]; + goto ok; + } + + // did not find it + return lit_Error; + ok:; + } + + return ret; + } + + + inline void Clause::strengthen(Lit p) + { + remove(*this, p); + calcAbstraction(); + } + + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Sort.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Sort.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Sort.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,93 ---- + /******************************************************************************************[Sort.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Sort_h + #define Sort_h + + #include "Vec.h" + + //================================================================================================= + // Some sorting algorithms for vec's + + + template<class T> + struct LessThan_default { + bool operator () (T x, T y) { return x < y; } + }; + + + template <class T, class LessThan> + void selectionSort(T* array, int size, LessThan lt) + { + int i, j, best_i; + T tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (lt(array[j], array[best_i])) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } + } + template <class T> static inline void selectionSort(T* array, int size) { + selectionSort(array, size, LessThan_default<T>()); } + + template <class T, class LessThan> + void sort(T* array, int size, LessThan lt) + { + if (size <= 15) + selectionSort(array, size, lt); + + else{ + T pivot = array[size / 2]; + T tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(lt(array[i], pivot)); + do j--; while(lt(pivot, array[j])); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sort(array , i , lt); + sort(&array[i], size-i, lt); + } + } + template <class T> static inline void sort(T* array, int size) { + sort(array, size, LessThan_default<T>()); } + + + //================================================================================================= + // For 'vec's: + + + template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { + sort((T*)v, v.size(), lt); } + template <class T> void sort(vec<T>& v) { + sort(v, LessThan_default<T>()); } + + + //================================================================================================= + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Vec.h diff -c /dev/null llvm-test/MultiSource/Benchmarks/minisat/Vec.h:1.1 *** /dev/null Thu Feb 8 11:52:09 2007 --- llvm-test/MultiSource/Benchmarks/minisat/Vec.h Thu Feb 8 11:51:53 2007 *************** *** 0 **** --- 1,133 ---- + /*******************************************************************************************[Vec.h] + MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + + Permission is hereby granted, free of charge, to any person obtaining a copy of this software and + associated documentation files (the "Software"), to deal in the Software without restriction, + including without limitation the rights to use, copy, modify, merge, publish, distribute, + sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all copies or + substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT + NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, + DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT + OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + + #ifndef Vec_h + #define Vec_h + + #include <cstdlib> + #include <cassert> + #include <new> + + //================================================================================================= + // Automatically resizable arrays + // + // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + + template<class T> + class vec { + T* data; + int sz; + int cap; + + void init(int size, const T& pad); + void grow(int min_cap); + + // Don't allow copying (error prone): + vec<T>& operator = (vec<T>& other) { assert(0); return *this; } + vec (vec<T>& other) { assert(0); } + + static inline int imin(int x, int y) { + int mask = (x-y) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + static inline int imax(int x, int y) { + int mask = (y-x) >> (sizeof(int)*8-1); + return (x&mask) + (y&(~mask)); } + + public: + // Types: + typedef int Key; + typedef T Datum; + + // Constructors: + vec(void) : data(NULL) , sz(0) , cap(0) { } + vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } + vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } + vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()') + ~vec(void) { clear(true); } + + // Ownership of underlying array: + T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } + operator T* (void) { return data; } // (unsafe but convenient) + operator const T* (void) const { return data; } + + // Size operations: + int size (void) const { return sz; } + void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } + void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; } + void pop (void) { sz--, data[sz].~T(); } + void growTo (int size); + void growTo (int size, const T& pad); + void clear (bool dealloc = false); + void capacity (int size) { grow(size); } + + // Stack interface: + #if 1 + void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } + //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; } + void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } + void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } + #else + void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } + void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } + #endif + + const T& last (void) const { return data[sz-1]; } + T& last (void) { return data[sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return data[index]; } + T& operator [] (int index) { return data[index]; } + + + // Duplicatation (preferred instead): + void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } + void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } + }; + + template<class T> + void vec<T>::grow(int min_cap) { + if (min_cap <= cap) return; + if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; + else do cap = (cap*3+1) >> 1; while (cap < min_cap); + data = (T*)realloc(data, cap * sizeof(T)); } + + template<class T> + void vec<T>::growTo(int size, const T& pad) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(pad); + sz = size; } + + template<class T> + void vec<T>::growTo(int size) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(); + sz = size; } + + template<class T> + void vec<T>::clear(bool dealloc) { + if (data != NULL){ + for (int i = 0; i < sz; i++) data[i].~T(); + sz = 0; + if (dealloc) free(data), data = NULL, cap = 0; } } + + + #endif Index: llvm-test/MultiSource/Benchmarks/minisat/Makefile diff -u llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.3 llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.4 --- llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.3 Thu Feb 8 02:47:12 2007 +++ llvm-test/MultiSource/Benchmarks/minisat/Makefile Thu Feb 8 11:51:53 2007 @@ -2,8 +2,11 @@ LEVEL = ../../.. PROG = minisat -CPPFLAGS = -D NDEBUG -Imtl +CPPFLAGS = -D NDEBUG LDFLAGS = -lz +RUN_OPTIONS = -verbosity=0 short.cnf.gz +ifdef LARGE_PROBLEM_SIZE RUN_OPTIONS = -verbosity=0 long.cnf.gz +endif include ../../Makefile.multisrc _______________________________________________ llvm-commits mailing list llvm-commits@cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits