diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 4a232f41eee..8dada3f3e24 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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) { diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index c97adc2c433..3c71f706a9c 100644 --- a/src/util/bitvector_expr.cpp +++ b/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(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 d7502b307df..17f1020f59c 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -895,6 +895,7 @@ class replication_exprt : public binary_exprt { } + // times() is non-negative; zero is ok. constant_exprt ×() { return static_cast(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 <> diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index caa69059f9d..e472c6cecd6 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/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") diff --git a/unit/util/bitvector_expr.cpp b/unit/util/bitvector_expr.cpp index f0a53ea61d6..317135644d8 100644 --- a/unit/util/bitvector_expr.cpp +++ b/unit/util/bitvector_expr.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include @@ -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]",