Struct ReplaceTrivialGuardsStatic 

pub struct ReplaceTrivialGuardsStatic {}

A lot of automatically generated benchmarks have guards of the form (var1 >= 1 || var1 == 0) or var >= 0 which are satisfied. This preprocessor replaces these guards with true.

This preprocessor only checks for a few trivial patterns, if you want a more general preprocessor use ReplaceTrivialGuardsSMT.

Note: If you assume variables can have values smaller than 0 this preprocessor should not be used!

Implementations

impl ReplaceTrivialGuardsStatic

fn is_trivially_true<T: Atomic>(expr: &BooleanExpression<T>) -> bool

? Can we generalize this to more expressions ?

fn replace_trivial_boolean_expr<T: Atomic>(expr: &mut BooleanExpression<T>)

Replace trivial boolean expressions with true

Note: If you assume variables can have values smaller than 0 this preprocessor should not be used!

pub fn new() -> Self

Create a new instance of the ReplaceTrivialGuardsStatic preprocessor

Trait Implementations

impl Default for ReplaceTrivialGuardsStatic

fn default() -> Self

Returns the “default value” for a type.

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for ReplaceTrivialGuardsStatic

fn process(&self, ta: &mut GeneralThresholdAutomaton, _spec: &S, _ctx: &C)

A lot of automatically generated benchmarks have guards of the form (var1 >= 1 || var1 == 0) or var >= 0 which are satisfied. This preprocessor replaces these guards with true.

This preprocessor only checks for a few trivial patterns, if you want a more general preprocessor use ReplaceTrivialGuardsSMT.

Note: If you assume variables can have values smaller than 0 this preprocessor should not be used!