Fixinhg HUGE bug with hashing

Ooops, out of mem bounds!
msoos · Oct 25, 2024 · 2cde4da · 2cde4da
1 parent 9ae58f3
commit 2cde4da
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 22 deletions.
diff --git a/src/solver.cpp b/src/solver.cpp
@@ -3615,27 +3615,6 @@ void Solver::copy_to_simp(SATSolver* s2)
     end_getting_constraints();
 }
 
-void hash_uint32_t(const uint32_t v, uint32_t& hash) {
-    uint8_t* s = (uint8_t*)(&v);
-    for(uint32_t i = 0; i < 4; i++, s++) { hash += *s; }
-    for(uint32_t i = 0; i < 4; i++, s++) { hash ^= *s; }
-}
-
-uint32_t hash_xcl(const Xor& x)
-{
-    uint32_t hash = 0;
-    for(const auto& v: x) hash_uint32_t(v, hash);
-    return hash;
-}
-
-
-uint32_t hash_xcl(const Clause& cl)
-{
-    uint32_t hash = 0;
-    for(const auto& l: cl) hash_uint32_t(l.var(), hash);
-    return hash;
-}
-
 bool Solver::check_clause_represented_by_xor(const Clause& cl) {
     for(const auto& l: cl) if (!seen[l.var()]) return false;
 
@@ -3689,7 +3668,7 @@ void Solver::detach_clauses_in_xors() {
         assert(!cl->freed());
         assert(!cl->get_removed());
         if (cl->size() <= maxsize_xor &&
-                xor_hashes.count(hash_xcl(*cl)) &&
+                xor_hashes.count(hash_xcl(cl)) &&
                 check_clause_represented_by_xor(*cl)) {
             detachClause(*cl);
             cl->stats.marked_clause = true;

diff --git a/src/solver.h b/src/solver.h
@@ -312,6 +312,25 @@ class Solver : public Searcher
         void detach_clauses_in_xors();
         vector<Lit> tmp_repr;
         bool check_clause_represented_by_xor(const Clause& cl);
+        void hash_uint32_t(const uint32_t v, uint32_t& hash) const {
+            uint8_t* s = (uint8_t*)(&v);
+            for(uint32_t i = 0; i < 4; i++, s++) { hash += *s; }
+            s = (uint8_t*)(&v);
+            for(uint32_t i = 0; i < 4; i++, s++) { hash ^= *s; }
+        }
+
+        uint32_t hash_xcl(const Xor& x) const {
+            uint32_t hash = 0;
+            for(const auto& v: x) hash_uint32_t(v, hash);
+            return hash;
+        }
+
+        uint32_t hash_xcl(const Clause* cl) const {
+            uint32_t hash = 0;
+            for(const auto& l: *cl) hash_uint32_t(l.var(), hash);
+            return hash;
+        }
+
 
         //assumptions
         void set_assumptions();