chore: basic skeleton

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

@@ -11,6 +11,7 @@ import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Rewrite
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AndFlatten
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.EmbeddedConstraint
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.IntToBitVec
 
 /-!
 This module contains the implementation of `bv_normalize`, the preprocessing tactic for `bv_decide`.
@@ -43,9 +44,16 @@ def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := d
     (go g).run cfg g
 where
   go (g : MVarId) : PreProcessM (Option MVarId) := do
-    let some g ← g.falseOrByContra | return none
+    let mut g := g
+    let some g' ← g.falseOrByContra | return none
+    g := g'
 
-    trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
+    let cfg ← PreProcessM.getConfig
+    if cfg.fixedInt then
+      let some g' ← intToBitVecPass.run g | return none
+      g := g'
+
+    trace[Meta.Tactic.bv] m!"Running fixpoint pipeline on:\n{g}"
     let pipeline ← passPipeline
     Pass.fixpointPipeline pipeline g
 

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

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic
+import Lean.Elab.Tactic.BVDecide.Frontend.Attr
+
+/-!
+This module contains the implementation of the pre processing pass for reducing `UIntX`/`IntX` to
+`BitVec` and thus allow `bv_decide` to reason about them.
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend.Normalize
+
+open Lean.Meta
+
+def intToBitVecPass : Pass where
+  name := `intToBitVec
+  run' goal := do
+    let intToBvThms ← intToBitVecExt.getTheorems
+    let cfg ← PreProcessM.getConfig
+    let simpCtx ← Simp.mkContext
+      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps := cfg.maxSteps })
+      (simpTheorems := #[intToBvThms])
+      (congrTheorems := (← getSimpCongrTheorems))
+
+    let hyps ← goal.getNondepPropHyps
+    let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
+    let some (_, newGoal) := result? | return none
+    return newGoal
+
+end Frontend.Normalize
+end Lean.Elab.Tactic.BVDecide

src/Std/Tactic/BVDecide/Syntax.lean

@@ -39,6 +39,11 @@ structure BVDecideConfig where
   -/
   embeddedConstraintSubst : Bool := true
   /--
+  Enable preprocessing with the `int_toBitVec` simp set to reduce `UIntX`/`IntX` to `BitVec` and
+  thus make them accessible for `bv_decide`.
+  -/
+  fixedInt : Bool := true
+  /--
   Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
   Lean process.
   -/

tests/lean/run/bv_uint.lean

@@ -0,0 +1,7 @@
+import Std.Tactic.BVDecide
+
+example (a b : UInt8) : a + b = b + a := by
+  bv_decide
+
+example (a b : UInt8) : a + b = a := by
+  bv_decide