feat: configure max rewrite steps in bv_normalize

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -157,14 +157,14 @@ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : MetaM (Optio
 /--
 Responsible for applying the Bitwuzla style rewrite rules.
 -/
-def rewriteRulesPass : Pass := fun goal => do
+def rewriteRulesPass (maxSteps : Nat) : Pass := fun goal => do
   let bvThms ← bvNormalizeExt.getTheorems
   let bvSimprocs ← bvNormalizeSimprocExt.getSimprocs
   let sevalThms ← getSEvalTheorems
   let sevalSimprocs ← Simp.getSEvalSimprocs
 
   let simpCtx : Simp.Context := {
-    config := { failIfUnchanged := false, zetaDelta := true }
+    config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
     simpTheorems := #[bvThms, sevalThms]
     congrTheorems := (← getSimpCongrTheorems)
   }
@@ -181,7 +181,7 @@ def rewriteRulesPass : Pass := fun goal => do
 Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
 them to substitute occurences of `x` within other hypotheses
 -/
-def embeddedConstraintPass : Pass := fun goal =>
+def embeddedConstraintPass (maxSteps : Nat) : Pass := fun goal =>
   goal.withContext do
     let hyps ← goal.getNondepPropHyps
     let relevanceFilter acc hyp := do
@@ -195,7 +195,7 @@ def embeddedConstraintPass : Pass := fun goal =>
     let relevantHyps : SimpTheoremsArray ← hyps.foldlM (init := #[]) relevanceFilter
 
     let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false }
+      config := { failIfUnchanged := false, maxSteps }
       simpTheorems := relevantHyps
       congrTheorems := (← getSimpCongrTheorems)
     }
@@ -222,10 +222,14 @@ def acNormalizePass : Pass := fun goal => do
 /--
 The normalization passes used by `bv_normalize` and thus `bv_decide`.
 -/
-def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass]
+def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
+  [
+    rewriteRulesPass cfg.maxSteps,
+    embeddedConstraintPass cfg.maxSteps
+  ]
 
 def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
-  let mut passPipeline := defaultPipeline
+  let mut passPipeline := defaultPipeline cfg
 
   if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]

src/Std/Tactic/BVDecide/Syntax.lean

@@ -33,6 +33,10 @@ structure BVDecideConfig where
   Lean process.
   -/
   graphviz : Bool := false
+  /--
+  The maximum number of subexpressions to visit when performing simplification.
+  -/
+  maxSteps : Nat := Lean.Meta.Simp.defaultMaxSteps
 
 end Lean.Elab.Tactic.BVDecide.Frontend