From 9c4028aab485f8e1c83e400af94b753e638d126c Mon Sep 17 00:00:00 2001
From: Clement Courbet <clement.courbet@gmail.com>
Date: Fri, 2 Aug 2024 20:32:36 +0200
Subject: [PATCH] perf: avoid expr copies in replace_rec_fn::apply (#4702)

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 <leomoura@amazon.com>
---
 src/kernel/replace_fn.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 0dde49600eb5..0a2b1030d12b 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <memory>
+#include <utility>
 #include <unordered_map>
 #include "kernel/replace_fn.h"
 
@@ -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;
@@ -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: