Trait SMTVariableContext 

pub trait SMTVariableContext<T> {
    // Required methods
    fn get_expr_for(&self, expr: &T) -> Result<SMTExpr, SMTSolverError>;
    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a T>
       where T: 'a;

    // Provided method
    fn get_solution<'a>(
        &'a self,
        solver: &mut SMTSolver,
        res: SMTSolution,
    ) -> Result<HashMap<T, u32>, SMTSolverError>
       where T: 'a + Eq + Hash + Clone { ... }
}

Trait of a context that provides mapping from type declaring SMT variables T to associated SMT expression

This trait is implemented by contexts that can provide the corresponding SMTExpr for a given expression stored in the context. Implementing this trait allows to encode integer and boolean expressions into SMTExprs.

Required Methods

fn get_expr_for(&self, expr: &T) -> Result<SMTExpr, SMTSolverError>

Get the corresponding SMTExpr for the given expression of type T

This function returns an error if the expression is not stored in the context, or it tried to declare a variable and the connection to the SMT solver broke.

fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a T>

where T: 'a,

Get all expressions for which the current context holds an assignment

Provided Methods

fn get_solution<'a>( &'a self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<HashMap<T, u32>, SMTSolverError>

where T: 'a + Eq + Hash + Clone,

Get the solution assignment

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl<T: Hash + Eq + DeclaresVariable> SMTVariableContext<T> for HashMap<T, SExpr>

fn get_expr_for(&self, expr: &T) -> Result<SMTExpr, SMTSolverError>

fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a T>

where T: 'a,

Implementors

impl SMTVariableContext<Location> for ConfigCtx

impl SMTVariableContext<Location> for StaticSMTContext

impl SMTVariableContext<Parameter> for ConfigCtx

impl SMTVariableContext<Parameter> for StaticSMTContext

impl SMTVariableContext<Variable> for ConfigCtx

impl SMTVariableContext<Variable> for StaticSMTContext

impl<TA, C> SMTVariableContext<Rule> for LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,