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.

Implementors§