Add .lower() methods to reduction and replication expressions

src/solvers/smt2/smt2_conv.cpp

@@ -2915,29 +2915,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

@@ -344,3 +344,60 @@ exprt onehot0_exprt::lower() const
   // at most one bit is set
   return let_exprt{symbol, op(), not_exprt{more_than_one_seen}};
 }
+
+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();
+  PRECONDITION(width >= 1);
+  exprt::operandst bits;
+  bits.reserve(width);
+  for(std::size_t i = 0; i < width; i++)
+    bits.push_back(extractbit_exprt{operand, i});
+  return xor_exprt{std::move(bits)};
+}
+
+exprt reduction_xnor_exprt::lower() const
+{
+  return not_exprt{reduction_xor_exprt{op()}.lower()};
+}
+
+exprt replication_exprt::lower() const
+{
+  // zero-replications are allowed, and yield a concatenation
+  // with no operands.
+  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

@@ -895,6 +895,7 @@ class replication_exprt : public binary_exprt
   {
   }
 
+  // times() is non-negative; zero is ok.
   constant_exprt &times()
   {
     return static_cast<constant_exprt &>(op0());
@@ -914,6 +915,10 @@ class replication_exprt : public binary_exprt
   {
     return op1();
   }
+
+  /// Lower to concatenation.
+  /// {N{x}} ≡ x :: x :: ... :: x (N times)
+  exprt lower() const;
 };
 
 template <>
@@ -954,6 +959,8 @@ inline replication_exprt &to_replication_expr(exprt &expr)
 ///
 /// This expression takes any number of operands, including
 /// zero-width operands.
+/// Concatenations without operands are allowed, and they
+/// yield a zero-width result.
 /// The ordering of the operands is the same as in the SMT-LIB 2 standard,
 /// i.e., most-significant operands come first.
 class concatenation_exprt : public multi_ary_exprt
@@ -1980,6 +1987,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 <>
@@ -2017,6 +2028,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 <>
@@ -2054,6 +2069,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 <>
@@ -2091,6 +2110,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 <>
@@ -2128,6 +2151,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 <>
@@ -2165,6 +2192,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

@@ -75,9 +75,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")

unit/util/bitvector_expr.cpp

@@ -4,6 +4,7 @@
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/cout_message.h>
+#include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
@@ -151,6 +152,85 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]")
   }
 }
 
+TEST_CASE("reduction and replication expression lowering", "[core][util][expr]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  // We prove full equivalence between an expression and its lowering by
+  // constraining a symbolic operand `x` such that the original expression
+  // and its lowering disagree, and then checking that this is unsatisfiable.
+  // boolbv handles the reduction/replication operators natively, so this
+  // compares the native encoding against the lowered form for every possible
+  // value of `x`.
+
+  GIVEN("A symbolic bit-vector operand and reduction_xor")
+  {
+    satcheckt satcheck{message_handler};
+    boolbvt boolbv{empty_namespace, satcheck, message_handler};
+    const symbol_exprt x{"x", unsignedbv_typet{8}};
+    const reduction_xor_exprt red{x};
+
+    // original != lowering is true exactly when they disagree
+    boolbv << notequal_exprt{red, red.lower()};
+
+    THEN("the lowering of reduction_xor is equivalent to the original")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A symbolic bit-vector operand and reduction_xnor")
+  {
+    satcheckt satcheck{message_handler};
+    boolbvt boolbv{empty_namespace, satcheck, message_handler};
+    const symbol_exprt x{"x", unsignedbv_typet{8}};
+    const reduction_xnor_exprt red{x};
+
+    boolbv << notequal_exprt{red, red.lower()};
+
+    THEN("the lowering of reduction_xnor is equivalent to the original")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A symbolic bit-vector operand and replication")
+  {
+    satcheckt satcheck{message_handler};
+    boolbvt boolbv{empty_namespace, satcheck, message_handler};
+    const unsignedbv_typet u4{4};
+    const symbol_exprt x{"x", u4};
+    const std::size_t times = 3;
+    const replication_exprt repl{
+      from_integer(times, integer_typet{}), x, unsignedbv_typet{4 * times}};
+
+    // original != lowering is true exactly when they disagree
+    boolbv << notequal_exprt{repl, repl.lower()};
+
+    THEN("the lowering of replication is equivalent to the original")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+
+  GIVEN("A symbolic bit-vector operand and a single replication")
+  {
+    satcheckt satcheck{message_handler};
+    boolbvt boolbv{empty_namespace, satcheck, message_handler};
+    const unsignedbv_typet u8{8};
+    const symbol_exprt x{"x", u8};
+    const replication_exprt repl{from_integer(1, integer_typet{}), x, u8};
+
+    boolbv << notequal_exprt{repl, repl.lower()};
+
+    THEN("the lowering of a single replication is equivalent to the original")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_UNSATISFIABLE);
+    }
+  }
+}
+
 TEMPLATE_TEST_CASE(
   "reduction expression sub classes",
   "[core][util][expr]",