Struct ClauseDatabase

pub struct ClauseDatabase { /* private fields */ }

Stores clauses in a flat buffer

Implementations

impl ClauseDatabase

pub fn number_of_clauses(&self) -> ClauseIdentifierType

Returns the total number that are stored.

pub fn last_clause(&self) -> Clause

Returns the clause that was added last.

pub fn pop_clause(&mut self)

Delete the last clause.

pub fn clause_to_string(&self, clause: Clause) -> String

Give the DIMACS representation of a clause.

Only used for debugging, prefer clause::write_clause().

pub fn clause(&self, clause: Clause) -> &[Literal]

The literals in the the clause.

pub fn clause_range(&self, clause: Clause) -> Range<usize>

The internal offsets of the literals in the the clause.

pub fn watches(&self, head: usize) -> [Literal; 2]

The first two literals in the clause.

pub fn clause2offset(&self, clause: Clause) -> usize

Convert a clause identifier to the offset of the clause.

pub fn offset2clause(&self, head: usize) -> Clause

Convert a clause offset to the identifier of the clause.

pub fn swap(&mut self, a: usize, b: usize)

Swap the literal at the given offsets in the clause database.

pub fn fields(&self, clause: Clause) -> &u32

Access the metadata for this clause.

pub fn fields_mut(&mut self, clause: Clause) -> &mut u32

Access the mutable metadata for this clause.

pub fn fields_from_offset(&self, offset: usize) -> &u32

Access the metadata for the clause with this offset. This is possibly more efficient than fields().

pub fn fields_mut_from_offset(&mut self, offset: usize) -> &mut u32

Access the mutable metadata for the clause with this offset. This is possibly more efficient than fields().

pub fn shrink_to_fit(&mut self)

See Vec::shrink_to_fit().

Trait Implementations

impl ClauseStorage for ClauseDatabase

fn open_clause(&mut self) -> Clause

Initialze a new clause.

fn push_literal(&mut self, literal: Literal, verbose: bool)

Add a literal to the current clause.

impl Debug for ClauseDatabase

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ClauseDatabase

fn default() -> ClauseDatabase

Create an empty clause database.

impl HeapSpace for ClauseDatabase

fn heap_space(&self) -> usize

The number of bytes allocated on the heap that this owns.

impl Index<usize> for ClauseDatabase

type Output = Literal

The returned type after indexing.

fn index(&self, offset: usize) -> &Literal

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for ClauseDatabase

fn index_mut(&mut self, offset: usize) -> &mut Literal

Performs the mutable indexing (container[index]) operation.

impl PartialEq for ClauseDatabase

fn eq(&self, other: &ClauseDatabase) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ClauseDatabase