Struct varisat::clause::alloc::ClauseAlloc

pub struct ClauseAlloc {
    buffer: Vec<LitIdx>,
}

Bump allocator for clause storage.

Clauses are allocated from a single continuous buffer. Clauses cannot be freed individually. To reclaim space from deleted clauses, a new ClauseAlloc is created and the remaining clauses are copied over.

When the ClauseAlloc's buffer is full, it is reallocated using the growing strategy of Vec. External references (ClauseRef) store an offset into the ClauseAlloc's memory and remaind valid when the buffer is grown. Clauses are aligned and the offset represents a multiple of the alignment size. This allows using 32-bit offsets while still supporting up to 16GB of clauses.

Fields

buffer: Vec<LitIdx>

Methods

impl ClauseAlloc

pub fn new() -> ClauseAlloc

Create an emtpy clause allocator.

pub fn with_capacity(capacity: usize) -> ClauseAlloc

Create a clause allocator with preallocated capacity.

pub fn add_clause(&mut self, header: ClauseHeader, lits: &[Lit]) -> ClauseRef

Allocate space for and add a new clause.

Clauses have a minimal size of 3, as binary and unit clauses are handled separately. This is enforced on the ClauseAlloc level to safely avoid extra bound checks when accessing the initial literals of a clause.

The size of the header will be set to the size of the given slice. The returned ClauseRef can be used to access the new clause.

pub fn header(&self, cref: ClauseRef) -> &ClauseHeader

Access the header of a clause.

pub fn header_mut(&mut self, cref: ClauseRef) -> &mut ClauseHeader

Mutate the header of a clause.

unsafe fn header_unchecked(&self, cref: ClauseRef) -> &ClauseHeader

pub unsafe fn header_unchecked_mut(
    &mut self,
    cref: ClauseRef
) -> &mut ClauseHeader

Mutate the header of a clause without bound checks.

pub fn clause(&self, cref: ClauseRef) -> &Clause

Access a clause.

pub fn clause_mut(&mut self, cref: ClauseRef) -> &mut Clause

Mutate a clause.

pub unsafe fn lits_ptr_mut_unchecked(&mut self, cref: ClauseRef) -> *mut Lit

Mutate the literals of a clause without bound checks.

pub fn check_bounds(&self, cref: ClauseRef, len: usize)

Perform a manual bound check on a ClauseRef assuming a given clause length.

unsafe fn clause_with_len_unchecked(
    &self,
    cref: ClauseRef,
    len: usize
) -> &Clause

unsafe fn clause_with_len_unchecked_mut(
    &mut self,
    cref: ClauseRef,
    len: usize
) -> &mut Clause

pub fn buffer_size(&self) -> usize

Current buffer size in multiples of LitIdx.

Trait Implementations

impl Default for ClauseAlloc

fn default() -> ClauseAlloc

Returns the "default value" for a type.