Add .lower() methods to reduction and replication expressions

src/solvers/smt2/smt2_conv.cpp

@@ -2909,29 +2909,19 @@ 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_reduction_and_expr(expr).op();
-    auto all_ones = to_bitvector_type(op.type()).all_ones_expr();
-    convert_expr(equal_exprt{op, all_ones});
+    convert_expr(to_reduction_and_expr(expr).lower());
   }
   else if(expr.id() == ID_reduction_nand)
   {
-    // This is the negation of "reduction and"
-    auto &op = to_reduction_nand_expr(expr).op();
-    convert_expr(not_exprt{reduction_and_exprt{op}});
+    convert_expr(to_reduction_nand_expr(expr).lower());
   }
   else if(expr.id() == ID_reduction_or)
   {
-    // This is true iff the operand is not zero
-    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});
+    convert_expr(to_reduction_or_expr(expr).lower());
   }
   else if(expr.id() == ID_reduction_nor)
   {
-    // This is the negation of "reduction or"
-    auto &op = to_reduction_nor_expr(expr).op();
-    convert_expr(not_exprt{reduction_or_exprt{op}});
+    convert_expr(to_reduction_nor_expr(expr).lower());
   }
   else if(expr.id() == ID_reduction_xor)
   {

src/util/bitvector_expr.cpp

@@ -340,3 +340,61 @@ exprt onehot0_exprt::lower() const
   // same as onehot, but on flipped operand bits
   return let_exprt{symbol, bitnot_exprt{op()}, onehot_lowering(symbol)};
 }
+
+exprt reduction_and_exprt::lower() const
+{
+  auto &operand = op();
+  return equal_exprt{
+    operand, to_bitvector_type(operand.type()).all_ones_expr()};
+}
+
+exprt reduction_nand_exprt::lower() const
+{
+  auto &operand = op();
+  return notequal_exprt{
+    operand, to_bitvector_type(operand.type()).all_ones_expr()};
+}
+
+exprt reduction_or_exprt::lower() const
+{
+  auto &operand = op();
+  return notequal_exprt{
+    operand, to_bitvector_type(operand.type()).all_zeros_expr()};
+}
+
+exprt reduction_nor_exprt::lower() const
+{
+  auto &operand = op();
+  return equal_exprt{
+    operand, to_bitvector_type(operand.type()).all_zeros_expr()};
+}
+
+exprt reduction_xor_exprt::lower() const
+{
+  auto &operand = op();
+  auto width = to_bitvector_type(operand.type()).width();
+  exprt result = extractbit_exprt{operand, 0};
+  for(std::size_t i = 1; i < width; i++)
+    result = xor_exprt{result, extractbit_exprt{operand, i}};
+  return result;
+}
+
+exprt reduction_xnor_exprt::lower() const
+{
+  auto &operand = op();
+  auto width = to_bitvector_type(operand.type()).width();
+  exprt result = extractbit_exprt{operand, 0};
+  for(std::size_t i = 1; i < width; i++)
+    result = xor_exprt{result, extractbit_exprt{operand, i}};
+  return not_exprt{result};
+}
+
+exprt replication_exprt::lower() const
+{
+  auto count = numeric_cast_v<std::size_t>(times());
+  exprt::operandst ops;
+  ops.reserve(count);
+  for(std::size_t i = 0; i < count; i++)
+    ops.push_back(op());
+  return concatenation_exprt{std::move(ops), type()};
+}

src/util/bitvector_expr.h

@@ -914,6 +914,10 @@ class replication_exprt : public binary_exprt
   {
     return op1();
   }
+
+  /// Lower to concatenation.
+  /// {N{x}} ≡ x :: x :: ... :: x (N times)
+  exprt lower() const;
 };
 
 template <>
@@ -1978,6 +1982,10 @@ class reduction_and_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_and, std::move(_op))
   {
   }
+
+  /// Lower to equality with all-ones constant.
+  /// reduction_and(a) ≡ (a = 0xFF...F)
+  exprt lower() const;
 };
 
 template <>
@@ -2015,6 +2023,10 @@ class reduction_or_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_or, std::move(_op))
   {
   }
+
+  /// Lower to inequality with zero.
+  /// reduction_or(a) ≡ (a != 0)
+  exprt lower() const;
 };
 
 template <>
@@ -2052,6 +2064,10 @@ class reduction_nor_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_nor, std::move(_op))
   {
   }
+
+  /// Lower to equality with zero.
+  /// reduction_nor(a) ≡ (a = 0)
+  exprt lower() const;
 };
 
 template <>
@@ -2089,6 +2105,10 @@ class reduction_nand_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_nand, std::move(_op))
   {
   }
+
+  /// Lower to inequality with all-ones constant.
+  /// reduction_nand(a) ≡ (a != 0xFF...F)
+  exprt lower() const;
 };
 
 template <>
@@ -2126,6 +2146,10 @@ class reduction_xor_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_xor, std::move(_op))
   {
   }
+
+  /// Lower to XOR of all individual bits.
+  /// reduction_xor(a) ≡ a[0] ^ a[1] ^ ... ^ a[n-1]
+  exprt lower() const;
 };
 
 template <>
@@ -2163,6 +2187,10 @@ class reduction_xnor_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_reduction_xnor, std::move(_op))
   {
   }
+
+  /// Lower to negation of XOR of all individual bits.
+  /// reduction_xnor(a) ≡ !(a[0] ^ a[1] ^ ... ^ a[n-1])
+  exprt lower() const;
 };
 
 template <>

unit/solvers/smt2/smt2_conv.cpp

@@ -74,9 +74,7 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]")
 
   SECTION("reduction_nor")
   {
-    REQUIRE(
-      get_assert(reduction_nor_exprt{sym}) ==
-      "(assert (not (not (= x (_ bv0 2)))))");
+    REQUIRE(get_assert(reduction_nor_exprt{sym}) == "(assert (= x (_ bv0 2)))");
   }
 
   SECTION("reduction_xor")