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 <[email protected]>

Author: conp-solutions

CHANGELOG

@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [unreleased]
 
+ * structures: allow 64bit CR index for using many clauses
  * parallel: support proof generation
  * testing: use modgen generator during fuzzing runs
  * fix FPU control to compile on ARM

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);
 }

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,18 @@ 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

minisat/mtl/Alloc.h

@@ -48,20 +48,20 @@ class AccessCounter
 template <class T> 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 T> 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 T> class RegionAllocator
     AccessCounter &get_counter() { return counter; }
 };
 
-template <class T> void RegionAllocator<T>::capacity(uint32_t min_cap)
+template <class T> void RegionAllocator<T>::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 <class T> typename RegionAllocator<T>::Ref RegionAllocator<T>::alloc(in
     assert(size > 0);
     capacity(sz + size);
 
-    uint32_t prev_sz = sz;
+    uint64_t prev_sz = sz;
     sz += size;
 
     // Handle overflow:

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);
 }