Skip to main content

​
Overview

The RegionAllocator<T> template class implements a simple region-based memory allocator. It allocates memory in a contiguous region and uses 32-bit references instead of pointers for memory efficiency. This allocator is primarily used in MiniSat for clause storage.
This allocator does not support individual deallocations. It tracks “wasted” space from freed objects but doesn’t reuse it.

​
Template parameters

​
T
typename
required
The unit type for the region. Typically uint32_t for byte-level allocation.

​
Type definitions

​
Ref
uint32_t
32-bit reference type used instead of pointers. More compact than 64-bit pointers.
​
Ref_Undef
Special value representing an undefined/null reference
​
Unit_Size
Size in bytes of each allocation unit

​
Constructor and destructor

explicit RegionAllocator(uint32_t start_cap = 1024*1024)
~RegionAllocator()
​
start_cap
uint32_t
default:"1024*1024"
Initial capacity in units (default is 1MB worth of units)
The allocator automatically grows as needed. Memory is freed when the allocator is destroyed.

​
Size tracking

​
size

uint32_t size() const
Returns the number of units currently allocated (including wasted space).

​
wasted

uint32_t wasted() const
Returns the number of units that have been freed and cannot be reused.
Monitoring wasted space helps determine when to trigger garbage collection in the solver.

​
Allocation operations

​
alloc

Ref alloc(int size)
Allocates a block of the specified size and returns a reference to it.
​
size
int
required
Number of units to allocate (must be > 0)
Returns: A Ref (32-bit reference) to the allocated block
Time complexity: O(1) amortized. May trigger capacity expansion.

​
free

void free(int size)
Marks units as wasted. Does not actually reclaim memory.
​
size
int
required
Number of units to mark as wasted
This does not reuse the memory. It only updates the wasted counter.

​
Reference operations

The allocator provides operations to convert between references and pointers:

​
operator[] (dereference)

T& operator[](Ref r)
const T& operator[](Ref r) const
Dereferences a reference to access the stored value.
​
r
Ref
required
Reference to dereference (must be < size())

​
lea (Load Effective Address)

T* lea(Ref r)
const T* lea(Ref r) const
Converts a reference to a pointer.
​
r
Ref
required
Reference to convert
Returns: Pointer to the data at the given reference

​
ael (Address to reference)

Ref ael(const T* t)
Converts a pointer back to a reference (inverse of lea).
​
t
const T*
required
Pointer within the allocated region
Returns: The Ref corresponding to the pointer
The pointer must point within the currently allocated region.

​
Capacity management

​
capacity (internal)

void capacity(uint32_t min_cap)
Ensures the allocator has at least the specified capacity. Called automatically by alloc().
​
min_cap
uint32_t
required
Minimum required capacity
The capacity grows by a factor of 13/8, carefully designed to reach close to the 2³²-1 limit when using uint32_t indices.
Growth sequence ensures maximum use of the 32-bit address space while avoiding overflow.

​
Transfer operations

​
moveTo

void moveTo(RegionAllocator& to)
Moves all allocated memory to another allocator, leaving this allocator empty.
​
to
RegionAllocator&
required
Destination allocator (its current contents are freed)

​
Usage example

#include "minisat/mtl/Alloc.h"

using namespace Minisat;

// Allocate storage for uint32_t units
RegionAllocator<uint32_t> ra(1024);

// Allocate space for 3 integers
RegionAllocator<uint32_t>::Ref ref = ra.alloc(3);

// Access allocated memory
ra[ref + 0] = 10;
ra[ref + 1] = 20;
ra[ref + 2] = 30;

// Convert to pointer
uint32_t* ptr = ra.lea(ref);
printf("%u %u %u\n", ptr[0], ptr[1], ptr[2]);

// Mark as wasted (doesn't reclaim)
ra.free(3);

printf("Size: %u, Wasted: %u\n", ra.size(), ra.wasted());

​
Typical use in MiniSat

MiniSat uses RegionAllocator<uint32_t> for clause storage: 
class Clause {
    // ... clause data
public:
    static int size(int num_lits) { 
        return sizeof(Clause) / sizeof(uint32_t) + num_lits; 
    }
};

RegionAllocator<uint32_t> ca;

// Allocate a clause
int size = Clause::size(3);
CRef cr = ca.alloc(size);

// Initialize clause
new (ca.lea(cr)) Clause(literals, 3, learnt);

// Access clause
Clause& c = ca[cr];

​
Design rationale

​
Why 32-bit references?

  • Memory efficiency: Clauses in SAT solvers are small objects referenced frequently. Using 32-bit references instead of 64-bit pointers saves significant memory.
  • Cache efficiency: Smaller references improve cache locality.
  • Sufficient range: 2³² units provides 16GB of addressable space when T = uint32_t, which is adequate for most SAT problems.

​
Why region-based allocation?

  • Fast allocation: O(1) bump-pointer allocation
  • No fragmentation: All memory is contiguous
  • Bulk deallocation: Can free entire region at once during garbage collection
  • Simplified management: No need to track individual deallocations

​
Limitations

  • No individual deallocation: Memory marked as “wasted” cannot be reused
  • Requires garbage collection: Periodic compaction needed to reclaim wasted space
  • Fixed unit size: Cannot efficiently mix allocations of very different sizes

​
Performance characteristics

  • Allocation: O(1) amortized (may trigger realloc)
  • Deallocation: O(1) (just increments wasted counter)
  • Dereference: O(1) (simple array access)
  • Space overhead: One pointer + two 32-bit integers
  • Growth factor: 13/8 (approximately 1.625)

​
Memory safety

References become invalid after:
  • Calling moveTo()
  • Allocating enough memory to trigger reallocation (internal realloc)
Store references, not pointers, to avoid dangling pointer issues.

Build docs developers (and LLMs) love

Get started for freeTalk to us