Trait StepSMT 

pub trait StepSMT: SMTVariableContext<Rule> {
    // Provided method
    fn get_rules_applied(
        &self,
        solver: &mut SMTSolver,
        res: SMTSolution,
    ) -> Result<impl Iterator<Item = (Rule, u32)>, SMTSolverError> { ... }
}

Trait implemented by symbolic steps

Provided Methods

fn get_rules_applied( &self, solver: &mut SMTSolver, res: SMTSolution, ) -> Result<impl Iterator<Item = (Rule, u32)>, SMTSolverError>

Returns the number of times a rule has been applied in the solution to this context

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<TA, C> StepSMT for LazyStepContext<TA, C>

where TA: ThresholdAutomaton, C: SMTVariableContext<Parameter> + SMTVariableContext<Location> + SMTVariableContext<Variable>,