Skip to content

fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface #15967

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 27, 2025
Merged

fix: Remove unnecessary Expression temporary in CHCSmtLib2Interface #15967

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions libsmtutil/CHCSmtLib2Interface.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -465,9 +465,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
smtSolverInteractionRequire(isAtom(nameSortPair[0]), "Invalid format of CHC model");
SortPointer varSort = scopedParser.toSort(nameSortPair[1]);
scopedParser.addVariableDeclaration(asAtom(nameSortPair[0]), varSort);
// FIXME: Why Expression here?
Expression arg = scopedParser.toSMTUtilExpression(nameSortPair[0]);
predicateArgs.push_back(arg);
predicateArgs.push_back(scopedParser.toSMTUtilExpression(nameSortPair[0]));
Copy link
Collaborator

@cameel cameel Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@VolodymyrBg VolodymyrBg Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Corrected. Thank you for your notice

Copy link
Collaborator

@blishko blishko Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@VolodymyrBg VolodymyrBg Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@blishko Corrected as you said

Copy link
Collaborator

@blishko blishko Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

@cameel cameel Mar 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You still have a merge commit there. A rebase should get rid of it.

Copy link
Contributor Author

@VolodymyrBg VolodymyrBg Mar 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@cameel like this? there is a file that i didn't edit - test/benchmarks/external.sh

Copy link
Contributor Author

@VolodymyrBg VolodymyrBg Mar 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused with rebase every time...

Copy link
Collaborator

@cameel cameel Mar 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@VolodymyrBg VolodymyrBg Mar 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you))

}

auto parsedInterpretation = scopedParser.toSMTUtilExpression(interpretation);
Expand All @@ -479,6 +477,7 @@ std::optional<smtutil::Expression> CHCSmtLib2Interface::invariantsFromSolverResp
});

Expression predicate(asAtom(args[1]), predicateArgs, SortProvider::boolSort);
// FIXME: Why do we need to represent the predicate as Expression?
definitions.push_back(predicate == parsedInterpretation);
}
return Expression::mkAnd(std::move(definitions));
Expand Down