Trait SmtBackend 

pub trait SmtBackend: SmtBackendReader {
    // Required methods
    fn compute_mutations(
        &self,
        updates: Vec<(Word, Word)>,
    ) -> Result<MutationSet<SMT_DEPTH, Word, Word>, Self::Error>;
    fn apply_mutations(
        &mut self,
        set: MutationSet<SMT_DEPTH, Word, Word>,
    ) -> Result<(), Self::Error>;
    fn apply_mutations_with_reversion(
        &mut self,
        set: MutationSet<SMT_DEPTH, Word, Word>,
    ) -> Result<MutationSet<SMT_DEPTH, Word, Word>, Self::Error>;
    fn insert(&mut self, key: Word, value: Word) -> Result<Word, Self::Error>;
}

Extension trait for SmtBackendReader that provides write methods.

Required Methods

fn compute_mutations( &self, updates: Vec<(Word, Word)>, ) -> Result<MutationSet<SMT_DEPTH, Word, Word>, Self::Error>

Computes the mutation set required to apply the given updates to the SMT.

fn apply_mutations( &mut self, set: MutationSet<SMT_DEPTH, Word, Word>, ) -> Result<(), Self::Error>

Applies the given mutation set to the SMT.

fn apply_mutations_with_reversion( &mut self, set: MutationSet<SMT_DEPTH, Word, Word>, ) -> Result<MutationSet<SMT_DEPTH, Word, Word>, Self::Error>

Applies the given mutation set to the SMT and returns the reverse mutation set.

The reverse mutation set can be used to revert the changes made by this operation.

fn insert(&mut self, key: Word, value: Word) -> Result<Word, Self::Error>

Inserts a key-value pair into the SMT, returning the previous value at that key.

Dyn Compatibility

This trait is not dyn compatible.

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

Implementors

impl SmtBackend for Smt

impl<Backend> SmtBackend for LargeSmt<Backend>

where Backend: SmtStorage,

Available on crate feature std only.