Documentation

Lean.Meta.Tactic.BVDecide.Prover.Bitblast

This module provides the implementation of the bv_decide frontend itself.

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

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

    Instances For