more float_bvt implementation

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3248 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/solvers/floatbv/float_bv.cpp

@@ -26,5 +26,98 @@ Function: float_bvt::convert
 
 exprt float_bvt::convert(const exprt &src)
 {
+  if(src.id()==ID_abs)
+    return convert_abs(to_abs_expr(src));
+  else if(src.id()==ID_unary_minus)
+    return convert_unary_minus(to_unary_minus_expr(src));
+//  else if(src.id()==ID_ieee_float_equal)
+//    return convert_ieee_float_equal(to_ieee_float_equal_expr(src));
+
   return nil_exprt();
 }
+
+/*******************************************************************\
+
+Function: float_bvt::convert_abs
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt float_bvt::convert_abs(const abs_exprt &src)
+{
+  // we mask away the sign bit, which is the most significand bit
+  const floatbv_typet &type=to_floatbv_type(src.type());
+  unsigned width=type.get_width();
+  
+  std::string mask_str;
+  mask_str.resize(width, '1');
+  mask_str[0]='0';
+  
+  constant_exprt mask(mask_str, src.type());
+  
+//  return bitand_exprt(src.op(), mask);
+}
+
+/*******************************************************************\
+
+Function: float_bvt::convert_unary_minus
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt float_bvt::convert_unary_minus(const unary_minus_exprt &src)
+{
+  // we flip the sign bit with an xor
+  const floatbv_typet &type=to_floatbv_type(src.type());
+  unsigned width=type.get_width();
+  
+  std::string mask_str;
+  mask_str.resize(width, '0');
+  mask_str[0]='1';
+  
+  constant_exprt mask(mask_str, src.type());
+  
+//  return bitxor_exprt(src.op(), mask);
+}
+
+/*******************************************************************\
+
+Function: float_bvt::convert_ieee_float_equal
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt float_bvt::convert_ieee_float_equal(const ieee_float_equal_exprt &src)
+{
+}
+
+/*******************************************************************\
+
+Function: float_bvt::convert_ieee_float_notequal
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+//exprt float_bvt::convert_ieee_float_notequal(const ieee_float_notequal_exprt &src)
+//{
+//}

src/solvers/floatbv/float_bv.h

@@ -9,9 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_FLOAT_BV_H
 #define CPROVER_FLOAT_BV_H
 
-//#include <util/ieee_float.h>
-
-#include <solvers/prop/prop_conv.h>
+#include <util/std_expr.h>
 
 class float_bvt
 {
@@ -20,7 +18,7 @@ class float_bvt
   {
   }
 
-  virtual ~float_bvt()
+  ~float_bvt()
   {
   }
 
@@ -30,7 +28,11 @@ class float_bvt
   }
 
 protected:
-  exprt convert(const exprt &src);
+  exprt convert(const exprt &);
+  exprt convert_abs(const abs_exprt &);
+  exprt convert_unary_minus(const unary_minus_exprt &);
+  exprt convert_ieee_float_equal(const ieee_float_equal_exprt &);
+  //exprt convert_ieee_float_notequal(const ieee_float_notequal_exprt &);
 
 #if 0
   // extraction