1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
#ifndef _util_hpp_INCLUDED
#define _util_hpp_INCLUDED
#include <cassert>
#include <cstdint>
#include <vector>
namespace CaDiCaL {
using namespace std;
// Common simple utility functions independent from 'Internal'.
/*------------------------------------------------------------------------*/
inline double relative (double a, double b) { return b ? a / b : 0; }
inline double percent (double a, double b) { return relative (100 * a, b); }
inline int sign (int lit) { return (lit > 0) - (lit < 0); }
inline unsigned bign (int lit) { return 1 + (lit < 0); }
/*------------------------------------------------------------------------*/
bool has_suffix (const char *str, const char *suffix);
bool has_prefix (const char *str, const char *prefix);
/*------------------------------------------------------------------------*/
// Parse integer string in the form of
//
// true
// false
// [-]<mantissa>[e<exponent>]
//
// and in the latter case '<val>' has to be within [-INT_MAX,INT_MAX].
//
// The function returns true if parsing is successful and then also sets
// the second argument to the parsed value.
bool parse_int_str (const char *str, int &);
/*------------------------------------------------------------------------*/
inline bool is_power_of_two (unsigned n) { return n && !(n & (n - 1)); }
inline bool contained (int64_t c, int64_t l, int64_t u) {
return l <= c && c <= u;
}
inline bool aligned (size_t n, size_t alignment) {
assert (is_power_of_two (alignment));
const size_t mask = alignment - 1;
return !(n & mask);
}
inline size_t align (size_t n, size_t alignment) {
size_t res = n;
assert (is_power_of_two (alignment));
const size_t mask = alignment - 1;
if (res & mask)
res = (res | mask) + 1;
assert (aligned (res, alignment));
return res;
}
/*------------------------------------------------------------------------*/
inline bool parity (unsigned a) {
assert (sizeof a == 4);
unsigned tmp = a;
tmp ^= (tmp >> 16);
tmp ^= (tmp >> 8);
tmp ^= (tmp >> 4);
tmp ^= (tmp >> 2);
tmp ^= (tmp >> 1);
return tmp & 1;
}
/*------------------------------------------------------------------------*/
// The standard 'Effective STL' way (though not guaranteed) to clear a
// vector and reduce its capacity to zero, thus deallocating all its
// internal memory. This is quite important for keeping the actual
// allocated size of watched and occurrence lists small particularly during
// bounded variable elimination where many clauses are added and removed.
template <class T> void erase_vector (std::vector<T> &v) {
if (v.capacity ()) {
std::vector<T> ().swap (v);
}
assert (!v.capacity ()); // not guaranteed though
}
// The standard 'Effective STL' way (though not guaranteed) to shrink the
// capacity of a vector to its size thus kind of releasing all the internal
// excess memory not needed at the moment any more.
template <class T> void shrink_vector (std::vector<T> &v) {
if (v.capacity () > v.size ()) {
std::vector<T> (v).swap (v);
}
assert (v.capacity () == v.size ()); // not guaranteed though
}
template <class T>
static void enlarge_init (vector<T> &v, size_t N, const T &i) {
if (v.size () < N)
v.resize (N, i);
}
template <class T> static void enlarge_only (vector<T> &v, size_t N) {
if (v.size () < N)
v.resize (N, T ());
}
template <class T> static void enlarge_zero (vector<T> &v, size_t N) {
enlarge_init (v, N, (const T &) 0);
}
// double the capacity until it fits. This is different from reserve
// that will allocate exactly the size requested, meaning that the
// amortized complexity is lost.
template <class T> static void reserve_at_least (vector<T> &v, size_t N) {
if (N < v.capacity ())
return;
size_t new_size = v.size ();
if (!new_size)
new_size = N;
while (new_size < N)
new_size *= 2;
v.reserve (new_size);
}
// Clean-up class for bad_alloc error safety.
template <typename T> struct DeferDeleteArray {
T *data;
DeferDeleteArray (T *t) : data (t) {}
~DeferDeleteArray () { delete[] data; }
void release () { data = nullptr; }
void free () {
delete[] data;
data = nullptr;
}
};
template <typename T> struct DeferDeletePtr {
T *data;
DeferDeletePtr (T *t) : data (t) {}
~DeferDeletePtr () { delete data; }
void release () { data = nullptr; }
void free () {
delete data;
data = nullptr;
}
};
/*------------------------------------------------------------------------*/
template <class T> inline void clear_n (T *base, size_t n) {
memset (base, 0, sizeof (T) * n);
}
/*------------------------------------------------------------------------*/
// These are options both to 'cadical' and 'mobical'. After wasting some
// on not remembering the spelling (British vs American), nor singular vs
// plural and then wanted to use '--color=false', and '--colours=0' too, I
// just factored this out into these two utility functions.
bool is_color_option (const char *arg); // --color, --colour, ...
bool is_no_color_option (const char *arg); // --no-color, --no-colour, ...
/*------------------------------------------------------------------------*/
uint64_t hash_string (const char *str);
/*------------------------------------------------------------------------*/
} // namespace CaDiCaL
#endif