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.eqToBEq : Lean.Meta.Simp.Simproc

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkPow (x y : Lean.Expr) : Lean.MetaM Lean.Expr

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

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

A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes the goal fully, indicated by returning none.

• name : Lean.Name
• run : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.fixpointPipeline (passes : List Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass) (goal : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Repeatedly run a list of Pass until they either close the goal or an iteration doesn't change the goal anymore.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.rewriteRulesPass (maxSteps : Nat) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass

Responsible for applying the Bitwuzla style rewrite rules.

Equations

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

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

Flatten out ands. That is look for hypotheses of the form h : (x && y) = true and replace them with h.left : x = true and h.right : y = true. This can enable more fine grained substitutions in embedded constraint substitution.

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.andFlatteningPass.splitAnds (hyp : Lean.Meta.Hypothesis) (hyps : Array Lean.Meta.Hypothesis) (first : Bool := true) : Lean.MetaM (Array Lean.Meta.Hypothesis)

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.andFlatteningPass.trySplit (hyp : Lean.Meta.Hypothesis) : Lean.MetaM (Option (Lean.Meta.Hypothesis × Lean.Meta.Hypothesis))

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.embeddedConstraintPass (maxSteps : Nat) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass

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. Additionally this drops all redundant top level hypotheses.

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

Normalize with respect to Associativity and Commutativity.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.passPipeline (cfg : Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig) : List Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvNormalize (g : Lean.MVarId) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig) : Lean.MetaM (Option Lean.MVarId)

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.