Struct ReplaceTrivialGuardsSMT 

pub struct ReplaceTrivialGuardsSMT {}

Preprocessor that checks for trivial guards using an SMT solver

This preprocessor replaces guards that are always satisfied with true. To do this, it uses an SMT solver to check whether the negation of the guard can be satisfied. If this is not possible, the guard is replaced with true.

This preprocessor can be very useful for automatically generated benchmarks where guards are often not meaningful. However, these checks can be very expensive. A more light weight preprocessor is ReplaceTrivialGuardsStatic, but it is not complete.

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

Implementations

impl ReplaceTrivialGuardsSMT

pub fn new() -> Self

Create a new instance of the preprocessor ReplaceTrivialGuardsSMT

fn is_trivially_true( expr: &BooleanExpression<Variable>, ctx: &mut StaticSMTContext, ) -> bool

Checks if a boolean expression is trivially true using an smt solver

Returns true if the expression is trivially true, false otherwise.

fn is_trivially_true_with_cache( expr: &BooleanExpression<Variable>, ctx: &mut StaticSMTContext, cached_checks: &mut HashMap<BooleanExpression<Variable>, bool>, ) -> bool

Check if a boolean expression is trivially true using an SMT solver and store the result in a cache

fn check_expr_and_replace_tautologies( expr: &mut BooleanExpression<Variable>, ctx: &mut StaticSMTContext, cached_checks: &mut HashMap<BooleanExpression<Variable>, bool>, )

Replace trivially true boolean expressions with true

This function checks if the expression is trivially true using an SMT solver. If it is, the expression is replaced with true.

This function also keeps track of known tautologies and guards to avoid repeated checks. These are stored in the known_tautologies and known_guards sets respectively.

Trait Implementations

impl Default for ReplaceTrivialGuardsSMT

fn default() -> Self

Returns the “default value” for a type.

impl<S: TargetSpec, C: ModelCheckerContext + ProvidesSMTSolverBuilder> Preprocessor<GeneralThresholdAutomaton, S, C> for ReplaceTrivialGuardsSMT

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

Process the threshold automaton and attempt to simplify it