public abstract class TacletLoader
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
TacletLoader.KeYsTacletsLoader |
static class |
TacletLoader.TacletFromFileLoader |
Modifier and Type | Field and Description |
---|---|
protected ProblemInitializer.ProblemInitializerListener |
listener |
protected ProgressMonitor |
monitor |
protected Profile |
profile |
protected ProofEnvironment |
proofEnvironment |
Constructor and Description |
---|
TacletLoader(ProgressMonitor monitor,
ProblemInitializer.ProblemInitializerListener listener,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
ProofEnvironment |
getProofEnvForTaclets() |
abstract ProofOblInput |
getTacletFile(Proof proof)
subclasses give a special proof obligation input per proof.
|
abstract ImmutableSet<Taclet> |
getTacletsAlreadyInUse()
get the taclet base which is considered fix (?)
|
abstract ImmutableSet<Taclet> |
loadAxioms()
get the set of axioms from the axiom files if applicable.
|
abstract ImmutableList<Taclet> |
loadTaclets()
get the set of taclets to examine
(either from the system or from a file)
|
void |
manageAvailableTaclets(InitConfig initConfig,
Taclet tacletToProve)
When proving existing system taclets, all rules which occurred prior to
the desired taclet need to be elminated from the set of available taclets
to avoid circular proofs.
|
protected final ProgressMonitor monitor
protected final ProblemInitializer.ProblemInitializerListener listener
protected final Profile profile
protected ProofEnvironment proofEnvironment
public TacletLoader(ProgressMonitor monitor, ProblemInitializer.ProblemInitializerListener listener, Profile profile)
public abstract ImmutableSet<Taclet> loadAxioms()
public abstract ImmutableList<Taclet> loadTaclets()
public abstract ImmutableSet<Taclet> getTacletsAlreadyInUse()
public abstract ProofOblInput getTacletFile(Proof proof)
public void manageAvailableTaclets(InitConfig initConfig, Taclet tacletToProve)
taclet
- the taclet for which PO will be generated. Remove all taclets
after this taclet.initConfig
- the initial config from which the taclet to prove and all
following taclets have been removed.public ProofEnvironment getProofEnvForTaclets()