Removing newer version of MiniSat for Dejan's preferred import

11 files changed, 0 insertions, 1053 deletions

diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
deleted file mode 100644
index bb1ee5ad2..000000000
--- a/src/prop/minisat/mtl/Alg.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/*******************************************************************************************[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 Minisat_Alg_h
-#define Minisat_Alg_h
-
-#include "mtl/Vec.h"
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
deleted file mode 100644
index 76322b8b6..000000000
--- a/src/prop/minisat/mtl/Alloc.h
+++ /dev/null
@@ -1,131 +0,0 @@
-/*****************************************************************************************[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 Minisat_Alloc_h
-#define Minisat_Alloc_h
-
-#include "mtl/XAlloc.h"
-#include "mtl/Vec.h"
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
deleted file mode 100644
index 226407e77..000000000
--- a/src/prop/minisat/mtl/Heap.h
+++ /dev/null
@@ -1,148 +0,0 @@
-/******************************************************************************************[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 Minisat_Heap_h
-#define Minisat_Heap_h
-
-#include "mtl/Vec.h"
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/IntTypes.h b/src/prop/minisat/mtl/IntTypes.h
deleted file mode 100644
index c48816284..000000000
--- a/src/prop/minisat/mtl/IntTypes.h
+++ /dev/null
@@ -1,42 +0,0 @@
-/**************************************************************************************[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 Minisat_IntTypes_h
-#define Minisat_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/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
deleted file mode 100644
index 8a82d0e28..000000000
--- a/src/prop/minisat/mtl/Map.h
+++ /dev/null
@@ -1,193 +0,0 @@
-/*******************************************************************************************[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 Minisat_Map_h
-#define Minisat_Map_h
-
-#include "mtl/IntTypes.h"
-#include "mtl/Vec.h"
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
deleted file mode 100644
index 17567d694..000000000
--- a/src/prop/minisat/mtl/Queue.h
+++ /dev/null
@@ -1,69 +0,0 @@
-/*****************************************************************************************[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 Minisat_Queue_h
-#define Minisat_Queue_h
-
-#include "mtl/Vec.h"
-
-namespace Minisat {
-
-//=================================================================================================
-
-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/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
deleted file mode 100644
index e9313ef86..000000000
--- a/src/prop/minisat/mtl/Sort.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/******************************************************************************************[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 Minisat_Sort_h
-#define Minisat_Sort_h
-
-#include "mtl/Vec.h"
-
-//=================================================================================================
-// Some sorting algorithms for vec's
-
-
-namespace Minisat {
-
-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/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
deleted file mode 100644
index 9e220852e..000000000
--- a/src/prop/minisat/mtl/Vec.h
+++ /dev/null
@@ -1,130 +0,0 @@
-/*******************************************************************************************[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 Minisat_Vec_h
-#define Minisat_Vec_h
-
-#include <assert.h>
-#include <new>
-
-#include "mtl/IntTypes.h"
-#include "mtl/XAlloc.h"
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
deleted file mode 100644
index 1da176028..000000000
--- a/src/prop/minisat/mtl/XAlloc.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/****************************************************************************************[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 Minisat_XAlloc_h
-#define Minisat_XAlloc_h
-
-#include <errno.h>
-#include <stdlib.h>
-
-namespace Minisat {
-
-//=================================================================================================
-// 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/minisat/mtl/config.mk b/src/prop/minisat/mtl/config.mk
deleted file mode 100644
index b5c36fc6b..000000000
--- a/src/prop/minisat/mtl/config.mk
+++ /dev/null
@@ -1,6 +0,0 @@
-##
-##  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/minisat/mtl/template.mk b/src/prop/minisat/mtl/template.mk
deleted file mode 100644
index 3f443fc38..000000000
--- a/src/prop/minisat/mtl/template.mk
+++ /dev/null
@@ -1,107 +0,0 @@
-##
-##  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