inductive Duper.ClauseSelectionStrategy : Type

• Weight : ClauseSelectionStrategy
• Age : ClauseSelectionStrategy
• Generation : ClauseSelectionStrategy

instance Duper.instInhabitedClauseSelectionStrategy : Inhabited ClauseSelectionStrategy

Equations

• Duper.instInhabitedClauseSelectionStrategy = { default := Duper.ClauseSelectionStrategy.Weight }

structure Duper.StrategyHeap (α : Type u) {β : Type} [BEq α] [Hashable α] : Type u

StrategyHeap models GivenClause Selection. StrategyHeap contains 3 internal heaps: a weight heap, a generation heap, and an age heap.

• The weight heap is used to select the "smallest" clause (with ties chosen arbitrarily). Here, "smallest" does not exactly refer to KBO size but instaed refers to size with penalties given by various clause selection heuristics. The "weight" of each clause, as used by this heap, is calculated in Clause.selectionPrecedence in Clause.lean.
• The generation heap is used to select the clause that has been generated with the fewest inferences (with older clauses being preferred over younger as a tiebreaker).
• The age heap is used to select the oldest clause.

Only the age heap is required for fairness, but empirically, it is best to usually select the smallest clause, and we've also found the generation heap helpful for making sure that Duper considers large facts that can't be clausified all at once (for instance, if a clause has a lit p ↔ q, then two clauses will be generated via clausification and if p and q are large, it can take a very long time for the second one to be selected).

• set : Std.HashSet α
• weightheap : Batteries.BinomialHeap (Nat × α) fun (c d : Nat × α) => decide (c.fst ≤ d.fst)
• generationheap : Batteries.BinomialHeap ((Nat × Nat) × α) fun (c d : (Nat × Nat) × α) => decide (c.fst.fst < d.fst.fst) || decide (c.fst.fst = d.fst.fst) && decide (c.fst.snd ≤ d.fst.snd)
• ageheap : Batteries.BinomialHeap (Nat × α) fun (c d : Nat × α) => decide (c.fst ≤ d.fst)
• status : β
• strategy : β → ClauseSelectionStrategy × β

instance Duper.instInhabitedStrategyHeap {a✝ : Type u_1} {a✝¹ : Type} [Inhabited a✝¹] {a✝² : BEq a✝} {a✝³ : Hashable a✝} : Inhabited (StrategyHeap a✝)

Equations

• Duper.instInhabitedStrategyHeap = { default := { set := default, weightheap := default, generationheap := default, ageheap := default, status := default, strategy := default } }

@[inline]

def Duper.StrategyHeap.isEmpty {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) : Bool

Equations

• sh.isEmpty = sh.set.isEmpty

@[inline]

def Duper.StrategyHeap.contains {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) (x : α) : Bool

Equations

• sh.contains x = sh.set.contains x

def Duper.StrategyHeap.toArray {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) : Array α

Equations

• sh.toArray = sh.set.toArray

def Duper.StrategyHeap.toList {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) : List α

Equations

• sh.toList = sh.set.toList

@[inline]

def Duper.StrategyHeap.insert {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) (x : α) (weight generation age : Nat) : StrategyHeap α

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Duper.StrategyHeap.erase {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) (x : α) : StrategyHeap α

Equations

• sh.erase x = { set := sh.set.erase x, weightheap := sh.weightheap, generationheap := sh.generationheap, ageheap := sh.ageheap, status := sh.status, strategy := sh.strategy }

@[inline]

def Duper.StrategyHeap.pop? {α : Type u_1} {β : Type} [BEq α] [Hashable α] (sh : StrategyHeap α) : Option (α × StrategyHeap α)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Duper.FairAgeHeap (α : Type u) [BEq α] [Hashable α] : Type u

A strategy heap that uses a fairnessCounter for its status

Equations

• Duper.FairAgeHeap α = Duper.StrategyHeap α

@[reducible, inline]

abbrev Duper.FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairAgeHeap α

Equations

• One or more equations did not get rendered due to their size.