This module contains the definition of the Formula typeclass. It is the interface that needs to be satisfied by any LRAT implementation that can be used by the generic LRATChecker module.

class Std.Tactic.BVDecide.LRAT.Internal.Formula (α : outParam (Type u)) (β : outParam (Type v)) [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (σ : Type w) [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] : Type (max (max u v) w)

Typeclass for formulas. An instance [Formula α β σ] indicates that σ is the type of a formula with variables of type α, clauses of type β, and clause ids of type Nat.

• toList : σ → List β

  A function used exclusively for defining Formula's satisfiability semantics.

• ReadyForRupAdd : σ → Prop

  A predicate that indicates whether a formula can soundly be passed into performRupAdd.

• ReadyForRatAdd : σ → Prop

  A predicate that indicates whether a formula can soundly be passed into performRatAdd.

• ofArray : Array (Option β) → σ
• readyForRupAdd_ofArray : ∀ (arr : Array (Option β)), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)
• readyForRatAdd_ofArray : ∀ (arr : Array (Option β)), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)
• insert : σ → β → σ
• insert_iff : ∀ (f : σ) (c1 c2 : β), c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c1) ↔ c2 = c1 ∨ c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f
• readyForRupAdd_insert : ∀ (f : σ) (c : β), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)
• readyForRatAdd_insert : ∀ (f : σ) (c : β), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)
• delete : σ → Array Nat → σ
• delete_subset : ∀ (f : σ) (arr : Array Nat) (c : β), c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr) → c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f
• readyForRupAdd_delete : ∀ (f : σ) (arr : Array Nat), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)
• readyForRatAdd_delete : ∀ (f : σ) (arr : Array Nat), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)
• formulaEntails_def : ∀ (p : α → Bool) (f : σ), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f = (((Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f).all fun (c : β) => decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) = true)
• performRupAdd : σ → β → Array Nat → σ × Bool
• rupAdd_result : ∀ (f : σ) (c : β) (rupHints : Array Nat) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) → f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c
• rupAdd_sound : ∀ (f : σ) (c : β) (rupHints : Array Nat) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) → Std.Tactic.BVDecide.LRAT.Internal.Liff α f f'
• performRatAdd : σ → β → Std.Sat.Literal α → Array Nat → Array (Nat × Array Nat) → σ × Bool
• ratAdd_result : ∀ (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) → f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c
• ratAdd_sound : ∀ (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) → Std.Tactic.BVDecide.LRAT.Internal.Equisat α f f'

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_ofArray {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (arr : Array (Option β)), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_ofArray {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (arr : Array (Option β)), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.insert_iff {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c1 c2 : β), c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c1) ↔ c2 = c1 ∨ c2 ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_insert {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_insert {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.delete_subset {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (arr : Array Nat) (c : β), c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr) → c ∈ Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_delete {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (arr : Array Nat), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRatAdd_delete {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (arr : Array Nat), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f arr)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.formulaEntails_def {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (p : α → Bool) (f : σ), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f = (((Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f).all fun (c : β) => decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) = true)

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.rupAdd_result {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β) (rupHints : Array Nat) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) → f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.rupAdd_sound {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β) (rupHints : Array Nat) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints = (f', true) → Std.Tactic.BVDecide.LRAT.Internal.Liff α f f'

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.ratAdd_result {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) → f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.ratAdd_sound {α : outParam (Type u)} {β : outParam (Type v)} : ∀ {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w} {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : σ), Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f → p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c → Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) → Std.Tactic.BVDecide.LRAT.Internal.Equisat α f f'