def Duper.ProverM.preprocessingForwardSimpRules : Array SimpRule

A restricted set of forward simplification rules that should be applied to unsupoorted facts that go directly into the active set (because they are not intended to be part of the set of support).

Equations

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

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

Equations

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

partial def Duper.ProverM.preprocessUnsupportedFact (c : Clause) : ProverM (Option (Clause × Bool))

Simplifies c using preprocessingForwardSimpRules. Returns some c' if preprocessUnsupportedFact is able to use simplification rules to transform c to c'. Returns none if preprocessUnsupportedFact is able to use simplification rules to show that c is unneeded.

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

def Duper.ProverM.preprocessUnsupportedFacts : ProverM Unit

Iterates through all facts in unsupportedFacts and clausifies them (as well as performs other cheap forward simplification rules), adding the resulting clauses directly to the active set (because they clauses are not intended to be part of the set of support).

Equations

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

def Duper.ProverM.preprocessingClausification : ProverM Unit

Naively applies clausificationStep.toSimpRule to everything in the passive set (and everything produced by clausifying clauses in the passive set) without removing anything from the passive set. This preprocessing clausification is not necessary (and might be removed later if it turns out to use more time than it saves), but it may be useful to make the KBO precedence and weight generation heuristics more accurate (e.g. preprocessing clausification will ensure that ¬ is not selected as the unary symbol with highest precedence)

Equations

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

partial def Duper.ProverM.preprocessingClausification.clausifyToFixedPoint (c : Clause) : ProverM (Option Clause)

partial def Duper.ProverM.updateSymbolFreqArityMap (f : Lean.Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat)) : ProverM (Std.HashMap Symbol (Nat × Nat))

Updates symbolFreqArityMap to increase the count of all symbols that appear in f (and if a symbol in f appears n times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight, this function may require revision to be more similar to Zipperposition's implementation once we actually start working on higher order things.

def Duper.ProverM.isInductiveAndNonPropAndNotTypeClass (t : Lean.Expr) : ProverM Bool

Checks whether the type t is an inductive datatype that is neither a type class nor a Prop

Equations

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

partial def Duper.ProverM.updateSymbolFreqArityMapAndDatatypeList (f : Lean.Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat)) (datatypeList : List (Lean.Expr × Array Lean.Name)) (paramNames : Array Lean.Name) : ProverM (Std.HashMap Symbol (Nat × Nat) × List (Lean.Expr × Array Lean.Name))

Updates symbolFreqArityMap to increase the count of all symbols that appear in f (and if a symbol in f appears n times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight, this function may require revision to be more similar to Zipperposition's implementation once we actually start working on higher order things. Additionally, updates datatypeList to make sure that all inductive datatypes that appear in the problem are contained in the datatypeList. The format in which inductive datatypes are recorded as elements of type Expr × Array Name is described in the comment above buildSymbolFreqArityMapAndDatatypeList

def Duper.ProverM.buildSymbolFreqArityMap (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat))

Builds a HashMap that maps each symbol to a tuple containing:

• The number of times they appear in formulas
• Its arity

Equations

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

def Duper.ProverM.buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat) × List (Lean.Expr × Array Lean.Name))

Builds:

• A HashMap that maps each symbol to a tuple containing:
  • The number of times they appear in formulas
  • Its arity
• A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented as universally quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype List α of where α : Type u is represented via ((∀ (α : Type u), List α), #[u])

Equations

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

def Duper.ProverM.buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)

Builds the symbolPrecMap from the input assumptions. Note that lower numbers in the symbol prec map correspond to higher precedences (so that symbol s is maximal iff s maps to 0).

In addition to returning the symbolPrecMap itself, we also return a boolean that indicates whether the highest precedence symbol has arity zero (i.e. is a first-order constant). This is necessary because if it is, then the firstmaximal0 weight generation scheme cannot be used.

Equations

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

def Duper.ProverM.buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolPrecMap × Bool × List (Lean.Expr × Array Lean.Name))

Like buildSymbolPrecMap but it also returns a list of all inductive datatypes that appear in any clause. Polymorphic inductive datatypes are represented as universally quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype List α of where α : Type u is represented via ((∀ (α : Type u), List α), #[u])

Equations

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