Hardly readable sequent

[JonasKlamroth]

some sequents are really hard to read and get prettyprinted super bad (see attached picture)

[mattulbrich]

Yes, looks rather complicated. How can the representation be simplified?

Is this a matter of the pretty printing (e.g., bad line breaks, spaces) or is this a problem with term representtation (e.g. is o.f@heap sensible)?

[JonasKlamroth]

i think its a combination. looking at the picture above i think that if this sequent is pretty printed reasonably (e.g. line breaks) this would help a great deal in understanding. On the other hand i think that these kind of "nested" references to different heaps is a bad idea in general i would prefer to have either speaking names for certain heaps (e.g. preHeap, postHead,...) or some kind of SSA like variable handling where instead of writing x@heap1 == x@heap2 its possible to display something like x1 == x2

[mattulbrich]

Is colour-coding an option?

Have you tried using the SSA sequenter? That should do something of the kind ...

[JonasKlamroth]

using the ssa sequenter i get the following exception:

java.lang.NullPointerException
at edu.kit.iti.algover.term.builder.SSASequenter.createNextFunctionSymbol(SSASequenter.java:178)
at edu.kit.iti.algover.term.builder.SSASequenter.createMapping(SSASequenter.java:133)
at edu.kit.iti.algover.term.builder.SSASequenter.translate(SSASequenter.java:65)
at edu.kit.iti.algover.proof.MethodPVCBuilder.ensureSequentExists(MethodPVCBuilder.java:157)
at edu.kit.iti.algover.proof.MethodPVCBuilder.getSequent(MethodPVCBuilder.java:166)
at edu.kit.iti.algover.proof.PVC.(PVC.java:96)
at edu.kit.iti.algover.proof.MethodPVCBuilder.build(MethodPVCBuilder.java:89)
at edu.kit.iti.algover.dafnystructures.DafnyDeclPVCCollector.visitMethod(DafnyDeclPVCCollector.java:69)
at edu.kit.iti.algover.dafnystructures.DafnyDeclPVCCollector.visitClass(DafnyDeclPVCCollector.java:48)
at edu.kit.iti.algover.dafnystructures.DafnyDeclPVCCollector.visitFile(DafnyDeclPVCCollector.java:119)
at edu.kit.iti.algover.project.Project.ensurePVCsExist(Project.java:302)
at edu.kit.iti.algover.project.Project.getPVCByNameMap(Project.java:321)
at edu.kit.iti.algover.project.DafnyProjectManager.generateAllProofObjects(DafnyProjectManager.java:93)
at edu.kit.iti.algover.project.DafnyProjectManager.reload(DafnyProjectManager.java:77)
at edu.kit.iti.algover.MainController$2.call(MainController.java:396)
at edu.kit.iti.algover.MainController$2.call(MainController.java:393)
at javafx.concurrent.Task$TaskCallable.call(Task.java:1423)
at java.util.concurrent.FutureTask.run(FutureTask.java:266)
at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
at java.lang.Thread.run(Thread.java:748)

so thats not an option.

Concerning colour-coding: I dont see how this would be sufficient but im happy to get convinced by the contrary

[mattulbrich]

That's obviously not as intended. On which input?

[JonasKlamroth]

the stack example currently checked in on the vstte branch

[mattulbrich]

I cannot reproduce this fault on d58a65f.

[JonasKlamroth]

checkout 56e6249 and open the stackexample to reproduce

[mattulbrich]

OK. I repaired the SSA sequenter and it parses your example (from vsste) now.
Don't know if it is correct, however.

Have a look!