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

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.

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass = (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 : 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.embeddedConstraintPass : 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

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.defaultPipeline : List Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass

The normalization passes used by bv_normalize and thus bv_decide.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.passPipeline : Lean.MetaM (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) : 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.