Skip to content

bv_utilst: mark non-modifying members static #5830

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 18, 2021
Merged

bv_utilst: mark non-modifying members static #5830

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/solvers/flattening/bv_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
15 changes: 8 additions & 7 deletions src/solvers/flattening/bv_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)); }
Expand All @@ -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,
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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 ∝
Expand Down