public static class TacletLoader.TacletFromFileLoader extends TacletLoader
TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader
Modifier and Type | Field and Description |
---|---|
private File |
fileForTaclets |
private Collection<File> |
filesForAxioms |
private InitConfig |
initConfig |
private ProblemInitializer |
problemInitializer |
listener, monitor, profile, proofEnvironment
Constructor and Description |
---|
TacletLoader.TacletFromFileLoader(ProgressMonitor pm,
ProblemInitializer.ProblemInitializerListener listener,
ProblemInitializer problemInitializer,
File fileForTaclets,
Collection<File> filesForAxioms,
InitConfig initConfig) |
TacletLoader.TacletFromFileLoader(ProgressMonitor pm,
ProblemInitializer.ProblemInitializerListener listener,
ProblemInitializer problemInitializer,
Profile profile,
File fileForTaclets,
Collection<File> filesForAxioms) |
TacletLoader.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(File file) |
getProofEnvForTaclets, manageAvailableTaclets
private InitConfig initConfig
private final File fileForTaclets
private final Collection<File> filesForAxioms
private final ProblemInitializer problemInitializer
public TacletLoader.TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, File fileForTaclets, Collection<File> filesForAxioms, InitConfig initConfig)
public TacletLoader.TacletFromFileLoader(ProgressMonitor pm, ProblemInitializer.ProblemInitializerListener listener, ProblemInitializer problemInitializer, Profile profile, File fileForTaclets, Collection<File> filesForAxioms)
public TacletLoader.TacletFromFileLoader(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)
private static ProblemInitializer makeProblemInitializer(TacletLoader.TacletFromFileLoader loader, InitConfig initConfig)
private void prepareKeYFile(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