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

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.

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

Equations

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

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

Equations

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

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.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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkPow x y = Lean.Meta.mkAppM `HPow.hPow #[x, y]

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

Equations

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

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.

Equations

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

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))

Equations

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

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.

Equations

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

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

Equations

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

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

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.