de.uka.ilkd.key.macros

Class FinishSymbolicExecutionMacro.FilterSymbexStrategy

java.lang.Object

de.uka.ilkd.key.macros.FilterStrategy

de.uka.ilkd.key.macros.FinishSymbolicExecutionMacro.FilterSymbexStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

FinishSymbolicExecutionMacro

private static class FinishSymbolicExecutionMacro.FilterSymbexStrategy
extends FilterStrategy

The Class FilterAppManager is a special strategy assigning to any rule infinite costs if the goal has no modality

Field Summary

Fields

Modifier and Type	Field and Description
private static Name	NAME

Constructor Summary

Constructors

Constructor and Description
FilterSymbexStrategy(Strategy delegate)

Method Summary

Modifier and Type	Method and Description
boolean	isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) Re-Evaluate a RuleApp.
boolean	isStopAtFirstNonCloseableGoal() Checks if the Strategy should stop at the first non closeable Goal.
Name	name() returns the name of this element

Methods inherited from class de.uka.ilkd.key.macros.FilterStrategy

computeCost, instantiateApp

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.strategy.Strategy

updateStrategySettings

Field Detail

NAME

private static final Name NAME

Constructor Detail

FilterSymbexStrategy

public FilterSymbexStrategy(Strategy delegate)

Method Detail

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

isApprovedApp

public boolean isApprovedApp(RuleApp app,
                             PosInOccurrence pio,
                             Goal goal)

Description copied from interface: Strategy

Re-Evaluate a RuleApp. This method is called immediately before a rule is really applied

Specified by:

isApprovedApp in interface Strategy

Overrides:

isApprovedApp in class FilterStrategy

Returns:

true iff the rule should be applied, false otherwise

isStopAtFirstNonCloseableGoal

public boolean isStopAtFirstNonCloseableGoal()

Description copied from interface: Strategy

Checks if the Strategy should stop at the first non closeable Goal.

Returns:

true stop, false continue on other Goals.