Struct WitnessDatabase

pub struct WitnessDatabase { /* private fields */ }

Stores witnesses in a flat buffer

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

Implementations

impl WitnessDatabase

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 ClauseStorage for WitnessDatabase

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 WitnessDatabase

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

Formats the value using the given formatter.

impl Default for WitnessDatabase

fn default() -> WitnessDatabase

Create an empty witness database.

impl HeapSpace for WitnessDatabase

fn heap_space(&self) -> usize

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

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 PartialEq for WitnessDatabase

fn eq(&self, other: &WitnessDatabase) -> 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 WitnessDatabase