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
#ifndef _range_hpp_INCLUDED
#define _range_hpp_INCLUDED
#include <cassert>
namespace CaDiCaL {
struct Clause;
/*----------------------------------------------------------------------*/
// Used for compact and safe iteration over positive ranges of integers,
// particularly for iterating over all variable indices.
//
// Range vars (max_var);
// for (auto idx : vars) ...
//
// This iterates over '1, ..., max_var' and is safe for non-negative
// numbers, thus also for 'max_var == 0' or 'max_var == INT_MAX'.
//
// Note that
//
// for (int idx = 1; idx <= max_var; idx++) ...
//
// leads to an overflow if 'max_var == INT_MAX' and thus depending on what
// the compiler does ('int' overflow is undefined) might lead to any
// behaviour (infinite loop or worse array access way out of bounds).
//
// If we make 'idx' in this last 'for' loop an 'unsigned' then it is safe to
// use this idiom, but we would need to cast 'max_var' explicitly to 'int'
// in order to avoid a warning in the loop condition and actually everywhere
// where 'idx' is compared to a 'signed' expression. Worse for instance
// 'vals[-idx]' will lead to out of bounds access too. This is awkward and
// using the range iterator provided here is safer in general.
//
// Another issue is that the dereferencing operator '*' below is required to
// return a reference to the internal index of the iterator. Thus the 'idx'
// in the auto loop is actually of the same type as the internal state of
// the iterator. To keep it 'signed' and still avoid overflow issues we
// just have to make sure to use the proper increment (with two implicit
// casts, i.e., from 'int' to 'unsigned', then 'unsigned' addition and the
// result is cast back from 'unsigned' to 'int').
//
// For simplicity we keep a reference to the actual maximum integer, e.g.,
// 'max_var', which makes the idiom 'for (auto idx : vars) ...' possible.
// Further note that the referenced integer has to be non-negative before
// starting to iterate (it can be zero though), otherwise it breaks.
class Range {
static unsigned inc (unsigned u) { return u + 1u; }
static unsigned dec (unsigned u) { return u - 1u; }
class iterator {
int idx;
public:
iterator (int i) : idx (i) {}
void operator++ () { idx = inc (idx); }
const int &operator* () const { return idx; }
friend bool operator!= (const iterator &a, const iterator &b) {
return a.idx != b.idx;
}
};
// Reverse iterator for iterating from max_var down to 1
class reverse_iterator {
int idx;
public:
reverse_iterator (int i) : idx (i) {}
void operator++ () { idx = dec (idx); }
const int &operator* () const { return idx; }
friend bool operator!= (const reverse_iterator &a,
const reverse_iterator &b) {
return a.idx != b.idx;
}
};
int &n;
public:
// forward iterator
iterator begin () const { return assert (n >= 0), iterator (inc (0)); }
iterator end () const { return assert (n >= 0), iterator (inc (n)); }
// Reverse iteration methods
reverse_iterator rbegin () const {
return assert (n >= 0), reverse_iterator (n);
}
reverse_iterator rend () const {
return assert (n >= 0), reverse_iterator (0);
}
Range (int &m) : n (m) { assert (m >= 0); }
};
// Same, but iterating over literals '-1,1,-2,2,....,-max_var,max_var'.
//
// The only difference to 'Range' is the 'inc' function, but I am too lazy
// to figure out how to properly factor the code into a generic range
// template with 'inc' as only parameter. This gives at least clean code.
class Sange {
static unsigned inc (unsigned u) { return ~u + (u >> 31); }
class iterator {
int lit;
public:
iterator (int i) : lit (i) {}
void operator++ () { lit = inc (lit); }
const int &operator* () const { return lit; }
friend bool operator!= (const iterator &a, const iterator &b) {
return a.lit != b.lit;
}
};
int &n;
public:
iterator begin () const { return assert (n >= 0), iterator (inc (0)); }
iterator end () const { return assert (n >= 0), iterator (inc (n)); }
Sange (int &m) : n (m) { assert (m >= 0); }
};
} // namespace CaDiCaL
#endif