Skip to content

zafer-esen/heap2array

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

16 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Heap2Array

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:https://www.philipp.ruemmer.org/princess.shtml Its lineariser is a slight modification of Princess SMTLineariser.

Documentation

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.

Papers

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published