Merge pull request #8509 from diffblue/simplify_power

simplify x^0 and x^1

Author: tautschnig

src/util/mathematical_expr.cpp

@@ -7,6 +7,8 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #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());
+}

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<power_exprt>(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<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

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)
   {

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 &);

src/util/simplify_expr_int.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #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<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());
+
+  if(exponent.value() == 1)
+    return expr.base();
+
+  if(!base.has_value())
     return unchanged(expr);
 
   mp_integer result = power(*base, *exponent);

unit/util/simplify_expr.cpp

@@ -6,14 +6,13 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
-#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>
@@ -22,6 +21,8 @@ Author: Michael Tautschnig
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+#include <testing-utils/use_catch.h>
+
 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);
+  }
+}