de.uka.ilkd.key.taclettranslation.lemma

Class TacletLoader

java.lang.Object

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

Direct Known Subclasses:

TacletLoader.KeYsTacletsLoader, TacletLoader.TacletFromFileLoader

public abstract class TacletLoader
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	TacletLoader.KeYsTacletsLoader
static class	TacletLoader.TacletFromFileLoader

Field Summary

Fields

Modifier and Type	Field and Description
protected ProblemInitializer.ProblemInitializerListener	listener
protected ProgressMonitor	monitor
protected Profile	profile
protected ProofEnvironment	proofEnvironment

Constructor Summary

Constructors

Constructor and Description
TacletLoader(ProgressMonitor monitor, ProblemInitializer.ProblemInitializerListener listener, Profile profile)

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

monitor

protected final ProgressMonitor monitor

listener

protected final ProblemInitializer.ProblemInitializerListener listener

profile

protected final Profile profile

proofEnvironment

protected ProofEnvironment proofEnvironment

Constructor Detail

TacletLoader

public TacletLoader(ProgressMonitor monitor,
                    ProblemInitializer.ProblemInitializerListener listener,
                    Profile profile)

Method Detail

loadAxioms

public abstract ImmutableSet<Taclet> loadAxioms()

get the set of axioms from the axiom files if applicable.

loadTaclets

public abstract ImmutableList<Taclet> loadTaclets()

get the set of taclets to examine (either from the system or from a file)

getTacletsAlreadyInUse

public abstract ImmutableSet<Taclet> getTacletsAlreadyInUse()

get the taclet base which is considered fix (?)

getTacletFile

public abstract ProofOblInput getTacletFile(Proof proof)

subclasses give a special proof obligation input per proof. They can choose the implementing class and pass to it any necessary information.

manageAvailableTaclets

public 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. This method removes all taclets in initConfig's taclet database from given first taclet. Taclets are stored in ImmutableSets which fortunately enough still have a fixed order due to their implementation using immutable lists.

Parameters:

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.

getProofEnvForTaclets

public ProofEnvironment getProofEnvForTaclets()