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.

structure Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• satAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = true.

• expr : Lean.Expr

  A cache for toExpr bvExpr

def Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical.of (h : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.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 : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) (y : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) : Lean.Elab.Tactic.BVDecide.Frontend.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 : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) (h : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.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.