de.uka.ilkd.key.proof.io

Class IntermediateProofReplayer

java.lang.Object

de.uka.ilkd.key.proof.io.IntermediateProofReplayer

public class IntermediateProofReplayer
extends java.lang.Object

This class is responsible for generating a KeY proof from an intermediate representation generated by 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.

Author:

Dominic Scheurer

See Also:

IntermediatePresentationProofFileParser

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	IntermediateProofReplayer.BuiltInConstructionException Signals an error during construction of a built-in rule app.
(package private) static class	IntermediateProofReplayer.Result Simple structure containing the results of the replay procedure.
(package private) static class	IntermediateProofReplayer.SkipSMTRuleException Signals that the execution of an SMT solver, that has been used before the now loaded proof was saved, has been skipped.
(package private) static class	IntermediateProofReplayer.TacletConstructionException Signals an error during construction of a taclet app.

Field Summary

Fields

Modifier and Type	Field and Description
private Goal	currGoal The current open goal
private static java.lang.String	ERROR_LOADING_PROOF_LINE
private java.util.List<java.lang.Throwable>	errors Encountered errors
private java.util.HashMap<java.lang.Integer,java.util.HashSet<Triple<Node,PosInOccurrence,NodeIntermediate>>>	joinPartnerNodes Maps join node IDs to previously seen join partners
private AbstractProblemLoader	loader The problem loader, for reporting errors
private static java.lang.String	NOT_APPLICABLE
private Proof	proof The proof object into which to load the replayed proof
private java.util.LinkedList<Pair<Node,NodeIntermediate>>	queue Stores open branches
private java.lang.String	status Error status

Constructor Summary

Constructors

Constructor and Description
IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, IntermediatePresentationProofFileParser.Result parserResult) Constructs a new IntermediateProofReplayer.

Method Summary

Modifier and Type	Method and Description
private void	addChildren(java.util.Iterator<Node> children, java.util.LinkedList<NodeIntermediate> intermChildren) Adds the pairs of proof node children and intermediate children to the queue.
private static ImmutableSet<IBuiltInRuleApp>	collectAppsForRule(java.lang.String ruleName, Goal g, PosInOccurrence pos) Retrieves all registered applications at the given goal and position for the rule corresponding to the given ruleName.
private IBuiltInRuleApp	constructBuiltinApp(BuiltInAppIntermediate currInterm, Goal currGoal) Constructs a built-in rule application from an intermediate one.
private static TacletApp	constructInsts(TacletApp app, Goal currGoal, java.util.LinkedList<java.lang.String> loadedInsts, Services services) Instantiates schema variables in the given taclet application.
private TacletApp	constructTacletApp(TacletAppIntermediate currInterm, Goal currGoal) Constructs a taclet application from an intermediate one.
java.util.Collection<java.lang.Throwable>	getErrors()
Goal	getLastSelectedGoal()
java.lang.String	getStatus() Communicates a non-fatal condition to the caller.
private MergeRuleBuiltInRuleApp	instantiateJoinApp(MergeAppIntermediate joinAppInterm, Node currNode, java.util.Set<Triple<Node,PosInOccurrence,NodeIntermediate>> partnerNodesInfo, Services services) Instantiates a Join Rule application.
private static SchemaVariable	lookupName(ImmutableSet<SchemaVariable> set, java.lang.String name) Finds a schema variable in the given set.
static TacletApp	parseSV1(TacletApp app, SchemaVariable sv, java.lang.String value, Services services) Instantiates a schema variable in the given taclet application. 1st pass: only VariableSV.
static TacletApp	parseSV2(TacletApp app, SchemaVariable sv, java.lang.String value, Goal targetGoal) Instantiates a schema variable in the given taclet application. 2nd pass: All other schema variables.
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.
IntermediateProofReplayer.Result	replay() Starts the actual replay process.
private void	reportError(java.lang.String string, java.lang.Throwable e) Stores an error in the list.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ERROR_LOADING_PROOF_LINE

private static final java.lang.String ERROR_LOADING_PROOF_LINE

See Also:

Constant Field Values

NOT_APPLICABLE

private static final java.lang.String NOT_APPLICABLE

See Also:

Constant Field Values

loader

private final AbstractProblemLoader loader

The problem loader, for reporting errors

proof

private Proof proof

The proof object into which to load the replayed proof

errors

private java.util.List<java.lang.Throwable> errors

Encountered errors

status

private java.lang.String status

Error status

queue

private java.util.LinkedList<Pair<Node,NodeIntermediate>> queue

Stores open branches

joinPartnerNodes

private java.util.HashMap<java.lang.Integer,java.util.HashSet<Triple<Node,PosInOccurrence,NodeIntermediate>>> joinPartnerNodes

Maps join node IDs to previously seen join partners

currGoal

private Goal currGoal

The current open goal

Constructor Detail

IntermediateProofReplayer

public IntermediateProofReplayer(AbstractProblemLoader loader,
                                 Proof proof,
                                 IntermediatePresentationProofFileParser.Result parserResult)

Constructs a new IntermediateProofReplayer.

Parameters:

loader - The problem loader, for reporting errors.

proof - The proof object into which to load the replayed proof.

intermediate -

Method Detail

getLastSelectedGoal

public Goal getLastSelectedGoal()

Returns:

the lastSelectedGoal

replay

public IntermediateProofReplayer.Result replay()

Starts the actual replay process. Results are stored in the supplied proof object; the last selected goal may be obtained by getLastSelectedGoal().

addChildren

private void addChildren(java.util.Iterator<Node> children,
                         java.util.LinkedList<NodeIntermediate> intermChildren)

Adds the pairs of proof node children and intermediate children to the queue. At the moment, they are added in the order they were parsed. For the future, it may be sensible to choose a different procedure, for instance one that minimizes the number of open goals per time interval to save memory. Note that in this case, some test cases might be adapted which depend on fixed node serial numbers.

Parameters:

children - Iterator of proof node children.

intermChildren - List of corresponding intermediate children.

getStatus

public java.lang.String getStatus()

Communicates a non-fatal condition to the caller. Empty string means everything is OK. The message will be displayed to the user in the GUI after the proof has been parsed.

getErrors

public java.util.Collection<java.lang.Throwable> getErrors()

Returns:

errors encountered during replay.

constructTacletApp

private TacletApp constructTacletApp(TacletAppIntermediate currInterm,
                                     Goal currGoal)
                              throws IntermediateProofReplayer.TacletConstructionException

Constructs a taclet application from an intermediate one.

Parameters:

currInterm - The intermediate taclet application to create a "real" application for.

currGoal - The goal on which to apply the taclet app.

Returns:

The taclet application corresponding to the supplied intermediate representation.

Throws:

IntermediateProofReplayer.TacletConstructionException - In case of an error during construction.

constructBuiltinApp

private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm,
                                            Goal currGoal)
                                     throws IntermediateProofReplayer.SkipSMTRuleException,
                                            IntermediateProofReplayer.BuiltInConstructionException

Constructs a built-in rule application from an intermediate one.

Parameters:

currInterm - The intermediate built-in application to create a "real" application for.

currGoal - The goal on which to apply the built-in app.

Returns:

The built-in application corresponding to the supplied intermediate representation.

Throws:

IntermediateProofReplayer.SkipSMTRuleException - If the proof has been loaded, but the SMT solvers have not been run.

IntermediateProofReplayer.BuiltInConstructionException - In case of an error during construction.

instantiateJoinApp

private MergeRuleBuiltInRuleApp instantiateJoinApp(MergeAppIntermediate joinAppInterm,
                                                   Node currNode,
                                                   java.util.Set<Triple<Node,PosInOccurrence,NodeIntermediate>> partnerNodesInfo,
                                                   Services services)
                                            throws IntermediateProofReplayer.SkipSMTRuleException,
                                                   IntermediateProofReplayer.BuiltInConstructionException

Instantiates a Join Rule application.

Parameters:

joinAppInterm - Intermediate join app.

services - The services object.

currNode - The current proof node.

partnerNodesInfo - Information about join partner nodes.

currNode -

partnerNodesInfo -

Returns:

The instantiated Join Rule application.

Throws:

IntermediateProofReplayer.SkipSMTRuleException - If the proof has been loaded, but the SMT solvers have not been run.

IntermediateProofReplayer.BuiltInConstructionException - In case of an error during construction of the builtin rule app.

reportError

private void reportError(java.lang.String string,
                         java.lang.Throwable e)

Stores an error in the list.

Parameters:

string - Description text.

e - Error encountered.

collectAppsForRule

private static ImmutableSet<IBuiltInRuleApp> collectAppsForRule(java.lang.String ruleName,
                                                                Goal g,
                                                                PosInOccurrence pos)

Retrieves all registered applications at the given goal and position for the rule corresponding to the given ruleName.

Parameters:

ruleName - Name of the rule to find applications for.

g - Goal to search.

pos - Position of interest in the given goal.

Returns:

All matching rule applications at pos in g.

constructInsts

private static TacletApp constructInsts(TacletApp app,
                                        Goal currGoal,
                                        java.util.LinkedList<java.lang.String> loadedInsts,
                                        Services services)

Instantiates schema variables in the given taclet application.

Parameters:

app - The taclet application to instantiate.

currGoal - The corresponding goal.

loadedInsts - Loaded schema variable instantiations.

services - The services object.

Returns:

The instantiated taclet.

lookupName

private static SchemaVariable lookupName(ImmutableSet<SchemaVariable> set,
                                         java.lang.String name)

Finds a schema variable in the given set.

Parameters:

set - The set to search.

name - The name to search for.

Returns:

The found schema variable, or null if it is not present in the set.

parseTerm

public 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.

Parameters:

value - String to parse.

proof - Proof object (for namespaces and Services object).

varNS - Variable namespace.

progVarNS - Program variable namespace.

Returns:

The parsed term.

Throws:

ParserException - In case of an error.

parseTerm

public static Term parseTerm(java.lang.String value,
                             Proof proof)

Parses a given term in String representation.

Parameters:

value - String to parse.

proof - Proof object (for namespaces and Services object).

Returns:

The parsed term.

parseSV1

public static TacletApp parseSV1(TacletApp app,
                                 SchemaVariable sv,
                                 java.lang.String value,
                                 Services services)

Instantiates a schema variable in the given taclet application. 1st pass: only VariableSV.

Parameters:

app - Application to instantiate.

sv - Schema variable (VariableSV) to instantiate.

value - Name for the instantiated logic variable.

services - The services object.

Returns:

An instantiated taclet application, where the schema variable has been instantiated by a logic variable of the given name.

parseSV2

public static TacletApp parseSV2(TacletApp app,
                                 SchemaVariable sv,
                                 java.lang.String value,
                                 Goal targetGoal)

Instantiates a schema variable in the given taclet application. 2nd pass: All other schema variables.

Parameters:

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.

Returns:

An instantiated taclet application, where the schema variable has been instantiated, depending on its type, by a Skolem constant, program element, or term of the given name.

See Also:

parseSV1(TacletApp, SchemaVariable, String, Services)