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", so this trait is not object safe.

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>,