public static class ProofStarter.UserProvidedInput extends java.lang.Object implements ProofOblInput
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
EMPTY_PROOF_HEADER |
private ProofEnvironment |
env |
private java.lang.String |
proofName |
private Sequent |
seq |
Constructor and Description |
---|
UserProvidedInput(Sequent seq,
ProofEnvironment env) |
UserProvidedInput(Sequent seq,
ProofEnvironment env,
java.lang.String proofName) |
UserProvidedInput(Term formula,
ProofEnvironment env) |
Modifier and Type | Method and Description |
---|---|
private Proof |
createProof(java.lang.String proofName) |
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
ProofAggregate |
getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
java.lang.String |
name()
Returns the name of the proof obligation input.
|
void |
readProblem() |
private static final java.lang.String EMPTY_PROOF_HEADER
private final ProofEnvironment env
private final Sequent seq
private final java.lang.String proofName
public UserProvidedInput(Sequent seq, ProofEnvironment env)
public UserProvidedInput(Sequent seq, ProofEnvironment env, java.lang.String proofName)
public UserProvidedInput(Term formula, ProofEnvironment env)
public java.lang.String name()
ProofOblInput
name
in interface ProofOblInput
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
private Proof createProof(java.lang.String proofName)
public ProofAggregate getPO() throws ProofInputException
ProofOblInput
getPO
in interface ProofOblInput
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
KeYJavaType
in which the proven element is contained in or null
if not available.