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

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.

source

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