Struct rate_common::parser::HashTable

pub struct HashTable(_);

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.

Methods

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.