public class InitConfig extends Object
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<Choice> |
activatedChoices
Set of the rule options activated for the current proof.
|
private Map<Name,Taclet> |
activatedTacletCache
HashMap for quick lookups taclet name->taclet
|
private HashMap<String,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 String |
originalKeYFileName |
private Services |
services
the services class allowing to access information about the underlying
program model
|
private ProofSettings |
settings |
private 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 |
---|---|
Iterable<Taclet> |
activatedTaclets()
returns the activated taclets of this initial configuration
|
void |
addCategory2DefaultChoices(HashMap<String,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 |
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 |
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() |
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 |
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(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 |
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(HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
void |
setTaclets(ImmutableList<Taclet> taclets) |
Namespace |
sortNS()
returns the sort namespace of this initial configuration
|
String |
toString() |
Namespace |
varNS()
returns the variable namespace of this initial configuration
|
private final Services services
private RuleJustificationInfo justifInfo
private ImmutableList<Taclet> taclets
private HashMap<String,String> category2DefaultChoice
private 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 Map<Name,Taclet> activatedTacletCache
private String originalKeYFileName
private ProofSettings settings
public InitConfig(Services services)
public final Services getServices()
public Profile getProfile()
public void addCategory2DefaultChoices(HashMap<String,String> init)
init with keys not already contained in
category2DefaultChoice are added.
public void setTaclet2Builder(HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder)
public 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 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(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 funcNS()
public Namespace sortNS()
public Namespace ruleSetNS()
public Namespace varNS()
public Namespace progVarNS()
public Namespace choiceNS()
public void setSettings(ProofSettings newSettings)
public ProofSettings getSettings()
public InitConfig copy()
public InitConfig deepCopy()
public InitConfig copyWithServices(Services services)