Heap2Array takes inputs in SMT-LIB v2.6 that contain heap theory declarations and operations, and encodes them using the theory of arrays.
Heap2Array depends on Princess: http://www.philipp.ruemmer.org/princess.shtml Its lineariser is a slight modification of Princess SMTLineariser.
You can either download a binary release of Heap2Array, or compile the Scala
code yourself. Since Eldarica uses sbt, compilation is quite
simple: you just need sbt installed on your machine,
and then type sbt assembly to download the compiler, all
required libraries, and produce a binary of Heap2Array.
After compilation (or downloading a binary release), calling Heap2Array is normally as easy as saying
./heap2array input.smt2
When using a binary release, one can instead also call
java -jar target/scala-2.*/heap2array-assembly*.jar input.smt2
A full list of options can be obtained by calling ./heap2array
.
If more than one input file is passed along with a single output file name, the specified output file name will be prefixed with an index for each input.
- An extended abstract introducing the theory of heap: "Towards an SMT-LIB Theory of Heap" https://arxiv.org/html/2008.02483v1/#EPTCS320.12