diff --git a/src/main/scala/ap/theories/arrays/SetTheory.scala b/src/main/scala/ap/theories/arrays/SetTheory.scala index 383c7261..e788eefc 100644 --- a/src/main/scala/ap/theories/arrays/SetTheory.scala +++ b/src/main/scala/ap/theories/arrays/SetTheory.scala @@ -75,6 +75,21 @@ object SetTheory { instances.getOrElseUpdate(elSort, new SetTheory(elSort)) } + /** + * Extractor for set sorts of any base type. + */ + object Sort { + def unapply(s : Sort) : Option[Sort] = s match { + case ps : Theory.TheorySort => + ps.theory match { + case ss : SetTheory => Some(ss.elementSort) + case _ => None + } + case _ => + None + } + } + } /** @@ -95,6 +110,8 @@ class SetTheory(val elementSort : Sort) import IExpression._ val theory = SetTheory.this + override val name: String = s"Set[${elementSort.name}]" + // TODO: implement further methods. In particular, we have to translate // back array terms to set terms, similar to how it is done in // ArraySeqTheory