Address incremental SMT2 related code review comments from PR6357 #6388
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
As suggested in code review.
There are 2 simplifications here. 1) A swap to a normal string literal, rather that a raw string literal, as there is only a single character which needs escaping. 2) A change to remove the `^` and `$` for matching the start and end of the string. These were redundant, because `std::regex_match` already requires the regex to match the full string rather than a partial sub-match. This simplification is already tested by the "smt_identifier_termt construction" test in the smt_terms unit tests.
Because the purpose of this INVARIANT was not neccessarily apparent without reading the doxygen in the header file.
In order to make it more explict that this function has side-effects on the stack of expressions to be defined.
thomasspriggs
requested review from
chrisr-diffblue,
NlightNFotis,
peterschrammel and
TGWDB
as code owners
TGWDB
approved these changes
Oct 11, 2021
Codecov Report
@@ Coverage Diff @@
## develop #6388 +/- ##
========================================
Coverage 75.97% 75.97%
========================================
Files 1523 1523
Lines 164194 164194
========================================
Hits 124750 124750
Misses 39444 39444
Continue to review full report at Codecov.
|
| @@ -49,7 +49,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( | |||
| return expr_identifier.first; | |||
| }); | |||
| std::stack<exprt> to_be_defined; | |||
| const auto dependencies_needed = [&](const exprt &expr) { | |||
| const auto push_dependencies_needed = [&](const exprt &expr) { | |||
There was a problem hiding this comment.
Can the type of the return value of the lambda also be defined there? -> bool - because it made it surprising to see a lambda named push-* in a context that demands a predicate without it having an explicit book return value.
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 PR addresses incremental SMT2 related code review comments from
#6357. Some of the outstanding comments on this PR were not blocking and the PR was therefore merged without addressing them. This is the follow up PR which cleans this up.