public class InitConfig
extends java.lang.Object
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.Map<java.lang.String,java.lang.String> init)
Adds default choices given in
init . |
boolean |
addCategoryDefaultChoice(java.lang.String category,
java.lang.String choice)
Adds a default option for a category.
|
void |
addTaclets(java.util.Collection<Taclet> tacs) |
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
|
Namespace<Function> |
funcNS()
returns the function namespace of this initial configuration.
|
ImmutableSet<Choice> |
getActivatedChoices()
Returns the choices which are currently active.
|
FileRepo |
getFileRepo() |
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 |
setFileRepo(FileRepo fileRepo) |
void |
setSettings(ProofSettings newSettings) |
void |
setTaclet2Builder(java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
void |
setTaclets(java.util.Collection<Taclet> tacs) |
void |
setTaclets(ImmutableList<Taclet> tacs) |
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
|
public InitConfig(Services services)
public final Services getServices()
public Profile getProfile()
public boolean addCategoryDefaultChoice(@Nonnull java.lang.String category, @Nonnull java.lang.String choice)
public void addCategory2DefaultChoices(@Nonnull java.util.Map<java.lang.String,java.lang.String> init)
init
.
Not overriding previous default choices.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 addTaclets(java.util.Collection<Taclet> tacs)
public void setTaclets(ImmutableList<Taclet> tacs)
public void setTaclets(java.util.Collection<Taclet> tacs)
public ImmutableList<Taclet> getTaclets()
public java.lang.Iterable<Taclet> activatedTaclets()
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
public FileRepo getFileRepo()
public void setFileRepo(FileRepo fileRepo)
Copyright © 2003-2019 The KeY-Project.