1 files changed, 0 insertions, 255 deletions
diff --git a/stp/sat/Global.h b/stp/sat/Global.h
deleted file mode 100644
index deaf8c24..00000000
--- a/stp/sat/Global.h
+++ /dev/null
@@ -1,255 +0,0 @@
-/****************************************************************************************[Global.h]
-MiniSat -- Copyright (c) 2003-2005, 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 Global_h
-#define Global_h
-
-#include <cassert>
-#include <cstdio>
-#include <cstdlib>
-#include <cstring>
-#include <new>
-
-// PKT: needs to be outside namespace MINISAT or mac os x compilation breaks
-#ifdef _MSC_VER
-#else
-#include <unistd.h>
-#endif
-
-namespace MINISAT {
-//=================================================================================================
-// Basic Types & Minor Things:
-
-// DWD: This is needed on darwin.
-typedef unsigned int uint;
-
-#ifdef _MSC_VER
-
-typedef INT64              int64;
-typedef UINT64             uint64;
-typedef INT_PTR            intp;
-typedef UINT_PTR           uintp;
-#define I64_fmt "I64d"
-#else
-
-typedef long long          int64;
-typedef unsigned long long uint64;
-typedef __PTRDIFF_TYPE__   intp;
-typedef unsigned __PTRDIFF_TYPE__ uintp;
-#define I64_fmt "lld"
-#endif
-
-template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
-template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; }
-
-template <bool> struct STATIC_ASSERTION_FAILURE;
-template <> struct STATIC_ASSERTION_FAILURE<true>{};
-#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
-
-
-//=================================================================================================
-// 'malloc()'-style memory allocation -- never returns NULL; aborts instead:
-
-
-template<class T> static inline T* xmalloc(size_t size) {
-    T*   tmp = (T*)malloc(size * sizeof(T));
-    assert(size == 0 || tmp != NULL);
-    return tmp; }
-
-template<class T> static inline T* xrealloc(T* ptr, size_t size) {
-    T*   tmp = (T*)realloc((void*)ptr, size * sizeof(T));
-    assert(size == 0 || tmp != NULL);
-    return tmp; }
-
-template<class T> static inline void xfree(T *ptr) {
-    if (ptr != NULL) free((void*)ptr); }
-
-
-//=================================================================================================
-// Random numbers:
-
-
-// Returns a random float 0 <= x < 1. Seed must never be 0.
-static inline double drand(double& seed) {
-    seed *= 1389796;
-    int q = (int)(seed / 2147483647);
-    seed -= (double)q * 2147483647;
-    return seed / 2147483647; }
-
-// Returns a random integer 0 <= x < size. Seed must never be 0.
-static inline int irand(double& seed, int size) {
-    return (int)(drand(seed) * size); }
-
-
-//=================================================================================================
-// 'vec' -- automatically resizable arrays (via 'push()' method):
-
-
-// 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);
-
-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 'xfree()')
-   ~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     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:
-    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++; }
-    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]; }
-
-    // Don't allow copying (error prone):
-    vec<T>&  operator = (vec<T>& other) { TEMPLATE_FAIL; }
-             vec        (vec<T>& other) { TEMPLATE_FAIL; }
-
-    // Duplicatation (preferred instead):
-    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[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 = xrealloc(data, cap); }
-
-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) xfree(data), data = NULL, cap = 0; } }
-
-
-//=================================================================================================
-// Useful functions on vectors
-
-
-template<class V, class T>
-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>
-bool find(V& ts, const T& t)
-{
-    int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++) ;
-    return j < ts.size();
-}
-
-//=================================================================================================
-// Lifted booleans:
-
-
-class lbool {
-    int     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 == (const lbool& other) const { return value == other.value; }
-    bool  operator != (const lbool& other) const { return value != other.value; }
-    lbool operator ~  (void)               const { return 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);
-
-
-//=================================================================================================
-// Relation operators -- extend definitions from '==' and '<'
-
-
-#ifndef __SGI_STL_INTERNAL_RELOPS   // (be aware of SGI's STL implementation...)
-#define __SGI_STL_INTERNAL_RELOPS
-template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
-template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
-template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
-template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }
-#endif
-
-
-//=================================================================================================
-}
-#endif