public static class TacletLoader.TacletFromFileLoader extends TacletLoader
TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader
listener, monitor, profile, proofEnvironment
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) |
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 TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, java.io.File fileForTaclets, java.util.Collection<java.io.File> filesForAxioms, InitConfig initConfig)
public TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, Profile profile, java.io.File fileForTaclets, java.util.Collection<java.io.File> filesForAxioms)
public TacletFromFileLoader(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)
public ImmutableList<Taclet> loadTaclets()
TacletLoader
loadTaclets
in class TacletLoader
public ImmutableSet<Taclet> loadAxioms()
TacletLoader
loadAxioms
in class TacletLoader
public ProofOblInput getTacletFile(Proof proof)
TacletLoader
getTacletFile
in class TacletLoader
public ImmutableSet<Taclet> getTacletsAlreadyInUse()
TacletLoader
getTacletsAlreadyInUse
in class TacletLoader
Copyright © 2003-2019 The KeY-Project.