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.
β
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
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 }
Equations
- Std.Tactic.BVDecide.LRAT.instBEqAction = { beq := Std.Tactic.BVDecide.LRAT.beqAction✝ }
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 α]
:
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 ""