public class OutputStreamProofSaver
extends java.lang.Object
OutputStream
.Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
internalVersion |
(package private) LogicPrinter |
printer |
protected Proof |
proof |
Constructor and Description |
---|
OutputStreamProofSaver(Proof proof) |
OutputStreamProofSaver(Proof proof,
java.lang.String internalVersion) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
private void |
collectProof(Node node,
java.lang.String prefix,
java.lang.Appendable output)
Print applied rule(s) for a proof node and its decendants into the passed writer.
|
private static LogicPrinter |
createLogicPrinter(Services serv,
boolean shortAttrNotation) |
static java.lang.String |
escapeCharacters(java.lang.String toEscape)
double escapes quotation marks and backslashes to be storeable in a text
file
|
protected java.lang.String |
getBasePath() |
java.lang.String |
getInteresting(SVInstantiations inst) |
static java.io.File |
getJavaSourceLocation(Proof proof)
Extracts java source directory from
Proof.header() , if it exists. |
java.lang.String |
ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
private java.lang.String |
makePathsRelative(java.lang.String header)
Searches in the header for absolute paths to Java files and tries to
replace them by paths relative to the proof file to be saved.
|
private java.lang.String |
newNames2Proof(Node n) |
void |
node2Proof(Node node,
java.lang.Appendable ps)
Print applied rule(s) for a proof node and its decendants into the passed writer
such that in can be loaded again as a proof.
|
static java.lang.String |
posInOccurrence2Proof(Sequent seq,
PosInOccurrence pos) |
static java.lang.String |
posInTerm2Proof(PosInTerm pos) |
static java.lang.String |
printAnything(java.lang.Object val,
Services services) |
static java.lang.StringBuffer |
printAnything(java.lang.Object val,
Services services,
boolean shortAttrNotation) |
private void |
printLatticeAbstractionForSingleMergeRuleApp(MergeWithLatticeAbstraction concreteRule,
java.lang.Appendable output)
Print predicates for applied merge rule application into the passed writer.
|
private void |
printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction predAbstrRule,
java.lang.Appendable output)
Print predicates for applied merge rule application into the passed writer.
|
static java.lang.StringBuffer |
printProgramElement(ProgramElement pe) |
private void |
printRuleJustification(IBuiltInRuleApp appliedRuleApp,
java.lang.Appendable output)
Print rule justification for applied built-in rule application into the passed writer.
|
private static java.lang.StringBuffer |
printSequent(Sequent val,
Services services) |
private void |
printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp,
Node node,
java.lang.String prefix,
java.lang.Appendable output)
Print applied built-in rule for a single built-in rule application into the passed writer.
|
private void |
printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp closeApp,
Node node,
java.lang.String prefix,
java.lang.Appendable output) |
private void |
printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp,
Node node,
java.lang.String prefix,
java.lang.Appendable output)
Print applied merge rule for a single merge rule application into the passed writer.
|
private void |
printSingleNode(Node node,
java.lang.String prefix,
java.lang.Appendable output)
Print applied rule (s) for a single proof node into the passed writer.
|
private void |
printSingleTacletApp(TacletApp appliedRuleApp,
Node node,
java.lang.String prefix,
java.lang.Appendable output)
Print applied taclet rule for a single taclet rule application into the passed writer.
|
static java.lang.StringBuffer |
printTerm(Term t,
Services serv) |
static java.lang.StringBuffer |
printTerm(Term t,
Services serv,
boolean shortAttrNotation) |
void |
save(java.io.OutputStream out) |
private static java.lang.String |
tryToMakeFilenameRelative(java.lang.String absPath,
java.lang.String basePath)
Try to create a relative path, but return the absolute path if a relative
path cannot be found.
|
private void |
userInteraction2Proof(Node node,
java.lang.Appendable output)
Check whether the applied rule of the passed proof node was performed interactively.
|
java.lang.StringBuffer |
writeLog()
Write the log information of the proof including the KeY version and the user name.
|
java.lang.String |
writeProfile(Profile profile) |
java.lang.String |
writeSettings(ProofSettings ps) |
protected final Proof proof
protected final java.lang.String internalVersion
LogicPrinter printer
public OutputStreamProofSaver(Proof proof)
public OutputStreamProofSaver(Proof proof, java.lang.String internalVersion)
public static java.io.File getJavaSourceLocation(Proof proof)
Proof.header()
, if it exists.proof
- the Proofpublic java.lang.StringBuffer writeLog()
public java.lang.String writeProfile(Profile profile)
public java.lang.String writeSettings(ProofSettings ps)
public void save(java.io.OutputStream out) throws java.io.IOException
java.io.IOException
protected java.lang.String getBasePath() throws java.io.IOException
java.io.IOException
private java.lang.String makePathsRelative(java.lang.String header)
private static java.lang.String tryToMakeFilenameRelative(java.lang.String absPath, java.lang.String basePath)
private java.lang.String newNames2Proof(Node n)
private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
appliedRuleApp
- the rule application to be printedprefix
- a string which the printed rule is concatenated tooutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction predAbstrRule, java.lang.Appendable output) throws java.io.IOException
predAbstrRule
- the rule application with the predicates to be printedoutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printLatticeAbstractionForSingleMergeRuleApp(MergeWithLatticeAbstraction concreteRule, java.lang.Appendable output) throws java.io.IOException
concreteRule
- the rule application with the abstract domain to be printedoutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
mergeApp
- the rule application to be printedprefix
- a string which the printed rule is concatenated tooutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp closeApp, Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
java.io.IOException
private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, java.lang.Appendable output) throws java.io.IOException
appliedRuleApp
- the rule application to be printedoutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
appliedRuleApp
- the rule application to be printedprefix
- a string which the printed rule is concatenated tooutput
- the writer in which the rule is printedjava.io.IOException
- an exception thrown when printing failsprivate void printSingleNode(Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
node
- the proof node to be printedprefix
- a string which the printed rules are concatenated tooutput
- the writer in which the rule(s) is /are printedjava.io.IOException
- an exception thrown when printing failsprivate void collectProof(Node node, java.lang.String prefix, java.lang.Appendable output) throws java.io.IOException
node
- the proof node from which to be printedprefix
- a string which the printed rules are concatenated tooutput
- the writer in which the rule(s) is/are printedjava.io.IOException
- an exception thrown when printing failsprivate void userInteraction2Proof(Node node, java.lang.Appendable output) throws java.io.IOException
node
- the proof node to be checkedoutput
- the writer to which the label is appendedjava.io.IOException
- an exception thrown when printing failspublic void node2Proof(Node node, java.lang.Appendable ps) throws java.io.IOException
node
- the proof node from which to be printedps
- the writer in which the rule(s) is/are printedjava.io.IOException
- an exception thrown when printing failspublic static java.lang.String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos)
public static java.lang.String posInTerm2Proof(PosInTerm pos)
public java.lang.String getInteresting(SVInstantiations inst)
public java.lang.String ifFormulaInsts(Node node, ImmutableList<IfFormulaInstantiation> l)
public java.lang.String builtinRuleIfInsts(Node node, ImmutableList<PosInOccurrence> ifInsts)
public static java.lang.String escapeCharacters(java.lang.String toEscape)
toEscape
- the String to double escapepublic static java.lang.StringBuffer printProgramElement(ProgramElement pe)
public static java.lang.StringBuffer printTerm(Term t, Services serv, boolean shortAttrNotation)
public static java.lang.String printAnything(java.lang.Object val, Services services)
public static java.lang.StringBuffer printAnything(java.lang.Object val, Services services, boolean shortAttrNotation)
private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation)