Std.Tactic.BVDecide.LRAT.Actions

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.

source

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

Instances For

source

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.Action.addEmpty default default }

source

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.beqAction✝ }

source

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.reprAction✝ }

source

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 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 ""

source

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 }

source

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

Instances For

Lean.Elab.Tactic.BVDecide.Frontend.instToExprIntAction