From bb23713542ff829cc9ed8bf507eb1dfa3ffdc16c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 28 Mar 2025 18:21:10 +0100 Subject: [PATCH] perf: skip computing hash of bv_decide BVExpr.Cache.Key (#7709) This PR skips computation of the hash of `BVExpr.Cache.Key` as the expression's hash is a computed field and the width is already mixed in by its hash function. This will probably only have a very minor effect but is visible in large SMTLIB benchmarks. --- .../Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 00433b2fbd..cef7b3436b 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -34,7 +34,11 @@ namespace BVExpr structure Cache.Key where w : Nat expr : BVExpr w - deriving DecidableEq, Hashable + deriving DecidableEq + +instance : Hashable Cache.Key where + -- The width is already mixed into the hash of `key.expr` which is completely cached. + hash key := hash key.expr structure Cache (aig : AIG BVBit) where map : Std.DHashMap Cache.Key (fun k => Vector (Nat × Bool) k.w)