public final class KeYUserProblemFile extends KeYFile implements ProofOblInput
Modifier and Type | Field and Description |
---|---|
private KeYParserF |
lastParser |
private java.lang.String |
problemHeader |
private Term |
problemTerm |
file, initConfig, monitor
Constructor and Description |
---|
KeYUserProblemFile(java.lang.String name,
java.io.File file,
ProgressMonitor monitor,
Profile profile)
Creates a new representation of a KeYUserFile with the given name,
a rule source representing the physical source of the input, and
a graphical representation to call back in order to report the progress
while reading.
|
KeYUserProblemFile(java.lang.String name,
java.io.File file,
ProgressMonitor monitor,
Profile profile,
boolean compressed)
Instantiates a new user problem file.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object o) |
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
protected Profile |
getDefaultProfile()
Returns the default
Profile which was defined by a constructor. |
ProofAggregate |
getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
Profile |
getProfile()
Returns the
Profile to use. |
int |
hashCode() |
boolean |
hasProofScript() |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
ImmutableSet<PositionedString> |
read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
void |
readProblem() |
protected Profile |
readProfileFromFile()
Tries to read the
Profile from the file to load. |
void |
readProof(IProofFileParser prl)
Reads a saved proof of a .key file.
|
Triple<java.lang.String,java.lang.Integer,java.lang.Integer> |
readProofScript() |
chooseContract, close, getInitialFile, getNewStream, getNumberOfChars, getPreferences, getProofObligation, name, readBootClassPath, readClassPath, readFuncAndPred, readIncludes, readJavaPath, readPreferences, readRulesAndProblem, readSorts, setInitConfig, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
name
private Term problemTerm
private java.lang.String problemHeader
private KeYParserF lastParser
public KeYUserProblemFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile)
public KeYUserProblemFile(java.lang.String name, java.io.File file, ProgressMonitor monitor, Profile profile, boolean compressed)
name
- the name of the filefile
- the file tp read frommonitor
- the possibly null monitor for progressprofile
- the KeY profile under which to loadcompressed
- true
iff the file is compressedpublic ImmutableSet<PositionedString> read() throws ProofInputException
EnvInput
read
in interface EnvInput
read
in class KeYFile
ImmutableSet
if no warnings occurred.ProofInputException
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
public ProofAggregate getPO() throws ProofInputException
ProofOblInput
getPO
in interface ProofOblInput
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
public boolean hasProofScript()
public Triple<java.lang.String,java.lang.Integer,java.lang.Integer> readProofScript() throws ProofInputException
ProofInputException
public void readProof(IProofFileParser prl) throws ProofInputException
ProofInputException
public Profile getProfile()
Profile
to use.getProfile
in interface EnvInput
getProfile
in class KeYFile
Profile
to use.protected Profile readProfileFromFile() throws java.lang.Exception
Profile
from the file to load.protected Profile getDefaultProfile()
Profile
which was defined by a constructor.Profile
.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.