From 7f5a455f1ba4e6b781c0e01168cfa576b0202667 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 3 May 2021 21:45:31 +0200 Subject: [PATCH] CRef: support 64 bit To be able to handle more clauses, make sure we can index the allocator area with 64bit values. This access allows to handle large formulas. Signed-off-by: Norbert Manthey --- minisat/core/Solver.cc | 2 +- minisat/core/SolverTypes.h | 9 ++++++--- minisat/mtl/Alloc.h | 32 ++++++++++++++++---------------- minisat/simp/SimpSolver.cc | 2 +- 4 files changed, 24 insertions(+), 21 deletions(-) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 42ea52e5..5fb035fa 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -3486,7 +3486,7 @@ void Solver::garbageCollect() relocAll(to); if (verbosity >= 2) - printf("c | Garbage collection: %12d bytes => %12d bytes |\n", + printf("c | Garbage collection: %12" PRIu64 " bytes => %12" PRIu64 " bytes |\n", ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); } diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 71650823..d7b361c1 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -247,7 +247,7 @@ class Clause float act; uint32_t abs; uint32_t touched; - CRef rel; + uint32_t rel; } data[0]; #if defined __clang__ #pragma clang diagnostic pop @@ -345,11 +345,14 @@ class Clause } bool reloced() const { return header.reloced; } - CRef relocation() const { return data[0].rel; } + CRef relocation() const { assert(size() > 1); return ((uint64_t)data[0].rel << 32) + data[1].rel; } void relocate(CRef c) { + assert(size() > 1 && "do not relocate non-unit clauses"); + assert(header.reloced == 0 && "do not relocate multiple times"); header.reloced = 1; - data[0].rel = c; + data[0].rel = (uint32_t)(c >> 32); + data[1].rel = (uint32_t)(c & (UINT32_MAX)); } /// remove the literal at the given position diff --git a/minisat/mtl/Alloc.h b/minisat/mtl/Alloc.h index 0c24afb2..666e6210 100644 --- a/minisat/mtl/Alloc.h +++ b/minisat/mtl/Alloc.h @@ -48,20 +48,20 @@ class AccessCounter template class RegionAllocator { T *memory; - uint32_t sz; - uint32_t cap; - uint32_t wasted_; + uint64_t sz; + uint64_t cap; + uint64_t wasted_; AccessCounter &counter; - void capacity(uint32_t min_cap); + void capacity(uint64_t min_cap); public: // TODO: make this a class for better type-checking? - typedef uint32_t Ref; - enum { Ref_Undef = UINT32_MAX }; - enum { Unit_Size = sizeof(uint32_t) }; + typedef uint64_t Ref; + enum { Ref_Undef = UINT64_MAX }; + enum { Unit_Size = sizeof(Ref) }; - explicit RegionAllocator(AccessCounter &_counter, uint32_t start_cap = 1024 * 1024) + explicit RegionAllocator(AccessCounter &_counter, uint64_t start_cap = 1024 * 1024) : memory(NULL), sz(0), cap(0), wasted_(0), counter(_counter) { capacity(start_cap); @@ -72,8 +72,8 @@ template class RegionAllocator } - uint32_t size() const { return sz; } - uint32_t wasted() const { return wasted_; } + uint64_t size() const { return sz; } + uint64_t wasted() const { return wasted_; } Ref alloc(int size); void free(int size) { wasted_ += size; } @@ -125,17 +125,17 @@ template class RegionAllocator AccessCounter &get_counter() { return counter; } }; -template void RegionAllocator::capacity(uint32_t min_cap) +template void RegionAllocator::capacity(uint64_t min_cap) { if (cap >= min_cap) return; - uint32_t prev_cap = cap; + uint64_t prev_cap = cap; while (cap < min_cap) { // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the // result even by clearing the least significant bit. The resulting sequence of capacities - // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when - // using 'uint32_t' as indices so that as much as possible of this space can be used. - uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1; + // is carefully chosen to hit a maximum capacity that is close to the '2^64-1' limit when + // using 'uint64_t' as indices so that as much as possible of this space can be used. + uint64_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1; cap += delta; if (cap <= prev_cap) throw OutOfMemoryException(); @@ -153,7 +153,7 @@ template typename RegionAllocator::Ref RegionAllocator::alloc(in assert(size > 0); capacity(sz + size); - uint32_t prev_sz = sz; + uint64_t prev_sz = sz; sz += size; // Handle overflow: diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc index aaa684b5..600bb57e 100644 --- a/minisat/simp/SimpSolver.cc +++ b/minisat/simp/SimpSolver.cc @@ -916,7 +916,7 @@ void SimpSolver::garbageCollect() relocAll(to); Solver::relocAll(to); if (verbosity >= 2) - printf("c | Garbage collection: %12d bytes => %12d bytes |\n", + printf("c | Garbage collection: %12" PRIu64 " bytes => %12" PRIu64 " bytes |\n", ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); }