Skip to content

Commit 6477e8b

Browse files
committed
Fixing scan-forward Windows
1 parent 3838b94 commit 6477e8b

File tree

1 file changed

+22
-17
lines changed

1 file changed

+22
-17
lines changed

src/packedrow.cpp

Lines changed: 22 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,22 @@ THE SOFTWARE.
3434

3535
using namespace CMSat;
3636

37+
#ifdef _MSC_VER
38+
inline int scan_fwd_64b(int64_t value)
39+
{
40+
unsigned long at;
41+
unsigned char ret = _BitScanForward64(&at, value);
42+
at++;
43+
if (!ret) at = 0;
44+
return at;
45+
}
46+
#else
47+
inline int scan_fwd_64b(uint64_t value)
48+
{
49+
return __builtin_ffsll(value);
50+
}
51+
#endif
52+
3753
///returns popcnt
3854
uint32_t PackedRow::find_watchVar(
3955
vector<Lit>& tmp_clause,
@@ -78,13 +94,7 @@ void PackedRow::get_reason(
7894
for (int i = 0; i < size; i++) if (mp[i]) {
7995
int64_t tmp = mp[i];
8096
unsigned long at;
81-
#ifdef _MSC_VER
82-
unsigned char ret = _BitScanForward64(&at, tmp);
83-
at++;
84-
if (!ret) at = 0;
85-
#else
86-
at = __builtin_ffsll(tmp);
87-
#endif
97+
at = scan_fwd_64b(tmp);
8898
int extra = 0;
8999
while (at != 0) {
90100
uint32_t col = extra + at-1 + i*64;
@@ -105,13 +115,7 @@ void PackedRow::get_reason(
105115
break;
106116

107117
tmp >>= at;
108-
#ifdef _MSC_VER
109-
unsigned char ret = _BitScanForward64(&at, tmp);
110-
at++;
111-
if (!ret) at = 0;
112-
#else
113-
at = __builtin_ffsll(tmp);
114-
#endif
118+
at = scan_fwd_64b(tmp);
115119
}
116120
}
117121

@@ -147,7 +151,8 @@ gret PackedRow::propGause(
147151
if (pop >= 2) {
148152
for (int i = 0; i < size; i++) if (tmp_col.mp[i]) {
149153
int64_t tmp = tmp_col.mp[i];
150-
int at = __builtin_ffsll(tmp);
154+
unsigned long at;
155+
at = scan_fwd_64b(tmp);
151156
int extra = 0;
152157
while (at != 0) {
153158
uint32_t col = extra + at-1 + i*64;
@@ -172,7 +177,7 @@ gret PackedRow::propGause(
172177
break;
173178

174179
tmp >>= at;
175-
at = __builtin_ffsll(tmp);
180+
at = scan_fwd_64b(tmp);
176181
}
177182
}
178183
assert(false && "Should have found a new watch!");
@@ -185,7 +190,7 @@ gret PackedRow::propGause(
185190
//Lazy prop
186191
if (pop == 1) {
187192
for (int i = 0; i < size; i++) if (tmp_col.mp[i]) {
188-
int at = __builtin_ffsll(tmp_col.mp[i]);
193+
int at = scan_fwd_64b(tmp_col.mp[i]);
189194

190195
// found prop
191196
uint32_t col = at-1 + i*64;

0 commit comments

Comments
 (0)