Problem in proof writing

[AFellner]

some proofs produce heap space errors when being written to a file

[ceilican]

Which proofs? After being processed by which algorithms?

[AFellner]

I've written a comment to the mailing list - would it've been better off here?

[ceilican]

Yes. It is better to try to keep the issues in the issue tracker self-contained... But if something needs a long discussion, it is ok to discuss in the mailing-list.

[ceilican]

The problem happens in my laptop too:

> compress -d examples/proofs/VeriT/ -a RPI prp-2-17.smt2 -f smt2
[info] Running at.logic.skeptik.ProofCompressionCLI -d examples/proofs/VeriT/ -a RPI prp-2-17.smt2 -f smt2
[error] Picked up JAVA_TOOL_OPTIONS: -Dfile.encoding=UTF-8 -Xmx512m -XX:MaxPermSize=256m
[info] 
[info] Reading and checking proof 'examples/proofs/VeriT/prp-2-17.smt2' ... (completed in 911ms)
[info] Measuring... (completed in 22ms)
[info] 
[info]      Compressing with algorithm: RPI... (completed in 110ms)
[error] java.lang.OutOfMemoryError: Java heap space
[error]     at java.util.Arrays.copyOf(Arrays.java:2882)
[error]     at java.lang.AbstractStringBuilder.expandCapacity(AbstractStringBuilder.java:100)
[error]     at java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:390)
[error]     at java.lang.StringBuilder.append(StringBuilder.java:119)
[error]     at scala.collection.mutable.StringBuilder.append(StringBuilder.scala:197)
[error]     at at.logic.skeptik.expression.App.toString(expressions.scala:52)
[error]     at java.lang.String.valueOf(String.java:2826)
[error]     at scala.collection.mutable.StringBuilder.append(StringBuilder.scala:197)
[error]     at scala.collection.TraversableOnce$$anonfun$addString$1.apply(TraversableOnce.scala:327)
[error]     at scala.collection.immutable.List.foreach(List.scala:318)
[error]     at scala.collection.TraversableOnce$class.addString(TraversableOnce.scala:320)
[error]     at scala.collection.AbstractTraversable.addString(Traversable.scala:105)
[error]     at scala.collection.TraversableOnce$class.mkString(TraversableOnce.scala:286)
[error]     at scala.collection.AbstractTraversable.mkString(Traversable.scala:105)
[error]     at scala.collection.TraversableOnce$class.mkString(TraversableOnce.scala:288)
[error]     at scala.collection.AbstractTraversable.mkString(Traversable.scala:105)
[error]     at at.logic.skeptik.expression.App.toString(expressions.scala:52)
[error]     at java.lang.String.valueOf(String.java:2826)
[error]     at scala.collection.mutable.StringBuilder.append(StringBuilder.scala:197)
[error]     at scala.collection.TraversableOnce$$anonfun$addString$1.apply(TraversableOnce.scala:327)
[error]     at scala.collection.immutable.List.foreach(List.scala:318)
[error]     at scala.collection.TraversableOnce$class.addString(TraversableOnce.scala:320)
[error]     at scala.collection.AbstractTraversable.addString(Traversable.scala:105)
[error]     at scala.collection.TraversableOnce$class.mkString(TraversableOnce.scala:286)
[error]     at scala.collection.AbstractTraversable.mkString(Traversable.scala:105)
[error]     at scala.collection.TraversableOnce$class.mkString(TraversableOnce.scala:288)
[error]     at scala.collection.AbstractTraversable.mkString(Traversable.scala:105)
[error]     at at.logic.skeptik.expression.App.toString(expressions.scala:52)
[error]     at java.lang.String.valueOf(String.java:2826)
[error]     at scala.collection.mutable.StringBuilder.append(StringBuilder.scala:197)
[error]     at scala.collection.TraversableOnce$$anonfun$addString$1.apply(TraversableOnce.scala:327)
[error]     at scala.collection.immutable.List.foreach(List.scala:318)
[info]      Writing compressed proof...
java.lang.RuntimeException: Nonzero exit code returned from runner: 1
    at scala.sys.package$.error(package.scala:27)
[trace] Stack trace suppressed: run last *:compress for the full output.
[error] (*:compress) Nonzero exit code returned from runner: 1
[error] Total time: 20 s, completed Aug 6, 2013 10:52:34 AM

[ceilican]

Is this the smallest proof for which this problem occurs for you, Andreas?

[AFellner]

I had a small list of possibly bad proofs. This is just one - I will try the other ones and see which one is the smallest

[ceilican]

Just send me the smallest file (in kiloBytes)...

[ceilican]

I think I have identified the problem. This proof contains an expression that is so big that the heap space is exhausted while this formula is converted to a string.

Formulas are represented as DAGs in the memory, but our naive toString method expands the DAGs to trees. The string representation of the tree expansion of the expression is too big for the heap.

We need a less naive way to output expressions to files. Among other things, it should name and reuse subexpressions, as is already done by VeriT in the proofs it provides to us.

I will think more about how to solve this issue elegantly.