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]>
conp-solutions · May 5, 2021 · e904a0b · e904a0b
1 parent 76cb34f
commit e904a0b
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 20 deletions.
diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
@@ -3483,7 +3483,7 @@ void Solver::garbageCollect()
 
     relocAll(to);
     if (verbosity >= 2)
-        printf("c |  Garbage collection:   %12d bytes => %12d bytes             |\n",
+        printf("c |  Garbage collection:   %12lu bytes => %12lu 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
@@ -192,7 +192,7 @@ class Clause
         float act;
         uint32_t abs;
         uint32_t touched;
-        CRef rel;
+        uint32_t rel;
     } data[0];
 
     friend class ClauseAllocator;
@@ -266,11 +266,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
@@ -33,19 +33,19 @@ namespace MERGESAT_NSPACE
 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_;
 
-    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 };
+    typedef uint64_t Ref;
+    enum { Ref_Undef = UINT64_MAX };
     enum { Unit_Size = sizeof(uint32_t) };
 
-    explicit RegionAllocator(uint32_t start_cap = 1024 * 1024) : memory(NULL), sz(0), cap(0), wasted_(0)
+    explicit RegionAllocator(uint64_t start_cap = 1024 * 1024) : memory(NULL), sz(0), cap(0), wasted_(0)
     {
         capacity(start_cap);
     }
@@ -55,8 +55,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; }
@@ -102,17 +102,17 @@ template <class T> class RegionAllocator
     }
 };
 
-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();
@@ -130,7 +130,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:

diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
@@ -933,7 +933,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:   %12lu bytes => %12lu bytes             |\n",
                ca.size() * ClauseAllocator::Unit_Size, to.size() * ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }