Struct SMTBddContext 

pub struct SMTBddContext {
    pub(crate) smt_solver_builder: SMTSolverBuilder,
    pub(crate) bdd_manager: BDDManager,
}

Simple context for model checkers containing SMT solver and BDD manager

Fields

smt_solver_builder: SMTSolverBuilder

Builder to construct new SMT solvers.

bdd_manager: BDDManager

The BDD manager to use for the model checking.

Implementations

impl SMTBddContext

pub fn smt_solver_builder(&self) -> &SMTSolverBuilder

returns the smt_solver_builder

pub fn bdd_manager(&self) -> &BDDManager

returns the bdd_manager

Trait Implementations

impl Clone for SMTBddContext

fn clone(&self) -> SMTBddContext

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SMTBddContext

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl ModelCheckerContext for SMTBddContext

type CreationError = SMTSolverBuilderError

Possible error that can occur during creation of the context

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

Options for the model checker context

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

Create a new model checking context

impl ProvidesSMTSolverBuilder for SMTBddContext

fn get_solver_builder(&self) -> SMTSolverBuilder

Get the configured [SMTSolverBuilder]