inductive Duper.FingerprintFeatureValue : Type

• F : Lean.Expr → FingerprintFeatureValue
• A : FingerprintFeatureValue
• B : FingerprintFeatureValue
• N : FingerprintFeatureValue

def Duper.FingerprintFeatureValue.format : FingerprintFeatureValue → Lean.MessageData

Equations

• Duper.FingerprintFeatureValue.A.format = (Lean.MessageData.ofFormat ∘ Std.format) "A"
• Duper.FingerprintFeatureValue.B.format = (Lean.MessageData.ofFormat ∘ Std.format) "B"
• Duper.FingerprintFeatureValue.N.format = (Lean.MessageData.ofFormat ∘ Std.format) "N"
• (Duper.FingerprintFeatureValue.F e).format = Lean.toMessageData "F(" ++ Lean.toMessageData e ++ Lean.toMessageData ")"

instance Duper.instToMessageDataFingerprintFeatureValue : Lean.ToMessageData FingerprintFeatureValue

Equations

• Duper.instToMessageDataFingerprintFeatureValue = { toMessageData := Duper.FingerprintFeatureValue.format }

@[reducible, inline]

abbrev Duper.Fingerprint : Type

Equations

• Duper.Fingerprint = List Duper.FingerprintFeatureValue

inductive Duper.FingerprintTrie (α : Type) [BEq α] [Hashable α] : Type

• node {α : Type} [BEq α] [Hashable α] (childA childB childN : FingerprintTrie α) (childF : Array (Lean.Expr × FingerprintTrie α)) : FingerprintTrie α
• leaf {α : Type} [BEq α] [Hashable α] (vals : Array α) : FingerprintTrie α

instance Duper.instInhabitedFingerprintTrie {a✝ : Type} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (FingerprintTrie a✝)

Equations

• Duper.instInhabitedFingerprintTrie = { default := Duper.FingerprintTrie.leaf default }

@[reducible, inline]

abbrev Duper.ClauseFingerprintTrie : Type

Equations

• Duper.ClauseFingerprintTrie = Duper.FingerprintTrie (Nat × Duper.Clause × Duper.ClausePos × Option Duper.Eligibility)

partial def Duper.FingerprintTrie.format {α : Type} [Lean.ToMessageData α] [BEq α] [Hashable α] (depth : Nat := 0) : FingerprintTrie α → Lean.MessageData

def Duper.FingerprintTrie.format.spaces (n : Nat) : String

Equations

• Duper.FingerprintTrie.format.spaces n = String.join (List.map (fun (x : Nat) => " ") (List.range n))

partial def Duper.countElems {α : Type} [BEq α] [Hashable α] : FingerprintTrie α → Nat

def Duper.foldMsgs (arr : Array Lean.MessageData) : Lean.MessageData

Equations

• Duper.foldMsgs arr = Array.foldl (fun (acc m : Lean.MessageData) => acc ++ Lean.toMessageData "\n" ++ m) (Lean.toMessageData "") arr

def Duper.FingerprintTrie.printElems {α : Type} [Lean.ToMessageData α] [BEq α] [Hashable α] (t : FingerprintTrie α) : Lean.MessageData

Equations

• t.printElems = Duper.foldMsgs (Duper.printElemsHelper✝ t)

def Duper.printVal (v : Nat × Clause × ClausePos × Option Eligibility) : Lean.MessageData

Equations

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

instance Duper.instToMessageDataProdNatClauseClausePosOptionEligibility : Lean.ToMessageData (Nat × Clause × ClausePos × Option Eligibility)

Equations

• Duper.instToMessageDataProdNatClauseClausePosOptionEligibility = { toMessageData := Duper.printVal }

instance Duper.instToMessageDataFingerprintTrie {α : Type} [Lean.ToMessageData α] [BEq α] [Hashable α] : Lean.ToMessageData (FingerprintTrie α)

Equations

• Duper.instToMessageDataFingerprintTrie = { toMessageData := Duper.FingerprintTrie.printElems }

def Duper.fingerprintFeatures : List ExprPos

Fingerprint features that will define levels of the fingerprint trie.

Equations

• Duper.fingerprintFeatures = [#[], #[0], #[1]]

def Duper.numFingerprintFeatures : Nat

Every ClauseFingerprintTrie (that isn't a subtrie of a different ClauseFingerprintTrie) must have a depth equal to numFingerprintFeatures

Equations

• Duper.numFingerprintFeatures = Duper.fingerprintFeatures.length

def Duper.mkEmptyWithDepth (d : Nat) : ClauseFingerprintTrie

Yields an empty ClauseFingerprintTrie with the given depth d

Equations

• Duper.mkEmptyWithDepth 0 = Duper.FingerprintTrie.leaf ∅
• Duper.mkEmptyWithDepth d'.succ = Duper.FingerprintTrie.node (Duper.mkEmptyWithDepth d') (Duper.mkEmptyWithDepth d') (Duper.mkEmptyWithDepth d') #[]

def Duper.emptyCFP : ClauseFingerprintTrie

Yields an empty ClauseFingerprintTrie with the correct depth

Equations

• Duper.emptyCFP = Duper.mkEmptyWithDepth Duper.numFingerprintFeatures

structure Duper.RootCFPTrie : Type

• root : ClauseFingerprintTrie
• filterSet : Std.HashSet Clause

instance Duper.instInhabitedRootCFPTrie : Inhabited RootCFPTrie

Equations

• Duper.instInhabitedRootCFPTrie = { default := { root := default, filterSet := default } }

def Duper.RootCFPTrie.gfpf {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (e : Lean.Expr) (pos : ExprPos) : m FingerprintFeatureValue

General fingerprint feature function (see: http://www.eprover.eu/EXPDATA/FP_INDEX/schulz_fp-index_ext.pdf) Note that this function assumes that e already has had its metavariables instantiated

Equations

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

def Duper.RootCFPTrie.transformToUntypedFirstOrderTerm {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (e : Lean.Expr) : m Lean.Expr

This implements the ⌊e⌋ function described in https://matryoshka-project.github.io/pubs/hounif_article.pdf. Although the ⌊e⌋ function description assumes that e is in η-long β-reduced normal form, this function assumes e is an expression on which beta, eta, and zeta reduction have been applied exhaustively. I believe that the same specification descrbied in the paper can be used with this assumption, but if it turns out I'm mistaken, we can add a step to the beginning to this function that converts e to η-long β-reduced normal form.

Note: The output of this function is not guaranteed (or expected) to be well-formed.

Equations

• One or more equations did not get rendered due to their size.
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm (Lean.Expr.forallE binderName binderType b binderInfo) = Duper.RootCFPTrie.transformToUntypedFirstOrderTerm b
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm (Lean.Expr.lam binderName binderType b binderInfo) = Duper.RootCFPTrie.transformToUntypedFirstOrderTerm b
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm (Lean.Expr.bvar bvarNum) = pure (Lean.Expr.bvar bvarNum)
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm (Lean.Expr.mdata data e_2) = Duper.RootCFPTrie.transformToUntypedFirstOrderTerm e_2
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm (Lean.Expr.const name us) = pure (Lean.Expr.const name [])
• Duper.RootCFPTrie.transformToUntypedFirstOrderTerm e = pure e

def Duper.RootCFPTrie.getFingerprint {m : Type → Type u_1} [Monad m] [MonadLiftT Lean.MetaM m] (e : Lean.Expr) : m Fingerprint

Equations

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

def Duper.RootCFPTrie.mkSingleton (f : Fingerprint) (v : Nat × Clause × ClausePos × Option Eligibility) : ClauseFingerprintTrie

Given a fingerprint f, yields a ClauseFingerprintTrie whose depth equals the length of f and whose only value is v (located at the position indiced by f)

Equations

• One or more equations did not get rendered due to their size.
• Duper.RootCFPTrie.mkSingleton [] v = Duper.FingerprintTrie.leaf #[v]

def Duper.RootCFPTrie.insertHelper (t : ClauseFingerprintTrie) (f : Fingerprint) (v : Nat × Clause × ClausePos × Option Eligibility) : RuleM.RuleM ClauseFingerprintTrie

Inserts v into t at the position indiced by fingerprint f. Throws an error if the length of f does not equal the depth of t

Equations

• One or more equations did not get rendered due to their size.
• Duper.RootCFPTrie.insertHelper (Duper.FingerprintTrie.leaf vals) [] v = pure (Duper.FingerprintTrie.leaf (vals.push v))

def Duper.RootCFPTrie.insert (t : RootCFPTrie) (e : Lean.Expr) (v : Nat × Clause × ClausePos × Option Eligibility) : RuleM.RuleM RootCFPTrie

Adds v to t.root at the location indiced by e and removes v.2.1 from t.filterSet so that previously deleted clauses can be readded

Equations

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

def Duper.RootCFPTrie.delete (t : RootCFPTrie) (c : Clause) : RuleM.RuleM RootCFPTrie

Adds c to t.filterSet so that Clause × ClausePos pairs with c as the clause are ignored going forward

Equations

• t.delete c = pure { root := t.root, filterSet := t.filterSet.insert c }

def Duper.RootCFPTrie.getUnificationPartners (t : RootCFPTrie) (e : Lean.Expr) : RuleM.RuleM (Array (Nat × Clause × ClausePos × Option Eligibility))

Returns all clause and position pairs that indicate subexpressions that may be unifiable with e

Equations

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

def Duper.RootCFPTrie.getMatchOntoPartners (t : RootCFPTrie) (e : Lean.Expr) : RuleM.RuleM (Array (Nat × Clause × ClausePos × Option Eligibility))

Returns all clause and position pairs that indicate subexpressions that e can match onto (i.e. assigning metavariables in e)

Equations

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

def Duper.RootCFPTrie.getMatchFromPartners (t : RootCFPTrie) (e : Lean.Expr) : RuleM.RuleM (Array (Nat × Clause × ClausePos × Option Eligibility))

Returns all clause and position pairs that indicate subexpressions that can be matched onto e (i.e. not assigning metavariables in e)

Equations

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