mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Fix popcnt64

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-30 12:53:13 +01:00
parent add66973c5
commit 3586c288ec
3 changed files with 4 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/xor_matrix_finder.cpp
View file

@ -75,8 +75,8 @@ namespace xr {
return true;
}
// Separate xor constraints in multiple gaussian matrixes
// Two xor clauses have to belong to the same matrix if they share at least one variable
// Assign xor constraints to (multiple) gaussian matrixes
// If two xor clauses share variables, the clauses have to be together in at least one matrix
bool_var_vector newSet;
uint_set to_merge;
unsigned matrix_no = 0;
@ -147,18 +147,13 @@ namespace xr {
}
m_xor.m_xorclauses.clear();
for (auto& m: matrix_shapes)
if (m.tot_size() > 0)
m.m_density = (double)m.m_sum_xor_sizes / (double)(m.tot_size());
std::sort(matrix_shapes.begin(), matrix_shapes.end(), m_sorter);
unsigned realMatrixNum = 0;
unsigned unusedMatrix = 0;
unsigned too_few_rows_matrix = 0;
unsigned unused_matrix_printed = 0;
for (unsigned a = matrix_no; a-- > 0; ) {
matrix_shape& m = matrix_shapes[a];
unsigned i = m.m_num;

5
src/sat/smt/xor_matrix_finder.h
View file

@ -36,11 +36,6 @@ namespace xr {
unsigned m_rows = 0;
unsigned m_cols = 0;
unsigned m_sum_xor_sizes = 0;
double m_density = 0;
uint64_t tot_size() const {
return (uint64_t)m_rows * (uint64_t)m_cols;
}
};
struct sorter {

2
src/util/util.h
View file

@ -135,7 +135,7 @@ static inline unsigned get_num_1bits(uint64_t v) {
v1 &= v1 - 1;
}
#endif
v = v - (v >> 1) & 0x5555555555555555;
v = v - ((v >> 1) & 0x5555555555555555);
v = (v & 0x3333333333333333) + ((v >> 2) & 0x3333333333333333);
v = (v + (v >> 4)) & 0x0F0F0F0F0F0F0F0F;
uint64_t r = (v * 0x0101010101010101) >> 56;