Struct IndexedSMTContext 

struct IndexedSMTContext {
    smt_solver: SMTSolver,
    config_ctxs: Vec<ConfigCtx>,
    param_to_smt: Rc<HashMap<Parameter, SMTExpr>>,
    curr_index: usize,
}

An indexed SMT Context which creates and manages smt variables for parameters and indexed smt variables for Locations, Variables and Rules

The context keeps track of the current index for locations, variables and rules

Fields

smt_solver: SMTSolver

smt solver which used to evaluate SMT constraints

config_ctxs: Vec<ConfigCtx>

smt variable contexts for configurations

param_to_smt: Rc<HashMap<Parameter, SMTExpr>>

mapping from parameter to smt variable

curr_index: usize

current index

Implementations

impl IndexedSMTContext

fn new<T: ThresholdAutomaton>( solver_builder: SMTSolverBuilder, len: usize, ta: &T, ) -> Self

creates a new IndexedSMTContext that creates smt variables for all indexed locations and shared variables up to index len, and all parameters

fn set_curr_index(&mut self, i: usize)

updates the current index

fn get_current_config_ctx(&self) -> &ConfigCtx

Get the current configuration context

fn get_indexed_shared_smt(&self, var: &Variable, i: usize) -> SMTExpr

Get the smt expression for the indexed shared variable at index i

fn get_indexed_loc_smt(&self, loc: &Location, i: usize) -> SMTExpr

Get the smt expression for the indexed location at index i

fn get_assigned_configs(&mut self, res: SMTSolution) -> Vec<Configuration>

Extract the assigned configurations

Trait Implementations

impl GetAssignment<Parameter> for IndexedSMTContext

fn get_assignment( &mut self, res: SMTSolution, var: &T, ) -> Result<Option<u64>, SMTSolverError>

Get the assigned solution of the variable

impl SMTSolverContext for IndexedSMTContext

fn get_smt_solver(&self) -> &SMTSolver

Get the SMT solver associated with this context

fn get_smt_solver_mut(&mut self) -> &mut SMTSolver

Get a mutable reference to the SMT solver associated with this context

fn assert_and_check_expr( &mut self, expr: SExpr, ) -> Result<SMTSolution, SMTSolverError>

Check the satisfiability of the given [SMTExpr]

impl SMTVariableContext<Parameter> for IndexedSMTContext

fn get_expr_for(&self, param: &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 Context, res: SMTSolution, ) -> Result<HashMap<T, u32>, SMTSolverError>

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

Get the solution assignment