def Duper.kFair : Nat

Equations

• Duper.kFair = 70

def Duper.kBest : Nat

Equations

• Duper.kBest = 3

def Duper.kHighest : Nat

Equations

• Duper.kHighest = 10

opaque Duper.forceProbeRetry : Lean.Option Nat

def Duper.getForceProbeRetry (opts : Lean.Options) : Nat

Equations

• Duper.getForceProbeRetry opts = Lean.Option.get opts Duper.forceProbeRetry

def Duper.logForceProbeRetry (max : Nat) : Lean.CoreM Unit

Equations

• Duper.logForceProbeRetry max = Lean.logInfo ((Lean.MessageData.ofFormat ∘ Std.format) (toString "forceProbe exceeded iteration limit " ++ toString max ++ toString ""))

opaque Duper.kStep : Lean.Option Nat

@[reducible, inline]

abbrev Duper.ClauseProof : Type

Equations

• Duper.ClauseProof = (Duper.Clause × Duper.Clause × Duper.RuleM.Proof)

def Duper.ClauseStream.takeAsProverM (cs : ClauseStream) : ProverM.ProverM (Option (Option ClauseProof × ClauseStream))

Equations

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

instance Duper.instOptionMStreamProverMClauseStreamClauseProof : OptionMStream ProverM.ProverM ClauseStream ClauseProof

Equations

• Duper.instOptionMStreamProverMClauseStreamClauseProof = { next? := fun (s : Duper.ClauseStream) => s.takeAsProverM }

def Duper.penalty (c : Clause) : ProverM.ProverM Nat

Equations

• Duper.penalty c = pure 1

def Duper.updateWeight (α? : Option ClauseProof) (weight nProbed : Nat) : ProverM.ProverM Nat

Equations

• Duper.updateWeight (some (clause, snd)) weight nProbed = do let __do_lift ← Duper.penalty clause pure (weight + __do_lift * Nat.max 1 (nProbed - 64))
• Duper.updateWeight α? weight nProbed = pure (weight + Nat.max 2 (nProbed - 16))

def Duper.ClauseStreamHeap.extractClause {σ : Type} [OptionMStream ProverM.ProverM σ ClauseProof] (Q : ClauseStreamHeap σ) (nProbed : Nat) (precs : Array Nat) (s : σ) : ProverM.ProverM (Option ClauseProof × ClauseStreamHeap σ)

Following Making Higher-Order Superposition Work. Extract an Option Clause from the stream. Add the rest of the stream to the heap.

Equations

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

def Duper.ClauseStreamHeap.heuristicProbe {σ : Type} [OptionMStream ProverM.ProverM σ ClauseProof] (Q : ClauseStreamHeap σ) : ProverM.ProverM (Array ClauseProof × ClauseStreamHeap σ)

Equations

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

def Duper.ClauseStreamHeap.fairProbe {σ : Type} [OptionMStream ProverM.ProverM σ ClauseProof] (nOldest : Nat) (Q : ClauseStreamHeap σ) : ProverM.ProverM (Array ClauseProof × ClauseStreamHeap σ)

Equations

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

def Duper.ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit

Here c is simplifiedGivenClause. This function is responsible for adding results of inference rules to the passive set.

Equations

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

def Duper.ProverM.performInferences (rules : List (Clause → MClause → Nat → RuleM.RuleM (Array ClauseStream))) (given : Clause) : ProverM Unit

Equations

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

def Duper.ProverM.runProbe (probe : ClauseStreamHeap ClauseStream → ProverM (Array ClauseProof × ClauseStreamHeap ClauseStream)) : ProverM PUnit

Equations

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

def Duper.ProverM.runForceProbe : ProverM Unit

We have to repeatedly call runProbe and test (← getPassiveSet).isEmpty If we return immediately when fairProbe yields a nonempty list of clauses, it is possible that all of these clauses are redundant and postProcessInferenceResult will remove all of them, which will cause saturate to think that the prover has saturated.

Equations

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