de.uka.ilkd.key.symbolic_execution.profile

Class SimplifyTermProfile

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractProfile

de.uka.ilkd.key.proof.init.JavaProfile

de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile

All Implemented Interfaces:

Profile

public class SimplifyTermProfile
extends JavaProfile

An extended JavaProfile used in side proofs to simplify a Term.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
static SimplifyTermProfile	defaultInstance The default instance of this class.
static java.lang.String	NAME The Name of this Profile.
private static StrategyFactory	SIDE_PROOF_FACTORY The used StrategyFactory of the SymbolicExecutionStrategy.

Fields inherited from class de.uka.ilkd.key.proof.init.JavaProfile

DEFAULT, defaultInstancePermissions, NAME_WITH_PERMISSIONS

Constructor Summary

Constructors

Constructor and Description
SimplifyTermProfile() Constructor.

Method Summary

Modifier and Type	Method and Description
protected ImmutableList<TermLabelManager.TermLabelConfiguration>	computeTermLabelConfiguration() Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.
static SimplifyTermProfile	getDefaultInstance() Returns the default instance of this class.
StrategyFactory	getDefaultStrategyFactory() the default strategy factory to be used
protected ImmutableSet<StrategyFactory>	getStrategyFactories()
java.lang.String	name() the name of the profile

Methods inherited from class de.uka.ilkd.key.proof.init.JavaProfile

getDefaultInstance, getJustification, getOneStepSimpilifier, initBuiltInRules, isSpecificationInvolvedInRuleApp, withPermissions

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractProfile

computeSupportedGoalChooserBuilder, getDefaultGoalChooserBuilder, getDefaultProfile, getInternalClassDirectory, getInternalClasslistFilename, getSelectedGoalChooserBuilder, getStandardRules, getStrategyFactory, getTermLabelManager, initTermLabelManager, lookupGC, setDefaultProfile, setSelectedGoalChooserBuilder, supportedGoalChoosers, supportedStrategies, supportsStrategyFactory

Methods inherited from class java.lang.Object

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

Field Detail

NAME

public static final java.lang.String NAME

The Name of this Profile.

See Also:

Constant Field Values

SIDE_PROOF_FACTORY

private static final StrategyFactory SIDE_PROOF_FACTORY

The used StrategyFactory of the SymbolicExecutionStrategy.

defaultInstance

public static SimplifyTermProfile defaultInstance

The default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

Constructor Detail

SimplifyTermProfile

public SimplifyTermProfile()

Constructor.

Method Detail

computeTermLabelConfiguration

protected ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()

Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.

Overrides:

computeTermLabelConfiguration in class JavaProfile

Returns:

The TermLabelManager.TermLabelConfiguration to use in this Profile.

getStrategyFactories

protected ImmutableSet<StrategyFactory> getStrategyFactories()

Overrides:

getStrategyFactories in class JavaProfile

getDefaultStrategyFactory

public StrategyFactory getDefaultStrategyFactory()

the default strategy factory to be used

Specified by:

getDefaultStrategyFactory in interface Profile

Overrides:

getDefaultStrategyFactory in class JavaProfile

Returns:

the default strategy factory

name

public java.lang.String name()

the name of the profile

Specified by:

name in interface Profile

Overrides:

name in class JavaProfile

Returns:

the name

getDefaultInstance

public static SimplifyTermProfile getDefaultInstance()

Returns the default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

Returns:

The default instance for usage in the Thread of the user interface.