public class IntermediateProofReplayer
extends java.lang.Object
IntermediatePresentationProofFileParser
.
Replay is started using replay()
. In the course of replaying, new
nodes are added to the supplied proof object. The last goal touched during
replay can be obtained by getLastSelectedGoal()
.
TODO: Check if joining with more than one partner works out of the box.
Potential problem: Different order may result in syntactically different
nodes.
IntermediatePresentationProofFileParser
Constructor and Description |
---|
IntermediateProofReplayer(AbstractProblemLoader loader,
Proof proof,
de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser.Result parserResult)
Constructs a new
IntermediateProofReplayer . |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<java.lang.Throwable> |
getErrors() |
Goal |
getLastSelectedGoal() |
java.lang.String |
getStatus()
Communicates a non-fatal condition to the caller.
|
static TacletApp |
parseSV1(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Services services)
Instantiates a schema variable in the given taclet application.
|
static TacletApp |
parseSV2(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Goal targetGoal)
Instantiates a schema variable in the given taclet application.
|
static Term |
parseTerm(java.lang.String value,
Proof proof)
Parses a given term in String representation.
|
static Term |
parseTerm(java.lang.String value,
Proof proof,
Namespace<QuantifiableVariable> varNS,
Namespace<IProgramVariable> progVarNS,
Namespace<Function> functNS)
Parses a given term in String representation.
|
de.uka.ilkd.key.proof.io.IntermediateProofReplayer.Result |
replay()
Starts the actual replay process.
|
public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser.Result parserResult)
IntermediateProofReplayer
.loader
- The problem loader, for reporting errors.proof
- The proof object into which to load the replayed proof.intermediate
- public Goal getLastSelectedGoal()
public de.uka.ilkd.key.proof.io.IntermediateProofReplayer.Result replay()
getLastSelectedGoal()
.public java.lang.String getStatus()
public java.util.Collection<java.lang.Throwable> getErrors()
public static Term parseTerm(java.lang.String value, Proof proof, Namespace<QuantifiableVariable> varNS, Namespace<IProgramVariable> progVarNS, Namespace<Function> functNS)
value
- String to parse.proof
- Proof object (for namespaces and Services object).varNS
- Variable namespace.progVarNS
- Program variable namespace.ParserException
- In case of an error.public static Term parseTerm(java.lang.String value, Proof proof)
value
- String to parse.proof
- Proof object (for namespaces and Services object).public static TacletApp parseSV1(TacletApp app, SchemaVariable sv, java.lang.String value, Services services)
app
- Application to instantiate.sv
- Schema variable (VariableSV) to instantiate.value
- Name for the instantiated logic variable.services
- The services object.public static TacletApp parseSV2(TacletApp app, SchemaVariable sv, java.lang.String value, Goal targetGoal)
app
- Application to instantiate.sv
- Schema variable to instantiate.value
- Name for the instantiated Skolem constant, program element or
term..targetGoal
- The goal corresponding to the given application.parseSV1(TacletApp, SchemaVariable, String, Services)
Copyright © 2003-2019 The KeY-Project.