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.

source
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 `BitVec`s.

Equations

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

Instances For

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

Instances For

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

Instances For