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.

• lastUse : Array Int

  Maps each clause id to the latest proof step id that references it or -1. Used to determine when a clause can be deleted.

@[reducible, inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M = ReaderT Lean.Elab.Tactic.BVDecide.LRAT.trim.Context (StateM Lean.Elab.Tactic.BVDecide.LRAT.trim.State)

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

Equations

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

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.

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getInitialId = do let ctx ← read pure ctx.initialId

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getEmptyId = do let ctx ← read pure ctx.addEmptyId

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getProofStep id = do let ctx ← read pure ctx.proof[id]?

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.isUsed id = do let s ← get let __do_lift ← Lean.Elab.Tactic.BVDecide.LRAT.trim.M.idIndex✝ id pure (s.used[__do_lift]! == 1)

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

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

@[inline]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.M.updateLastUse (hint user : Nat) : M Unit

Equations

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

@[inline]

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

Equations

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

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.

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

• Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis = do let emptyId ← Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getEmptyId Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis.go✝ #[emptyId]

def Lean.Elab.Tactic.BVDecide.LRAT.trim.computeToDelete : M (Std.HashMap Nat (Array Nat))

Equations

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

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. Inserts .del actions immediately after a clause's last use.

Equations

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

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.go = do Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis Lean.Elab.Tactic.BVDecide.LRAT.trim.mapping

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

• Lean.Elab.Tactic.BVDecide.LRAT.trim proof = Lean.Elab.Tactic.BVDecide.LRAT.trim.M.run proof Lean.Elab.Tactic.BVDecide.LRAT.trim.go