bv_arithmetict: Lift precondition to from_expr's interface

Only constant_exprt are accepted, thus input parameter's type should guarantee
this. Also update to_expr, which can only generate constant_exprt. Note that
neither of these functions is currently used in the code base.

Author: tautschnig

src/util/bv_arithmetic.cpp

@@ -82,7 +82,7 @@ mp_integer bv_arithmetict::pack() const
   return value+power(2, spec.width);
 }
 
-exprt bv_arithmetict::to_expr() const
+constant_exprt bv_arithmetict::to_expr() const
 {
   return constant_exprt(integer2bvrep(value, spec.width), spec.to_type());
 }
@@ -180,10 +180,8 @@ void bv_arithmetict::change_spec(const bv_spect &dest_spec)
   adjust();
 }
 
-void bv_arithmetict::from_expr(const exprt &expr)
+void bv_arithmetict::from_expr(const constant_exprt &expr)
 {
-  PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value = bvrep2integer(
-    to_constant_expr(expr).get_value(), spec.width, spec.is_signed);
+  value = bvrep2integer(expr.get_value(), spec.width, spec.is_signed);
 }

src/util/bv_arithmetic.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include "mp_arith.h"
 #include "format_spec.h"
 
+class constant_exprt;
 class exprt;
 class typet;
 
@@ -60,7 +61,7 @@ class bv_arithmetict
   {
   }
 
-  explicit bv_arithmetict(const exprt &expr)
+  explicit bv_arithmetict(const constant_exprt &expr)
   {
     from_expr(expr);
   }
@@ -91,8 +92,8 @@ class bv_arithmetict
   std::string format(const format_spect &format_spec) const;
 
   // expressions
-  exprt to_expr() const;
-  void from_expr(const exprt &expr);
+  constant_exprt to_expr() const;
+  void from_expr(const constant_exprt &expr);
 
   bv_arithmetict &operator/=(const bv_arithmetict &other);
   bv_arithmetict &operator*=(const bv_arithmetict &other);