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

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

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.

def Lean.Elab.Tactic.BVDecide.Frontend.TacticContext.new.determineSolver : CoreM System.FilePath

Equations

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

@[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

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.

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.

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.

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.