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
min(T x,T y)58 template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
max(T x,T 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):
154 vec<T>& operator = (vec<T>& other) { TEMPLATE_FAIL; }
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 (©[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
235