Simplify complex_{imag,real}_exprt

When the operand is a complex_exprt we can just extract the respective member.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2303,6 +2303,32 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   return true;
 }
 
+bool simplify_exprt::simplify_complex(exprt &expr)
+{
+  if(expr.id() == ID_complex_real)
+  {
+    complex_real_exprt &complex_real_expr = to_complex_real_expr(expr);
+
+    if(complex_real_expr.op().id() == ID_complex)
+    {
+      expr = to_complex_expr(complex_real_expr.op()).real();
+      return false;
+    }
+  }
+  else if(expr.id() == ID_complex_imag)
+  {
+    complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(expr);
+
+    if(complex_imag_expr.op().id() == ID_complex)
+    {
+      expr = to_complex_expr(complex_imag_expr.op()).imag();
+      return false;
+    }
+  }
+
+  return true;
+}
+
 bool simplify_exprt::simplify_node_preorder(exprt &expr)
 {
   bool result=true;
@@ -2445,6 +2471,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result = simplify_popcount(to_popcount_expr(expr)) && result;
   else if(expr.id() == ID_function_application)
     result = simplify_function_application(expr) && result;
+  else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
+    result = simplify_complex(expr) && result;
 
   #ifdef DEBUGX
   if(!result

src/util/simplify_expr_class.h

@@ -113,6 +113,7 @@ class simplify_exprt
   bool simplify_abs(exprt &expr);
   bool simplify_sign(exprt &expr);
   bool simplify_popcount(popcount_exprt &expr);
+  bool simplify_complex(exprt &expr);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.