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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M.addSizeTerm (e : Expr) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M.addSizeHyp (f : FVarId) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Unit

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.intToBitVecPass.handleSize (goal : MVarId) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ MVarId

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.intToBitVecPass.detectSize (goal : MVarId) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Bool

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.intToBitVecPass.replaceSize (goal : MVarId) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ MVarId

Turn goal into a goal containing BitVec const instead of USize/ISize.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.intToBitVecPass.findNumBitsEq (goal : MVarId) : MetaM (Option (Nat × Expr))

Builds an expression of type: const = System.Platform.numBits from the hypotheses in the context if possible.

Equations

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