SMT2: support onehot and onehot0
#8524
Merged
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
kroening
requested review from
martin-cs,
peterschrammel,
TGWDB and
tautschnig
as code owners
kroening
force-pushed
the
smt2-onehot
branch
2 times, most recently
from
d343868 to
572d67c
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8524 +/- ##
===========================================
- Coverage 78.88% 78.46% -0.42%
===========================================
Files 1728 1728
Lines 198669 199820 +1151
Branches 18393 18356 -37
===========================================
+ Hits 156719 156792 +73
- Misses 41950 43028 +1078 ☔ View full report in Codecov by Sentry. |
tautschnig
reviewed
Dec 1, 2024
Comment on lines
+1834
to
+1837
| else if(expr.id() == ID_onehot) | ||
| { | ||
| convert_expr(to_onehot_expr(expr).lower()); | ||
| } |
| { | ||
| exprt one_seen = false_exprt{}; | ||
| const auto width = to_bitvector_type(expr.type()).get_width(); | ||
| exprt::operandst more_than_one_seen_disjuncts; |
There was a problem hiding this comment.
May I suggest more_than_one_seen_disjuncts.reserve(width);?
| @@ -64,3 +71,34 @@ TEMPLATE_TEST_CASE( | |||
| } | |||
| } | |||
| } | |||
|
|
|||
| TEST_CASE("onehot expression lowering", "[core][util][expr]") | |||
There was a problem hiding this comment.
Thank you for adding this test; but could onehot0 please also be included?
This adds support for the onehot and onehot0 predicates to the SMT2 backend.
tautschnig
approved these changes
Dec 2, 2024
TGWDB
approved these changes
Dec 3, 2024
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.
This adds support for the
onehotandonehot0predicates to the SMT2 backend.