This module contains the definition of the LRAT format (https://www.cs.utexas.edu/~marijn/publications/lrat.pdf) as a type Action, that is polymorphic over the variables used in the CNF. The type IntAction := Action (Array Int) Nat is the version that is used by the checker as input and should be considered the parsing target for LRAT proofs.

inductive Std.Tactic.BVDecide.LRAT.Action (β : Type u) (α : Type v) : Type (max u v)

β is for the type of a clause, α is for the type of variables

• addEmpty {β : Type u} {α : Type v} (id : Nat) (rupHints : Array Nat) : Action β α
• addRup {β : Type u} {α : Type v} (id : Nat) (c : β) (rupHints : Array Nat) : Action β α
• addRat {β : Type u} {α : Type v} (id : Nat) (c : β) (pivot : Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) : Action β α
• del {β : Type u} {α : Type v} (ids : Array Nat) : Action β α

@[implicit_reducible]

instance Std.Tactic.BVDecide.LRAT.instInhabitedAction {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (Action a✝ a✝¹)

@[implicit_reducible]

instance Std.Tactic.BVDecide.LRAT.instBEqAction {β✝ : Type u_1} {α✝ : Type u_2} [BEq β✝] [BEq α✝] : BEq (Action β✝ α✝)

def Std.Tactic.BVDecide.LRAT.instBEqAction.beq {β✝ : Type u_1} {α✝ : Type u_2} [BEq β✝] [BEq α✝] : Action β✝ α✝ → Action β✝ α✝ → Bool

@[implicit_reducible]

instance Std.Tactic.BVDecide.LRAT.instReprAction {β✝ : Type u_1} {α✝ : Type u_2} [Repr β✝] [Repr α✝] : Repr (Action β✝ α✝)

def Std.Tactic.BVDecide.LRAT.instReprAction.repr {β✝ : Type u_1} {α✝ : Type u_2} [Repr β✝] [Repr α✝] : Action β✝ α✝ → Nat → Format

def Std.Tactic.BVDecide.LRAT.Action.toString {β : Type u_1} {α : Type u_2} [ToString β] [ToString α] : Action β α → String

@[implicit_reducible]

instance Std.Tactic.BVDecide.LRAT.instToStringAction {β : Type u_1} {α : Type u_2} [ToString β] [ToString α] : ToString (Action β α)

@[reducible, inline]

abbrev Std.Tactic.BVDecide.LRAT.IntAction : Type

Action where variables are (positive) Nat, clauses are arrays of Int, and ids are Nat. This Action type is meant to be a convenient target for parsing LRAT proofs.