[YICES-HELP] Represent a set

[Paulo J. Matos]

Hi all,

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
Webpage: http://www.personal.soton.ac.uk/pocm