SMV: set type

src/smvlang/smv_types.h

@@ -72,6 +72,42 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
   return static_cast<smv_enumeration_typet &>(type);
 }
 
+/// The SMV set type -- NuSMV distinguishes the boolean set, the integer set,
+/// the symbolic set, and the integers-and-symbolic set.
+class smv_set_typet : public type_with_subtypet
+{
+public:
+  explicit smv_set_typet(typet subtype)
+    : type_with_subtypet(ID_smv_set, std::move(subtype))
+  {
+  }
+};
+
+/*! \brief Cast a generic typet to a \ref smv_set_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * smv_set_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref smv_set_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const smv_set_typet &to_smv_set_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_set);
+  return static_cast<const smv_set_typet &>(type);
+}
+
+/*! \copydoc to_smv_set_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline smv_set_typet &to_smv_set_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_set);
+  return static_cast<smv_set_typet &>(type);
+}
+
 /// The type used for VAR declarations that are in fact module instantiations
 class smv_module_instance_typet : public typet
 {