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
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.
|
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 and Description |
---|
IntermediateProofReplayer(AbstractProblemLoader loader,
Proof proof,
IntermediatePresentationProofFileParser.Result parserResult)
Constructs a new
IntermediateProofReplayer . |
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.
|
private static final java.lang.String ERROR_LOADING_PROOF_LINE
private static final java.lang.String NOT_APPLICABLE
private final AbstractProblemLoader loader
private Proof proof
private java.util.List<java.lang.Throwable> errors
private java.lang.String status
private java.util.LinkedList<Pair<Node,NodeIntermediate>> queue
private java.util.HashMap<java.lang.Integer,java.util.HashSet<Triple<Node,PosInOccurrence,NodeIntermediate>>> joinPartnerNodes
private Goal currGoal
public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, 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 IntermediateProofReplayer.Result replay()
getLastSelectedGoal()
.private void addChildren(java.util.Iterator<Node> children, java.util.LinkedList<NodeIntermediate> intermChildren)
children
- Iterator of proof node children.intermChildren
- List of corresponding intermediate children.public java.lang.String getStatus()
public java.util.Collection<java.lang.Throwable> getErrors()
private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal currGoal) throws IntermediateProofReplayer.TacletConstructionException
currInterm
- The intermediate taclet application to create a "real"
application for.currGoal
- The goal on which to apply the taclet app.IntermediateProofReplayer.TacletConstructionException
- In case of an error during construction.private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, Goal currGoal) throws IntermediateProofReplayer.SkipSMTRuleException, IntermediateProofReplayer.BuiltInConstructionException
currInterm
- The intermediate built-in application to create a "real"
application for.currGoal
- The goal on which to apply the built-in app.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.private MergeRuleBuiltInRuleApp instantiateJoinApp(MergeAppIntermediate joinAppInterm, Node currNode, java.util.Set<Triple<Node,PosInOccurrence,NodeIntermediate>> partnerNodesInfo, Services services) throws IntermediateProofReplayer.SkipSMTRuleException, IntermediateProofReplayer.BuiltInConstructionException
joinAppInterm
- Intermediate join app.services
- The services object.currNode
- The current proof node.partnerNodesInfo
- Information about join partner nodes.currNode
- partnerNodesInfo
- 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.private void reportError(java.lang.String string, java.lang.Throwable e)
string
- Description text.e
- Error encountered.private static ImmutableSet<IBuiltInRuleApp> collectAppsForRule(java.lang.String ruleName, Goal g, PosInOccurrence pos)
ruleName
- Name of the rule to find applications for.g
- Goal to search.pos
- Position of interest in the given goal.private static TacletApp constructInsts(TacletApp app, Goal currGoal, java.util.LinkedList<java.lang.String> loadedInsts, Services services)
app
- The taclet application to instantiate.currGoal
- The corresponding goal.loadedInsts
- Loaded schema variable instantiations.services
- The services object.private static SchemaVariable lookupName(ImmutableSet<SchemaVariable> set, java.lang.String name)
set
- The set to search.name
- The name to search for.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)