Documentation

Lean.Elab.Tactic.BVDecide.LRAT.Trim

This module implements the LRAT trimming algorithm described in section 4 of "Faster LRAT Checking Than Solving with CaDiCaL" (https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.21/LIPIcs.SAT.2023.21.pdf).

source
structure Lean.Elab.Tactic.BVDecide.LRAT.trim.Context :
Type

The context used for trimming LRAT proofs.

source
structure Lean.Elab.Tactic.BVDecide.LRAT.trim.State :
Type
  • used : ByteArray

    For each proof step i contains at index i - initialId 0 if i is unused, 1 if it is used.

  • mapped : Array Nat

    For each proof step i contains at index i - initialId the step that i maps to in the new proof or 0 if that step is not yet set. Used such that the proof remains a sequence without gaps.

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.BVDecide.LRAT.trim.M :
Type → Type
Equations
source
partial def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.findInitialId (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (curr : Nat := 0) :
Except String Nat
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.findEmptyId (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) :
Except String Nat
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.run {α : Type} (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (x : M α) :
Except String α
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getInitialId :
M Nat
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getEmptyId :
M Nat
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getProofStep (id : Nat) :
M (Option Std.Tactic.BVDecide.LRAT.IntAction)
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.isUsed (id : Nat) :
M Bool
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.markUsed (id : Nat) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.registerIdMap (oldId newId : Nat) :
M Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.mapStep (step : Std.Tactic.BVDecide.LRAT.IntAction) :
M Std.Tactic.BVDecide.LRAT.IntAction
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.mapStep.mapIdent (ident : Nat) :
M Nat
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis :
M Unit

Perform a use-def analysis of LRAT proof steps, starting at the empty clause and working its way up with DFS.

Equations
source
partial def Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis.go (worklist : Array Nat) :
M Unit
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.mapping :
M (Array Std.Tactic.BVDecide.LRAT.IntAction)

Map the set of used proof steps to a new LRAT proof that has no holes in the sequence of proof identifiers.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim.go :
M (Array Std.Tactic.BVDecide.LRAT.IntAction)
Equations
source
def Lean.Elab.Tactic.BVDecide.LRAT.trim (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) :
Except String (Array Std.Tactic.BVDecide.LRAT.IntAction)

Trim the LRAT proof by removing all steps that are not used in reaching the empty clause conclusion.

Equations