SMV: set type

NuSMV 2.7 distinguishes four set types; this introduces a class for these.

Author: kroening

src/smvlang/smv_typecheck.cpp

@@ -1533,6 +1533,16 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode, bool next)
     for(auto &op : expr.operands())
       typecheck_expr_rec(op, mode, next);
   }
+  else if(expr.id() == ID_smv_union)
+  {
+    auto &lhs = to_binary_expr(expr).lhs();
+    auto &rhs = to_binary_expr(expr).rhs();
+
+    typecheck_expr_rec(lhs, mode, next);
+    typecheck_expr_rec(rhs, mode, next);
+
+    expr.type() = smv_set_typet{smv_enumeration_typet{}};
+  }
   else
   {
     throw errort().with_location(expr.find_source_location())
@@ -1959,8 +1969,7 @@ void smv_typecheckt::convert(exprt &expr)
     throw errort().with_location(expr.source_location())
       << "no support for self";
   }
-  else if(expr.id()=="smv_nondet_choice" ||
-          expr.id()=="smv_union")
+  else if(expr.id() == "smv_nondet_choice")
   {
     if(expr.operands().size()==0)
     {

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
 {