This module contains the logic for loading LRAT proofs into Lean.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.LratCert : Type

An LRAT proof read from a file. This will get parsed using native evaluation.

Equations

• Lean.Meta.Tactic.BVDecide.LratCert = String

def Lean.Meta.Tactic.BVDecide.LratCert.load (lratPath : System.FilePath) (trimProofs : Bool) : CoreM (Array Std.Tactic.BVDecide.LRAT.IntAction)

Equations

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

def Lean.Meta.Tactic.BVDecide.LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM LratCert

Equations

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

def Lean.Meta.Tactic.BVDecide.runExternal (cnf : Std.Sat.CNF Nat) (solver lratPath : System.FilePath) (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) (solverMode : Elab.Tactic.BVDecide.SolverMode) : CoreM (Except (Array (Bool × Nat)) LratCert)

Run an external SAT solver on the CNF to obtain an LRAT proof.

This will obtain an LratCert if the formula is UNSAT and throw errors otherwise.

Equations

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