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.

It:

1. runs the int_toBitVec simp set
2. If USize.toBitVec/ISize.toBitVec is used anywhere looks for equations of the form System.Platform.numBits = constant (or flipped) and uses them to convert the system back to fixed width.

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.SizeState : Type

Contains information for the USize/ISize elimination pass.

• relevantTerms : Std.HashSet Expr

  Contains terms of the form USize.toBitVec e and ISize.toBitVec e that we will translate to constant width BitVec.

• relevantHyps : Std.HashSet FVarId

  Contains all hypotheses that contain terms from relevantTerms

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.intToBitVecPass : Pass

Equations

• One or more equations did not get rendered due to their size.