SMV: union operator

The SMV union operator computes the union of two set expressions.

Author: kroening

regression/smv/expressions/smv_union2.desc

@@ -1,11 +1,10 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_union2.smv
 
-^\[spec1\] x != 3: PROVED \(CT=1\)$
+^\[spec1\] x != 3: PROVED \(CT=0\)$
 ^\[spec2\] x != 2: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The type checker rejects this.

regression/smv/range-type/range_type3.smv

@@ -6,6 +6,7 @@ INIT x=0
 
 DEFINE n:=0 union 1;
 
+-- assignment RHS is a set
 ASSIGN next(x):=n;
 
 SPEC AG x=0

src/smvlang/smv_typecheck.cpp

@@ -950,6 +950,37 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     // only get added by type checker
     PRECONDITION(false);
   }
+  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);
+    typecheck_expr_rec(rhs, mode);
+
+    // create smv_set expression
+    exprt::operandst elements;
+
+    if(lhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), lhs.operands().begin(), lhs.operands().end());
+    }
+    else
+      elements.push_back(lhs);
+
+    if(rhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), rhs.operands().begin(), rhs.operands().end());
+    }
+    else
+      elements.push_back(rhs);
+
+    expr.id(ID_smv_set);
+    expr.operands() = std::move(elements);
+    expr.type() = smv_set_typet{smv_enumeration_typet{}};
+  }
   else if(expr.id() == ID_smv_setin)
   {
     auto &lhs = to_binary_expr(expr).lhs();
@@ -1319,7 +1350,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
   else if(expr.id() == ID_smv_set)
   {
     // a set literal
-    expr.type() = typet{ID_smv_set};
+    expr.type() = smv_set_typet{smv_enumeration_typet{}};
 
     for(auto &op : expr.operands())
       typecheck_expr_rec(op, mode);
@@ -1719,23 +1750,6 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
         expr.id(ID_next_symbol);
     }
   }
-  else if(expr.id()=="smv_nondet_choice" ||
-          expr.id()=="smv_union")
-  {
-    if(expr.operands().size()==0)
-    {
-      throw errort().with_location(expr.find_source_location())
-        << "expected operand here";
-    }
-
-    std::string identifier=
-      module+"::var::"+std::to_string(nondet_count++);
-
-    expr.set(ID_identifier, identifier);
-    expr.set("#smv_nondet_choice", true);
-
-    expr.id(ID_constraint_select_one);
-  }
   else if(expr.id()=="smv_cases") // cases
   {
     if(expr.operands().size()<1)

src/smvlang/smv_types.h

@@ -71,4 +71,43 @@ 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))
+  {
+  }
+};
+
+/// compute the union of the given set types
+smv_set_typet type_union(const smv_set_typet &, const smv_set_typet &);
+
+/*! \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);
+}
+
 #endif // CPROVER_SMV_TYPES_H