Skip to main content

SolverCache

liblisa::smt

Trait SolverCache 

pub trait SolverCache {
    // Required methods
    fn get(&mut self, hash: &AssertionHash) -> Option<CacheResult>;
    fn insert(&mut self, hash: AssertionHash, result: CacheResult);
}
Expand description

Methods that allow the type to be used as a cache for SMT solver assertions.

Required Methods§

fn get(&mut self, hash: &AssertionHash) -> Option<CacheResult>

Reads an entry from the solver cache.

fn insert(&mut self, hash: AssertionHash, result: CacheResult)

Inserts a new entry into the solver cache.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§