This module contains the implementation of bv_normalize which is effectively a custom bv_normalize simp set that is called like this: simp only [seval, bv_normalize]. The rules in bv_normalize fulfill two goals:

1. Turn all hypothesis involving Bool and BitVec into the form x = true where x only consists of a operations on Bool and BitVec. In particular no Prop should be contained. This makes the reflection procedure further down the pipeline much easier to implement.
2. Apply simplification rules from the Bitwuzla SMT solver.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mulConst : Lean.Meta.Simp.Simproc

The bitblaster for multiplication introduces symbolic branches over the right hand side. If we have an expression of the form c * x where c is constant we should change it to x * c such that these symbolic branches get constant folded by the AIG framework.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqToBEq : Lean.Meta.Simp.Simproc

Equations

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

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

• goal : Option Lean.MVarId
• stats : Lean.Meta.Simp.Stats

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvNormalize (g : Lean.MVarId) : Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Result

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.evalBVNormalize : Lean.Elab.Tactic.Tactic

Equations

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