diff --git a/src/solver.cpp b/src/solver.cpp index 33f21bd80..baab4590b 100644 --- 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 index 92e08a338..428cc8255 100644 --- a/src/solver.h +++ b/src/solver.h @@ -312,6 +312,25 @@ class Solver : public Searcher void detach_clauses_in_xors(); vector 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();