This module provides the implementation of the bv_decide frontend itself.

structure Lean.Meta.Tactic.BVDecide.UnsatProver.Result (α : Type) : Type

• proof : Expr

  A proof that the input BVLogicalExpr of the UnsatProver is Unsat

• cert : α

  Potential meta data that can aid in squeezing the proof. Used by bv_decide? to exfiltrate the LRAT certificate to avoid calling the SAT solver again.

structure Lean.Meta.Tactic.BVDecide.ReflectionResult : Type

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reflected expression.

• proveFalse : Expr → M Expr

  Function to prove False given an unsatisfiability proof of bvExpr

• unusedHypotheses : Std.HashSet FVarId

  Set of unused hypotheses for diagnostic purposes.

• expr : Expr

  A cache for toExpr bvExpr.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.UnsatProver (α : Type) : Type

Equations

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

def Lean.Meta.Tactic.BVDecide.reflectBV (g : MVarId) : M ReflectionResult

Equations

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

def Lean.Meta.Tactic.BVDecide.closeWithBVReflection {α : Type} (g : MVarId) (unsatProver : UnsatProver α) : MetaM (Except CounterExample α)

Equations

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