Struct StaticSMTContext 

pub struct StaticSMTContext {
    solver: SMTSolver,
    params: HashMap<Parameter, SMTExpr>,
    locs: HashMap<Location, SMTExpr>,
    vars: HashMap<Variable, Vec<SMTExpr>>,
}

A simple static context for encoding expressions related to threshold automata into SMT constraints and checking satisfiability

This context is used to encode expressions into SMT constraints and check their satisfiability. It should be only used to encode simple expressions, and is not designed to handle expressions over multiple configurations.

Fields

solver: SMTSolver

params: HashMap<Parameter, SMTExpr>

locs: HashMap<Location, SMTExpr>

vars: HashMap<Variable, Vec<SMTExpr>>

Implementations

impl StaticSMTContext

pub fn new( solver_builder: SMTSolverBuilder, params: impl IntoIterator<Item = Parameter>, locs: impl IntoIterator<Item = Location>, vars: impl IntoIterator<Item = Variable>, ) -> Result<Self, SMTSolverError>

Create a new static SMT context

This function creates a new static SMT context with the given solver builder and declares variables for the given parameters, locations, and variables.

pub fn get_true(&self) -> SMTExpr

Get the SMT expression for the true value

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

where T: EncodeToSMT<T, Self>,

Encode the given expression into an SMT expression and return the expression

Trait Implementations

impl GetAssignment<Location> for StaticSMTContext

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

Get the assigned solution of the variable

impl GetAssignment<Parameter> for StaticSMTContext

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

Get the assigned solution of the variable

impl GetAssignment<Variable> for StaticSMTContext

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

Get the assigned solution of the variable

impl SMTSolverContext for StaticSMTContext

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

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

fn get_smt_solver(&self) -> &SMTSolver

Get the SMT solver associated with this context

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

Check the satisfiability of the given SMTExpr

impl SMTVariableContext<Location> for StaticSMTContext

fn get_expr_for(&self, loc: &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 StaticSMTContext

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 SMTSolver, res: SMTSolution, ) -> Result<HashMap<T, u32>, SMTSolverError>

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

Get the solution assignment

impl SMTVariableContext<Variable> for StaticSMTContext

fn get_expr_for(&self, var: &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