Struct HashTable

pub struct HashTable(/* private fields */);

A fixed-size hash table that maps clauses (sets of literals) to clause identifiers.

This should work exactly like the one used in drat-trim. Given that we expect the number of clauses in the hash table not to exceed a couple million this should be faster and leaner than DynamicHashTable.

Implementations

impl HashTable

pub fn new() -> HashTable

Allocate the hash table.

pub fn add_clause(&mut self, clause_db: &ClauseDatabase, clause: Clause)

Add a new clause to the hashtable.

pub fn find_equal_clause( &mut self, clause_db: &ClauseDatabase, needle: Clause, delete: bool, ) -> Option<Clause>

Find a clause that is equivalent to given clause.

If delete is true, delete the found clause.

pub fn clause_is_active( &self, clause_db: &ClauseDatabase, needle: Clause, ) -> bool

Return true if this exact clause is active.

pub fn delete_clause( &mut self, clause_db: &ClauseDatabase, needle: Clause, ) -> bool

Delete this exact clause, return true if that succeeded.

Trait Implementations

impl HeapSpace for HashTable

fn heap_space(&self) -> usize

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

impl<'a> IntoIterator for &'a HashTable

type Item = &'a Clause

The type of the elements being iterated over.

type IntoIter = HashTableIterator<'a>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.