This module implements an LRAT checker that acts on an Array IntAction and only explodes it into
the DefaultClauseAction when required instead of upfront. This allows for a significantly smaller
memory footprint compared to the generic LRAT checker.
def
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker
{n : Nat}
(f : DefaultFormula n)
(proof : Array IntAction)
:
Equations
Instances For
@[irreducible]
def
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go
{n : Nat}
(f : DefaultFormula n)
(proof : Array IntAction)
(idx : Nat)
:
Equations
- One or more equations did not get rendered due to their size.