minisat_global.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_global.h
00004  *\brief MiniSat global functions
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 /****************************************************************************************[Global.h]
00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
00023 
00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00025 associated documentation files (the "Software"), to deal in the Software without restriction,
00026 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00028 furnished to do so, subject to the following conditions:
00029 
00030 The above copyright notice and this permission notice shall be included in all copies or
00031 substantial portions of the Software.
00032 
00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00038 **************************************************************************************************/
00039 
00040 #ifndef _cvc3__minisat__global_h_
00041 #define _cvc3__minisat__global_h_
00042 
00043 //=================================================================================================
00044 // Basic Types & Minor Things:
00045 // provides lbool and vec
00046 
00047 #include "debug.h"
00048 #include <cstdio>
00049 #include <cstdlib>
00050 #include <climits>
00051 #include <cfloat>
00052 #include <cstring>
00053 #include <new>
00054 
00055 
00056 namespace MiniSat {
00057 
00058 template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
00059 template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; }
00060 
00061 template <bool> struct STATIC_ASSERTION_FAILURE;
00062 template <> struct STATIC_ASSERTION_FAILURE<true>{};
00063 #define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
00064 
00065 
00066 //=================================================================================================
00067 // 'malloc()'-style memory allocation -- never returns NULL; aborts instead:
00068 
00069 
00070 template<class T> static inline T* xmalloc(size_t size) {
00071     T*   tmp = (T*)malloc(size * sizeof(T));
00072     DebugAssert(size == 0 || tmp != NULL, "Minisat::Global::xmalloc");
00073     return tmp; }
00074 
00075 template<class T> static inline T* xrealloc(T* ptr, size_t size) {
00076     T*   tmp = (T*)realloc((void*)ptr, size * sizeof(T));
00077     DebugAssert(size == 0 || tmp != NULL, "Minisat::Global::xrealloc");
00078     return tmp; }
00079 
00080 template<class T> static inline void xfree(T *ptr) {
00081     if (ptr != NULL) free((void*)ptr); }
00082 
00083 
00084 //=================================================================================================
00085 // Random numbers:
00086 
00087 
00088 // Returns a random float 0 <= x < 1. Seed must never be 0.
00089 static inline double drand(double& seed) {
00090     seed *= 1389796;
00091     int q = (int)(seed / 2147483647);
00092     seed -= (double)q * 2147483647;
00093     return seed / 2147483647; }
00094 
00095 // Returns a random integer 0 <= x < size. Seed must never be 0.
00096 static inline int irand(double& seed, int size) {
00097     return (int)(drand(seed) * size); }
00098 
00099 
00100 
00101 //=================================================================================================
00102 // 'vec' -- automatically resizable arrays (via 'push()' method):
00103 
00104 
00105 // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
00106 
00107 template<class T>
00108 class vec {
00109     T*  data;
00110     int sz;
00111     int cap;
00112 
00113     void     init(int size, const T& pad);
00114     void     grow(int min_cap);
00115 
00116 public:
00117     // Types:
00118     typedef int Key;
00119     typedef T   Datum;
00120 
00121     // Constructors:
00122     vec(void)                   : data(NULL) , sz(0)   , cap(0)    { }
00123     vec(int size)               : data(NULL) , sz(0)   , cap(0)    { growTo(size); }
00124     vec(int size, const T& pad) : data(NULL) , sz(0)   , cap(0)    { growTo(size, pad); }
00125     vec(T* array, int size)     : data(array), sz(size), cap(size) { }      // (takes ownership of array -- will be deallocated with 'xfree()')
00126    ~vec(void)                                                      { clear(true); }
00127 
00128     // Ownership of underlying array:
00129     T*       release  (void)           { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
00130     operator T*       (void)           { return data; }     // (unsafe but convenient)
00131     operator const T* (void) const     { return data; }
00132 
00133     // Size operations:
00134     int      size   (void) const       { return sz; }
00135     void     shrink (int nelems)       { DebugAssert(nelems <= sz, "MiniSat::vec::shrink");
00136                                          for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
00137     void     pop    (void)             { sz--, data[sz].~T(); }
00138     void     growTo (int size);
00139     void     growTo (int size, const T& pad);
00140     void     clear  (bool dealloc = false);
00141     void     capacity (int size) { grow(size); }
00142 
00143     // Stack interface:
00144     void     push  (void)              { if (sz == cap) grow(sz+1); new (&data[sz]) T()    ; sz++; }
00145     void     push  (const T& elem)     { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
00146     const T& last  (void) const        { return data[sz-1]; }
00147     T&       last  (void)              { return data[sz-1]; }
00148 
00149     // Vector interface:
00150     const T& operator [] (int index) const  { return data[index]; }
00151     T&       operator [] (int index)        { return data[index]; }
00152 
00153     // Don't allow copying (error prone):
00154     vec<T>&  operator = (vec<T>& other) { TEMPLATE_FAIL; }
00155              vec        (vec<T>& other) { TEMPLATE_FAIL; }
00156 
00157     // Duplicatation (preferred instead):
00158     void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
00159     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
00160 };
00161 
00162 template<class T>
00163 void vec<T>::grow(int min_cap) {
00164     if (min_cap <= cap) return;
00165     if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
00166     else          do cap = (cap*3+1) >> 1; while (cap < min_cap);
00167     data = xrealloc(data, cap); }
00168 
00169 template<class T>
00170 void vec<T>::growTo(int size, const T& pad) {
00171     if (sz >= size) return;
00172     grow(size);
00173     for (int i = sz; i < size; i++) new (&data[i]) T(pad);
00174     sz = size; }
00175 
00176 template<class T>
00177 void vec<T>::growTo(int size) {
00178     if (sz >= size) return;
00179     grow(size);
00180     for (int i = sz; i < size; i++) new (&data[i]) T();
00181     sz = size; }
00182 
00183 template<class T>
00184 void vec<T>::clear(bool dealloc) {
00185     if (data != NULL){
00186         for (int i = 0; i < sz; i++) data[i].~T();
00187         sz = 0;
00188         if (dealloc) xfree(data), data = NULL, cap = 0; } }
00189 
00190 
00191 //=================================================================================================
00192 // Lifted booleans:
00193 
00194 
00195 class lbool {
00196     int     value;
00197     explicit lbool(int v) : value(v) { }
00198 
00199 public:
00200     lbool()       : value(0) { }
00201     lbool(bool x) : value((int)x*2-1) { }
00202     int toInt(void) const { return value; }
00203 
00204     bool  operator == (const lbool& other) const { return value == other.value; }
00205     bool  operator != (const lbool& other) const { return value != other.value; }
00206     lbool operator ~  (void)               const { return lbool(-value); }
00207 
00208     friend int   toInt  (lbool l);
00209     friend lbool toLbool(int   v);
00210 };
00211 inline int   toInt  (lbool l) { return l.toInt(); }
00212 inline lbool toLbool(int   v) { return lbool(v);  }
00213 
00214 const lbool l_True  = toLbool( 1);
00215 const lbool l_False = toLbool(-1);
00216 const lbool l_Undef = toLbool( 0);
00217 
00218 
00219 //=================================================================================================
00220 // Relation operators -- extend definitions from '==' and '<'
00221 
00222 
00223 #ifndef __SGI_STL_INTERNAL_RELOPS   // (be aware of SGI's STL implementation...)
00224 #define __SGI_STL_INTERNAL_RELOPS
00225 template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
00226 template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
00227 template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
00228 template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }
00229 #endif
00230 
00231 }
00232 
00233 //=================================================================================================
00234 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2