update_bits_exprt #8182
Merged
update_bits_exprt #8182
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
Member
kroening
commented
Feb 4, 2024
kroening
commented
- 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).
- 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
update_bits_exprt
branch
from
5d198d1 to
0e2502e
Compare
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #8182 +/- ##
===========================================
- Coverage 79.69% 79.68% -0.02%
===========================================
Files 1680 1681 +1
Lines 195256 195296 +40
===========================================
+ Hits 155617 155625 +8
- Misses 39639 39671 +32 ☔ View full report in Codecov by Sentry. |
kroening
force-pushed
the
update_bits_exprt
branch
2 times, most recently
from
a472554 to
133c09f
Compare
kroening
requested review from
tautschnig,
peterschrammel,
TGWDB,
esteffin and
martin-cs
as code owners
tautschnig
approved these changes
Feb 5, 2024
src/solvers/smt2/smt2_conv.h
Outdated
| @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com | |||
| #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H | |||
| #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H | |||
|
|
|||
| #include <util/bitvector_expr.h> | |||
There was a problem hiding this comment.
Include-what-you-use suggests that this header file isn't required here. I am pretty sure you can get away with class update_bits_exprt; instead.
3 tasks
This replaces op1/op2 by identifiers that clearly state the purpose of the operand.
This introduces update_bits_exprt, which allows replacing parts of a bit-vector identified by a (potentially variable) index by a given bit-vector. This supersedes with_exprt in the case of single-bit operands.
This replaces the conversion of the 'with' expression on bit-vectors by using update_bits_exprt.
kroening
force-pushed
the
update_bits_exprt
branch
from
133c09f to
cefb96a
Compare
martin-cs
approved these changes
Feb 5, 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.