Enum ExistingPreprocessors 

pub enum ExistingPreprocessors {
    DropSelfLoops,
    DropUnreachableLocations,
    ReplaceTrivialGuardsStatic,
    ReplaceTrivialGuardsSMT,
    RemoveUnusedVariables,
    DropUnsatisfiableRules,
    CollapseLocations,
    CheckInitCondSatSMT,
}

Enum representing all available preprocessors

This enum is used to configure what preprocessors can be used in TACO

Variants

DropSelfLoops

Removes self loops from the threshold automaton if the transition rule has no effect on the shared variables.

DropUnreachableLocations

Removes unreachable locations from the threshold automaton by performing a graph search

ReplaceTrivialGuardsStatic

Replaces some frequently generated guards that are always enabled with true

ReplaceTrivialGuardsSMT

Replaces guards which are always satisfied, uses SMT to determine which guards are always satisfied.

RemoveUnusedVariables

Remove variables that do not appear in any guard

DropUnsatisfiableRules

Remove Rules for which a guard can never be satisfied

CollapseLocations

Collapse locations which have the same incoming rules

CheckInitCondSatSMT

Checks whether the initial location of the threshold automaton can be satisfied at all

Trait Implementations

impl Clone for ExistingPreprocessors

fn clone(&self) -> ExistingPreprocessors

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ExistingPreprocessors

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ExistingPreprocessors

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for ExistingPreprocessors

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<S, C> From<ExistingPreprocessors> for Box<dyn Preprocessor<GeneralThresholdAutomaton, S, C>>

where S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder,

fn from(val: ExistingPreprocessors) -> Self

Converts to this type from the input type.

impl PartialEq for ExistingPreprocessors

fn eq(&self, other: &ExistingPreprocessors) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ExistingPreprocessors