Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions src/util/mathematical_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
\*******************************************************************/

#include "mathematical_expr.h"

#include "arith_tools.h"
#include "mathematical_types.h"

function_application_exprt::function_application_exprt(
Expand Down Expand Up @@ -49,3 +51,9 @@
lambda_type(_variables, _where))
{
}

power_exprt::power_exprt(const mp_integer &_base, const exprt &_exp)
: power_exprt{from_integer(_base, _exp.type()), _exp}

Check warning on line 56 in src/util/mathematical_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/mathematical_expr.cpp#L55-L56

Added lines #L55 - L56 were not covered by tests
{
PRECONDITION(base().is_not_nil());
}

Check warning on line 59 in src/util/mathematical_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/mathematical_expr.cpp#L58-L59

Added lines #L58 - L59 were not covered by tests
38 changes: 27 additions & 11 deletions src/util/mathematical_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,29 @@
: 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()

Check warning on line 109 in src/util/mathematical_expr.h

View check run for this annotation

Codecov / codecov/patch

src/util/mathematical_expr.h#L109

Added line #L109 was not covered by tests
{
return op0();

Check warning on line 111 in src/util/mathematical_expr.h

View check run for this annotation

Codecov / codecov/patch

src/util/mathematical_expr.h#L111

Added line #L111 was not covered by tests
}

const exprt &exponent() const
{
return op1();
}

exprt &exponent()
{
return op1();
}
};

template <>
Expand All @@ -105,11 +128,6 @@
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.
Expand All @@ -119,18 +137,16 @@
inline const power_exprt &to_power_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_power);
const power_exprt &ret = static_cast<const power_exprt &>(expr);
validate_expr(ret);
return ret;
power_exprt::check(expr);
return static_cast<const power_exprt &>(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<power_exprt &>(expr);
validate_expr(ret);
return ret;
power_exprt::check(expr);
return static_cast<power_exprt &>(expr);
}

/// \brief Falling factorial power
Expand Down
2 changes: 1 addition & 1 deletion src/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down
3 changes: 2 additions & 1 deletion src/util/simplify_expr_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 &);
Expand Down
17 changes: 12 additions & 5 deletions src/util/simplify_expr_int.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
#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"
Expand Down Expand Up @@ -1120,18 +1121,24 @@
}

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<mp_integer>(expr.op0());
const auto exponent = numeric_cast<mp_integer>(expr.op1());
const auto base = numeric_cast<mp_integer>(expr.base());
const auto exponent = numeric_cast<mp_integer>(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());

Check warning on line 1136 in src/util/simplify_expr_int.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/simplify_expr_int.cpp#L1136

Added line #L1136 was not covered by tests

if(exponent.value() == 1)
return expr.base();

if(!base.has_value())
return unchanged(expr);

mp_integer result = power(*base, *exponent);
Expand Down
19 changes: 17 additions & 2 deletions unit/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,13 @@

\*******************************************************************/

#include <testing-utils/use_catch.h>

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/cmdline.h>
#include <util/config.h>
#include <util/mathematical_expr.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
Expand All @@ -22,6 +21,8 @@
#include <util/std_expr.h>
#include <util/symbol_table.h>

#include <testing-utils/use_catch.h>

Check warning on line 25 in unit/util/simplify_expr.cpp

View check run for this annotation

Codecov / codecov/patch

unit/util/simplify_expr.cpp#L25

Added line #L25 was not covered by tests
TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]")
{
config.set_arch("none");
Expand Down Expand Up @@ -571,3 +572,17 @@
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);
}
}
Loading