summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/mtl
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvminisat/mtl')
-rw-r--r--src/prop/bvminisat/mtl/Alg.h84
-rw-r--r--src/prop/bvminisat/mtl/Alloc.h131
-rw-r--r--src/prop/bvminisat/mtl/Heap.h148
-rw-r--r--src/prop/bvminisat/mtl/IntTypes.h42
-rw-r--r--src/prop/bvminisat/mtl/Map.h193
-rw-r--r--src/prop/bvminisat/mtl/Queue.h69
-rw-r--r--src/prop/bvminisat/mtl/Sort.h98
-rw-r--r--src/prop/bvminisat/mtl/Vec.h130
-rw-r--r--src/prop/bvminisat/mtl/XAlloc.h45
-rw-r--r--src/prop/bvminisat/mtl/config.mk6
-rw-r--r--src/prop/bvminisat/mtl/template.mk107
11 files changed, 1053 insertions, 0 deletions
diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h
new file mode 100644
index 000000000..f3ecdecc5
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Alg.h
@@ -0,0 +1,84 @@
+/*******************************************************************************************[Alg.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 BVMinisat_Alg_h
+#define BVMinisat_Alg_h
+
+#include "prop/bvminisat/mtl/Vec.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+// Useful functions on vector-like types:
+
+//=================================================================================================
+// Removing and searching for elements:
+//
+
+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();
+}
+
+
+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();
+}
+
+
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
+{
+ to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+ if (!append)
+ to.clear();
+ for (int i = 0; i < from.size(); i++){
+ to.push();
+ copy(from[i], to.last());
+ }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h
new file mode 100644
index 000000000..f4303044f
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Alloc.h
@@ -0,0 +1,131 @@
+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-2010, 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 BVMinisat_Alloc_h
+#define BVMinisat_Alloc_h
+
+#include "prop/bvminisat/mtl/XAlloc.h"
+#include "prop/bvminisat/mtl/Vec.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+ T* memory;
+ uint32_t sz;
+ uint32_t cap;
+ uint32_t wasted_;
+
+ void capacity(uint32_t min_cap);
+
+ public:
+ // TODO: make this a class for better type-checking?
+ typedef uint32_t Ref;
+ enum { Ref_Undef = UINT32_MAX };
+ enum { Unit_Size = sizeof(uint32_t) };
+
+ explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+ ~RegionAllocator()
+ {
+ if (memory != NULL)
+ ::free(memory);
+ }
+
+
+ uint32_t size () const { return sz; }
+ uint32_t wasted () const { return wasted_; }
+
+ Ref alloc (int size);
+ void free (int size) { wasted_ += size; }
+
+ // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+ T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; }
+ const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+
+ T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; }
+ const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
+ Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+ return (Ref)(t - &memory[0]); }
+
+ void moveTo(RegionAllocator& to) {
+ if (to.memory != NULL) ::free(to.memory);
+ to.memory = memory;
+ to.sz = sz;
+ to.cap = cap;
+ to.wasted_ = wasted_;
+
+ memory = NULL;
+ sz = cap = wasted_ = 0;
+ }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+ if (cap >= min_cap) return;
+
+ uint32_t prev_cap = cap;
+ while (cap < min_cap){
+ // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+ // result even by clearing the least significant bit. The resulting sequence of capacities
+ // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+ // using 'uint32_t' as indices so that as much as possible of this space can be used.
+ uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+ cap += delta;
+
+ if (cap <= prev_cap)
+ throw OutOfMemoryException();
+ }
+ // printf(" .. (%p) cap = %u\n", this, cap);
+
+ assert(cap > 0);
+ memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{
+ // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+ assert(size > 0);
+ capacity(sz + size);
+
+ uint32_t prev_sz = sz;
+ sz += size;
+
+ // Handle overflow:
+ if (sz < prev_sz)
+ throw OutOfMemoryException();
+
+ return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h
new file mode 100644
index 000000000..d57824ba1
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Heap.h
@@ -0,0 +1,148 @@
+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 BVMinisat_Heap_h
+#define BVMinisat_Heap_h
+
+#include "prop/bvminisat/mtl/Vec.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp>
+class Heap {
+ Comp lt; // The heap is a minimum-heap with respect to this comparator
+ vec<int> heap; // Heap of integers
+ vec<int> indices; // Each integers position (index) in the 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; }
+
+
+ void percolateUp(int i)
+ {
+ int x = heap[i];
+ int p = parent(i);
+
+ while (i != 0 && lt(x, heap[p])){
+ heap[i] = heap[p];
+ indices[heap[p]] = i;
+ i = p;
+ p = parent(p);
+ }
+ heap [i] = x;
+ indices[x] = i;
+ }
+
+
+ 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;
+ }
+
+
+ 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]); }
+ void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+
+
+ // Safe variant of insert/decrease/increase:
+ void update(int n)
+ {
+ if (!inHeap(n))
+ insert(n);
+ else {
+ percolateUp(indices[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;
+ }
+
+
+ // Rebuild the heap from scratch, using the elements in 'ns':
+ void build(vec<int>& ns) {
+ for (int i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+ heap.clear();
+
+ for (int i = 0; i < ns.size(); i++){
+ indices[ns[i]] = i;
+ heap.push(ns[i]); }
+
+ for (int i = heap.size() / 2 - 1; i >= 0; i--)
+ percolateDown(i);
+ }
+
+ void clear(bool dealloc = false)
+ {
+ for (int i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+ heap.clear(dealloc);
+ }
+};
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/bvminisat/mtl/IntTypes.h b/src/prop/bvminisat/mtl/IntTypes.h
new file mode 100644
index 000000000..19ca38bea
--- /dev/null
+++ b/src/prop/bvminisat/mtl/IntTypes.h
@@ -0,0 +1,42 @@
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-2010, 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 BVMinisat_IntTypes_h
+#define BVMinisat_IntTypes_h
+
+#ifdef __sun
+ // Not sure if there are newer versions that support C99 headers. The
+ // needed features are implemented in the headers below though:
+
+# include <sys/int_types.h>
+# include <sys/int_fmtio.h>
+# include <sys/int_limits.h>
+
+#else
+
+# include <stdint.h>
+# include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
new file mode 100644
index 000000000..8bd5659bc
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Map.h
@@ -0,0 +1,193 @@
+/*******************************************************************************************[Map.h]
+Copyright (c) 2006-2010, 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 BVMinisat_Map_h
+#define BVMinisat_Map_h
+
+#include "prop/bvminisat/mtl/IntTypes.h"
+#include "prop/bvminisat/mtl/Vec.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+// 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; } };
+
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
+//=================================================================================================
+// 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 {
+ public:
+ struct Pair { K key; D data; };
+
+ private:
+ 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); }
+
+ bool checkCap(int new_size) const { return new_size > cap; }
+
+ int32_t index (const K& k) const { return hash(k) % cap; }
+ void _insert (const K& k, const D& d) {
+ vec<Pair>& ps = table[index(k)];
+ ps.push(); ps.last().key = k; ps.last().data = d; }
+
+ void rehash () {
+ const vec<Pair>* old = table;
+
+ int old_cap = cap;
+ int newsize = primes[0];
+ for (int i = 1; newsize <= cap && i < nprimes; i++)
+ newsize = primes[i];
+
+ table = new vec<Pair>[newsize];
+ cap = newsize;
+
+ for (int i = 0; i < old_cap; i++){
+ for (int j = 0; j < old[i].size(); j++){
+ _insert(old[i][j].key, old[i][j].data); }}
+
+ delete [] old;
+
+ // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
+ }
+
+
+ public:
+
+ Map () : table(NULL), cap(0), size(0) {}
+ Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
+ ~Map () { delete [] table; }
+
+ // PRECONDITION: the key must already exist in the map.
+ const D& operator [] (const K& k) const
+ {
+ assert(size != 0);
+ const D* res = NULL;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
+
+ // PRECONDITION: the key must already exist in the map.
+ D& operator [] (const K& k)
+ {
+ assert(size != 0);
+ D* res = NULL;
+ vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
+
+ // PRECONDITION: the key must *NOT* exist in the map.
+ void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+ bool peek (const K& k, D& d) const {
+ 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;
+ }
+
+ bool has (const K& k) const {
+ 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))
+ return true;
+ return false;
+ }
+
+ // PRECONDITION: the key must exist in the map.
+ 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();
+ size--;
+ }
+
+ void clear () {
+ cap = size = 0;
+ delete [] table;
+ table = NULL;
+ }
+
+ int elems() const { return size; }
+ int bucket_count() const { return cap; }
+
+ // NOTE: the hash and equality objects are not moved by this method:
+ void moveTo(Map& other){
+ delete [] other.table;
+
+ other.table = table;
+ other.cap = cap;
+ other.size = size;
+
+ table = NULL;
+ size = cap = 0;
+ }
+
+ // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+ const vec<Pair>& bucket(int i) const { return table[i]; }
+};
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h
new file mode 100644
index 000000000..83321ba95
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Queue.h
@@ -0,0 +1,69 @@
+/*****************************************************************************************[Queue.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 BVMinisat_Queue_h
+#define BVMinisat_Queue_h
+
+#include "prop/bvminisat/mtl/Vec.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+
+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 (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+ int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+ const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+ T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+ T peek () const { 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
diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
new file mode 100644
index 000000000..9bab9a0df
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Sort.h
@@ -0,0 +1,98 @@
+/******************************************************************************************[Sort.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 BVMinisat_Sort_h
+#define BVMinisat_Sort_h
+
+#include "mtl/Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+namespace BVMinisat {
+
+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
diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h
new file mode 100644
index 000000000..8c568dfe9
--- /dev/null
+++ b/src/prop/bvminisat/mtl/Vec.h
@@ -0,0 +1,130 @@
+/*******************************************************************************************[Vec.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 BVMinisat_Vec_h
+#define BVMinisat_Vec_h
+
+#include <assert.h>
+#include <new>
+
+#include "prop/bvminisat/mtl/IntTypes.h"
+#include "prop/bvminisat/mtl/XAlloc.h"
+
+namespace BVMinisat {
+
+//=================================================================================================
+// 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;
+
+ // Don't allow copying (error prone):
+ vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
+ vec (vec<T>& other) { assert(0); }
+
+ // Helpers for calculating next capacity:
+ static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
+ //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+ static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+
+public:
+ // Constructors:
+ vec() : data(NULL) , sz(0) , cap(0) { }
+ explicit 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() { clear(true); }
+
+ // Pointer to first element:
+ operator T* (void) { 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; }
+ int capacity (void) const { return cap; }
+ void capacity (int min_cap);
+ void growTo (int size);
+ void growTo (int size, const T& pad);
+ void clear (bool dealloc = false);
+
+ // Stack interface:
+ void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+ void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
+ void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
+ void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+ // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+ // happen given the way capacities are calculated (below). Essentially, all capacities are
+ // even, but INT_MAX is odd.
+
+ 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++) copy[i] = 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>::capacity(int min_cap) {
+ if (cap >= min_cap) return;
+ int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
+ throw OutOfMemoryException();
+ }
+
+
+template<class T>
+void vec<T>::growTo(int size, const T& pad) {
+ if (sz >= size) return;
+ capacity(size);
+ for (int i = sz; i < size; i++) data[i] = pad;
+ sz = size; }
+
+
+template<class T>
+void vec<T>::growTo(int size) {
+ if (sz >= size) return;
+ capacity(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
diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h
new file mode 100644
index 000000000..7b89d1803
--- /dev/null
+++ b/src/prop/bvminisat/mtl/XAlloc.h
@@ -0,0 +1,45 @@
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-2010, 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 BVMinisat_XAlloc_h
+#define BVMinisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace BVMinisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+ void* mem = realloc(ptr, size);
+ if (mem == NULL && errno == ENOMEM){
+ throw OutOfMemoryException();
+ }else
+ return mem;
+}
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/bvminisat/mtl/config.mk b/src/prop/bvminisat/mtl/config.mk
new file mode 100644
index 000000000..b5c36fc6b
--- /dev/null
+++ b/src/prop/bvminisat/mtl/config.mk
@@ -0,0 +1,6 @@
+##
+## This file is for system specific configurations. For instance, on
+## some systems the path to zlib needs to be added. Example:
+##
+## CFLAGS += -I/usr/local/include
+## LFLAGS += -L/usr/local/lib
diff --git a/src/prop/bvminisat/mtl/template.mk b/src/prop/bvminisat/mtl/template.mk
new file mode 100644
index 000000000..3f443fc38
--- /dev/null
+++ b/src/prop/bvminisat/mtl/template.mk
@@ -0,0 +1,107 @@
+##
+## Template makefile for Standard, Profile, Debug, Release, and Release-static versions
+##
+## eg: "make rs" for a statically linked release version.
+## "make d" for a debug version (no optimizations).
+## "make" for the standard version (optimized, but with debug information and assertions active)
+
+PWD = $(shell pwd)
+EXEC ?= $(notdir $(PWD))
+
+CSRCS = $(wildcard $(PWD)/*.cc)
+DSRCS = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
+CHDRS = $(wildcard $(PWD)/*.h)
+COBJS = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
+
+PCOBJS = $(addsuffix p, $(COBJS))
+DCOBJS = $(addsuffix d, $(COBJS))
+RCOBJS = $(addsuffix r, $(COBJS))
+
+
+CXX ?= g++
+CFLAGS ?= -Wall -Wno-parentheses
+LFLAGS ?= -Wall
+
+COPTIMIZE ?= -O3
+
+CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
+LFLAGS += -lz
+
+.PHONY : s p d r rs clean
+
+s: $(EXEC)
+p: $(EXEC)_profile
+d: $(EXEC)_debug
+r: $(EXEC)_release
+rs: $(EXEC)_static
+
+libs: lib$(LIB)_standard.a
+libp: lib$(LIB)_profile.a
+libd: lib$(LIB)_debug.a
+libr: lib$(LIB)_release.a
+
+## Compile options
+%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
+%.od: CFLAGS +=-O0 -g -D DEBUG
+%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
+
+## Link options
+$(EXEC): LFLAGS += -g
+$(EXEC)_profile: LFLAGS += -g -pg
+$(EXEC)_debug: LFLAGS += -g
+#$(EXEC)_release: LFLAGS += ...
+$(EXEC)_static: LFLAGS += --static
+
+## Dependencies
+$(EXEC): $(COBJS)
+$(EXEC)_profile: $(PCOBJS)
+$(EXEC)_debug: $(DCOBJS)
+$(EXEC)_release: $(RCOBJS)
+$(EXEC)_static: $(RCOBJS)
+
+lib$(LIB)_standard.a: $(filter-out */Main.o, $(COBJS))
+lib$(LIB)_profile.a: $(filter-out */Main.op, $(PCOBJS))
+lib$(LIB)_debug.a: $(filter-out */Main.od, $(DCOBJS))
+lib$(LIB)_release.a: $(filter-out */Main.or, $(RCOBJS))
+
+
+## Build rule
+%.o %.op %.od %.or: %.cc
+ @echo Compiling: $(subst $(MROOT)/,,$@)
+ @$(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+ @echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(CXX) $^ $(LFLAGS) -o $@
+
+## Library rules (standard/profile/debug/release)
+lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
+ @echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(AR) -rcsv $@ $^
+
+## Library Soft Link rule:
+libs libp libd libr:
+ @echo "Making Soft Link: $^ -> lib$(LIB).a"
+ @ln -sf $^ lib$(LIB).a
+
+## Clean rule
+clean:
+ @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk
+
+## Make dependencies
+depend.mk: $(CSRCS) $(CHDRS)
+ @echo Making dependencies
+ @$(CXX) $(CFLAGS) -I$(MROOT) \
+ $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
+ @for dir in $(DEPDIR); do \
+ if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
+ echo Depends on: $${dir}; \
+ cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
+ fi; \
+ done
+
+-include $(MROOT)/mtl/config.mk
+-include depend.mk
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback