public final class ProblemInitializer
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static interface |
ProblemInitializer.ProblemInitializerListener |
Constructor and Description |
---|
ProblemInitializer(Profile profile) |
ProblemInitializer(ProgressMonitor mon,
Services services,
ProblemInitializer.ProblemInitializerListener listener) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<PositionedString> |
getWarnings()
Returns the found warnings.
|
InitConfig |
prepare(EnvInput envInput)
Creates an initConfig / a proof environment and reads an EnvInput into it
|
void |
readEnvInput(EnvInput envInput,
InitConfig initConfig) |
void |
setFileRepo(FileRepo fileRepo)
Sets the FileRepo responsible for consistency between source code and proof.
|
ProofAggregate |
startProver(EnvInput envInput,
ProofOblInput po) |
ProofAggregate |
startProver(InitConfig initConfig,
ProofOblInput po) |
void |
tryReadProof(IProofFileParser pfp,
KeYUserProblemFile kupf) |
public ProblemInitializer(ProgressMonitor mon, Services services, ProblemInitializer.ProblemInitializerListener listener)
public ProblemInitializer(Profile profile)
public final void readEnvInput(EnvInput envInput, InitConfig initConfig) throws ProofInputException
ProofInputException
public InitConfig prepare(EnvInput envInput) throws ProofInputException
ProofInputException
public ProofAggregate startProver(InitConfig initConfig, ProofOblInput po) throws ProofInputException
ProofInputException
public ProofAggregate startProver(EnvInput envInput, ProofOblInput po) throws ProofInputException
ProofInputException
public void tryReadProof(IProofFileParser pfp, KeYUserProblemFile kupf) throws ProofInputException
ProofInputException
public ImmutableSet<PositionedString> getWarnings()
public void setFileRepo(FileRepo fileRepo)
fileRepo
- the FileRepo to setCopyright © 2003-2019 The KeY-Project.