1 files changed, 255 insertions, 0 deletions
diff --git a/stp/sat/Global.h b/stp/sat/Global.h
new file mode 100644
index 00000000..a428975c
--- /dev/null
+++ b/stp/sat/Global.h
@@ -0,0 +1,255 @@
+/****************************************************************************************[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