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

def Lean.Meta.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.Meta.Tactic.BVDecide.LRAT.trim proof = Lean.Meta.Tactic.BVDecide.LRAT.trim.M.run✝ proof Lean.Meta.Tactic.BVDecide.LRAT.trim.go✝