Another clause selection strategy update

Duper/ProverM.lean

@@ -316,17 +316,17 @@ def addNewToPassive (c : Clause) (proof : Proof) (generationNumber : Nat) (gener
       let ci := {ci with generatingAncestors := generatingAncestors, isOrphan := false}
       setAllClauses ((← getAllClauses).insert c ci)
       markAsDescendantToGeneratingAncestors c generatingAncestors -- For each generating ancestor of c, add c as a descendant of said ancestor
-      setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number)
+      setPassiveSet $ (← getPassiveSet).insert c c.weight ci.generationNumber ci.number
     else pure () -- c exists in allClauses and is not an orphan, so it has already been produced and can safely be ignored
   | none =>
     let ci ← addNewClause c proof generationNumber generatingAncestors
-    setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number)
+    setPassiveSet $ (← getPassiveSet).insert c c.weight ci.generationNumber ci.number
 
 /-- Takes a clause that was generated by preprocessing clausification and re-adds it to the passive set and its associated heaps -/
 def addClausifiedToPassive (c : Clause) : ProverM Unit := do
   match (← getAllClauses).find? c with
   | some ci =>
-    setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number)
+    setPassiveSet $ (← getPassiveSet).insert c c.weight ci.generationNumber ci.number
   | none => throwError "Unable to find information for clausified clause {c}"
 
 def ProverM.runWithExprs (x : ProverM α) (es : List (Expr × Expr × Array Name)) (ctx : Context) (s : State) : MetaM (α × State) := do

Duper/Tests/test_regression.lean

@@ -540,9 +540,8 @@ def neg3 : g (True → True) (fun _ => True.intro) = g (True → True) (fun _ =>
 end NegativeBoolSimpTests
 
 /- ClauseStreamHeap tests -/
-set_option maxHeartbeats 250000 in
 tptp MGT008 "../TPTP-v8.0.0/Problems/MGT/MGT008+1.p"
-  by duper [*] {portfolioInstance := 3} -- Runs out of time if run in portfolio mode
+  by duper [*] {portfolioInstance := 5} -- Runs out of time if run in portfolio mode
 
 example (f : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat)
   (g : Nat → Nat → Nat → Nat → Nat → Nat)

Duper/Util/StrategyHeap.lean

@@ -6,32 +6,32 @@ open Std
 
 namespace Duper
 
-/-- The age of each clause will be treated as a tuple of Nats. The first Nat in the tuple will be the
-    number of inference (not simplification) rules that have been used to generate the clause. The second
-    Nat in the tuple will be the clause id (lower ids are created before greater ids). This method is
-    used rather than just using the clause id (which would be a fair measure of Age) because empirically,
-    having generation number (the number of inference rules used to generate a clause) be a consideration in
-    clause selection helps problems where there are large facts that aren't clausified all at once (e.g. if
-    a clause has lit `p ↔ q`, then two clauses will be generated via clausification, and it can take a very
-    long time for the second one to be selected).
-
-    Note: This current strategy does not guarantee total fairness in the presence of inference rules that can
-    generate infinitely many children.
-
-    TODO: Rather than make the generation number the first Nat in an age heap, just add an additional generation
-    heap to be used in addition to the weight and age heaps. The age heap would then guarantee fairness and the
-    generation heap would hopefully confer the same empirical benefits that this strategy has over just using
-    clause id for fairness. -/
-def Age := Nat × Nat
-def Age.le (x y : Age) : Bool := x.1 < y.1 || (x.1 = y.1 && x.2 ≤ y.2)
-
--- `StrategyHeap` models GivenClause Selection
+inductive ClauseSelectionStrategy where
+  | Weight
+  | Age
+  | Generation
+  deriving Inhabited
+
+open ClauseSelectionStrategy
+
+/-- `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).
+    - 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). -/
 structure StrategyHeap (α : Type u) {β : Type} [BEq α] [Hashable α] where
   set             : HashSet α := HashSet.empty -- Set of elements of `α`
   weightheap      : BinomialHeap (Nat × α) fun c d => c.1 ≤ d.1 := BinomialHeap.empty
-  ageheap         : BinomialHeap (Age × α) (fun c d => Age.le c.1 d.1) := BinomialHeap.empty
+  generationheap  : BinomialHeap ((Nat × Nat) × α) fun c d => c.1.1 < d.1.1 || (c.1.1 = d.1.1 && c.1.2 ≤ d.1.2) := BinomialHeap.empty
+  ageheap         : BinomialHeap (Nat × α) fun c d => c.1 ≤ d.1 := BinomialHeap.empty
   status          : β
-  strategy        : β → Bool × β
+  strategy        : β → ClauseSelectionStrategy × β
   deriving Inhabited
 
 @[inline] def StrategyHeap.isEmpty [BEq α] [Hashable α]
@@ -47,64 +47,82 @@ def StrategyHeap.toList [BEq α] [Hashable α]
   (sh : StrategyHeap α (β:=β)) := sh.set.toList
 
 @[inline] def StrategyHeap.insert [BEq α] [Hashable α]
-  (sh : StrategyHeap α (β:=β)) (x : α) (weight : Nat) (age : Age) : StrategyHeap α (β:=β) :=
+  (sh : StrategyHeap α (β:=β)) (x : α) (weight generation age : Nat) : StrategyHeap α (β:=β) :=
   {sh with set := sh.set.insert x,
+           weightheap := sh.weightheap.insert (weight, x),
            ageheap := sh.ageheap.insert (age, x),
-           weightheap := sh.weightheap.insert (weight, x)}
+           generationheap := sh.generationheap.insert ((generation, age), x)}
 
 @[inline] def StrategyHeap.erase [BEq α] [Hashable α]
   (sh : StrategyHeap α (β:=β)) (x : α) : StrategyHeap α (β:=β) :=
   {sh with set := sh.set.erase x}
 
 @[inline] partial def StrategyHeap.pop? [BEq α] [Hashable α]
   (sh : StrategyHeap α (β:=β)) : Option (α × StrategyHeap α (β:=β)) := Id.run <| do
-  let (hid, status') := sh.strategy sh.status
-  if hid then
+  match sh.strategy sh.status with
+  | (Weight, status') =>
     let mut heap := sh.weightheap
     while true do
       if let some (x, h') := heap.deleteMin then
         let x := x.2
         if sh.set.contains x then
           return (x, {sh with set := sh.set.erase x,
-                              weightheap := heap,
+                              weightheap := h',
                               status := status'})
         else
           heap := h'
       else
         break
     return none
-  else
+  | (Age, status') =>
     let mut heap := sh.ageheap
     while true do
       if let some (x, h') := heap.deleteMin then
         let x := x.2
         if sh.set.contains x then
           return (x, {sh with set := sh.set.erase x,
-                              ageheap := heap,
+                              ageheap := h',
+                              status := status'})
+        else
+          heap := h'
+      else
+        break
+    return none
+  | (Generation, status') =>
+    let mut heap := sh.generationheap
+    while true do
+      if let some (x, h') := heap.deleteMin then
+        let x := x.2
+        if sh.set.contains x then
+          return (x, {sh with set := sh.set.erase x,
+                              generationheap := h',
                               status := status'})
         else
           heap := h'
       else
         break
     return none
 
--- The clause heap, for givenClause selection
--- The size of `heaps` should be 2. The first heap is the
---   weight heap and the second heap is the age heap
+/-- A strategy heap that uses a fairnessCounter for its status -/
 abbrev FairAgeHeap (α : Type u) [BEq α] [Hashable α]
   := StrategyHeap α (β:=Nat)
 
 abbrev FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairAgeHeap α :=
-  -- status : fairnessCounter
-  -- true   : weight heap
-  -- false  : age heap
-  { status := 0, strategy := fun b => if b >= fN then (false, 0) else (true, b + 1)}
+  /- Choose weight heap most of the time. Choose generation heap when the fairness counter is fN - 1
+     and choose the age heap when the fairness counter is fN. When the fairness counter reaches fN, reset
+     back to 0. -/
+  let strategy :=
+    fun fairnessCounter =>
+      if fairnessCounter = fN - 1 then (Generation, fN)
+      else if fairnessCounter ≥ fN then (Age, 0)
+      else (Weight, fairnessCounter + 1)
+  { status := 0, strategy := strategy }
 
 -- Test
 private def heap₁ := Id.run <| do
   let mut fah := FairAgeHeap.empty Nat 3
   for i in List.range 40 do
-    fah := fah.insert i (2 * i) (0, 100 - (i - 20) * (i - 20))
+    fah := fah.insert i (2 * i) 0 (100 - (i - 20) * (i - 20))
   return fah
 
 private def testheap₁ : IO Unit := do

DuperOnMathlib/DuperOnMathlib/Function.lean

@@ -58,9 +58,8 @@ example : f '' (f ⁻¹' u) ⊆ u := by
   rintro y ⟨x, xmem, rfl⟩
   exact xmem
 
--- Zipperposition (non-portfolio): 27 iterations in 0.083s
 example : f '' (f ⁻¹' u) ⊆ u := by
-  duper [subset_def, mem_image, mem_preimage] {portfolioInstance := 2}
+  duper [subset_def, mem_image, mem_preimage]
 
 example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
   intro y yu

DuperOnMathlib/DuperOnMathlib/Prime.lean

@@ -8,9 +8,11 @@ set_option auto.tptp.solver.name "zipperposition"
 
 #check Nat.prime_def_lt -- Reproving this theorem using duper:
 
+/- Note: This example struggles when full preprocessing is enabled. It can be solved reasonably quickly
+   if preprocessing is set to monomorphization or no_preprocessing -/
 theorem prime_def_lt_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 := by
   have : 2 ≤ p → 0 < p := by intro; linarith
-  duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl] {portfolioInstance := 9}
+  duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl] {preprocessing := monomorphization}
 
 #check Nat.prime_def_lt' -- Reproving this theorem using duper:
 

DuperOnMathlib/DuperOnMathlib/Prime2.lean

@@ -3,9 +3,6 @@ import Mathlib.Data.Nat.Prime
 
 set_option includeExpensiveRules false
 
-/- Duper can solve this theorem when `preprocessFact` in Util.Reduction.lean is disabled (set to the identity function).
-   When `preprocessFact` runs as it usually does, Duper times out when attempting to solve this theorem. Previously,
-   there were PANIC error messages caused by Duper's precCompare being incomplete, but those issues have since been resolved. -/
 theorem prime_def_lt''_new {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ : m ∣ p), m = 1 ∨ m = p := by
   have h1 : (1 : Nat) < 2 := @one_lt_two Nat _ _ _ _ _
   have h2 : ∀ {a b c : ℕ}, a < b → b ≤ c → a < c := @LT.lt.trans_le Nat _
@@ -23,6 +20,8 @@ theorem prime_def_lt''_new {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ :
 
 set_option reduceInstances false
 
+-- Previously, turning reduceInstances off was sufficient to solve this problem.
+-- TODO: Look into why duper no longer solves it
 theorem prime_def_lt''_new2 {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ : m ∣ p), m = 1 ∨ m = p := by
   have h1 : (1 : Nat) < 2 := @one_lt_two Nat _ _ _ _ _
   have h2 : ∀ {a b c : ℕ}, a < b → b ≤ c → a < c := @LT.lt.trans_le Nat _