de.uka.ilkd.key.taclettranslation.lemma

Class TacletLoader.TacletFromFileLoader

java.lang.Object

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

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

Enclosing class:

TacletLoader

public static class TacletLoader.TacletFromFileLoader
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

Modifier and Type	Field and Description
private java.io.File	fileForTaclets
private java.util.Collection<java.io.File>	filesForAxioms
private InitConfig	initConfig
private ProblemInitializer	problemInitializer

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

listener, monitor, profile, proofEnvironment

Constructor Summary

Constructors

Constructor and Description
TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, java.io.File fileForTaclets, java.util.Collection<java.io.File> filesForAxioms, InitConfig initConfig)
TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, Profile profile, java.io.File fileForTaclets, java.util.Collection<java.io.File> filesForAxioms)
TacletFromFileLoader(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)

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)
private static ProblemInitializer	makeProblemInitializer(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)
private void	prepareKeYFile(java.io.File 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

Field Detail

initConfig

private InitConfig initConfig

fileForTaclets

private final java.io.File fileForTaclets

filesForAxioms

private final java.util.Collection<java.io.File> filesForAxioms

problemInitializer

private final ProblemInitializer problemInitializer

Constructor Detail

TacletFromFileLoader

public TacletFromFileLoader(ProgressMonitor pm,
                            ProblemInitializer.ProblemInitializerListener listener,
                            ProblemInitializer problemInitializer,
                            java.io.File fileForTaclets,
                            java.util.Collection<java.io.File> filesForAxioms,
                            InitConfig initConfig)

TacletFromFileLoader

public TacletFromFileLoader(ProgressMonitor pm,
                            ProblemInitializer.ProblemInitializerListener listener,
                            ProblemInitializer problemInitializer,
                            Profile profile,
                            java.io.File fileForTaclets,
                            java.util.Collection<java.io.File> filesForAxioms)

TacletFromFileLoader

public TacletFromFileLoader(TacletLoader.TacletFromFileLoader loader,
                            InitConfig initConfig)

Method Detail

makeProblemInitializer

private static ProblemInitializer makeProblemInitializer(TacletLoader.TacletFromFileLoader loader,
                                                         InitConfig initConfig)

prepareKeYFile

private void prepareKeYFile(java.io.File file)

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

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

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