public class ProofObligationCreator
extends java.lang.Object
create(...)
.Constructor and Description |
---|
ProofObligationCreator() |
Modifier and Type | Method and Description |
---|---|
private UserDefinedSymbols |
analyzeTaclets(ImmutableSet<Taclet> taclets,
NamespaceSet referenceNamespaces) |
private void |
collectUserDefinedSymbols(Term term,
UserDefinedSymbols userDefinedSymbols) |
ProofAggregate |
create(ImmutableSet<Taclet> taclets,
InitConfig[] initConfigs,
ImmutableSet<Taclet> axioms,
java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
Creates for each taclet in
taclets a proof obligation
containing the corresponding FOL formula of the taclet. |
private ProofAggregate |
create(Taclet taclet,
InitConfig initConfig,
UserDefinedSymbols symbolsForAxioms) |
private java.lang.String |
createName(ProofAggregate[] singleProofs) |
private java.lang.String createName(ProofAggregate[] singleProofs)
public ProofAggregate create(ImmutableSet<Taclet> taclets, InitConfig[] initConfigs, ImmutableSet<Taclet> axioms, java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
taclets
a proof obligation
containing the corresponding FOL formula of the taclet.taclets
- Sets of taclets the proof obligations should be created for.initConfig
- the initial configuration that should be used for creating the proofs.axioms
- The set of user-defined taclets that should be used as additional rules. This
taclets are added to the single proof obligation so that they can be used for the proof.listeners
- a listener that observes the single steps. Used for status information.private UserDefinedSymbols analyzeTaclets(ImmutableSet<Taclet> taclets, NamespaceSet referenceNamespaces)
private void collectUserDefinedSymbols(Term term, UserDefinedSymbols userDefinedSymbols)
private ProofAggregate create(Taclet taclet, InitConfig initConfig, UserDefinedSymbols symbolsForAxioms)