Maude-help mailing list

[Alban Linard <Alban.Linard AT unige.ch>]

Hello,

In the SMV group (see signature), people think that Decision Diagram  
operations can be viewed as term rewriting, so i plan to try  
implementing a DD library in Maude.

But Decision Diagrams heavily rely on unique representation of their  
representation. If a DD is encoded as a term, can Maude check equality  
between two DDs/terms in constant time ? Is there a mechanism like  
hash-consing/flyweight/unicity-table for Maude terms ?

If it does not exist, is there a way to avoid deep comparison of two  
terms ?
Do you know other similar projects ?

Moreover, is there an easy way to implement the operation cache ? Or  
should it be given explicitly together with the operations' terms ?

Thanks,

Alban Linard,
Software Modeling and Verification Group,
University of Geneva