Merge pull request #5830 from tautschnig/bv-utils-cleanup

bv_utilst: mark non-modifying members static

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -75,7 +75,7 @@ bvt bv_utilst::extract_lsb(const bvt &a, std::size_t n)
   return result;
 }
 
-bvt bv_utilst::concatenate(const bvt &a, const bvt &b) const
+bvt bv_utilst::concatenate(const bvt &a, const bvt &b)
 {
   bvt result;
 

src/solvers/flattening/bv_utils.h

@@ -30,7 +30,7 @@ class bv_utilst
 
   enum class representationt { SIGNED, UNSIGNED };
 
-  bvt build_constant(const mp_integer &i, std::size_t width);
+  static bvt build_constant(const mp_integer &i, std::size_t width);
 
   bvt incrementer(const bvt &op, literalt carry_in);
   bvt inc(const bvt &op) { return incrementer(op, const_literal(true)); }
@@ -44,7 +44,7 @@ class bv_utilst
   literalt overflow_negate(const bvt &op);
 
   // bit-wise negation
-  bvt inverted(const bvt &op);
+  static bvt inverted(const bvt &op);
 
   literalt full_adder(
     const literalt a,
@@ -73,7 +73,7 @@ class bv_utilst
     SHIFT_LEFT, SHIFT_LRIGHT, SHIFT_ARIGHT, ROTATE_LEFT, ROTATE_RIGHT
   };
 
-  bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
+  static bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
   bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
 
   bvt unsigned_multiplier(const bvt &op0, const bvt &op1);
@@ -172,9 +172,10 @@ class bv_utilst
   literalt unsigned_less_than(const bvt &bv0, const bvt &bv1);
   literalt signed_less_than(const bvt &bv0, const bvt &bv1);
 
-  bool is_constant(const bvt &bv);
+  static bool is_constant(const bvt &bv);
 
-  bvt extension(const bvt &bv, std::size_t new_size, representationt rep);
+  static bvt
+  extension(const bvt &bv, std::size_t new_size, representationt rep);
 
   bvt sign_extension(const bvt &bv, std::size_t new_size)
   {
@@ -212,10 +213,10 @@ class bv_utilst
   static bvt extract_lsb(const bvt &a, std::size_t n);
 
   // put a and b together, where a comes first (lower indices)
-  bvt concatenate(const bvt &a, const bvt &b) const;
+  static bvt concatenate(const bvt &a, const bvt &b);
 
   literalt verilog_bv_has_x_or_z(const bvt &);
-  bvt verilog_bv_normal_bits(const bvt &);
+  static bvt verilog_bv_normal_bits(const bvt &);
 
 protected:
   propt ∝