Skip to content
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

Jump to bottom

optimized reserve call for memory allocation in advance #15479

Closed
wants to merge 1 commit into from
Closed

optimized reserve call for memory allocation in advance #15479

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
50 changes: 29 additions & 21 deletions libsmtutil/SMTLib2Interface.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,29 +189,37 @@ std::string SMTLib2Interface::toSExpr(solidity::smtutil::Expression const& _expr

std::string SMTLib2Interface::checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate)
{
std::string command;
if (_expressionsToEvaluate.empty())
command = "(check-sat)\n";
else
{
// TODO make sure these are unique
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{
auto const& e = _expressionsToEvaluate.at(i);
smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
command += "(declare-const |EVALEXPR_" + std::to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
command += "(assert (= |EVALEXPR_" + std::to_string(i) + "| " + toSExpr(e) + "))\n";
}
command += "(check-sat)\n";
command += "(get-value (";
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
command += "|EVALEXPR_" + std::to_string(i) + "| ";
command += "))\n";
}

return command;
std::string command;
if (_expressionsToEvaluate.empty())
command = "(check-sat)\n";
else
{
// Reserve space for efficiency
size_t numExpressions = _expressionsToEvaluate.size();
command.reserve(command.size() + numExpressions * 100); // Estimate space needed
Copy link
Collaborator

Choose a reason for hiding this comment

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

Where did you come up with the 100 chars per expression heuristic? Also, you're not using shrink_to_fit() before returning the command, so you're most likely returning a much larger command string than you should be.

@blishko I'd be inclined towards closing this is a mostly unnecessary optimization, but it's up to you.

Copy link
Contributor

Choose a reason for hiding this comment

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

I agree that this is unnecessary optimisation, with a magic number involved.
If anything, command should be a stringstream. That would also achieve the desired result in a clearer way.
But this is definitely not any bottleneck, AFAIK.

Copy link
Member

Choose a reason for hiding this comment

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

Caching of vector's size() is unnecessary as well. It's guaranteed O(1) and introducing an extra local variable for something so trivial is a hit to readability (it's another name you have to keep track of in your head when reading the code) so not a good trade-off.

I'd not be against us using things like reserve() more in places where the size is non-trivial and known ahead of time, but TBH most of the time the impact is probably insignificant so it does not matter all that much in the big picture. Just changing it randomly in a single spot that is not a known bottleneck is pointless.


for (size_t i = 0; i < numExpressions; i++)
{
auto const& e = _expressionsToEvaluate.at(i);
smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
command += "(declare-const |EVALEXPR_" + std::to_string(i) + "| " +
(e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n" +
"(assert (= |EVALEXPR_" + std::to_string(i) + "| " + toSExpr(e) + "))\n";
}

command += "(check-sat)\n";
command += "(get-value (";

for (size_t i = 0; i < numExpressions; i++)
command += "|EVALEXPR_" + std::to_string(i) + "| ";

command += "))\n";
}

return command;
}


std::string SMTLib2Interface::querySolver(std::string const& _input)
{
h256 inputHash = keccak256(_input);
Expand Down