CVC3  2.4.1
minisat_global.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_global.h
4  *\brief MiniSat global functions
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 /****************************************************************************************[Global.h]
22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
23 
24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
25 associated documentation files (the "Software"), to deal in the Software without restriction,
26 including without limitation the rights to use, copy, modify, merge, publish, distribute,
27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
28 furnished to do so, subject to the following conditions:
29 
30 The above copyright notice and this permission notice shall be included in all copies or
31 substantial portions of the Software.
32 
33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
38 **************************************************************************************************/
39 
40 #ifndef _cvc3__minisat__global_h_
41 #define _cvc3__minisat__global_h_
42 
43 //=================================================================================================
44 // Basic Types & Minor Things:
45 // provides lbool and vec
46 
47 #include "debug.h"
48 #include <cstdio>
49 #include <cstdlib>
50 #include <climits>
51 #include <cfloat>
52 #include <cstring>
53 #include <new>
54 
55 
56 namespace MiniSat {
57 
58 template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
59 template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; }
60 
61 template <bool> struct STATIC_ASSERTION_FAILURE;
62 template <> struct STATIC_ASSERTION_FAILURE<true>{};
63 #define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
64 
65 
66 //=================================================================================================
67 // 'malloc()'-style memory allocation -- never returns NULL; aborts instead:
68 
69 
70 template<class T> static inline T* xmalloc(size_t size) {
71  T* tmp = (T*)malloc(size * sizeof(T));
72  DebugAssert(size == 0 || tmp != NULL, "Minisat::Global::xmalloc");
73  return tmp; }
74 
75 template<class T> static inline T* xrealloc(T* ptr, size_t size) {
76  T* tmp = (T*)realloc((void*)ptr, size * sizeof(T));
77  DebugAssert(size == 0 || tmp != NULL, "Minisat::Global::xrealloc");
78  return tmp; }
79 
80 template<class T> static inline void xfree(T *ptr) {
81  if (ptr != NULL) free((void*)ptr); }
82 
83 
84 //=================================================================================================
85 // Random numbers:
86 
87 
88 // Returns a random float 0 <= x < 1. Seed must never be 0.
89 static inline double drand(double& seed) {
90  seed *= 1389796;
91  int q = (int)(seed / 2147483647);
92  seed -= (double)q * 2147483647;
93  return seed / 2147483647; }
94 
95 // Returns a random integer 0 <= x < size. Seed must never be 0.
96 static inline int irand(double& seed, int size) {
97  return (int)(drand(seed) * size); }
98 
99 
100 
101 //=================================================================================================
102 // 'vec' -- automatically resizable arrays (via 'push()' method):
103 
104 
105 // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
106 
107 template<class T>
108 class vec {
109  T* data;
110  int sz;
111  int cap;
112 
113  void init(int size, const T& pad);
114  void grow(int min_cap);
115 
116 public:
117  // Types:
118  typedef int Key;
119  typedef T Datum;
120 
121  // Constructors:
122  vec(void) : data(NULL) , sz(0) , cap(0) { }
123  vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
124  vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
125  vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'xfree()')
126  ~vec(void) { clear(true); }
127 
128  // Ownership of underlying array:
129  T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
130  operator T* (void) { return data; } // (unsafe but convenient)
131  operator const T* (void) const { return data; }
132 
133  // Size operations:
134  int size (void) const { return sz; }
135  void shrink (int nelems) { DebugAssert(nelems <= sz, "MiniSat::vec::shrink");
136  for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
137  void pop (void) { sz--, data[sz].~T(); }
138  void growTo (int size);
139  void growTo (int size, const T& pad);
140  void clear (bool dealloc = false);
141  void capacity (int size) { grow(size); }
142 
143  // Stack interface:
144  void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; }
145  void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
146  const T& last (void) const { return data[sz-1]; }
147  T& last (void) { return data[sz-1]; }
148 
149  // Vector interface:
150  const T& operator [] (int index) const { return data[index]; }
151  T& operator [] (int index) { return data[index]; }
152 
153  // Don't allow copying (error prone):
155  vec (vec<T>& other) { TEMPLATE_FAIL; }
156 
157  // Duplicatation (preferred instead):
158  void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
159  void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
160 };
161 
162 template<class T>
163 void vec<T>::grow(int min_cap) {
164  if (min_cap <= cap) return;
165  if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
166  else do cap = (cap*3+1) >> 1; while (cap < min_cap);
167  data = xrealloc(data, cap); }
168 
169 template<class T>
170 void vec<T>::growTo(int size, const T& pad) {
171  if (sz >= size) return;
172  grow(size);
173  for (int i = sz; i < size; i++) new (&data[i]) T(pad);
174  sz = size; }
175 
176 template<class T>
177 void vec<T>::growTo(int size) {
178  if (sz >= size) return;
179  grow(size);
180  for (int i = sz; i < size; i++) new (&data[i]) T();
181  sz = size; }
182 
183 template<class T>
184 void vec<T>::clear(bool dealloc) {
185  if (data != NULL){
186  for (int i = 0; i < sz; i++) data[i].~T();
187  sz = 0;
188  if (dealloc) xfree(data), data = NULL, cap = 0; } }
189 
190 
191 //=================================================================================================
192 // Lifted booleans:
193 
194 
195 class lbool {
196  int value;
197  explicit lbool(int v) : value(v) { }
198 
199 public:
200  lbool() : value(0) { }
201  lbool(bool x) : value((int)x*2-1) { }
202  int toInt(void) const { return value; }
203 
204  bool operator == (const lbool& other) const { return value == other.value; }
205  bool operator != (const lbool& other) const { return value != other.value; }
206  lbool operator ~ (void) const { return lbool(-value); }
207 
208  friend int toInt (lbool l);
209  friend lbool toLbool(int v);
210 };
211 inline int toInt (lbool l) { return l.toInt(); }
212 inline lbool toLbool(int v) { return lbool(v); }
213 
214 const lbool l_True = toLbool( 1);
215 const lbool l_False = toLbool(-1);
216 const lbool l_Undef = toLbool( 0);
217 
218 
219 //=================================================================================================
220 // Relation operators -- extend definitions from '==' and '<'
221 
222 
223 #ifndef __SGI_STL_INTERNAL_RELOPS // (be aware of SGI's STL implementation...)
224 #define __SGI_STL_INTERNAL_RELOPS
225 template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
226 template <class T> static inline bool operator > (const T& x, const T& y) { return y < x; }
227 template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x); }
228 template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y); }
229 #endif
230 
231 }
232 
233 //=================================================================================================
234 #endif