Merge pull request #979 from diffblue/reduction-expression-classes

Verilog: classes for the reduction operator expressions

Author: tautschnig

src/verilog/expr2verilog.cpp

@@ -1670,27 +1670,27 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id()==ID_reduction_or)
     return convert_unary(
-      to_unary_expr(src), "|", precedence = verilog_precedencet::NOT);
+      to_reduction_or_expr(src), "|", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_reduction_and)
     return convert_unary(
-      to_unary_expr(src), "&", precedence = verilog_precedencet::NOT);
+      to_reduction_and_expr(src), "&", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_reduction_nor)
     return convert_unary(
-      to_unary_expr(src), "~|", precedence = verilog_precedencet::NOT);
+      to_reduction_nor_expr(src), "~|", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_reduction_nand)
     return convert_unary(
-      to_unary_expr(src), "~&", precedence = verilog_precedencet::NOT);
+      to_reduction_nand_expr(src), "~&", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_reduction_xor)
     return convert_unary(
-      to_unary_expr(src), "^", precedence = verilog_precedencet::NOT);
+      to_reduction_xor_expr(src), "^", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_reduction_xnor)
     return convert_unary(
-      to_unary_expr(src), "~^", precedence = verilog_precedencet::NOT);
+      to_reduction_xnor_expr(src), "~^", precedence = verilog_precedencet::NOT);
 
   else if(src.id()==ID_AG || src.id()==ID_EG ||
           src.id()==ID_AX || src.id()==ID_EX)

src/verilog/verilog_expr.h

@@ -3046,4 +3046,184 @@ inline verilog_package_scope_exprt &to_verilog_package_scope_expr(exprt &expr)
   return static_cast<verilog_package_scope_exprt &>(expr);
 }
 
+class reduction_and_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_and_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_and, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_and_exprt>(const exprt &expr)
+{
+  reduction_and_exprt::check(expr);
+  return expr.id() == ID_reduction_and;
+}
+
+inline const reduction_and_exprt &to_reduction_and_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_and);
+  reduction_and_exprt::check(expr);
+  return static_cast<const reduction_and_exprt &>(expr);
+}
+
+inline reduction_and_exprt &to_reduction_and_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_and);
+  reduction_and_exprt::check(expr);
+  return static_cast<reduction_and_exprt &>(expr);
+}
+
+class reduction_or_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_or_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_or, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_or_exprt>(const exprt &expr)
+{
+  reduction_or_exprt::check(expr);
+  return expr.id() == ID_reduction_or;
+}
+
+inline const reduction_or_exprt &to_reduction_or_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_or);
+  reduction_or_exprt::check(expr);
+  return static_cast<const reduction_or_exprt &>(expr);
+}
+
+inline reduction_or_exprt &to_reduction_or_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_or);
+  reduction_or_exprt::check(expr);
+  return static_cast<reduction_or_exprt &>(expr);
+}
+
+class reduction_nor_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_nor_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_nor, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_nor_exprt>(const exprt &expr)
+{
+  reduction_nor_exprt::check(expr);
+  return expr.id() == ID_reduction_nor;
+}
+
+inline const reduction_nor_exprt &to_reduction_nor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_nor);
+  reduction_nor_exprt::check(expr);
+  return static_cast<const reduction_nor_exprt &>(expr);
+}
+
+inline reduction_nor_exprt &to_reduction_nor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_nor);
+  reduction_nor_exprt::check(expr);
+  return static_cast<reduction_nor_exprt &>(expr);
+}
+
+class reduction_nand_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_nand_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_nand, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_nand_exprt>(const exprt &expr)
+{
+  reduction_nand_exprt::check(expr);
+  return expr.id() == ID_reduction_nand;
+}
+
+inline const reduction_nand_exprt &to_reduction_nand_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_nand);
+  reduction_nand_exprt::check(expr);
+  return static_cast<const reduction_nand_exprt &>(expr);
+}
+
+inline reduction_nand_exprt &to_reduction_nand_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_nand);
+  reduction_nand_exprt::check(expr);
+  return static_cast<reduction_nand_exprt &>(expr);
+}
+
+class reduction_xor_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_xor_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_xor, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_xor_exprt>(const exprt &expr)
+{
+  reduction_xor_exprt::check(expr);
+  return expr.id() == ID_reduction_xor;
+}
+
+inline const reduction_xor_exprt &to_reduction_xor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_xor);
+  reduction_xor_exprt::check(expr);
+  return static_cast<const reduction_xor_exprt &>(expr);
+}
+
+inline reduction_xor_exprt &to_reduction_xor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_xor);
+  reduction_xor_exprt::check(expr);
+  return static_cast<reduction_xor_exprt &>(expr);
+}
+
+class reduction_xnor_exprt : public unary_predicate_exprt
+{
+public:
+  explicit reduction_xnor_exprt(exprt _op)
+    : unary_predicate_exprt(ID_reduction_xnor, std::move(_op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<reduction_xnor_exprt>(const exprt &expr)
+{
+  reduction_xnor_exprt::check(expr);
+  return expr.id() == ID_reduction_xnor;
+}
+
+inline const reduction_xnor_exprt &to_reduction_xnor_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_xnor);
+  reduction_xnor_exprt::check(expr);
+  return static_cast<const reduction_xnor_exprt &>(expr);
+}
+
+inline reduction_xnor_exprt &to_reduction_xnor_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_reduction_xnor);
+  reduction_xnor_exprt::check(expr);
+  return static_cast<reduction_xnor_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_simplifier.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ebmc/ebmc_error.h>
 
+#include "verilog_expr.h"
 #include "verilog_types.h"
 
 static constant_exprt
@@ -76,44 +77,44 @@ static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
   if(expr.id() == ID_reduction_or)
   {
     // The simplifier doesn't know how to simplify reduction_or
-    auto &reduction_or = to_unary_expr(expr);
+    auto &reduction_or = to_reduction_or_expr(expr);
     expr = notequal_exprt(
       reduction_or.op(), from_integer(0, reduction_or.op().type()));
   }
   else if(expr.id() == ID_reduction_nor)
   {
     // The simplifier doesn't know how to simplify reduction_nor
-    auto &reduction_nor = to_unary_expr(expr);
+    auto &reduction_nor = to_reduction_nor_expr(expr);
     expr = equal_exprt(
       reduction_nor.op(), from_integer(0, reduction_nor.op().type()));
   }
   else if(expr.id() == ID_reduction_and)
   {
     // The simplifier doesn't know how to simplify reduction_and
-    auto &reduction_and = to_unary_expr(expr);
+    auto &reduction_and = to_reduction_and_expr(expr);
     expr =
       equal_exprt{reduction_and.op(), make_all_ones(reduction_and.op().type())};
   }
   else if(expr.id() == ID_reduction_nand)
   {
     // The simplifier doesn't know how to simplify reduction_nand
-    auto &reduction_nand = to_unary_expr(expr);
+    auto &reduction_nand = to_reduction_nand_expr(expr);
     expr = notequal_exprt{
       reduction_nand.op(), make_all_ones(reduction_nand.op().type())};
   }
   else if(expr.id() == ID_reduction_xor)
   {
     // The simplifier doesn't know how to simplify reduction_xor
     // Lower to countones.
-    auto &reduction_xor = to_unary_expr(expr);
+    auto &reduction_xor = to_reduction_xor_expr(expr);
     auto ones = countones(to_constant_expr(reduction_xor.op()), ns);
     expr = extractbit_exprt{ones, from_integer(0, natural_typet{})};
   }
   else if(expr.id() == ID_reduction_xnor)
   {
     // The simplifier doesn't know how to simplify reduction_xnor
     // Lower to countones.
-    auto &reduction_xnor = to_unary_expr(expr);
+    auto &reduction_xnor = to_reduction_xnor_expr(expr);
     auto ones = countones(to_constant_expr(reduction_xnor.op()), ns);
     expr = not_exprt{extractbit_exprt{ones, from_integer(0, natural_typet{})}};
   }