Struct _ReplacingContext 

struct _ReplacingContext {
    var_to_smt: HashMap<Variable, SMTExpr>,
    param: Rc<HashMap<Parameter, SMTExpr>>,
}

This context allows to use a custom SMT expression instead of a variable when encoding expressions into SMT

Fields

var_to_smt: HashMap<Variable, SMTExpr>

param: Rc<HashMap<Parameter, SMTExpr>>

Implementations

impl _ReplacingContext

fn _new( var_to_smt: HashMap<Variable, SMTExpr>, param: Rc<HashMap<Parameter, SMTExpr>>, ) -> Self

Create a new ReplacingContext

Trait Implementations

impl SMTVariableContext<Parameter> for _ReplacingContext

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

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

Get the solution assignment

impl SMTVariableContext<Variable> for _ReplacingContext

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

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

Get the solution assignment