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) : Std.Tactic.BVDecide.LRAT.Action β α
• addRup {β : Type u} {α : Type v} (id : Nat) (c : β) (rupHints : Array Nat) : Std.Tactic.BVDecide.LRAT.Action β α
• addRat {β : Type u} {α : Type v} (id : Nat) (c : β) (pivot : Std.Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) : Std.Tactic.BVDecide.LRAT.Action β α
• del {β : Type u} {α : Type v} (ids : Array Nat) : Std.Tactic.BVDecide.LRAT.Action β α

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

Equations

• Std.Tactic.BVDecide.LRAT.instInhabitedAction = { default := Std.Tactic.BVDecide.LRAT.Action.addEmpty default default }

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

Equations

• Std.Tactic.BVDecide.LRAT.instBEqAction = { beq := Std.Tactic.BVDecide.LRAT.beqAction✝ }

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

Equations

• Std.Tactic.BVDecide.LRAT.instReprAction = { reprPrec := Std.Tactic.BVDecide.LRAT.reprAction✝ }

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

Equations

• One or more equations did not get rendered due to their size.
• (Std.Tactic.BVDecide.LRAT.Action.addEmpty a a_1).toString = toString "addEmpty (id: " ++ toString a ++ toString ") (hints: " ++ toString a_1 ++ toString ")"
• (Std.Tactic.BVDecide.LRAT.Action.addRup a a_1 a_2).toString = toString "addRup " ++ toString a_1 ++ toString " (id : " ++ toString a ++ toString ") (hints: " ++ toString a_2 ++ toString ")"
• (Std.Tactic.BVDecide.LRAT.Action.del a).toString = toString "del " ++ toString a ++ toString ""

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

Equations

• Std.Tactic.BVDecide.LRAT.instToStringAction = { toString := Std.Tactic.BVDecide.LRAT.Action.toString }

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

Equations

• Std.Tactic.BVDecide.LRAT.IntAction = Std.Tactic.BVDecide.LRAT.Action (Array Int) Nat