From 3586c288ecdc737f25ecddee3abc01507e8149ed Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
Date: Wed, 30 Nov 2022 12:53:13 +0100
Subject: [PATCH] Fix popcnt64

---
 src/sat/smt/xor_matrix_finder.cpp | 11 +++--------
 src/sat/smt/xor_matrix_finder.h   |  5 -----
 src/util/util.h                   |  2 +-
 3 files changed, 4 insertions(+), 14 deletions(-)

diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp
index a770e99ea..9283a43be 100644
--- a/src/sat/smt/xor_matrix_finder.cpp
+++ b/src/sat/smt/xor_matrix_finder.cpp
@@ -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;
diff --git a/src/sat/smt/xor_matrix_finder.h b/src/sat/smt/xor_matrix_finder.h
index 99165b563..0afdcba5d 100644
--- a/src/sat/smt/xor_matrix_finder.h
+++ b/src/sat/smt/xor_matrix_finder.h
@@ -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 {
diff --git a/src/util/util.h b/src/util/util.h
index f15566258..ebd5bd3f4 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -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;