|
| |
|
| java.lang.Object
 de.uka.ilkd.key.proof.init.InitConfig
| InitConfig | | public class InitConfig (Code) | | an instance of this class describes the initial configuration of the prover.
This includes sorts, functions, heuristics, and variables namespaces,
information on the underlying java model, and a set of rules.
|
| InitConfig | | public InitConfig()(Code) | | |
| activatedTaclets | | public SetOfTaclet activatedTaclets()(Code) | | returns the activated taclets of this initial configuration
|
| addCategory2DefaultChoices | | public void addCategory2DefaultChoices(HashMap init)(Code) | | adds entries to the HashMap that maps categories to their
default choices.
Only entries of init with keys not already contained in
category2DefaultChoice are added.
|
| builtInRules | | public ListOfBuiltInRule builtInRules()(Code) | | returns the built-in rules of this initial configuration
|
| choiceNS | | public Namespace choiceNS()(Code) | | returns the choice namespace of this initial configuration
|
| copy | | public InitConfig copy()(Code) | | returns a copy of this initial configuration copying the namespaces,
the contained JavaInfo while using the immutable set of taclets in the
copy
|
| createBuiltInRuleIndex | | public BuiltInRuleIndex createBuiltInRuleIndex()(Code) | | returns a new created index for built in rules (at the moment immutable
list)
|
| createNamespacesForActivatedChoices | | public void createNamespacesForActivatedChoices()(Code) | | |
| createTacletIndex | | public TacletIndex createTacletIndex()(Code) | | returns a newly created taclet index for the set of activated
taclets contained in this initial configuration
|
| funcNS | | public Namespace funcNS()(Code) | | returns the function namespace of this initial configuration
|
| getActivatedChoices | | public SetOfChoice getActivatedChoices()(Code) | | Returns the choices which are currently active.
For getting the active choices for a specific proof,
getChoices in de.uka.ilkd.key.proof.Proof
has to be used.
|
| getProofEnv | | public ProofEnvironment getProofEnv()(Code) | | returns the proof environment using this initial configuration
the ProofEnvironment using this configuration |
| getServices | | public Services getServices()(Code) | | returns the Services of this initial configuration providing access
to the used program model
the Services of this initial configuration |
| getTaclet2Builder | | public HashMap getTaclet2Builder()(Code) | | 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 demand
the map from a taclet to its builder |
| getTaclets | | public SetOfTaclet getTaclets()(Code) | | |
| namespaces | | public NamespaceSet namespaces()(Code) | | returns the namespaces of this initial configuration
|
| progVarNS | | public Namespace progVarNS()(Code) | | returns the program variable namespace of this initial configuration
|
| ruleSetNS | | public Namespace ruleSetNS()(Code) | | returns the heuristics namespace of this initial configuration
|
| setActivatedChoices | | public void setActivatedChoices(SetOfChoice activatedChoices)(Code) | | sets the set of activated choices of this initial configuration.
For categories without a specified choice the default choice contained
in category2DefaultChoice is added.
|
| setTaclet2Builder | | public void setTaclet2Builder(HashMap taclet2Builder)(Code) | | |
| setTaclets | | public void setTaclets(SetOfTaclet taclets)(Code) | | |
| sortNS | | public Namespace sortNS()(Code) | | returns the sort namespace of this initial configuration
|
| varNS | | public Namespace varNS()(Code) | | returns the variable namespace of this initial configuration
|
|
|
|