opaque duper.maxSaturationTime : Lean.Option Nat

def Duper.ProverM.getMaxSaturationTime (opts : Lean.Options) : Nat

Equations

• Duper.ProverM.getMaxSaturationTime opts = Lean.Option.get opts duper.maxSaturationTime * 1000

def Duper.ProverM.logSaturationTimeout (max : Nat) : Lean.CoreM Unit

Equations

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

def Duper.ProverM.checkSaturationTimeout (startTime : Nat) : Lean.CoreM Bool

Equations

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

opaque Duper.ProverM.maxSaturationIteration : Lean.Option Nat

def Duper.ProverM.getMaxSaturationIteration (opts : Lean.Options) : Nat

Equations

• Duper.ProverM.getMaxSaturationIteration opts = Lean.Option.get opts Duper.ProverM.maxSaturationIteration

def Duper.ProverM.checkSaturationIterout (iter : Nat) : Lean.CoreM Bool

Used to check that the current instance of duper does not exceed the number of iterations allocated to it.

Equations

• Duper.ProverM.checkSaturationIterout iter = do let opts ← Lean.getOptions let maxiter : Nat := Duper.ProverM.getMaxSaturationIteration opts pure (decide (iter > maxiter))

def Duper.ProverM.checkInstanceMaxHeartbeats (initHeartbeats instanceMaxHeartBeats : Nat) : ProverM Bool

Used to check that the current instance of duper does not exceed the number of heartbeats allocated to it (which may be less than the overall tactic's max heartbeats if duper is running in portfolio mode). Returns true if this duper instance has exceeded its instance heartbeat allocation.

Equations

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

def Duper.ProverM.checkSaturationTerminationCriterion : ProverM Bool

Throws an error if duper has exceeded the total allowed max heartbeats, and returns true if duper has exeeded the max heartbeats or max iterations for this instance of duper. Returns false if neither of these are the case and duper may proceed

Equations

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

def Duper.ProverM.printTimeoutDebugStatements : ProverM Unit

Equations

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

def Duper.ProverM.forwardSimpRules : ProverM (Array SimpRule)

Equations

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

def Duper.ProverM.inferenceRules : ProverM (List (Clause → MClause → Nat → RuleM.RuleM (Array ClauseStream)))

Equations

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

def Duper.ProverM.applyForwardSimpRules (givenClause : Clause) : ProverM (SimpResult Clause)

Equations

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

partial def Duper.ProverM.forwardSimplify (givenClause : Clause) : ProverM (Option (Clause × Bool))

Uses other clauses in the active set to attempt to simplify the given clause. Returns some simplifiedGivenClause if forwardSimplify is able to use simplification rules to transform givenClause to simplifiedGivenClause. Returns none if forwardSimplify is able to use simplification rules to show that givenClause is unneeded.

In addition to returning the simplifiedGivenClause, forwardSimplify also returns a Bool which indicates whether the clause can safely be used to simplify away other clauses.

def Duper.ProverM.saturate : ProverM Unit

Equations

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

def Duper.ProverM.clausifyThenSaturate : ProverM Unit

Note: This definition is outdated (does not support datatype exhaustiveness reasoning). See saturateNoPreprocessingClausification for additions that need to be made to make this usable.

Equations

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

def Duper.ProverM.saturateNoPreprocessingClausification (withDatatypeExhaustivenessFacts : Bool) : ProverM Unit

Equations

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