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 : Lake.Name
• certDef : Lake.Name
• reflectionDef : Lake.Name
• solver : Lake.FilePath
• lratPath : Lake.FilePath
• graphviz : Bool
• timeout : Nat
• trimProofs : Bool
• binaryProofs : Bool

def Lean.Elab.Tactic.BVDecide.Frontend.TacticContext.new (lratPath : Lake.FilePath) : Lean.Elab.TermElabM Lean.Elab.Tactic.BVDecide.Frontend.TacticContext

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.TacticContext.new.determineSolver : Lean.Elab.TermElabM Lake.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 : Lean.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.ofFile (lratPath : Lake.FilePath) (trimProofs : Bool) : Lean.MetaM Lean.Elab.Tactic.BVDecide.Frontend.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 : Lake.FilePath) (lratPath : Lake.FilePath) (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) : Lean.MetaM (Except (Array (Bool × Nat)) Lean.Elab.Tactic.BVDecide.Frontend.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.

def Lean.Elab.Tactic.BVDecide.Frontend.mkAuxDecl (name : Lake.Name) (value : Lean.Expr) (type : Lean.Expr) : Lean.MetaM Unit

Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.LratCert.toReflectionProof {α : Type u_1} [Lean.ToExpr α] (cert : Lean.Elab.Tactic.BVDecide.Frontend.LratCert) (cfg : Lean.Elab.Tactic.BVDecide.Frontend.TacticContext) (reflected : α) (verifier : Lake.Name) (unsat_of_verifier_eq_true : Lake.Name) : Lean.MetaM Lean.Expr

Turn an LratCert into a proof that some reflected expression is UNSAT by providing a verifier function together with a correctness theorem for it.

• verifier is expected to have type α → LratCert → Bool
• unsat_of_verifier_eq_true is expected to have type ∀ (b : α) (c : LratCert), verifier b c = true → unsat b

Equations

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