This module contains the logic around writing proofs of UNSAT, using LRAT proofs, as meta code.

source
structure Lean.Elab.Tactic.BVDecide.Frontend.TacticContext :
Type

The context for the `bv_decide` tactic.

- exprDef : Name
- certDef : Name
- reflectionDef : Name
- solver : System.FilePath
- lratPath : System.FilePath
- config : BVDecideConfig

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
TermElabM TacticContext
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.BVDecide.Frontend.LratCert :
Type

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

Equations

- Lean.Elab.Tactic.BVDecide.Frontend.LratCert = String

Instances For

source
instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprIntAction :
ToExpr Std.Tactic.BVDecide.LRAT.IntAction
Equations

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

source
def Lean.Elab.Tactic.BVDecide.Frontend.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.

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) :
CoreM LratCert
Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.runExternal (cnf : Std.Sat.CNF Nat) (solver lratPath : System.FilePath) (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
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.

Instances For