This module provides the implementation of the bv_decide frontend itself.

def Lean.Meta.Tactic.BVDecide.lratBitblaster (ctx : TacticContext) : UnsatProver LratCert

Run a SAT solver to obtain an LRAT certificate and use it to produce a proof of UNSAT.

Equations

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

def Lean.Meta.Tactic.BVDecide.lratChecker (ctx : TacticContext) : UnsatProver Unit

Given a pre-existing LRAT certificate in ctx.lratPath use it to produce a proof of UNSAT.

Equations

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