Trait SolverProvider

pub trait SolverProvider: Send + Sync {
    type Solver<'a>: SmtSolver<'a>;

    // Required method
    fn with_solver<T>(&self, f: impl FnOnce(Self::Solver<'_>) -> T) -> T;
}

Provides SmtSolvers without having to know all of the configuration details of the individual solvers.

Required Associated Types

type Solver<'a>: SmtSolver<'a>

The solver that this type provides.

Required Methods

fn with_solver<T>(&self, f: impl FnOnce(Self::Solver<'_>) -> T) -> T

Runs the function f with a provided solver.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl SolverProvider for ThreadLocalZ3

type Solver<'a> = Z3Solver<'a>

impl<C: SolverCache + Send + Sync + Copy, I: SolverProvider> SolverProvider for CachedSolverProvider<C, I>

where for<'a> I::Solver<'a>: 'a,

type Solver<'a> = CachedSolver<'a, <I as SolverProvider>::Solver<'a>, C>