public class InitConfig
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<Choice> |
activatedChoices
Set of the rule options activated for the current proof.
|
private java.util.Map<Name,Taclet> |
activatedTacletCache
HashMap for quick lookups taclet name->taclet
|
private java.util.HashMap<java.lang.String,java.lang.String> |
category2DefaultChoice
maps categories to their default choice (both represented as Strings),
which is used if no other choice is specified in the problemfile
|
private RuleJustificationInfo |
justifInfo |
private java.lang.String |
originalKeYFileName |
private Services |
services
the services class allowing to access information about the underlying
program model
|
private ProofSettings |
settings |
private java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> |
taclet2Builder
maps taclets to their TacletBuilders.
|
private ImmutableList<Taclet> |
taclets |
Constructor and Description |
---|
InitConfig(Services services) |
Modifier and Type | Method and Description |
---|---|
java.lang.Iterable<Taclet> |
activatedTaclets()
returns the activated taclets of this initial configuration
|
void |
addCategory2DefaultChoices(java.util.HashMap<java.lang.String,java.lang.String> init)
adds entries to the HashMap that maps categories to their
default choices.
|
ImmutableList<BuiltInRule> |
builtInRules()
returns the built-in rules of this initial configuration
|
Namespace<Choice> |
choiceNS()
returns the choice namespace of this initial configuration
|
InitConfig |
copy()
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
InitConfig |
copyWithServices(Services services)
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
BuiltInRuleIndex |
createBuiltInRuleIndex()
returns a new created index for built in rules (at the moment immutable
list)
|
TacletIndex |
createTacletIndex()
returns a newly created taclet index for the set of activated
taclets contained in this initial configuration
|
InitConfig |
deepCopy()
returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
private void |
fillActiveTacletCache()
fills the active taclet cache
|
Namespace<Function> |
funcNS()
returns the function namespace of this initial configuration.
|
ImmutableSet<Choice> |
getActivatedChoices()
Returns the choices which are currently active.
|
RuleJustificationInfo |
getJustifInfo()
returns the object managing the rules in this environment and
their justifications.
|
Profile |
getProfile() |
Services |
getServices()
returns the Services of this initial configuration providing access
to the used program model
|
ProofSettings |
getSettings() |
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> |
getTaclet2Builder()
Taclet s are constructed using TacletBuilder s this map
contains the pair of a taclet and its builder which is important as
goals of a taclet may depend of the selected choices. |
ImmutableList<Taclet> |
getTaclets() |
Taclet |
lookupActiveTaclet(Name name) |
NamespaceSet |
namespaces()
returns the namespaces of this initial configuration
|
Namespace<IProgramVariable> |
progVarNS()
returns the program variable namespace of this initial configuration
|
void |
registerRule(Rule r,
RuleJustification j)
registers a rule with the given justification at the
justification managing
RuleJustification object of this
environment. |
void |
registerRuleIntroducedAtNode(RuleApp r,
Node node,
boolean isAxiom) |
void |
registerRules(java.lang.Iterable<? extends Rule> s,
RuleJustification j)
registers a list of rules with the given justification at the
justification managing
RuleJustification object of this
environment. |
Namespace<RuleSet> |
ruleSetNS()
returns the heuristics namespace of this initial configuration
|
void |
setActivatedChoices(ImmutableSet<Choice> activatedChoices)
sets the set of activated choices of this initial configuration.
|
void |
setSettings(ProofSettings newSettings) |
void |
setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
void |
setTaclets(ImmutableList<Taclet> taclets) |
Namespace<Sort> |
sortNS()
returns the sort namespace of this initial configuration
|
java.lang.String |
toString() |
Namespace<QuantifiableVariable> |
varNS()
returns the variable namespace of this initial configuration
|
private final Services services
private RuleJustificationInfo justifInfo
private ImmutableList<Taclet> taclets
private java.util.HashMap<java.lang.String,java.lang.String> category2DefaultChoice
private java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder
private ImmutableSet<Choice> activatedChoices
Choice
s) allow to use different ruleset modelling or skipping
certain features (e.g. nullpointer checks when resolving references)private java.util.Map<Name,Taclet> activatedTacletCache
private java.lang.String originalKeYFileName
private ProofSettings settings
public InitConfig(Services services)
public final Services getServices()
public Profile getProfile()
public void addCategory2DefaultChoices(java.util.HashMap<java.lang.String,java.lang.String> init)
init with keys not already contained in
category2DefaultChoice are added.
public void setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder)
public java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> getTaclet2Builder()
Taclet
s are constructed using TacletBuilder
s this map
contains the pair of a taclet and its builder which is important as
goals of a taclet may depend of the selected choices. Instead of
creating all possible combinations in advance this is done by demandpublic void setActivatedChoices(ImmutableSet<Choice> activatedChoices)
public ImmutableSet<Choice> getActivatedChoices()
getChoices
in de.uka.ilkd.key.proof.Proof
has to be used.public void setTaclets(ImmutableList<Taclet> taclets)
public ImmutableList<Taclet> getTaclets()
public java.lang.Iterable<Taclet> activatedTaclets()
private void fillActiveTacletCache()
public ImmutableList<BuiltInRule> builtInRules()
public void registerRule(Rule r, RuleJustification j)
RuleJustification
object of this
environment.public void registerRuleIntroducedAtNode(RuleApp r, Node node, boolean isAxiom)
public void registerRules(java.lang.Iterable<? extends Rule> s, RuleJustification j)
RuleJustification
object of this
environment. All rules of the list are given the same
justification.public RuleJustificationInfo getJustifInfo()
public TacletIndex createTacletIndex()
public BuiltInRuleIndex createBuiltInRuleIndex()
public NamespaceSet namespaces()
public Namespace<Function> funcNS()
public Namespace<RuleSet> ruleSetNS()
public Namespace<QuantifiableVariable> varNS()
public Namespace<IProgramVariable> progVarNS()
public Namespace<Choice> choiceNS()
public void setSettings(ProofSettings newSettings)
public ProofSettings getSettings()
public InitConfig copy()
public InitConfig deepCopy()
public InitConfig copyWithServices(Services services)
public java.lang.String toString()
toString
in class java.lang.Object