From 9cc63a2025b559171ecdc30f25d64489d175c6f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Feb 2021 22:42:31 +0000 Subject: [PATCH] bv_utilst: mark non-modifying members static Some members were marked as const already, but can really be marked as static; others did not make any use of the (sole) "prop" member, and can thus be marked static as well. --- src/solvers/flattening/bv_utils.cpp | 2 +- src/solvers/flattening/bv_utils.h | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index cc5a9b55760..d03d3f5ff86 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/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; diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index c76ad8274ff..ec16ce3a39e 100644 --- a/src/solvers/flattening/bv_utils.h +++ b/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 ∝