From 67842c65e6e1b43b32afa18e4bcce3ff6c3005ab Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 21 Jul 2026 04:29:41 -0700 Subject: [PATCH] Add .lower() methods to reduction and replication expressions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add lower() methods to reduction_and_exprt, reduction_nand_exprt, reduction_or_exprt, reduction_nor_exprt, reduction_xor_exprt, reduction_xnor_exprt, and replication_exprt in bitvector_expr.h/cpp. These methods lower high-level bitvector reduction and replication operators to simpler expression forms: - reduction_and(a) → (a = all_ones) - reduction_nand(a) → (a != all_ones) - reduction_or(a) → (a != 0) - reduction_nor(a) → (a = 0) - reduction_xor(a) → a[0] ^ a[1] ^ ... ^ a[n-1] - reduction_xnor(a) → !(a[0] ^ a[1] ^ ... ^ a[n-1]) - replication(n, x) → x :: x :: ... :: x (n times) Use the new .lower() methods in smt2_conv.cpp to replace inline lowering code for reduction_and, reduction_nand, reduction_or, reduction_nor, and reduction_xnor. The reduction_xor case retains its native SMT-LIB encoding using extract + bvxor for efficiency. --- src/solvers/smt2/smt2_conv.cpp | 18 +++------- src/util/bitvector_expr.cpp | 58 +++++++++++++++++++++++++++++++++ src/util/bitvector_expr.h | 28 ++++++++++++++++ unit/solvers/smt2/smt2_conv.cpp | 4 +-- 4 files changed, 91 insertions(+), 17 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 8ee689aabec..84169261535 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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) { diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index e578f52b6ea..dae09af0edb 100644 --- a/src/util/bitvector_expr.cpp +++ b/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(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()}; +} diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index b3dcb793602..16783965c4e 100644 --- a/src/util/bitvector_expr.h +++ b/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 <> diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index 28556c6ac34..75d4551d95e 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/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")