de.uka.ilkd.key.taclettranslation.lemma

Class TacletLoader.KeYsTacletsLoader

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.TacletLoader

de.uka.ilkd.key.taclettranslation.lemma.TacletLoader.KeYsTacletsLoader

Enclosing class:

TacletLoader

public static class TacletLoader.KeYsTacletsLoader
extends TacletLoader

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.taclettranslation.lemma.TacletLoader

TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader

Field Summary

Fields inherited from class de.uka.ilkd.key.taclettranslation.lemma.TacletLoader

listener, monitor, profile, proofEnvironment

Constructor Summary

Constructors

Constructor and Description
KeYsTacletsLoader(ProgressMonitor monitor, ProblemInitializer.ProblemInitializerListener listener, Profile profile)

Method Summary

Modifier and Type	Method and Description
ProofOblInput	getTacletFile(Proof proof) subclasses give a special proof obligation input per proof.
ImmutableSet<Taclet>	getTacletsAlreadyInUse() get the taclet base which is considered fix (?)
ImmutableSet<Taclet>	loadAxioms() get the set of axioms from the axiom files if applicable.
ImmutableList<Taclet>	loadTaclets() get the set of taclets to examine (either from the system or from a file)

Methods inherited from class de.uka.ilkd.key.taclettranslation.lemma.TacletLoader

getProofEnvForTaclets, manageAvailableTaclets

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

KeYsTacletsLoader

public KeYsTacletsLoader(ProgressMonitor monitor,
                         ProblemInitializer.ProblemInitializerListener listener,
                         Profile profile)

Method Detail

loadAxioms

public ImmutableSet<Taclet> loadAxioms()

Description copied from class: TacletLoader

get the set of axioms from the axiom files if applicable.

Specified by:

loadAxioms in class TacletLoader

loadTaclets

public ImmutableList<Taclet> loadTaclets()

Description copied from class: TacletLoader

get the set of taclets to examine (either from the system or from a file)

Specified by:

loadTaclets in class TacletLoader

getTacletFile

public ProofOblInput getTacletFile(Proof proof)

Description copied from class: TacletLoader

subclasses give a special proof obligation input per proof. They can choose the implementing class and pass to it any necessary information.

Specified by:

getTacletFile in class TacletLoader

getTacletsAlreadyInUse

public ImmutableSet<Taclet> getTacletsAlreadyInUse()

Description copied from class: TacletLoader

get the taclet base which is considered fix (?)

Specified by:

getTacletsAlreadyInUse in class TacletLoader