restrict lazy WHNF to reducible (test)

src/Lean/Meta/ExprDefEq.lean

@@ -17,7 +17,7 @@ register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
 }
 
 register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
-  defValue := true
+  defValue := false
   descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
 }
 

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

@@ -205,21 +205,27 @@ where
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateLeft)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩
       | .rotateRight distance =>
         let res := bitblast.blastRotateRight eaig ⟨evec, distance⟩
         have := by
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateRight)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩
       | .arithShiftRightConst distance =>
         let res := bitblast.blastArithShiftRightConst eaig ⟨evec, distance⟩
         have := by
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastArithShiftRightConst)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩
       | .reverse =>
         let res := bitblast.blastReverse eaig evec
         have := by
@@ -250,23 +256,29 @@ where
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend)
         dsimp only at hlaig hraig
         omega
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩
     | .replicate n expr h =>
       let ⟨⟨⟨aig, expr⟩, haig⟩, cache⟩ := goCache aig expr cache
       let res := bitblast.blastReplicate aig ⟨n, expr, h⟩
       have := by
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate)
         dsimp only at haig
         assumption
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩
     | .extract start len expr =>
       let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache
       let res := bitblast.blastExtract eaig ⟨evec, start⟩
       have := by
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastExtract)
         dsimp only at heaig
         exact heaig
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩
     | .shiftLeft lhs rhs =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache

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

@@ -227,6 +227,11 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size
       exact h1
     have h4 : idx < (mkFullAdder aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by
+      /-
+      Without the unfolding of `mkFullAdder`, `apply` will pick the wrong `f`, and simply adding
+      `(f := mkFullAdderCarry)` runs into the heartbeat limit.
+      -/
+      simp only [mkFullAdder]
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size
       exact h3
     rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)]

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

@@ -51,7 +51,9 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai
         apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
         dsimp only at hlhs hrhs
         omega
-      ⟨⟨res, this⟩, cache⟩
+      ⟨⟨res, this⟩, by
+        simp only
+        exact cache⟩
   | .getLsbD expr idx =>
     /-
     Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.