Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.Class

This module contains the definition of the Formula typeclass. It is the interface that needs to be satisified 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'

Instances

theorem Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_ofArray {α : outParam (Type u)} {β : outParam (Type v)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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)} [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] {σ : Type w} [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'