From 17767589711b70706ac91cda6d9feade86ff618c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 31 Jan 2025 23:25:15 +0100
Subject: [PATCH] perf: inline a few functions in the bv_decide circuit cache
 (#6889)

This PR inlines a few functions in the `bv_decide` circuit cache.
---
 src/Std/Sat/AIG/Basic.lean                        | 15 +++++----------
 .../Tactic/BVDecide/Bitblast/BVExpr/Basic.lean    |  8 ++++----
 2 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 9d56ded152..1e14edf900 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -71,10 +71,10 @@ def Cache (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Decl α)) :
 /--
 Create an empty `Cache`, valid with respect to any `Array Decl`.
 -/
-@[irreducible]
+@[irreducible, inline]
 def Cache.empty (decls : Array (Decl α)) : Cache α decls := ⟨{}, WF.empty⟩
 
-@[inherit_doc Cache.WF.push_id, irreducible]
+@[inherit_doc Cache.WF.push_id, irreducible, inline]
 def Cache.noUpdate (cache : Cache α decls) : Cache α (decls.push decl) :=
   ⟨cache.val, Cache.WF.push_id cache.property⟩
 
@@ -82,7 +82,7 @@ def Cache.noUpdate (cache : Cache α decls) : Cache α (decls.push decl) :=
 We require the `decls` as an explicit argument because we use `decls.size` so accidentally mutating
 `decls` before calling `Cache.insert` will destroy `decl` linearity.
 -/
-@[inherit_doc Cache.WF.push_cache, irreducible]
+@[inherit_doc Cache.WF.push_cache, irreducible, inline]
 def Cache.insert (decls : Array (Decl α)) (cache : Cache α decls) (decl : Decl α) :
     Cache α (decls.push decl) :=
   ⟨cache.val.insert decl decls.size, Cache.WF.push_cache cache.property⟩
@@ -167,13 +167,8 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
 /--
 Lookup a `Decl` in a `Cache`.
 -/
-opaque Cache.get? (cache : Cache α decls) (decl : Decl α) : Option (CacheHit decls decl) :=
-  /-
-  This function is marked as `opaque` to make sure it never, ever gets unfolded anywhere.
-  Unfolding it will often cause `HashMap.find?` to be symbolically evaluated by reducing
-  it either in `whnf` or in the kernel. This causes *huge* performance issues in practice.
-  The function can still be fully verified as all the proofs we need are in `CacheHit`.
-  -/
+@[irreducible, inline]
+def Cache.get? (cache : Cache α decls) (decl : Decl α) : Option (CacheHit decls decl) :=
   match hfound : cache.val[decl]? with
   | some hit =>
     some ⟨hit, Cache.get?_bounds _ _ hfound, Cache.get?_property _ _ hfound⟩
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index d157fd7cd1..28e1eb9955 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -22,15 +22,15 @@ namespace Std.Tactic.BVDecide
 The variable definition used by the bitblaster.
 -/
 structure BVBit where
-  /--
-  The width of the BitVec variable.
-  -/
-  {w : Nat}
   /--
   A numeric identifier for the BitVec variable.
   -/
   var : Nat
   /--
+  The width of the BitVec variable.
+  -/
+  {w : Nat}
+  /--
   The bit that we take out of the BitVec variable by getLsb.
   -/
   idx : Fin w