public class TacletSoundnessPOLoader
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static interface |
TacletSoundnessPOLoader.LoaderListener |
static interface |
TacletSoundnessPOLoader.TacletFilter |
static class |
TacletSoundnessPOLoader.TacletInfo |
private class |
TacletSoundnessPOLoader.Working |
Modifier and Type | Field and Description |
---|---|
private boolean |
isOnlyUsedForProvingTaclets |
private java.util.List<TacletSoundnessPOLoader.LoaderListener> |
listeners |
private boolean |
loadAsLemmata |
private InitConfig |
originalConfig
If this InitConfig is unequal to null, the taclets will be loaded using this config
as well.
|
private ProofAggregate |
resultingProof |
private ImmutableSet<Taclet> |
resultingTaclets |
private ImmutableSet<Taclet> |
resultingTacletsForOriginalProof |
private TacletSoundnessPOLoader.TacletFilter |
tacletFilter |
private TacletLoader |
tacletLoader |
Constructor and Description |
---|
TacletSoundnessPOLoader(TacletSoundnessPOLoader.LoaderListener listener,
TacletSoundnessPOLoader.TacletFilter filter,
boolean loadAsLemmata,
TacletLoader loader,
InitConfig originalConfig,
boolean isOnlyUsedForProvingTaclets) |
private final boolean loadAsLemmata
private final InitConfig originalConfig
private final java.util.List<TacletSoundnessPOLoader.LoaderListener> listeners
private ProofAggregate resultingProof
private ImmutableSet<Taclet> resultingTaclets
private ImmutableSet<Taclet> resultingTacletsForOriginalProof
private final boolean isOnlyUsedForProvingTaclets
private final TacletLoader tacletLoader
private final TacletSoundnessPOLoader.TacletFilter tacletFilter
public TacletSoundnessPOLoader(TacletSoundnessPOLoader.LoaderListener listener, TacletSoundnessPOLoader.TacletFilter filter, boolean loadAsLemmata, TacletLoader loader, InitConfig originalConfig, boolean isOnlyUsedForProvingTaclets)
public void addListener(TacletSoundnessPOLoader.LoaderListener listener)
public void removeListener(TacletSoundnessPOLoader.LoaderListener listener)
public void start()
public void startSynchronously()
public ImmutableSet<Taclet> getResultingTacletsForOriginalProof()
private java.util.Vector<TacletSoundnessPOLoader.TacletInfo> createTacletInfo(ImmutableList<Taclet> taclets, ImmutableSet<Taclet> base)
private boolean check(Taclet taclet)
private void doWork() throws ProofInputException
ProofInputException
private ImmutableSet<Taclet> computeCommonTaclets(ImmutableList<Taclet> taclets, ImmutableSet<Taclet> reference)
private void computeResultingTaclets(java.util.List<TacletSoundnessPOLoader.TacletInfo> collectionOfTacletInfo)
private ImmutableSet<Taclet> getAlreadyInUseTaclets()
private boolean isUsedOnlyForProvingTaclets()
true
if and only if the taclets should be proved sound
and are not added to an already existing proof obligation.private ProofAggregate createProof(ProofEnvironment proofEnvForTaclets, ImmutableSet<Taclet> tacletsToProve, ImmutableSet<Taclet> axioms, ImmutableList<Taclet> loadedTaclets)
public void registerProofs(ProofAggregate aggregate, ProofEnvironment proofEnv)
public ProofAggregate getResultingProof()
public ImmutableSet<Taclet> getResultingTaclets()