[YICES-HELP] Represent a set
Paulo J. Matos
pocmatos at gmail.com
Thu Nov 27 09:07:16 PST 2008
I would like to represent a datatype set in Yices, however, I don't
really know what's the best way to approach this.
Yices seems to supports lots of datatypes but I can't see the best way
to extend any of them to represent sets. For example if I chose arrays
(which I think yices support), how would I assure that no element is
added twice, since in a set there are no duplicated elements?
And by the way, would it be possible for a set to contain itself another set?
Paulo Jorge Matos - pocmatos at gmail.com
More information about the YICES-HELP