Struct ConfigCtx 

pub struct ConfigCtx {
    index: usize,
    params: Rc<HashMap<Parameter, SMTExpr>>,
    loc_vars: HashMap<Location, SMTExpr>,
    variable_vars: HashMap<Variable, SMTExpr>,
}

SMT context for a configuration of a threshold automaton

Fields

index: usize

index of the configuration

params: Rc<HashMap<Parameter, SMTExpr>>

reference to parameter variables

loc_vars: HashMap<Location, SMTExpr>

location variables

variable_vars: HashMap<Variable, SMTExpr>

variable variables

Implementations

impl ConfigCtx

pub fn new( solver: &mut SMTSolver, ta: &impl ThresholdAutomaton, params: Rc<HashMap<Parameter, SMTExpr>>, index: usize, ) -> ConfigCtx

Create a new set of variables for a configuration of the given threshold automaton

Trait Implementations

impl Clone for ConfigCtx

fn clone(&self) -> ConfigCtx

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl ConfigFromSMT for ConfigCtx

fn get_assigned_configuration( &self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<Configuration, SMTSolverError>

Extract the assignment found by the SMT solver

impl Debug for ConfigCtx

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

Formats the value using the given formatter.

impl Display for ConfigCtx

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

Formats the value using the given formatter.

impl SMTVariableContext<Location> for ConfigCtx

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

Get the corresponding SMTExpr for the given expression of type T

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

where Location: 'a,

Get all expressions for which the current context holds an assignment

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

impl SMTVariableContext<Parameter> for ConfigCtx

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

Get the corresponding SMTExpr for the given expression of type T

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

where Parameter: 'a,

Get all expressions for which the current context holds an assignment

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

impl SMTVariableContext<Variable> for ConfigCtx

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

Get the corresponding SMTExpr for the given expression of type T

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

where Variable: 'a,

Get all expressions for which the current context holds an assignment

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