Merge pull request #1531 from diffblue/smv_set_exprt

introduce `smv_set_exprt` and others

Author: tautschnig

src/smvlang/expr2smv.cpp

@@ -26,7 +26,7 @@ Function: expr2smvt::convert_smv_set
 
 \*******************************************************************/
 
-expr2smvt::resultt expr2smvt::convert_smv_set(const exprt &src)
+expr2smvt::resultt expr2smvt::convert_smv_set(const smv_set_exprt &src)
 {
   std::string dest = "{ ";
 
@@ -777,16 +777,16 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_binary(to_mod_expr(src), src.id_string(), precedencet::MULT);
 
   else if(src.id() == ID_smv_set)
-    return convert_smv_set(src);
+    return convert_smv_set(to_smv_set_expr(src));
 
   else if(src.id() == ID_smv_setin)
-    return convert_binary(to_binary_expr(src), "in", precedencet::IN);
+    return convert_binary(to_smv_setin_expr(src), "in", precedencet::IN);
 
   else if(src.id() == ID_smv_setnotin)
     return convert_binary(to_binary_expr(src), "notin", precedencet::IN);
 
   else if(src.id() == ID_smv_union)
-    return convert_binary(to_binary_expr(src), "union", precedencet::UNION);
+    return convert_binary(to_smv_union_expr(src), "union", precedencet::UNION);
 
   else if(src.id()==ID_lt || src.id()==ID_gt ||
           src.id()==ID_le || src.id()==ID_ge)
@@ -912,13 +912,7 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_constant(to_constant_expr(src));
 
   else if(src.id()==ID_nondet_bool)
-  {
-    exprt smv_set_expr(ID_smv_set);
-    smv_set_expr.operands().clear();
-    smv_set_expr.operands().push_back(false_exprt());
-    smv_set_expr.operands().push_back(true_exprt());
-    return convert_smv_set(smv_set_expr);
-  }
+    return convert_smv_set(smv_set_exprt{{false_exprt(), true_exprt()}});
 
   else if(src.id()==ID_cond)
     return convert_cond(src);

src/smvlang/expr2smv_class.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2smv.h"
 
+class smv_set_exprt;
+
 class expr2smvt
 {
 public:
@@ -86,7 +88,7 @@ class expr2smvt
 
   virtual resultt convert_rec(const exprt &);
 
-  resultt convert_smv_set(const exprt &);
+  resultt convert_smv_set(const smv_set_exprt &);
 
   resultt convert_binary(
     const binary_exprt &src,

src/smvlang/smv_expr.h

@@ -369,4 +369,80 @@ inline smv_identifier_exprt &to_smv_identifier_expr(exprt &expr)
   return static_cast<smv_identifier_exprt &>(expr);
 }
 
+/// set constructor expression
+class smv_set_exprt : public multi_ary_exprt
+{
+public:
+  explicit smv_set_exprt(exprt::operandst __elements)
+    : multi_ary_exprt{ID_smv_set, std::move(__elements), typet{ID_smv_set}}
+  {
+  }
+};
+
+inline const smv_set_exprt &to_smv_set_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_set);
+  smv_set_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const smv_set_exprt &>(expr);
+}
+
+inline smv_set_exprt &to_smv_set_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_set);
+  smv_set_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<smv_set_exprt &>(expr);
+}
+
+/// set union expression
+class smv_union_exprt : public binary_exprt
+{
+public:
+  smv_union_exprt(exprt lhs, exprt rhs, typet type)
+    : binary_exprt{
+        std::move(lhs),
+        ID_smv_union,
+        std::move(rhs),
+        std::move(type)}
+  {
+  }
+};
+
+inline const smv_union_exprt &to_smv_union_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_union);
+  smv_union_exprt::check(expr);
+  return static_cast<const smv_union_exprt &>(expr);
+}
+
+inline smv_union_exprt &to_smv_union_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_union);
+  smv_union_exprt::check(expr);
+  return static_cast<smv_union_exprt &>(expr);
+}
+
+/// set inclusion expression
+class smv_setin_exprt : public binary_predicate_exprt
+{
+public:
+  smv_setin_exprt(exprt lhs, exprt rhs)
+    : binary_predicate_exprt{std::move(lhs), ID_smv_setin, std::move(rhs)}
+  {
+  }
+};
+
+inline const smv_setin_exprt &to_smv_setin_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_setin);
+  smv_setin_exprt::check(expr);
+  return static_cast<const smv_setin_exprt &>(expr);
+}
+
+inline smv_setin_exprt &to_smv_setin_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_setin);
+  smv_setin_exprt::check(expr);
+  return static_cast<smv_setin_exprt &>(expr);
+}
+
 #endif // CPROVER_SMV_EXPR_H