introduce reduction_*_exprt classes

src/solvers/smt2/smt2_conv.cpp

@@ -2736,34 +2736,34 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id() == ID_reduction_and)
   {
     // This is true iff all bits in the operand are true
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_reduction_and_expr(expr).op();
     auto all_ones = to_bitvector_type(op.type()).all_ones_expr();
     convert_expr(equal_exprt{op, all_ones});
   }
   else if(expr.id() == ID_reduction_nand)
   {
     // This is the negation of "reduction and"
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_reduction_nand_expr(expr).op();
     convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_and, op}});
   }
   else if(expr.id() == ID_reduction_or)
   {
     // This is true iff the operand is not zero
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_reduction_or_expr(expr).op();
     auto all_zeros = to_bitvector_type(op.type()).all_zeros_expr();
     convert_expr(notequal_exprt{op, all_zeros});
   }
   else if(expr.id() == ID_reduction_nor)
   {
     // This is the negation of "reduction or"
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_reduction_nor_expr(expr).op();
     convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_or, op}});
   }
   else if(expr.id() == ID_reduction_xor)
   {
     // This is the parity of the operand. No SMT-LIB 2 equivalent.
     // Do bit-wise. SMT-LIB 3.0 could do this with "fold bvxor".
-    auto &op = to_unary_expr(expr).op();
+    auto &op = to_reduction_xor_expr(expr).op();
     auto width = to_bitvector_type(op.type()).get_width();
     PRECONDITION(width >= 1);
 
@@ -2791,8 +2791,8 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id() == ID_reduction_xnor)
   {
     // This is the negation of "reduction xor"
-    auto &op = to_unary_expr(expr).op();
-    convert_expr(not_exprt{unary_predicate_exprt{ID_reduction_xor, op}});
+    auto &op = to_reduction_xnor_expr(expr).op();
+    convert_expr(not_exprt{reduction_xor_exprt{op}});
   }
   else
     INVARIANT_WITH_DIAGNOSTICS(

src/util/bitvector_expr.h

@@ -1970,4 +1970,190 @@ inline onehot0_exprt &to_onehot0_expr(exprt &expr)
   return static_cast<onehot0_exprt &>(expr);
 }
 
+/// the logical 'and' of all bits in the operand
+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);
+}
+
+/// the logical 'or' of all bits in the operand
+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);
+}
+
+/// the negation of reduction_or_exprt
+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);
+}
+
+/// the negation of reduction_and_exprt
+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);
+}
+
+/// the logical 'xor' of all bits in the operand
+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);
+}
+
+/// the negation of reduction_xor_exprt
+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 // CPROVER_UTIL_BITVECTOR_EXPR_H

unit/solvers/smt2/smt2_conv.cpp

@@ -53,70 +53,63 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]")
 
   SECTION("reduction_and")
   {
-    REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_and, sym}) ==
-      "(assert (= x (_ bv3 2)))");
+    REQUIRE(get_assert(reduction_and_exprt{sym}) == "(assert (= x (_ bv3 2)))");
   }
 
   SECTION("reduction_nand")
   {
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_nand, sym}) ==
+      get_assert(reduction_nand_exprt{sym}) ==
       "(assert (not (= x (_ bv3 2))))");
   }
 
   SECTION("reduction_or")
   {
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_or, sym}) ==
-      "(assert (not (= x (_ bv0 2))))");
+      get_assert(reduction_or_exprt{sym}) == "(assert (not (= x (_ bv0 2))))");
   }
 
   SECTION("reduction_nor")
   {
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_nor, sym}) ==
+      get_assert(reduction_nor_exprt{sym}) ==
       "(assert (not (not (= x (_ bv0 2)))))");
   }
 
   SECTION("reduction_xor")
   {
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_xor, sym}) ==
+      get_assert(reduction_xor_exprt{sym}) ==
       "(assert (let ((?rop x)) "
       "(= (bvxor ((_ extract 0 0) ?rop) ((_ extract 1 1) ?rop)) #b1)))");
   }
 
   SECTION("reduction_xnor")
   {
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_xnor, sym}) ==
+      get_assert(reduction_xnor_exprt{sym}) ==
       "(assert (not (let ((?rop x)) "
       "(= (bvxor ((_ extract 0 0) ?rop) ((_ extract 1 1) ?rop)) #b1))))");
   }
 
   SECTION("reduction_xor 1-bit")
   {
     symbol_exprt sym1("y", unsignedbv_typet(1));
-    REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_xor, sym1}) ==
-      "(assert (= y #b1))");
+    REQUIRE(get_assert(reduction_xor_exprt{sym1}) == "(assert (= y #b1))");
   }
 
   SECTION("reduction_and 1-bit")
   {
     symbol_exprt sym1("y", unsignedbv_typet(1));
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_and, sym1}) ==
-      "(assert (= y (_ bv1 1)))");
+      get_assert(reduction_and_exprt{sym1}) == "(assert (= y (_ bv1 1)))");
   }
 
   SECTION("reduction_or 1-bit")
   {
     symbol_exprt sym1("y", unsignedbv_typet(1));
     REQUIRE(
-      get_assert(unary_predicate_exprt{ID_reduction_or, sym1}) ==
-      "(assert (not (= y (_ bv0 1))))");
+      get_assert(reduction_or_exprt{sym1}) == "(assert (not (= y (_ bv0 1))))");
   }
 }