This module is the main entry point for reifying BitVec problems with boolean substructure. Given some proof h : exp = true where exp is a BitVec problem with boolean substructure, it returns a SatAtBVLogical, containing the reified version as well as a proof that the reified version must be equal to true.

def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.of (h : Expr) : LemmaM (Option SatAtBVLogical)

Reify an Expr that is a proof of some boolean structure on top of predicates about BitVecs.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.and (x y : SatAtBVLogical) : SatAtBVLogical

Logical conjunction of two ReifiedBVLogical.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.proveFalse (x : SatAtBVLogical) (h : Expr) : M Expr

Given a proof that x.expr.Unsat, produce a proof of False.

Equations

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