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).

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

The context used for trimming LRAT proofs.

• proof : Std.HashMap Nat Std.Tactic.BVDecide.LRAT.IntAction

  The proof as a map from proof step ids to their actions.

• initialId : Nat

  The id of the first proof step.

• addEmptyId : Nat

  The id of the empty proof step.

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.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.LRAT.trim.M : Type → Type

partial def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.findInitialId (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (curr : Nat := 0) : Except String Nat

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.findEmptyId (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) : Except String Nat

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.run {α : Type} (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (x : M α) : Except String α

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getInitialId : M Nat

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getEmptyId : M Nat

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getProofStep (id : Nat) : M (Option Std.Tactic.BVDecide.LRAT.IntAction)

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.isUsed (id : Nat) : M Bool

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.markUsed (id : Nat) : M Unit

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.registerIdMap (oldId newId : Nat) : M Unit

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.mapStep (step : Std.Tactic.BVDecide.LRAT.IntAction) : M Std.Tactic.BVDecide.LRAT.IntAction

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.mapStep.mapIdent (ident : Nat) : M Nat

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.

partial def Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis.go (worklist : Array Nat) : M Unit

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.

def Lean.Elab.Tactic.BVDecide.LRAT.trim.go : M (Array Std.Tactic.BVDecide.LRAT.IntAction)

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.