Struct rate_common::clausedatabase::ClauseDatabase

pub struct ClauseDatabase { /* fields omitted */ }

Stores clauses in a flat buffer

Methods

impl ClauseDatabase

pub fn new() -> ClauseDatabase

Create an empty clause database.

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 push_literal(&mut self, literal: Literal)

Add a literal to the current clause. Finish the clause if the literal is 0.

This must be called after a call to open_clause() but before the call to close_clause().

pub fn open_clause(&mut self) -> Clause

Make a new clause.

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.

FIXME: possibly inefficient, use clause::write_clause() instead.

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 HeapSpace for ClauseDatabase

fn heap_space(&self) -> usize

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

impl PartialEq<ClauseDatabase> for ClauseDatabase

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

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 Debug for ClauseDatabase

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

Formats the value using the given formatter.