inductive Duper.SubsumptionTrieFeatureValue : Type

• N : Nat → SubsumptionTrieFeatureValue
• S : Std.HashSet Lean.Expr → SubsumptionTrieFeatureValue
• M : Std.HashMap Lean.Expr Nat → SubsumptionTrieFeatureValue

instance Duper.instInhabitedSubsumptionTrieFeatureValue : Inhabited SubsumptionTrieFeatureValue

Equations

• Duper.instInhabitedSubsumptionTrieFeatureValue = { default := Duper.SubsumptionTrieFeatureValue.N default }

def Duper.SubsumptionTrieFeatureValueLe (f1 f2 : SubsumptionTrieFeatureValue) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Duper.SubsumptionTrieFeatureValueLe (Duper.SubsumptionTrieFeatureValue.N n1) (Duper.SubsumptionTrieFeatureValue.N n2) = decide (n1 ≤ n2)
• Duper.SubsumptionTrieFeatureValueLe f1 f2 = false

def Duper.SubsumptionTrieFeatureValueEq (f1 f2 : SubsumptionTrieFeatureValue) : Bool

Equations

• Duper.SubsumptionTrieFeatureValueEq (Duper.SubsumptionTrieFeatureValue.N n1) (Duper.SubsumptionTrieFeatureValue.N n2) = (n1 == n2)
• Duper.SubsumptionTrieFeatureValueEq (Duper.SubsumptionTrieFeatureValue.S s1) (Duper.SubsumptionTrieFeatureValue.S s2) = (s1.toArray == s2.toArray)
• Duper.SubsumptionTrieFeatureValueEq (Duper.SubsumptionTrieFeatureValue.M m1) (Duper.SubsumptionTrieFeatureValue.M m2) = (m1.toArray == m2.toArray)
• Duper.SubsumptionTrieFeatureValueEq f1 f2 = false

@[reducible, inline]

abbrev Duper.FeatureVector : Type

Equations

• Duper.FeatureVector = List Duper.SubsumptionTrieFeatureValue

inductive Duper.SubsumptionTrie : Type

• node (children : Array (SubsumptionTrieFeatureValue × SubsumptionTrie)) : SubsumptionTrie
• leaf (vals : Std.HashSet Clause) : SubsumptionTrie

instance Duper.instInhabitedSubsumptionTrie : Inhabited SubsumptionTrie

Equations

• Duper.instInhabitedSubsumptionTrie = { default := Duper.SubsumptionTrie.node default }

def Duper.SubsumptionTrie.SubsumptionTrieFeatureValue.format : SubsumptionTrieFeatureValue → Lean.MessageData

Equations

• Duper.SubsumptionTrie.SubsumptionTrieFeatureValue.format (Duper.SubsumptionTrieFeatureValue.N n) = Lean.toMessageData "" ++ Lean.toMessageData n ++ Lean.toMessageData ""
• Duper.SubsumptionTrie.SubsumptionTrieFeatureValue.format (Duper.SubsumptionTrieFeatureValue.S s) = Lean.toMessageData "" ++ Lean.toMessageData s.toArray ++ Lean.toMessageData ""
• Duper.SubsumptionTrie.SubsumptionTrieFeatureValue.format (Duper.SubsumptionTrieFeatureValue.M m) = Lean.toMessageData "" ++ Lean.toMessageData m.toArray ++ Lean.toMessageData ""

instance Duper.SubsumptionTrie.instToMessageDataSubsumptionTrieFeatureValue : Lean.ToMessageData SubsumptionTrieFeatureValue

Equations

• Duper.SubsumptionTrie.instToMessageDataSubsumptionTrieFeatureValue = { toMessageData := Duper.SubsumptionTrie.SubsumptionTrieFeatureValue.format }

partial def Duper.SubsumptionTrie.format : SubsumptionTrie → Lean.MessageData

instance Duper.SubsumptionTrie.instToMessageData : Lean.ToMessageData SubsumptionTrie

Equations

• Duper.SubsumptionTrie.instToMessageData = { toMessageData := Duper.SubsumptionTrie.format }

partial def Duper.SubsumptionTrie.collectSymbolsInExpr (acc : Std.HashSet Lean.Expr) (e : Lean.Expr) : Std.HashSet Lean.Expr

Inserts every variable and constant that appears in e into acc. 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.SubsumptionTrie.collectSymbolsInLit (acc : Std.HashSet Lean.Expr) (l : Lit) : Std.HashSet Lean.Expr

Inserts every variable and constant that appears in l into acc.

Equations

• Duper.SubsumptionTrie.collectSymbolsInLit acc l = Duper.SubsumptionTrie.collectSymbolsInExpr (Duper.SubsumptionTrie.collectSymbolsInExpr acc l.lhs) l.rhs

partial def Duper.SubsumptionTrie.updateDepthMapWithExpr (acc : Std.HashMap Lean.Expr Nat) (e : Lean.Expr) (curDepth : Nat := 0) : Std.HashMap Lean.Expr Nat

Updates acc with maps each symbol to its maximal depth in a clause. 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. See https://github.com/sneeuwballen/zipperposition/blob/master/src/core/FV_tree.ml#L182

def Duper.SubsumptionTrie.updateDepthMapWithLit (acc : Std.HashMap Lean.Expr Nat) (l : Lit) : Std.HashMap Lean.Expr Nat

Updates acc which maps each symbol to its maximal depth in a clause.

Equations

• Duper.SubsumptionTrie.updateDepthMapWithLit acc l = Duper.SubsumptionTrie.updateDepthMapWithExpr (Duper.SubsumptionTrie.updateDepthMapWithExpr acc l.lhs) l.rhs

partial def Duper.SubsumptionTrie.updateOccurrenceMapWithExpr (acc : Std.HashMap Lean.Expr Nat) (e : Lean.Expr) : Std.HashMap Lean.Expr Nat

Updates acc which maps each symbol to the number of times it occurs in a clause. 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.SubsumptionTrie.updateOccurrenceMapWithLit (acc : Std.HashMap Lean.Expr Nat) (l : Lit) : Std.HashMap Lean.Expr Nat

Updates acc which maps each symbol to the number of times it occurs in a clause.

Equations

• Duper.SubsumptionTrie.updateOccurrenceMapWithLit acc l = Duper.SubsumptionTrie.updateOccurrenceMapWithExpr (Duper.SubsumptionTrie.updateOccurrenceMapWithExpr acc l.lhs) l.rhs

def Duper.SubsumptionTrie.getFeatureVector (c : Clause) : FeatureVector

Equations

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

def Duper.SubsumptionTrie.getFeatureVector' (c : MClause) : FeatureVector

Identical to getFeatureVector except it is written to taken an MClause rather than a Clause

Equations

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

def Duper.SubsumptionTrie.emptyLeaf : SubsumptionTrie

Equations

• Duper.SubsumptionTrie.emptyLeaf = Duper.SubsumptionTrie.leaf ∅

def Duper.SubsumptionTrie.emptyNode : SubsumptionTrie

Equations

• Duper.SubsumptionTrie.emptyNode = Duper.SubsumptionTrie.node #[]

def Duper.SubsumptionTrie.singleton (c : Clause) (features : FeatureVector) : SubsumptionTrie

Equations

• Duper.SubsumptionTrie.singleton c [] = Duper.SubsumptionTrie.leaf (Std.HashSet.emptyWithCapacity.insert c)
• Duper.SubsumptionTrie.singleton c (fstFeature :: restFeatures) = Duper.SubsumptionTrie.node #[(fstFeature, Duper.SubsumptionTrie.singleton c restFeatures)]

def Duper.SubsumptionTrie.insert (t : SubsumptionTrie) (c : Clause) : RuleM.RuleM SubsumptionTrie

Equations

• t.insert c = Duper.SubsumptionTrie.insertHelper✝ t c (Duper.SubsumptionTrie.getFeatureVector c)

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

Equations

• t.delete c = Duper.SubsumptionTrie.deleteHelper✝ t c (Duper.SubsumptionTrie.getFeatureVector c)

def Duper.SubsumptionTrie.getPotentialSubsumingClauses (t : SubsumptionTrie) (c : Clause) : RuleM.RuleM (Array Clause)

Equations

• t.getPotentialSubsumingClauses c = Duper.SubsumptionTrie.getPotentialSubsumingClausesHelper✝ t (Duper.SubsumptionTrie.getFeatureVector c)

def Duper.SubsumptionTrie.getPotentialSubsumingClauses' (t : SubsumptionTrie) (c : MClause) : RuleM.RuleM (Array Clause)

Identical to getPotentialSubsumingClauses except it takes an MClause rather than a Clause

Equations

• t.getPotentialSubsumingClauses' c = Duper.SubsumptionTrie.getPotentialSubsumingClausesHelper✝ t (Duper.SubsumptionTrie.getFeatureVector' c)

def Duper.SubsumptionTrie.getPotentialSubsumedClauses (t : SubsumptionTrie) (c : Clause) : RuleM.RuleM (Array Clause)

Equations

• t.getPotentialSubsumedClauses c = Duper.SubsumptionTrie.getPotentialSubsumedClausesHelper✝ t (Duper.SubsumptionTrie.getFeatureVector c)

def Duper.SubsumptionTrie.getPotentialSubsumedClauses' (t : SubsumptionTrie) (c : MClause) : RuleM.RuleM (Array Clause)

Identical to getPotentialSubsumedClauses except that it takes an MClause rather than a Clause

Equations

• t.getPotentialSubsumedClauses' c = Duper.SubsumptionTrie.getPotentialSubsumedClausesHelper✝ t (Duper.SubsumptionTrie.getFeatureVector' c)