public static class TacletLoader.TacletFromFileLoader extends TacletLoader
TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader
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 |
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)
|
private static ProblemInitializer |
makeProblemInitializer(TacletLoader.TacletFromFileLoader loader,
InitConfig initConfig) |
private void |
prepareKeYFile(java.io.File file) |
getProofEnvForTaclets, manageAvailableTaclets
private InitConfig initConfig
private final java.io.File fileForTaclets
private final java.util.Collection<java.io.File> filesForAxioms
private final ProblemInitializer problemInitializer
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)
private static ProblemInitializer makeProblemInitializer(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)
private void prepareKeYFile(java.io.File file)
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