From 797ad73b5eced32889129be9309b892ad529ec72 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 12 May 2026 09:28:25 -0700 Subject: [PATCH] introduce reduction_*_exprt classes This adds classes for the already existing bit-wise reduction operators. These are used by Verilog and BTOR. --- src/solvers/smt2/smt2_conv.cpp | 14 +-- src/util/bitvector_expr.h | 186 ++++++++++++++++++++++++++++++++ unit/solvers/smt2/smt2_conv.cpp | 25 ++--- 3 files changed, 202 insertions(+), 23 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 70624dab03c..36b84e16199 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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( diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index dd89fdffc9f..0c476107a80 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -1970,4 +1970,190 @@ inline onehot0_exprt &to_onehot0_expr(exprt &expr) return static_cast(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(expr); +} + #endif // CPROVER_UTIL_BITVECTOR_EXPR_H diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index 0b34ba62757..3e7581d62d5 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -53,36 +53,33 @@ 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)))"); } @@ -90,7 +87,7 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]") 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))))"); } @@ -98,25 +95,21 @@ TEST_CASE("smt2_convt reduction operators", "[core][solvers][smt2]") 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))))"); } }