Use FloatingPoint theory when using --cprover-smt2 #6132
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Member
kroening
commented
May 20, 2021
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- n/a 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.
kroening
force-pushed
the
smt2_solver_FPA
branch
3 times, most recently
from
a8a325f to
3b2a021
Compare
kroening
requested review from
allredj,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
martin-cs
approved these changes
May 20, 2021
Codecov Report
@@ Coverage Diff @@
## develop #6132 +/- ##
===========================================
- Coverage 75.42% 75.26% -0.16%
===========================================
Files 1447 1447
Lines 158094 158181 +87
===========================================
- Hits 119249 119062 -187
- Misses 38845 39119 +274
Continue to review full report at Codecov.
|
tautschnig
approved these changes
May 20, 2021
src/solvers/smt2/smt2_parser.cpp
Outdated
| } | ||
| else | ||
| { | ||
| // remove the '.', if any |
There was a problem hiding this comment.
The ", if any" in the comment seems strange, because we know that there is a '.' in the else case.
src/solvers/smt2/smt2_parser.cpp
Outdated
Comment on lines
768
to
771
| for(auto ch : real_number) | ||
| if(ch != '.') | ||
| significand_str += ch; |
There was a problem hiding this comment.
- Is the intended behaviour really such that the '.' is the only character not being copied over?
- Nit pick: Braces around the body of the for-loop would be nice.
- Perhaps just use
eraseinstead:
std::string significand_str = real_number;
significand_str.erase(significand_str.begin() + dot_pos);
- As further alternative, create
significand_strby concatenating two substrings, which perhaps is more efficient in some future version of C++ with string views.
This commit adds the obvious mapping from fp.abs to our abs_exprt.
This adds support for floating-point literals to the SMT2 expression formatter.
SMT-LIB to_fp has a number of variants, and this commit adds two of them to enable the use of cprover_smt2 with CBMC.
This adds support for three floating-point constants to the SMT2 parser, to enable the use of cprover_smt2 with CBMC.
This fixes an off-by-one bug in the SMT2 backend when parsing +oo, -oo and NaN expressions.
This enables the use of the FloatingPoint theory when using cprover_smt2. The resulting SMT-LIB files are much smaller, and easier to read. The commit also enables existing tests that now pass with --cprover-smt2.
TGWDB
approved these changes
May 20, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.