added simplify_exprt::simplify_power

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -2509,6 +2509,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_bitwise(expr) && result;
   else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
     result=simplify_shifts(expr) && result;
+  else if(expr.id()==ID_power)
+    result=simplify_power(expr) && result;
   else if(expr.id()==ID_plus)
     result=simplify_plus(expr) && result;
   else if(expr.id()==ID_minus)

src/util/simplify_expr_class.h

@@ -71,6 +71,7 @@ class simplify_exprt
   bool simplify_floatbv_op(exprt &expr);
   bool simplify_floatbv_typecast(exprt &expr);
   bool simplify_shifts(exprt &expr);
+  bool simplify_power(exprt &expr);
   bool simplify_bitwise(exprt &expr);
   bool simplify_if_preorder(if_exprt &expr);
   bool simplify_if(if_exprt &expr);

src/util/simplify_expr_int.cpp

@@ -1016,6 +1016,40 @@ bool simplify_exprt::simplify_shifts(exprt &expr)
 
 /*******************************************************************\
 
+Function: simplify_exprt::simplify_power
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool simplify_exprt::simplify_power(exprt &expr)
+{
+  if(!is_number(expr.type()))
+    return true;
+
+  if(expr.operands().size()!=2)
+    return true;
+
+  mp_integer base, exponent;
+  
+  if(to_integer(expr.op0(), base))
+    return true;
+    
+  if(to_integer(expr.op1(), exponent))
+    return true;
+    
+  mp_integer result=power(base, exponent);
+  
+  expr=from_integer(result, expr.type());
+  return false;
+}
+
+/*******************************************************************\
+
 Function: simplify_exprt::simplify_extractbits
 
   Inputs: