Unit tests for simplifying boolean and cast expressions #5229
Conversation
This file contains 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
thk123
changed the title
xbauch
reviewed
Feb 7, 2020
unit/util/simplify_expr.cpp
Outdated
| } | ||
| SECTION("Nested boolean expressions") | ||
| { | ||
| INFO("((!true) || true) && (false => false))") |
There was a problem hiding this comment.
Suggested change
| INFO("((!true) || true) && (false => false))") | |
| INFO("((!true) || (false => false)) && true)") |
xbauch
reviewed
Feb 7, 2020
unit/util/simplify_expr.cpp
Outdated
| { | ||
| struct test_entryt | ||
| { | ||
| irep_idt comparision; |
There was a problem hiding this comment.
Suggested change
| irep_idt comparision; | |
| irep_idt comparison; |
xbauch
reviewed
Feb 7, 2020
unit/util/simplify_expr.cpp
Outdated
| const auto binary_relation_from = [](const test_entryt &entry) { | ||
| const signedbv_typet int_type(32); | ||
| return binary_relation_exprt{from_integer(entry.lhs, int_type), | ||
| entry.comparision, |
There was a problem hiding this comment.
Suggested change
| entry.comparision, | |
| entry.comparison, |
xbauch
reviewed
Feb 7, 2020
unit/util/simplify_expr.cpp
Outdated
| symbol_tablet symbol_table; | ||
| namespacet ns(symbol_table); | ||
| const auto int_type = signedbv_typet(32); | ||
| const auto long_type = signedbv_typet(32); |
There was a problem hiding this comment.
Is it intentional that int and long are of the same width?
xbauch
reviewed
Feb 7, 2020
thk123
force-pushed
the
test-simplify-boolean-expr
branch
from
281a155 to
a8c1571
Compare
martin-cs
approved these changes
Feb 7, 2020
|
Restarted one CI job - looks spurious (apt get failure) |
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.
Added some new unit tests to check simplification of boolean formula (so function can be used as basis for testing #5200) Also imported and updated the tests I wrote in #1075.
@tautschnig I notice in #1075 you seemed to say the following shouldn't be simplified:It was because I'd left long type as the same as int type, so was redundant. Now that's corrected, the tests behave as expected: