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 : RBMap Nat Unit compare

  The set of used proof step ids.

• mapped : Std.HashMap Nat Nat

  A mapping from old proof step ids to new ones. Used such that the proof remains a sequence without gaps.

@[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 (ExceptT String (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 pure (s.used.contains id)

@[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.getUsedSet : M (RBMap Nat Unit compare)

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.getUsedSet = do let s ← get pure s.used

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.registerIdMap oldId newId = modify fun (s : Lean.Elab.Tactic.BVDecide.LRAT.trim.State) => { used := s.used, mapped := s.mapped.insert oldId newId }

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.

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.LRAT.trim.M.mapStep.mapIdent ident = do let s ← get pure (s.mapped[ident]?.getD ident)

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]

partial def Lean.Elab.Tactic.BVDecide.LRAT.trim.useAnalysis.go (workList : List 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.

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