@[reducible, inline]

abbrev Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction (n : Nat) : Type

Action where variables have type PosFin n, clauses are DefaultClause, and ids are Nat. This Action type is meant to be usable for verifying LRAT proofs that operate on default formulas.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n = Std.Tactic.BVDecide.LRAT.Action (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

def Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction {α : Type u_1} {β : Type u_2} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] : Std.Tactic.BVDecide.LRAT.Action β α → Prop

A predicate for Actions that ensures that the pivot of a clause is always included in the clause. In the LRAT format, the clause's pivot is always its first literal. However, from an interface perspective, it is awkward to require that all Clause implementations preserve the ordering of their literals. It is also awkward to have the pivot in the addRat action not included in the clause itself, since then the pivot would need to be readded to the clause when it is added to the formula. So to avoid imposing awkward constraints on the Clause interface, and to avoid requiring Formula implementations to add pivots to the clauses provided by the addRat action, we use this predicate to indicate that the pivot provided by the addRat action is indeed in the provided clause.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction (Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints) = Std.Tactic.BVDecide.LRAT.Internal.Limplies α p c
• Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction x = True

def Std.Tactic.BVDecide.LRAT.Internal.natLiteralToPosFinLiteral {n : Nat} (x : Std.Sat.Literal Nat) (x_ne_zero : x.fst ≠ 0) : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))

Equations

• Std.Tactic.BVDecide.LRAT.Internal.natLiteralToPosFinLiteral x x_ne_zero = if h : x.fst < n then some (⟨x.fst, ⋯⟩, x.snd) else none

def Std.Tactic.BVDecide.LRAT.Internal.intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))

Equations

• Std.Tactic.BVDecide.LRAT.Internal.intToLiteralPure x x_ne_zero = if h : x.natAbs < n then if x > 0 then some (⟨x.natAbs, ⋯⟩, true) else some (⟨x.natAbs, ⋯⟩, false) else none

def Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction (n : Nat) : Std.Tactic.BVDecide.LRAT.IntAction → Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)

Since IntAction is a convenient parsing target and DefaultClauseAction is a useful Action type for working with default clauses, an expected workflow pattern is to parse an external LRAT proof into a list of IntActions, and then use this function to convert that list of IntActions to DefaultClauseActions.

This function returns an Option type so that none can be returned if converting from the IntAction to DefaultClauseAction fails. This can occur if any of the literals in the IntAction are 0 or ≥ n.

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n (Std.Tactic.BVDecide.LRAT.Action.addEmpty cId rupHints) = some (Std.Tactic.BVDecide.LRAT.Action.addEmpty cId rupHints)
• Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n (Std.Tactic.BVDecide.LRAT.Action.del ids) = some (Std.Tactic.BVDecide.LRAT.Action.del ids)