public abstract class AbstractProfile extends java.lang.Object implements Profile
Modifier and Type | Field and Description |
---|---|
private static Profile |
defaultProfile
The default profile which is used if no profile is defined in custom problem files (loaded via
KeYUserProblemFile ). |
private GoalChooserBuilder |
prototype |
private RuleCollection |
standardRules |
private ImmutableSet<StrategyFactory> |
strategies |
private ImmutableSet<java.lang.String> |
supportedGC |
private ImmutableSet<GoalChooserBuilder> |
supportedGCB |
private TermLabelManager |
termLabelManager |
Modifier | Constructor and Description |
---|---|
protected |
AbstractProfile(java.lang.String standardRuleFilename) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<GoalChooserBuilder> |
computeSupportedGoalChooserBuilder() |
protected abstract ImmutableList<TermLabelManager.TermLabelConfiguration> |
computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
private static ImmutableSet<java.lang.String> |
extractNames(ImmutableSet<GoalChooserBuilder> supportedGCB) |
GoalChooserBuilder |
getDefaultGoalChooserBuilder()
returns the default builder for a goal chooser
|
static Profile |
getDefaultProfile()
Returns the default profile which is used if no profile is defined in custom problem files (loaded via
KeYUserProblemFile ). |
java.lang.String |
getInternalClassDirectory()
returns the file name of the internal class directory relative to JavaRedux
|
java.lang.String |
getInternalClasslistFilename()
returns the file name of the internal class list
|
RuleJustification |
getJustification(Rule r)
any standard rule has is by default justified by an axiom rule
justification
|
GoalChooserBuilder |
getSelectedGoalChooserBuilder()
returns a copy of the selected goal chooser builder
|
RuleCollection |
getStandardRules()
returns the rule source containg all taclets for this profile
|
protected ImmutableSet<StrategyFactory> |
getStrategyFactories() |
StrategyFactory |
getStrategyFactory(Name n)
returns the StrategyFactory for strategy
strategyName |
TermLabelManager |
getTermLabelManager() |
protected ImmutableList<BuiltInRule> |
initBuiltInRules() |
protected void |
initTermLabelManager()
Initializes the
TermLabelManager . |
GoalChooserBuilder |
lookupGC(java.lang.String name)
looks up the demanded goal chooser is supported and returns a
new instance if possible otherwise
null is returned |
static void |
setDefaultProfile(Profile defaultProfile)
Sets the default profile which is used if no profile is defined in custom problem files (loaded via
KeYUserProblemFile ). |
void |
setSelectedGoalChooserBuilder(java.lang.String name)
sets the user selected goal chooser builder to be used as prototype
|
ImmutableSet<java.lang.String> |
supportedGoalChoosers()
returns the names of the supported goal chooser
builders
|
ImmutableSet<StrategyFactory> |
supportedStrategies()
returns the strategy factories for the supported strategies
|
boolean |
supportsStrategyFactory(Name strategy)
returns true if strategy
strategyName may be
used with this profile. |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getDefaultStrategyFactory, isSpecificationInvolvedInRuleApp, name
private static Profile defaultProfile
KeYUserProblemFile
).private final RuleCollection standardRules
private final ImmutableSet<StrategyFactory> strategies
private final ImmutableSet<java.lang.String> supportedGC
private final ImmutableSet<GoalChooserBuilder> supportedGCB
private GoalChooserBuilder prototype
private TermLabelManager termLabelManager
private static ImmutableSet<java.lang.String> extractNames(ImmutableSet<GoalChooserBuilder> supportedGCB)
protected ImmutableSet<GoalChooserBuilder> computeSupportedGoalChooserBuilder()
protected void initTermLabelManager()
TermLabelManager
.protected abstract ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()
TermLabelManager.TermLabelConfiguration
to use in this Profile
.TermLabelManager.TermLabelConfiguration
to use in this Profile
.public RuleCollection getStandardRules()
Profile
getStandardRules
in interface Profile
protected ImmutableSet<StrategyFactory> getStrategyFactories()
protected ImmutableList<BuiltInRule> initBuiltInRules()
public ImmutableSet<StrategyFactory> supportedStrategies()
Profile
supportedStrategies
in interface Profile
public boolean supportsStrategyFactory(Name strategy)
Profile
strategyName
may be
used with this profile.supportsStrategyFactory
in interface Profile
public StrategyFactory getStrategyFactory(Name n)
Profile
strategyName
getStrategyFactory
in interface Profile
n
- the Name of the strategypublic ImmutableSet<java.lang.String> supportedGoalChoosers()
supportedGoalChoosers
in interface Profile
public GoalChooserBuilder getDefaultGoalChooserBuilder()
getDefaultGoalChooserBuilder
in interface Profile
DefaultGoalChooserBuilder
public void setSelectedGoalChooserBuilder(java.lang.String name)
setSelectedGoalChooserBuilder
in interface Profile
name
- the String with the name of the goal chooser to be usedjava.lang.IllegalArgumentException
- if a goal chooser of the given name is not
supportedpublic GoalChooserBuilder lookupGC(java.lang.String name)
null
is returnedname
- the String with the goal choosers namenull
if the
demanded chooser is not supportedpublic GoalChooserBuilder getSelectedGoalChooserBuilder()
getSelectedGoalChooserBuilder
in interface Profile
public RuleJustification getJustification(Rule r)
getJustification
in interface Profile
public java.lang.String getInternalClassDirectory()
Profile
getInternalClassDirectory
in interface Profile
public java.lang.String getInternalClasslistFilename()
Profile
getInternalClasslistFilename
in interface Profile
public static Profile getDefaultProfile()
KeYUserProblemFile
).KeYUserProblemFile
).public static void setDefaultProfile(Profile defaultProfile)
KeYUserProblemFile
).defaultProfile
- The default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile
).public TermLabelManager getTermLabelManager()
getTermLabelManager
in interface Profile