Skip to content

Commit

Permalink
perf: avoid expr copies in replace_rec_fn::apply (#4702)
Browse files Browse the repository at this point in the history
Those represent ~13% of the time spent in `save_result`,
even though `r` is a temporary in all cases but one.

See #4698 for details.

---------

Co-authored-by: Leonardo de Moura <[email protected]>
  • Loading branch information
legrosbuffle and leodemoura authored Aug 2, 2024
1 parent 2c00271 commit 9c4028a
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/kernel/replace_fn.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <vector>
#include <memory>
#include <utility>
#include <unordered_map>
#include "kernel/replace_fn.h"

Expand All @@ -21,7 +22,7 @@ class replace_rec_fn {
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;

expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
expr save_result(expr const & e, unsigned offset, expr r, bool shared) {
if (shared)
m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
return r;
Expand All @@ -36,7 +37,7 @@ class replace_rec_fn {
shared = true;
}
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);
return save_result(e, offset, std::move(*r), shared);
} else {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort:
Expand Down

0 comments on commit 9c4028a

Please sign in to comment.