Built-in support for Abstract Data Types in the Σ Decision Diagram framework
Edmundo López Bóbeda · Archive ouverte UNIGE (University of Geneva) · 2010
Encoding and rewriting of large sets of terms is very useful in different do- mains such as model checking and theorem proving. Σ Decision Diagrams (ΣDD) have been developed to encode and rewrite large sets of terms in efficient manner, both in terms of space and memory. ΣDD encode terms in a symbolic and canonical way to ensure the sharing of redundant terms and subterms and also to be able to apply rewriting rules. In certain cases however the computer's built-in implementation might be faster than the symbolic approach. In this thesis we first extend the ΣDDs definition in or- der to support built-in types. Afterwards we extend the ΣDDs set operations to handle the extended ΣDD. Then, we modify the rewriting mechanism in order to perform built-in operations on the extended ΣDD by bypassing the normal mechanism and using the computer built-in mechanisms. Finally, we show that the new approach is much faster than the previous one in almost all different cases.