Trait ModelCheckerContext 

pub trait ModelCheckerContext:
    Sized
    + Clone
    + Debug {
    type CreationError: Error;
    type ContextOptions;

    // Required method
    fn try_new(
        opt: Option<Self::ContextOptions>,
    ) -> Result<Self, Self::CreationError>;
}

Trait of contexts for model checker

A context to a model checker supplies backend functionality such as, for example an SMT solver to the model checker

Required Associated Types

type CreationError: Error

Possible error that can occur during creation of the context

type ContextOptions

Options for the model checker context

Required Methods

fn try_new( opt: Option<Self::ContextOptions>, ) -> Result<Self, Self::CreationError>

Create a new model checking context

Tries to create a new context with the given options

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.

Implementations on Foreign Types

impl ModelCheckerContext for SMTSolverBuilder

Implement ModelCheckerContext for the SMT solver builder

type CreationError = SMTSolverBuilderError

type ContextOptions = SMTSolverBuilderCfg

fn try_new( opt: Option<Self::ContextOptions>, ) -> Result<Self, Self::CreationError>

Implementors

impl ModelCheckerContext for SMTBddContext

type CreationError = SMTSolverBuilderError

type ContextOptions = (Option<SMTSolverBuilderCfg>, Option<BDDManagerConfig>)