Struct rate_common::clausedatabase::WitnessDatabase

pub struct WitnessDatabase { /* fields omitted */ }

Stores witnesses in a flat buffer

Each witness is a set of literals that are associated with a clause.

Methods

impl WitnessDatabase

pub fn new() -> WitnessDatabase

Create an empty witness database.

pub fn open_witness(&mut self) -> Clause

Make a new witness. Similar to open_clause().

pub fn push_literal(&mut self, literal: Literal)

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

This must be called after a call to open_witness() but before the call to close_witness().

Similar to push_literal().

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

Give the DIMACS representation of a witness.

Similar to clause_to_string().

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

The literals in the the witness.

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

The internal offsets of the literals in the the witness.

pub fn shrink_to_fit(&mut self)

See Vec::shrink_to_fit().

Trait Implementations

impl HeapSpace for WitnessDatabase

fn heap_space(&self) -> usize

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

impl PartialEq<WitnessDatabase> for WitnessDatabase

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

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

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

This method tests for !=.

impl Index<usize> for WitnessDatabase

type Output = Literal

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for WitnessDatabase

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

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

impl Debug for WitnessDatabase

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

Formats the value using the given formatter.