From bdf00f484e3ae9e93fa98b8f2152d9a1a0123604 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 14 Nov 2023 16:36:00 -0500 Subject: [PATCH] Another clause selection strategy update --- Duper/ProverM.lean | 6 +- Duper/Tests/test_regression.lean | 3 +- Duper/Util/StrategyHeap.lean | 92 ++++++++++++--------- DuperOnMathlib/DuperOnMathlib/Function.lean | 3 +- DuperOnMathlib/DuperOnMathlib/Prime.lean | 4 +- DuperOnMathlib/DuperOnMathlib/Prime2.lean | 5 +- 6 files changed, 65 insertions(+), 48 deletions(-) diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean index 37446a3..bdcb939 100644 --- a/Duper/ProverM.lean +++ b/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 diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 0028e95..f5ef2dc 100644 --- a/Duper/Tests/test_regression.lean +++ b/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) diff --git a/Duper/Util/StrategyHeap.lean b/Duper/Util/StrategyHeap.lean index b8515db..3dafa2b 100644 --- a/Duper/Util/StrategyHeap.lean +++ b/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,10 +47,11 @@ 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 α (β:=β) := @@ -58,29 +59,43 @@ def StrategyHeap.toList [BEq α] [Hashable α] @[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' @@ -88,23 +103,26 @@ def StrategyHeap.toList [BEq α] [Hashable α] 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 diff --git a/DuperOnMathlib/DuperOnMathlib/Function.lean b/DuperOnMathlib/DuperOnMathlib/Function.lean index a92dfd1..0e5c274 100644 --- a/DuperOnMathlib/DuperOnMathlib/Function.lean +++ b/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 diff --git a/DuperOnMathlib/DuperOnMathlib/Prime.lean b/DuperOnMathlib/DuperOnMathlib/Prime.lean index f15ae33..94fa275 100644 --- a/DuperOnMathlib/DuperOnMathlib/Prime.lean +++ b/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: diff --git a/DuperOnMathlib/DuperOnMathlib/Prime2.lean b/DuperOnMathlib/DuperOnMathlib/Prime2.lean index 89ecf6d..c66a688 100644 --- a/DuperOnMathlib/DuperOnMathlib/Prime2.lean +++ b/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 _