public static class TacletLoader.KeYsTacletsLoader extends TacletLoader
TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader
listener, monitor, profile, proofEnvironment
Constructor and Description |
---|
KeYsTacletsLoader(ProgressMonitor monitor,
ProblemInitializer.ProblemInitializerListener listener,
Profile profile) |
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)
|
getProofEnvForTaclets, manageAvailableTaclets
public KeYsTacletsLoader(ProgressMonitor monitor, ProblemInitializer.ProblemInitializerListener listener, Profile profile)
public ImmutableSet<Taclet> loadAxioms()
TacletLoader
loadAxioms
in class TacletLoader
public ImmutableList<Taclet> loadTaclets()
TacletLoader
loadTaclets
in class TacletLoader
public ProofOblInput getTacletFile(Proof proof)
TacletLoader
getTacletFile
in class TacletLoader
public ImmutableSet<Taclet> getTacletsAlreadyInUse()
TacletLoader
getTacletsAlreadyInUse
in class TacletLoader