Documentation

Lean.Elab.Tactic.BVDecide.Frontend.LRAT

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

The context for the bv_decide tactic.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

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

Equations
Equations
  • One or more equations did not get rendered due to their size.
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) :

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.

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} [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α) (verifier unsat_of_verifier_eq_true : Name) :

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 α → LratCertBool
  • 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.