public final class ProblemInitializer
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static interface |
ProblemInitializer.ProblemInitializerListener |
Modifier and Type | Field and Description |
---|---|
private java.util.HashSet<EnvInput> |
alreadyParsed |
private static InitConfig |
baseConfig |
private ProblemInitializer.ProblemInitializerListener |
listener |
private ProgressMonitor |
progMon |
private Services |
services |
private ImmutableSet<PositionedString> |
warnings |
Constructor and Description |
---|
ProblemInitializer(Profile profile) |
ProblemInitializer(ProgressMonitor mon,
Services services,
ProblemInitializer.ProblemInitializerListener listener) |
Modifier and Type | Method and Description |
---|---|
private void |
cleanupNamespaces(InitConfig initConfig)
Removes all schema variables, all generic sorts and all sort
depending symbols for a generic sort out of the namespaces.
|
private InitConfig |
determineEnvironment(ProofOblInput po,
InitConfig initConfig) |
private java.util.Vector<java.lang.String> |
getClasses(java.lang.String f)
get a vector of Strings containing all .java file names
in the cfile directory.
|
ImmutableSet<PositionedString> |
getWarnings()
Returns the found warnings.
|
private void |
populateNamespaces(Proof proof)
Ensures that the passed proof's namespaces contain all functions
and program variables used in its root sequent.
|
private void |
populateNamespaces(Term term,
NamespaceSet namespaces,
Goal rootGoal) |
InitConfig |
prepare(EnvInput envInput)
Creates an initConfig / a proof environment and reads an EnvInput into it
|
private InitConfig |
prepare(EnvInput envInput,
InitConfig referenceConfig) |
private void |
progressStarted(java.lang.Object sender) |
private void |
progressStopped(java.lang.Object sender) |
private void |
proofCreated(ProofAggregate proofAggregate) |
void |
readEnvInput(EnvInput envInput,
InitConfig initConfig) |
private void |
readIncludes(EnvInput envInput,
InitConfig initConfig)
Helper for readEnvInput().
|
private void |
readJava(EnvInput envInput,
InitConfig initConfig)
Helper for readEnvInput().
|
private void |
readLDTIncludes(Includes in,
InitConfig initConfig)
Helper for readIncludes().
|
private void |
reportException(ProofOblInput input,
java.lang.Exception e) |
private void |
reportStatus(java.lang.String status)
displays the status report in the status line
|
private void |
reportStatus(java.lang.String status,
int progressMax)
displays the status report in the status line
and the maximum used by a progress bar
|
private void |
setProgress(int progress) |
private void |
setUpProofHelper(ProofOblInput problem,
ProofAggregate pl) |
ProofAggregate |
startProver(EnvInput envInput,
ProofOblInput po) |
ProofAggregate |
startProver(InitConfig initConfig,
ProofOblInput po) |
void |
tryReadProof(IProofFileParser pfp,
KeYUserProblemFile kupf) |
private static InitConfig baseConfig
private final Services services
private final ProgressMonitor progMon
private final java.util.HashSet<EnvInput> alreadyParsed
private final ProblemInitializer.ProblemInitializerListener listener
private ImmutableSet<PositionedString> warnings
public ProblemInitializer(ProgressMonitor mon, Services services, ProblemInitializer.ProblemInitializerListener listener)
public ProblemInitializer(Profile profile)
private void progressStarted(java.lang.Object sender)
private void progressStopped(java.lang.Object sender)
private void proofCreated(ProofAggregate proofAggregate)
private void reportStatus(java.lang.String status)
private void reportStatus(java.lang.String status, int progressMax)
status
- the String to be displayed in the status lineprogressMax
- an int describing what is 100 per centprivate void reportException(ProofOblInput input, java.lang.Exception e)
private void setProgress(int progress)
private void readLDTIncludes(Includes in, InitConfig initConfig) throws ProofInputException
ProofInputException
private void readIncludes(EnvInput envInput, InitConfig initConfig) throws ProofInputException
ProofInputException
private java.util.Vector<java.lang.String> getClasses(java.lang.String f) throws ProofInputException
ProofInputException
private void readJava(EnvInput envInput, InitConfig initConfig) throws ProofInputException
ProofInputException
private void cleanupNamespaces(InitConfig initConfig)
public final void readEnvInput(EnvInput envInput, InitConfig initConfig) throws ProofInputException
ProofInputException
private void populateNamespaces(Term term, NamespaceSet namespaces, Goal rootGoal)
private void populateNamespaces(Proof proof)
private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) throws ProofInputException
ProofInputException
private void setUpProofHelper(ProofOblInput problem, ProofAggregate pl) throws ProofInputException
ProofInputException
public InitConfig prepare(EnvInput envInput) throws ProofInputException
ProofInputException
private InitConfig prepare(EnvInput envInput, InitConfig referenceConfig) 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()