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 β α

def Std.Tactic.BVDecide.LRAT.instInhabitedAction.default {a✝ : Type u_1} {a✝¹ : Type u_2} : Action a✝ a✝¹

Equations

• Std.Tactic.BVDecide.LRAT.instInhabitedAction.default = Std.Tactic.BVDecide.LRAT.Action.addEmpty default default

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.LRAT.instBEqAction.beq (Std.Tactic.BVDecide.LRAT.Action.addEmpty a a_1) (Std.Tactic.BVDecide.LRAT.Action.addEmpty b b_1) = (a == b && a_1 == b_1)
• Std.Tactic.BVDecide.LRAT.instBEqAction.beq (Std.Tactic.BVDecide.LRAT.Action.addRup a a_1 a_2) (Std.Tactic.BVDecide.LRAT.Action.addRup b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Std.Tactic.BVDecide.LRAT.instBEqAction.beq (Std.Tactic.BVDecide.LRAT.Action.del a) (Std.Tactic.BVDecide.LRAT.Action.del b) = (a == b)
• Std.Tactic.BVDecide.LRAT.instBEqAction.beq x✝¹ x✝ = false

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

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

instance Std.Tactic.BVDecide.LRAT.instToStringAction {β : Type u_1} {α : Type u_2} [ToString β] [ToString α] : ToString (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