diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 2e7341be03b..b9b2181d678 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -275,13 +275,6 @@ class simplify_exprt virtual bool simplify(exprt &expr); - static bool is_bitvector_type(const typet &type) - { - return type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_bv; - } - protected: const namespacet &ns; #ifdef DEBUG_ON_DEMAND diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 826cf4ae34d..d33aea0b955 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -662,7 +662,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr) simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) { - if(!is_bitvector_type(expr.type())) + if(!can_cast_type(expr.type())) return unchanged(expr); // check if these are really boolean @@ -838,7 +838,7 @@ simplify_exprt::simplify_extractbit(const extractbit_exprt &expr) { const typet &src_type = expr.src().type(); - if(!is_bitvector_type(src_type)) + if(!can_cast_type(src_type)) return unchanged(expr); const std::size_t src_bit_width = to_bitvector_type(src_type).get_width(); @@ -869,7 +869,7 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) concatenation_exprt new_expr = expr; - if(is_bitvector_type(new_expr.type())) + if(can_cast_type(new_expr.type())) { // first, turn bool into bvec[1] Forall_operands(it, new_expr) @@ -891,10 +891,10 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) exprt &opi = new_expr.operands()[i]; exprt &opn = new_expr.operands()[i + 1]; - if(opi.is_constant() && - opn.is_constant() && - is_bitvector_type(opi.type()) && - is_bitvector_type(opn.type())) + if( + opi.is_constant() && opn.is_constant() && + can_cast_type(opi.type()) && + can_cast_type(opn.type())) { // merge! const auto &value_i = to_constant_expr(opi).get_value(); @@ -963,12 +963,10 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) exprt &opi = new_expr.operands()[i]; exprt &opn = new_expr.operands()[i + 1]; - if(opi.is_constant() && - opn.is_constant() && - (opi.type().id()==ID_verilog_unsignedbv || - is_bitvector_type(opi.type())) && - (opn.type().id()==ID_verilog_unsignedbv || - is_bitvector_type(opn.type()))) + if( + opi.is_constant() && opn.is_constant() && + can_cast_type(opi.type()) && + can_cast_type(opn.type())) { // merge! const std::string new_value= @@ -1001,7 +999,7 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) simplify_exprt::resultt<> simplify_exprt::simplify_shifts(const shift_exprt &expr) { - if(!is_bitvector_type(expr.type())) + if(!can_cast_type(expr.type())) return unchanged(expr); const auto distance = numeric_cast(expr.distance()); @@ -1132,8 +1130,9 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) { const typet &op0_type = expr.src().type(); - if(!is_bitvector_type(op0_type) && - !is_bitvector_type(expr.type())) + if( + !can_cast_type(op0_type) && + !can_cast_type(expr.type())) { return unchanged(expr); } diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 8219df4f45f..e0f61b744d1 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -554,3 +554,20 @@ TEST_CASE("Simplify inequality", "[core][util]") REQUIRE(simp == true_exprt{}); } } + +TEST_CASE("Simplify bitxor", "[core][util]") +{ + config.set_arch("none"); + + const symbol_tablet symbol_table; + const namespacet ns(symbol_table); + + SECTION("Simplification for c_bool") + { + constant_exprt false_c_bool = from_integer(0, c_bool_type()); + + REQUIRE( + simplify_expr(bitxor_exprt{false_c_bool, false_c_bool}, ns) == + false_c_bool); + } +}