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

Instances For

source

instance Std.Tactic.BVDecide.LRAT.instInhabitedAction :

{a : Type u_1} → {a_1 : Type u_2} → Inhabited (Std.Tactic.BVDecide.LRAT.Action a a_1)

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} → [inst : BEq β] → [inst : BEq α] → BEq (Std.Tactic.BVDecide.LRAT.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} → [inst : Repr β] → [inst : Repr α] → Repr (Std.Tactic.BVDecide.LRAT.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 α] :

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

source

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 }

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