CORAL: a modern C++ library for the manipulation of Boolean functions

The purpose of this work is to describe the CORAL library, which provides an efficient implementation of Boolean functions; it has been known for a long time that almost all of the interesting computations on Boolean functions, such as the satisfiability problem, are NP-hard, so this is not an easy task. The library was originally designed to be used by the China analyzer, in particular in the context of the groundness analysis problem of CLP languages, for which high performance operations on very large Boolean functions are needed (the internal representation of the functions involved can reach a size in the order of megabytes). However, we are confident that the library can and will be used succesfully in other areas of application, and we will not discuss particular applications in this work. In order to perform operations on Boolean functions we need a way to represent them: CORAL utilizes reduced ordered binary decision diagrams (ROBDDs), which means that the most important part of this work will deal with their properties and the algorithms used to manipulate them. We also describe how CORAL supports alternative, mixed representations to optimize efficiency and memory occupation in contexts where entailed, disentailed and/or equivalent variables are frequent.