diff --git a/src/util/mathematical_expr.cpp b/src/util/mathematical_expr.cpp index 1c467b924ca..90fef5f4ca5 100644 --- a/src/util/mathematical_expr.cpp +++ b/src/util/mathematical_expr.cpp @@ -7,6 +7,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "mathematical_expr.h" + +#include "arith_tools.h" #include "mathematical_types.h" function_application_exprt::function_application_exprt( @@ -49,3 +51,9 @@ lambda_exprt::lambda_exprt(const variablest &_variables, const exprt &_where) lambda_type(_variables, _where)) { } + +power_exprt::power_exprt(const mp_integer &_base, const exprt &_exp) + : power_exprt{from_integer(_base, _exp.type()), _exp} +{ + PRECONDITION(base().is_not_nil()); +} diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h index 87332355cf4..b8c0eb76a6c 100644 --- a/src/util/mathematical_expr.h +++ b/src/util/mathematical_expr.h @@ -97,6 +97,29 @@ class power_exprt : public binary_exprt : binary_exprt(_base, ID_power, _exp) { } + + // convenience helper + power_exprt(const mp_integer &_base, const exprt &_exp); + + const exprt &base() const + { + return op0(); + } + + exprt &base() + { + return op0(); + } + + const exprt &exponent() const + { + return op1(); + } + + exprt &exponent() + { + return op1(); + } }; template <> @@ -105,11 +128,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_power; } -inline void validate_expr(const power_exprt &value) -{ - validate_operands(value, 2, "Power must have two operands"); -} - /// \brief Cast an exprt to a \ref power_exprt /// /// \a expr must be known to be \ref power_exprt. @@ -119,18 +137,16 @@ inline void validate_expr(const power_exprt &value) inline const power_exprt &to_power_expr(const exprt &expr) { PRECONDITION(expr.id() == ID_power); - const power_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + power_exprt::check(expr); + return static_cast(expr); } /// \copydoc to_power_expr(const exprt &) inline power_exprt &to_power_expr(exprt &expr) { PRECONDITION(expr.id() == ID_power); - power_exprt &ret = static_cast(expr); - validate_expr(ret); - return ret; + power_exprt::check(expr); + return static_cast(expr); } /// \brief Falling factorial power diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index d7bd7f7ad45..c425602cbf5 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2962,7 +2962,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node) } else if(expr.id()==ID_power) { - r = simplify_power(to_binary_expr(expr)); + r = simplify_power(to_power_expr(expr)); } else if(expr.id()==ID_plus) { diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 78c1fc4e71c..284a314fde2 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -64,6 +64,7 @@ class plus_exprt; class pointer_object_exprt; class pointer_offset_exprt; class popcount_exprt; +class power_exprt; class prophecy_pointer_in_range_exprt; class prophecy_r_or_w_ok_exprt; class refined_string_exprt; @@ -163,7 +164,7 @@ class simplify_exprt [[nodiscard]] resultt<> simplify_floatbv_typecast(const floatbv_typecast_exprt &); [[nodiscard]] resultt<> simplify_shifts(const shift_exprt &); - [[nodiscard]] resultt<> simplify_power(const binary_exprt &); + [[nodiscard]] resultt<> simplify_power(const power_exprt &); [[nodiscard]] resultt<> simplify_bitwise(const multi_ary_exprt &); [[nodiscard]] resultt<> simplify_if_preorder(const if_exprt &expr); [[nodiscard]] resultt<> simplify_if(const if_exprt &); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 9c0966eb56e..6cdb467e25b 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "fixedbv.h" #include "ieee_float.h" #include "invariant.h" +#include "mathematical_expr.h" #include "mathematical_types.h" #include "namespace.h" #include "pointer_expr.h" @@ -1120,18 +1121,24 @@ simplify_exprt::simplify_shifts(const shift_exprt &expr) } simplify_exprt::resultt<> -simplify_exprt::simplify_power(const binary_exprt &expr) +simplify_exprt::simplify_power(const power_exprt &expr) { if(!is_number(expr.type())) return unchanged(expr); - const auto base = numeric_cast(expr.op0()); - const auto exponent = numeric_cast(expr.op1()); + const auto base = numeric_cast(expr.base()); + const auto exponent = numeric_cast(expr.exponent()); - if(!base.has_value()) + if(!exponent.has_value()) return unchanged(expr); - if(!exponent.has_value()) + if(exponent.value() == 0) + return from_integer(1, expr.type()); + + if(exponent.value() == 1) + return expr.base(); + + if(!base.has_value()) return unchanged(expr); mp_integer result = power(*base, *exponent); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 18a4f4b88c5..a3a288295f7 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -6,14 +6,13 @@ Author: Michael Tautschnig \*******************************************************************/ -#include - #include #include #include #include #include #include +#include #include #include #include @@ -22,6 +21,8 @@ Author: Michael Tautschnig #include #include +#include + TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]") { config.set_arch("none"); @@ -571,3 +572,17 @@ TEST_CASE("Simplify bitxor", "[core][util]") false_c_bool); } } + +TEST_CASE("Simplify power", "[core][util]") +{ + const symbol_tablet symbol_table; + const namespacet ns{symbol_table}; + + SECTION("Simplification for power") + { + symbol_exprt a{"a", integer_typet{}}; + + REQUIRE( + simplify_expr(power_exprt{a, from_integer(1, integer_typet{})}, ns) == a); + } +}