Sigma Decision Diagrams

Encoding and rewriting of large set of terms is very useful in a number of domains, such as model checking and theorem proving. The challenge of encoding and normalizing several billions of terms requires efficient ways of representing and manipulating them. Term Graph Rewriting is a well-known technique to share common sub-terms and thus to save both memory and processing time. However, this does not always fit well to the operational framework since it destroys the original structure and replaces it by a new one. This paper introduces a new kind of Decision Diagrams (DD), especially designed to handle set of terms in an efficient way. Based on the Set Decision Diagrams(SDD), an evolution of the well-known Binary Decision Diagrams(BDD), we propose the Sigma Decision Diagrams (ΣDD), a new approach to perform Term Rewriting on a set of terms in order to compute the image of that set efficiently