In this paper we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as databasestyle relations and operations on relations, and provides static type rules to ensure that relational operations are used correctly. The paper provides a description of the Jedd language and reports on the design and implementation of the Jedd translator and associated runtime system. Of particular interest is the approach to assigning attributes from the high-level relations to physical domains in the underlying BDDs, which is done by expressing the constraints as a SAT problem and using a modern SAT solver to compute the solution. Further, a runtime system is defined that handles memory management issues and supports a browsable profiling tool for tuning the key BDD operations. The motivation for designing Jedd was to support the development of whole program analyses based on BDDs, and we have us...
Ondrej Lhoták, Laurie J. Hendren