Built-in support for Abstract Data Types in the Σ Decision Diagram framework

Defense date2010

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.

  • ∑DD
  • Decision diagram
  • Term rewriting
  • Symbolic techniques
  • Set of terms
Citation (ISO format)
LOPEZ BOBEDA, Edmundo. Built-in support for Abstract Data Types in the Σ Decision Diagram framework. 2010.
Main files (1)
Master thesis
  • PID : unige:15811

Technical informations

Creation12/14/2010 5:28:00 PM
First validation12/14/2010 5:28:00 PM
Update time03/14/2023 4:51:34 PM
Status update03/14/2023 4:51:34 PM
Last indexation01/29/2024 7:09:55 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack