Updating clause selection strategy

There is still more work to be done on the clause selection strategy
(some of which is documented at the stop of StrategyHeap.lean), but this
commit already makes Duper able to solve one of the problems in
DuperOnMathlib/Function.lean that it couldn't before.

Duper/ClauseStreamHeap.lean

@@ -136,15 +136,23 @@ def ClauseStreamHeap.fairProbe {σ} [OptionMStream ProverM σ ClauseProof]
 -- Note: This function is responsible for adding results of inference rules to the passive set.
 def ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit := do
   let (given, c, proof) := cp
+  let allClauses ← getAllClauses
+  let parentClauseInfoOpts ← proof.parents.mapM
+    (fun p =>
+      match allClauses.find? p.clause with
+      | some pi => pure pi
+      | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause}")
+  -- c's generation number is one greater than the sum of its parents generation numbers
+  let generationNumber := parentClauseInfoOpts.foldl (fun acc parentInfo => acc + parentInfo.generationNumber) 1
   match ← immediateSimplification given c with
   | some subsumingClause => -- subsumingClause subsumes c so we can remove c and only need to add subsumingClause
     removeClause given [subsumingClause]
     if c == subsumingClause then
-      addNewToPassive c proof (proof.parents.map (fun p => p.clause))
+      addNewToPassive c proof generationNumber (proof.parents.map (fun p => p.clause))
     else
       throwError "Unable to find {subsumingClause} in resultClauses"
   | none => -- No result clause subsumes c, so add each result clause to the passive set
-    addNewToPassive c proof (proof.parents.map (fun p => p.clause))
+    addNewToPassive c proof generationNumber (proof.parents.map (fun p => p.clause))
 
 def ProverM.performInferences (rules : List (Clause → MClause → Nat → RuleM (Array ClauseStream))) (given : Clause) : ProverM Unit := do
   trace[Prover.saturate] "perform inference with given clause {given}"

Duper/ProverM.lean

@@ -33,6 +33,7 @@ open Result
 
 structure ClauseInfo where
 (number : Nat)
+(generationNumber : Nat) -- The total number of inference (not simplification) rules that were used to create this clause
 (proof : Proof)
 (generatingAncestors : Array Clause)
 (descendants : List Clause)
@@ -45,7 +46,7 @@ abbrev FairAgeClauseHeap := StrategyHeap Clause (β:=Nat)
 abbrev abstractedMVarList := List Meta.AbstractMVarsResult
 abbrev abstractedMVarAndClauseList := List (Meta.AbstractMVarsResult × Clause)
 
-instance : ToMessageData Result := 
+instance : ToMessageData Result :=
 ⟨fun r => match r with
 | unknown => "unknown"
 | saturated => "saturated"
@@ -103,6 +104,7 @@ instance [MetaEval α] : MetaEval (ProverM α) :=
 initialize
   registerTraceClass `Prover
   registerTraceClass `Prover.saturate
+  registerTraceClass `Prover.createdClauses
 
 def getInstanceMaxHeartbeats : ProverM Nat :=
   return (← get).instanceMaxHeartbeats
@@ -259,7 +261,7 @@ def markAsDescendantToGeneratingAncestors (c : Clause) (generatingAncestors : Ar
 
 /-- Registers a new clause, but does not add it to active or passive set.
     Typically, you'll want to use `addNewToPassive` instead. -/
-def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Clause) : ProverM ClauseInfo := do
+def addNewClause (c : Clause) (proof : Proof) (generationNumber : Nat) (generatingAncestors : Array Clause) : ProverM ClauseInfo := do
   markAsDescendantToGeneratingAncestors c generatingAncestors
   let allClauses ← getAllClauses
   let ci ← (do
@@ -274,6 +276,7 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus
     | none =>
       let ci : ClauseInfo := {
         number := allClauses.size
+        generationNumber := generationNumber
         proof := proof
         generatingAncestors := generatingAncestors
         descendants := []
@@ -282,7 +285,7 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus
       }
       setAllClauses (allClauses.insert c ci)
       if ← getInhabitationReasoningM then
-        if c.lits.size == 0 && c.bVarTypes.size == 0 then 
+        if c.lits.size == 0 && c.bVarTypes.size == 0 then
           setEmptyClause c
           throwEmptyClauseException
         return ci
@@ -295,11 +298,15 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus
     let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause)
     m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}"
   )
+  trace[Prover.createdClauses] (
+    let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause)
+    m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}"
+  )
   return ci
 
 /-- Registers a new clause and adds it to the passive set. The `generatingAncestors` argument contains the list of clauses that were
     used to generate `c` (or `c`'s ancestor which generated `c` by a modifying inference). See page 8 of "E – A Brainiac Theorem Prover" -/
-def addNewToPassive (c : Clause) (proof : Proof) (generatingAncestors : Array Clause) : ProverM Unit := do
+def addNewToPassive (c : Clause) (proof : Proof) (generationNumber : Nat) (generatingAncestors : Array Clause) : ProverM Unit := do
   match (← getAllClauses).find? c with
   | some ci =>
     if (ci.wasSimplified) then pure () -- No need to add c to the passive set because it would just be simplified away later
@@ -309,25 +316,25 @@ def addNewToPassive (c : Clause) (proof : Proof) (generatingAncestors : Array Cl
       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.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 generatingAncestors
-    setPassiveSet $ (← getPassiveSet).insert c c.weight ci.number
+    let ci ← addNewClause c proof generationNumber generatingAncestors
+    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.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
   ProverM.run (s := s) (ctx := ctx) do
     for (e, proof, paramNames) in es do
       let c := Clause.fromSingleExpr paramNames e
       let mkProof := fun _ _ _ _ => pure proof
-      addNewToPassive c {parents := #[], ruleName := "assumption", mkProof := mkProof} #[]
+      addNewToPassive c {parents := #[], ruleName := "assumption", mkProof := mkProof} 0 #[]
     x
 
 @[inline] def runRuleM (x : RuleM α) : ProverM.ProverM α := do
@@ -541,4 +548,4 @@ def immediateSimplification (givenClause : Clause) (resultClause : Clause) :
     return none
 
 end ProverM
-end Duper
+end Duper

Duper/Simp.lean

@@ -52,7 +52,7 @@ abbrev BackwardSimpRule := Clause → ProverM Unit
 def MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule := fun givenClause => do
   let res ← runRuleM (rule givenClause)
   match res with
-  | none => 
+  | none =>
     return Unapplicable
   | some cs => do
     trace[Simplification.debug] "About to remove {givenClause} because it was simplified away to produce {cs.map (fun x => x.1)}"
@@ -64,10 +64,12 @@ def MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule := fun givenClause => do
       | some givenClauseInfo =>
         -- For forward simplification rules, each result clause has the same set of generating ancestors as givenClause
         let generatingAncestors := givenClauseInfo.generatingAncestors
+        -- For forward simplification rules, each result clause has the same generation number as givenClause
+        let generationNumber := givenClauseInfo.generationNumber
         -- Register and return first result clause without adding it to the active or passive set. Add other result clauses to passive set
-        let ci ← addNewClause c proof generatingAncestors
+        let ci ← addNewClause c proof generationNumber generatingAncestors
         for (c, proof) in restCs do
-          addNewToPassive c proof generatingAncestors
+          addNewToPassive c proof generationNumber generatingAncestors
         if ci.wasSimplified then return Removed -- No need to continue working on c because we've already seen previously that it will be simplified away
         return Applied c
       | none => throwError "givenClause {givenClause} was not found"
@@ -77,16 +79,17 @@ def BackwardMSimpRule.toBackwardSimpRule (rule : BackwardMSimpRule) : BackwardSi
   let backwardSimpRes ← runRuleM do
     withoutModifyingMCtx do
       rule givenClause
-  let mut generatingAncestorsArray : Array (Array Clause) := #[]
+  let mut generatingNumberAndAncestorsArray : Array (Nat × Array Clause) := #[]
   -- It is important that we remove each clause in clausesToRemove before reading the newly generated clauses
   for (c, _) in backwardSimpRes do
     trace[Simplification.debug] "About to remove {c} because it was simplified away"
     removeClause c [givenClause] -- givenClause must be protected when we remove c and its descendants because givenClause was used to eliminate c
     match (← getAllClauses).find? c with
-    | some ci => generatingAncestorsArray := generatingAncestorsArray.push ci.generatingAncestors
+    | some ci =>
+      generatingNumberAndAncestorsArray := generatingNumberAndAncestorsArray.push (ci.generationNumber, ci.generatingAncestors)
     | none => throwError "Could not find {c} in all clauses"
-  for (generatingAncestors, _, ocp) in generatingAncestorsArray.zip backwardSimpRes do
+  for ((generationNumber, generatingAncestors), _, ocp) in generatingNumberAndAncestorsArray.zip backwardSimpRes do
     if let some (c, proof) := ocp then
-      addNewToPassive c proof generatingAncestors
+      addNewToPassive c proof generationNumber generatingAncestors
 
 end Duper

Duper/Tests/test_regression.lean

@@ -540,6 +540,7 @@ 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
 

Duper/Util/StrategyHeap.lean

@@ -6,11 +6,30 @@ 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
 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 (Nat × α) fun c d => c.1 ≤ d.1 := BinomialHeap.empty
+  ageheap         : BinomialHeap (Age × α) (fun c d => Age.le c.1 d.1) := BinomialHeap.empty
   status          : β
   strategy        : β → Bool × β
   deriving Inhabited
@@ -28,7 +47,7 @@ def StrategyHeap.toList [BEq α] [Hashable α]
   (sh : StrategyHeap α (β:=β)) := sh.set.toList
 
 @[inline] def StrategyHeap.insert [BEq α] [Hashable α]
-  (sh : StrategyHeap α (β:=β)) (x : α) (weight age : Nat) : StrategyHeap α (β:=β) :=
+  (sh : StrategyHeap α (β:=β)) (x : α) (weight : Nat) (age : Age) : StrategyHeap α (β:=β) :=
   {sh with set := sh.set.insert x,
            ageheap := sh.ageheap.insert (age, x),
            weightheap := sh.weightheap.insert (weight, x)}
@@ -40,31 +59,41 @@ 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
-  let mut heap := if hid then sh.weightheap else sh.ageheap
-  while true do
-    if let some (x, h') := heap.deleteMin then
-      let x := x.2
-      if sh.set.contains x then
-        if hid then
+  if hid then
+    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,
                               status := status'})
         else
+          heap := h'
+      else
+        break
+    return none
+  else
+    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,
                               status := status'})
+        else
+          heap := h'
       else
-        heap := h'
-    else
-      break
-  return none
+        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
 abbrev FairAgeHeap (α : Type u) [BEq α] [Hashable α]
   := StrategyHeap α (β:=Nat)
-  
+
 abbrev FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairAgeHeap α :=
   -- status : fairnessCounter
   -- true   : weight heap
@@ -75,7 +104,7 @@ abbrev FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairA
 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) (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
@@ -87,4 +116,4 @@ private def testheap₁ : IO Unit := do
     else
       println! "No"
 
-#eval testheap₁
+#eval testheap₁