Introduce floatbv_round_to_integral_exprt

[kroening]

This adds a new expression, floatbv_round_to_integral, which rounds an IEEE 754 floating-point number given as bit-vector to the nearest integer, considering the explicitly given rounding mode.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 88.97638% with 28 lines in your changes missing coverage. Please review.

Project coverage is 78.94%. Comparing base (af4e2e4) to head (8b80200).

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	8.33%	11 Missing ⚠️
src/solvers/smt2/smt2_parser.cpp	12.50%	7 Missing ⚠️
src/util/ieee_float.cpp	82.14%	5 Missing ⚠️
src/ansi-c/c_typecheck_expr.cpp	75.00%	3 Missing ⚠️
src/solvers/flattening/boolbv_floatbv_op.cpp	87.50%	1 Missing ⚠️
unit/util/ieee_float.cpp	98.50%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8538      +/-   ##
===========================================
+ Coverage    78.92%   78.94%   +0.01%     
===========================================
  Files         1732     1732              
  Lines       198958   199206     +248     
  Branches     18543    18609      +66     
===========================================
+ Hits        157037   157266     +229     
- Misses       41921    41940      +19     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

Where does this actually consider the rounding mode?

[kroening]

It calls add_sub.

[tautschnig]

If ieee_floatt::round_to_integral is to be trusted, shouldn't the sign bit be used instead of hard-coding false and true?

[kroening]

Note line 153 -- this variant tweaks the sign bit of the magic constant instead.

[remi-delmas-3000]

looks good but could use some comments to explain how fractional bits get cleared due to the exponent alignment with the magic constant, and tests for halfway values and different tie breaking modes

[remi-delmas-3000]

Could we also test for some small and large values halfway between integers, previous below, next above, x (e.g. 0.5, 0.49999999, 0.500000001) and cross that with the different rounding modes so check that ties are actually resolved as expected?

'