def Duper.checkDirectMatch (l1 l2 : Lit) (protectedMVarIds : Array Lean.MVarId) : RuleM.RuleM Bool

Determines whether there is any σ such that σ(l1.lhs) = l2.lhs and σ(l1.rhs) = l2.rhs. Returns true and applies σ if so, returns false (without applying any substitution) otherwise

Equations

• Duper.checkDirectMatch l1 l2 protectedMVarIds = liftM (Lean.Meta.performMatch #[(l2.lhs, l1.lhs), (l2.rhs, l1.rhs)] protectedMVarIds)

def Duper.checkCrossMatch (l1 l2 : Lit) (protectedMVarIds : Array Lean.MVarId) : RuleM.RuleM Bool

Determines whether there is any σ such that σ(l1.rhs) = l2.lhs and σ(l1.lhs) = l2.rhs. Returns true and applies σ if so, returns false (without applying any substitution) otherwise

Equations

• Duper.checkCrossMatch l1 l2 protectedMVarIds = liftM (Lean.Meta.performMatch #[(l2.lhs, l1.rhs), (l2.rhs, l1.lhs)] protectedMVarIds)

def Duper.litsMatch (l1 l2 : Lit) (protectedMVarIds : Array Lean.MVarId) : RuleM.RuleM (Option Bool)

Determines whether σ(l1) = l2 for any substitution σ. Importantly, litsMatch can return true if l1.sign = l2.sign and either:

• σ(l1.lhs) = l2.lhs and σ(l1.rhs) = l2.rhs
• σ(l1.rhs) = l2.lhs and σ(l1.lhs) = l2.rhs In the former case, litsMatch returns some false, in the latter case, litsMatch returns some true, and if no match can be found, then it returns none

Equations

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

def Duper.litInClause (l : Lit) (c : MClause) (cMVarIds : Array Lean.MVarId) (exclude : Std.HashSet Nat) (startIdx : Nat) : RuleM.RuleM (Option (Nat × Bool))

Determines whether, for any substitution σ, σ(l) is in c at startIdx or after startIdx. If it is, then metavariables are assigned so that σ is applied and the index of σ(l) in c is returned (as well as whether a flip was necessary to perform the match). If there are multiple indices in c that l can match, then litInClause returns the first one. If there is no substitution σ such that σ(l) is in c at or after startIdx, the MetavarContext is left unchanged and none is returned.

Additionally, litInClause is not allowed to return any Nat that is part of the exclude set. This is to prevent instances in which multiple literals in the subsumingClause all map onto the same literal in the subsumedClause.

Equations

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

partial def Duper.subsumptionCheckHelper (subsumingClauseLits : List Lit) (subsumedClauseLits : MClause) (subsumedClauseMVarIds : Array Lean.MVarId) (exclude : Std.HashSet Nat) (assignment : List (Nat × Bool)) (fstStart : Nat := 0) : RuleM.RuleM (Option (List (Nat × Bool)))

Attempts to find an injective mapping f from subsumingClauseLits to subsumedClauseLits and a substitution σ such that for every literal l ∈ subsumingClauseLits, σ(l) = f(l). If subsumptionCheckHelper fails to find such a mapping and substitution, then subsumptionCheckHelper returns none without modifying the state's MetavarContext.

If subsumptionCheckHelper succeeds, then it assigns MVars to apply σ and returns a list assignment such that:

• ∀ i ∈ [0, subsumingClauseLits.length], σ(subsumingClauseLits.get! i) = subsumedClauseLits[(assignment.reverse.get! i).1] if (assignment.reverse.get! i).2 is false
• ∀ i ∈ [0, subsumingClauseLits.length], σ(subsumingClauseLits.get! i) = subsumedClauseLits[(assignment.reverse.get! i).1] with swapped lhs/rhs if (assignment.reverse.get! i).2 is true
• Note that assignment is reversed in the above lines. This is so that when we add additional nats to the assignment list, we can cons them onto the front of the list in constant time rather than concat them onto the back of the list in linear time

The argument exclude contains a set of Nats that cannot be mapped to (so that injectivity is preserved). The argument fstStart is provided to facilitate backtracking. The argument assignment is used to build the final result described above, and the argument assignmentIsFlipped is used to indicate whether the match indicated by assignment needed to be flipped or not.

subsumptionCheckHelper is defined as a partialDef, but should always terminate because every recursive call either makes subsumingClauseLits smaller or makes fstStart bigger (and once fstStart exceeds the size of subsumedClauseLits.lits, litInClause is certain to fail)

def Duper.subsumptionCheck (subsumingClause subsumedClause : MClause) (subsumedClauseMVarIds : Array Lean.MVarId) : RuleM.RuleM Bool

Returns true if subsumedClause is indeed subsumed by subsumingClause and returns false otherwise. If the check succeeds (meaning true is returned) then any changes to the MCtx are preserved (meaning any mvar substitutions are applied) and if the check fails, then the MCtx is left unchanged.

Equations

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

def Duper.subsumptionCheck' (subsumingClause subsumedClause : MClause) (subsumedClauseMVarIds : Array Lean.MVarId) : RuleM.RuleM (Option (List (Nat × Bool)))

Same as subsumptionCheck, but if the subsumption check succeeds, it additionally returns lists assignment and assignmentIsFlipped such that:

• ∀ i ∈ [0, subsumingClauseLits.length], σ(subsumingClauseLits.get! i) = subsumedClauseLits[(assignment.reverse.get! i).1] if (assignment.reverse.get! i).2 is false
• ∀ i ∈ [0, subsumingClauseLits.length], σ(subsumingClauseLits.get! i) = subsumedClauseLits[(assignment.reverse.get! i).1] with swapped lhs/rhs if (assignment.reverse.get! i).2 is true
• Note that assignment is not reversed in the above lines because this function reverses the output of subsumptionCheckHelper

Equations

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