fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface #15967
Conversation
|
Thank you for your contribution to the Solidity compiler! A team member will follow up shortly. If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother. If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix. |
| // FIXME: Why Expression here? | ||
| Expression arg = scopedParser.toSMTUtilExpression(nameSortPair[0]); | ||
| predicateArgs.push_back(arg); | ||
| predicateArgs.push_back(scopedParser.toSMTUtilExpression(nameSortPair[0])); |
There was a problem hiding this comment.
Isn't the comment asking why we need to convert this to an Expression in the first place and not simply why we have the local variable? The PR does not seem to address that question and just blindly removes it.
There was a problem hiding this comment.
Corrected. Thank you for your notice
There was a problem hiding this comment.
The comment you've inserted instead of the FIXME does not really address the question. I was questioning the original design choice there. I admit the question is poorly phrased and probably should be placed elsewhere.
The question there is why are we even creating the predicate representation as Expression in the first place.
After some thinking, I have an idea how the code can be improved, but it is going to require a larger change.
I suggest to go back to your original change and move the fixme to line 480 with wording "FIXME: Why do we need to represent the predicate as Expression?".
I can take it from there.
There was a problem hiding this comment.
@blishko Corrected as you said
There was a problem hiding this comment.
Looks good!
I think you should squash the commits (only the first one has a meaningful message).
Also, it looks like you should rebase on top latest develop.
There was a problem hiding this comment.
You still have a merge commit there. A rebase should get rid of it.
There was a problem hiding this comment.
@cameel like this? there is a file that i didn't edit - test/benchmarks/external.sh
There was a problem hiding this comment.
I'm confused with rebase every time...
There was a problem hiding this comment.
The merge commit is gone so it looks ok. Still not on develop, but now github at least let me use the "Update branch" feature now so it's fine.
VolodymyrBg
force-pushed
the
vbg
branch
3 times, most recently
from
c33cd9b to
ede0f06
Compare
fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface Update CHCSmtLib2Interface.cpp Update CHCSmtLib2Interface.cpp add repeats to external.sh
Remove an unnecessary intermediate Expression variable when populating predicateArgs vector in the invariantsFromSolverResponse method. This simplifies the code by directly using the result of toSMTUtilExpression without storing it in a temporary variable first.