Use complex_real_exprt and complex_imag_exprt in bitvector flattening

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -279,9 +279,9 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_complex)
     return convert_complex(expr);
   else if(expr.id()==ID_complex_real)
-    return convert_complex_real(expr);
+    return convert_complex_real(to_complex_real_expr(expr));
   else if(expr.id()==ID_complex_imag)
-    return convert_complex_imag(expr);
+    return convert_complex_imag(to_complex_imag_expr(expr));
   else if(expr.id()==ID_lambda)
     return convert_lambda(expr);
   else if(expr.id()==ID_array_of)

src/solvers/flattening/boolbv.h

@@ -142,8 +142,8 @@ class boolbvt:public arrayst
   virtual bvt convert_array(const exprt &expr);
   virtual bvt convert_vector(const exprt &expr);
   virtual bvt convert_complex(const exprt &expr);
-  virtual bvt convert_complex_real(const exprt &expr);
-  virtual bvt convert_complex_imag(const exprt &expr);
+  virtual bvt convert_complex_real(const complex_real_exprt &expr);
+  virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
   virtual bvt convert_lambda(const exprt &expr);
   virtual bvt convert_let(const let_exprt &);
   virtual bvt convert_array_of(const array_of_exprt &expr);

src/solvers/flattening/boolbv_complex.cpp

@@ -45,35 +45,29 @@ bvt boolbvt::convert_complex(const exprt &expr)
   return conversion_failed(expr);
 }
 
-bvt boolbvt::convert_complex_real(const exprt &expr)
+bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.operands().size()!=1)
-    return conversion_failed(expr);
-
-  bvt bv=convert_bv(expr.op0());
+  bvt bv = convert_bv(expr.op());
 
   assert(bv.size()==width*2);
   bv.resize(width); // chop
 
   return bv;
 }
 
-bvt boolbvt::convert_complex_imag(const exprt &expr)
+bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.operands().size()!=1)
-    return conversion_failed(expr);
-
-  bvt bv=convert_bv(expr.op0());
+  bvt bv = convert_bv(expr.op());
 
   assert(bv.size()==width*2);
   bv.erase(bv.begin(), bv.begin()+width);