Skip to content

Cleanup of float_bvt #2565

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
Jul 9, 2018
Merged

Cleanup of float_bvt #2565

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
13 changes: 2 additions & 11 deletions src/solvers/floatbv/float_bv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,6 @@ Author: Daniel Kroening, [email protected]
class float_bvt
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

mark the class as final?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I contemplated that, but it wasn't entirely clear whether there is value in this? What would the desired benefit be? (FWIW, I don't think deriving from this class would strictly be wrong.)

{
public:
float_bvt()
{
}

~float_bvt()
{
}

exprt operator()(const exprt &src)
{
return convert(src);
Expand Down Expand Up @@ -101,7 +93,7 @@ class float_bvt
const exprt &,
const ieee_float_spect &);

protected:
private:
// helpers
ieee_float_spect get_spec(const exprt &);
// still biased
Expand All @@ -116,7 +108,6 @@ class float_bvt

struct rounding_mode_bitst
{
public:
// these are mutually exclusive, obviously
exprt round_to_even;
exprt round_to_zero;
Expand Down Expand Up @@ -168,7 +159,7 @@ class float_bvt
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &);

// this takes unpacked format, and returns packed
virtual exprt rounder(
exprt rounder(
const unbiased_floatt &,
const exprt &rm,
const ieee_float_spect &);
Expand Down