pub trait DeclaresVariable {
// Required methods
fn get_name(&self, index: u32) -> String;
fn get_undeclared_error(&self) -> SMTSolverError;
// Provided method
fn declare_variable(
&self,
solver: &mut SMTSolver,
index: u32,
) -> Result<SMTExpr, SMTSolverError> { ... }
}Expand description
Trait for types that have associated SMT variables
This trait is implemented by types that are usually encoded as variables when constructing formulas over threshold automata. A type implementing this trait needs to provide a naming scheme for the smt variables associated with the type and a method to construct an error if the variable is not declared.
Required Methods§
Sourcefn get_name(&self, index: u32) -> String
fn get_name(&self, index: u32) -> String
Get the name of the associated variable for the given index
This function should return the name of the variable associated with the type for the given index. The naming scheme must result in a unique name across all variables used in the SMT solver.
The index field is used for variables that are usually indexed. For
example, along a path, the location variable (representing the number of
processes in this location) is usually indexed by the configuration.
Sourcefn get_undeclared_error(&self) -> SMTSolverError
fn get_undeclared_error(&self) -> SMTSolverError
Returns an error indicating that self was not declared in the current
SMT context.
Provided Methods§
Sourcefn declare_variable(
&self,
solver: &mut SMTSolver,
index: u32,
) -> Result<SMTExpr, SMTSolverError>
fn declare_variable( &self, solver: &mut SMTSolver, index: u32, ) -> Result<SMTExpr, SMTSolverError>
Declare the variable in the SMT solver
This function declares the variable in the SMT solver and returns the SMT expression. Returns an error if the connection to the SMT solver broke.