perf: Add RefVec.emptyWithCapacity to the AIG framework (#7521)

This PR adds the equivalent of `Array.emptyWithCapacity` to the AIG
framework and applies it to `bv_decide`. This is particularly useful as
we are only working with capacities that are always known at run time so
we should never have to reallocate a `RefVec`.

src/Std/Sat/AIG/If.lean

@@ -116,7 +116,7 @@ structure IfInput (aig : AIG α) (w : Nat) where
 
 def ite (aig : AIG α) (input : IfInput aig w) : RefVecEntry α w :=
   let ⟨discr, lhs, rhs⟩ := input
-  go aig 0 (by omega) discr lhs rhs .empty
+  go aig 0 (by omega) discr lhs rhs (.emptyWithCapacity w)
 where
   go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
       (lhs rhs : RefVec aig w) (s : RefVec aig curr) : RefVecEntry α w :=

src/Std/Sat/AIG/RefVec.lean

@@ -21,6 +21,15 @@ def empty : RefVec aig 0 where
   hlen := by simp
   hrefs := by intros; contradiction
 
+def emptyWithCapacity (c : Nat) : RefVec aig 0 where
+  refs := Array.emptyWithCapacity c
+  hlen := by simp
+  hrefs := by intros; contradiction
+
+@[simp]
+theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
+  rfl
+
 @[inline]
 def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
     (h :

src/Std/Sat/AIG/RefVecOperator/Map.lean

@@ -52,7 +52,7 @@ attribute [instance] MapTarget.chainable
 
 @[specialize]
 def map (aig : AIG α) (target : MapTarget aig len) : RefVecEntry α len :=
-  go aig 0 (by omega) .empty target.vec target.func
+  go aig 0 (by omega) (.emptyWithCapacity len) target.vec target.func
 where
   @[specialize]
   go {len : Nat} (aig : AIG α) (idx : Nat) (hidx : idx ≤ len) (s : RefVec aig idx)

src/Std/Sat/AIG/RefVecOperator/Zip.lean

@@ -81,7 +81,7 @@ attribute [instance] ZipTarget.chainable
 
 @[specialize]
 def zip (aig : AIG α) (target : ZipTarget aig len) : RefVecEntry α len :=
-  go aig 0 .empty (by omega) target.input.lhs target.input.rhs target.func
+  go aig 0 (.emptyWithCapacity len) (by omega) target.input.lhs target.input.rhs target.func
 where
   @[specialize]
   go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len)

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean

@@ -22,7 +22,7 @@ namespace bitblast
 variable [Hashable α] [DecidableEq α]
 
 def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVecEntry α w :=
-  go aig val 0 .empty (by omega)
+  go aig val 0 (.emptyWithCapacity w) (by omega)
 where
   go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
       AIG.RefVecEntry α w :=

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean

@@ -166,7 +166,7 @@ def blastAdd (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry
   let cin := res.ref
   let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
   let ⟨lhs, rhs⟩ := input
-  go aig lhs rhs 0 (by omega) cin .empty
+  go aig lhs rhs 0 (by omega) cin (.emptyWithCapacity w)
 where
   go (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.Ref aig)
       (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean

@@ -32,7 +32,7 @@ def blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth) :
   let aig := res.aig
   let falseRef := res.ref
   let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  ⟨aig, go input start falseRef 0 (by omega) .empty⟩
+  ⟨aig, go input start falseRef 0 (by omega) (.emptyWithCapacity newWidth)⟩
 where
   go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (falseRef : AIG.Ref aig)
       (curr : Nat) (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean

@@ -29,7 +29,7 @@ structure ReplicateTarget (aig : AIG α) (combined : Nat) where
 def blastReplicate (aig : AIG α) (target : ReplicateTarget aig newWidth) :
     AIG.RefVecEntry α newWidth :=
   let ⟨n, inner, h⟩ := target
-  let ref := go n inner 0 (by omega) .empty
+  let ref := go n inner 0 (by omega) (.emptyWithCapacity newWidth)
   ⟨aig, h ▸ ref⟩
 where
   go {aig : AIG α} {w : Nat} (n : Nat) (input : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ n)

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean

@@ -25,7 +25,7 @@ variable [Hashable α] [DecidableEq α]
 def blastRotateLeft (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean

@@ -25,7 +25,7 @@ variable [Hashable α] [DecidableEq α]
 def blastRotateRight (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean

@@ -28,7 +28,7 @@ variable [Hashable α] [DecidableEq α]
 def blastShiftLeftConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  go aig input distance 0 (by omega) .empty
+  go aig input distance 0 (by omega) (.emptyWithCapacity w)
 where
   go (aig : AIG α) (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean

@@ -28,7 +28,7 @@ variable [Hashable α] [DecidableEq α]
 def blastShiftRightConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  go aig input distance 0 (by omega) .empty
+  go aig input distance 0 (by omega) (.emptyWithCapacity w)
 where
   go (aig : AIG α) (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
@@ -99,7 +99,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastShiftRightConst where
 def blastArithShiftRightConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean

@@ -33,9 +33,9 @@ structure ShiftConcatInput (aig : AIG α) (len : Nat) where
 
 def blastShiftConcat (aig : AIG α) (input : ShiftConcatInput aig w) : AIG.RefVecEntry α w :=
   let ⟨lhs, bit⟩ := input
-  let bit := AIG.RefVec.empty.push bit
+  let bit := AIG.RefVec.emptyWithCapacity (w + 1) |>.push bit
   let new := bit.append lhs
-  blastZeroExtend aig ⟨_, new⟩
+  blastZeroExtend aig ⟨1 + w, new⟩
 
 instance : AIG.LawfulVecOperator α ShiftConcatInput blastShiftConcat where
   le_size := by

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean

@@ -24,7 +24,7 @@ variable [Hashable α] [DecidableEq α]
 def blastZeroExtend (aig : AIG α) (target : AIG.ExtendTarget aig newWidth) :
     AIG.RefVecEntry α newWidth :=
   let ⟨width, input⟩ := target
-  go aig width input newWidth 0 (by omega) .empty
+  go aig width input newWidth 0 (by omega) (.emptyWithCapacity newWidth)
 where
   go (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth : Nat) (curr : Nat)
       (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean

@@ -23,7 +23,7 @@ structure BVVar (width : Nat) where
   ident : Nat
 
 def blastVar (aig : AIG BVBit) (var : BVVar w) : AIG.RefVecEntry BVBit w :=
-  go aig w var.ident 0 .empty (by omega)
+  go aig w var.ident 0 (.emptyWithCapacity w) (by omega)
 where
   go (aig : AIG BVBit) (w : Nat) (a : Nat) (curr : Nat) (s : AIG.RefVec aig curr)
     (hcurr : curr ≤ w) :