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.

Object Safety

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>