def Duper.isNegative (l : Lit) (inclusive : Bool := true) : Bool

Determines whether given lit l is negative. If inclusive is true, then this includies literals of the form e = False and False = e. If inclusive is false, then this only includes literals whose sign is negative.

Equations

• Duper.isNegative l inclusive = (!l.sign || inclusive && (l.rhs == Lean.mkConst `False || l.lhs == Lean.mkConst `False))

def Duper.selectFirstNegLit (c : MClause) : Lean.CoreM (List Nat)

Selection function that returns the first negative literal (including lits of the form e = False)

Equations

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

def Duper.selectFirstNegLitExclusive (c : MClause) : Lean.CoreM (List Nat)

Selection function that returns the first negative literal (excluding lits of the form e = False)

Equations

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

def Duper.isPureVarLit (l : Lit) : Bool

Equations

• Duper.isPureVarLit l = match l.lhs, l.rhs with | Lean.Expr.mvar mvarId, Lean.Expr.mvar mvarId_1 => true | x, x_1 => false

def Duper.selectFirstPureVarNegLit (c : MClause) : Lean.CoreM (List Nat)

Based on E's SelectPureVarNegLiterals: Select the first negative literal of the form x ≠ y

Equations

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

def Duper.selectFirstMaximalNegLit (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectLargestNegLit: Select the first maximal negative literal

Note: This coincides with Zipperposition's max_goal selection function (with strict set to true) which is Zipperposition's default selection function (outside of portfolio mode)

Equations

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

def Duper.selectFirstMaximalNegLitAndAllPosLits (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on Zipperposition's max_goal selection function with strict set to false: Select the first maximal negative literal and all positive literals

Equations

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

def Duper.selectFirstMinimalNegLit (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectSmallestNegLit: Select the first minimal negative literal

Equations

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

def Duper.selectFirstMaxDiffNegLit (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectDiffNegLit: Select the first negative literal for which the size difference between both terms is maximal

Equations

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

def Duper.isGround (l : Lit) : Bool

Equations

• Duper.isGround l = (!l.lhs.hasExprMVar && !l.rhs.hasExprMVar)

def Duper.selectFirstGroundNegLit (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectGroundNegLit: Select the first negative ground literal for which the size difference between both terms is maximal

Equations

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

def Duper.selectFirstGroundNegLitIfPossible (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectOptimalLit: If there is a negative ground literal, select as in selectFirstGroundNegLit. Otherwise, select as in selectFirstMaxDiffNegLit

Equations

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

def Duper.selectMaxLitComplex (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectMaxLComplex: Select a maximal negative literal. If there are no maximal negative literals, select nothing. If there is just one maximal negative literal, select that. If there are multiple maximal negative literals, try to find one that satisfies any of the following properties (listed in order of precedence):

• Is a pure variable literal (i.e. of the form x ≠ y)
• Is a ground literal with the largest size difference
• Is a non-ground literal with the largest size difference

Equations

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

def Duper.selectMaxLitComplexAvoidPosPred (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectMaxLComplexAvoidPosPred (which coincides with Zipperposition's e_sel): It does the same as selectMaxLitComplex but uses the number of positive literals with a shared predicate symbol as a tiebreaker (preferring to select literals that share a predicate symbol with as few positive literals as possible). For this, specification, I am defining a predicate symbol as the top symbol for the lhs of a literal of the form e = True or e = False.

Note: According to "Extending a Brainiac Prover to Lambda-Free Higher-Order Logic", SelectMaxLComplexAvoidPosPred (aka SelectMLCAPP) should be have very similarly to E's SelectMLCAPPPreferAppVar and SelectMLCAPPAvoidAppVar. So it should be unnecessary to separately implement those two selection functions.

Equations

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

def Duper.selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectCQIPrecWNTNp (which coincides with Zipperposition's e_sel2): Selects the negative literal with the highest-precedence predicate (as in selectMaxLitComplexAvoidPosPred, I define predicates as the top symbol for the lhs of a literal of the form e = True or e = False). If there are multiple negative literals with the same largest predicate, then the size difference between the lit's lhs and rhs will be the tiebreaker (with larger size differences being preferred).

Equations

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

def Duper.selectComplexG (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Based on E's SelectComplexG (which coincides with Zipperposition's e_sel3): Attempts to select a negative pure variable literal (if there are multiple, selects the first arbitrarily). If that fails and there is at least one negative ground literal, selects the smallest negative ground literal. If that also fails, it selects the negative literal with the largest size difference.

Equations

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

def Duper.getSelections (c : MClause) (alreadyReduced : Bool) : RuleM.RuleM (List Nat)

Equations

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

def Duper.litSelectedOrNothingSelected (c : MClause) (i : Nat) (alreadyReduced : Bool) : RuleM.RuleM Bool

Equations

• Duper.litSelectedOrNothingSelected c i alreadyReduced = do let sel ← Duper.getSelections c alreadyReduced if (sel == []) = true then pure true else pure (sel.contains i)

def Duper.litSelected (c : MClause) (i : Nat) (alreadyReduced : Bool) : RuleM.RuleM Bool

Equations

• Duper.litSelected c i alreadyReduced = do let sel ← Duper.getSelections c alreadyReduced pure (sel.contains i)

inductive Duper.Eligibility : Type

Data type to capture whether a literal in a clause is eligible. If it is not eligible, we distinguish the cases where there might be substitutions that make the literal eligble (potentiallyEligible) or not (notEligible).

• eligible : Eligibility
• potentiallyEligible : Eligibility
• notEligible : Eligibility

instance Duper.instInhabitedEligibility : Inhabited Eligibility

Equations

• Duper.instInhabitedEligibility = { default := Duper.Eligibility.eligible }

instance Duper.instBEqEligibility : BEq Eligibility

Equations

• Duper.instBEqEligibility = { beq := Duper.beqEligibility✝ }

instance Duper.instReprEligibility : Repr Eligibility

Equations

• Duper.instReprEligibility = { reprPrec := Duper.reprEligibility✝ }

instance Duper.instHashableEligibility : Hashable Eligibility

Equations

• Duper.instHashableEligibility = { hash := Duper.hashEligibility✝ }

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

Equations

• Duper.Eligibility.eligible.format = Lean.toMessageData "eligibile"
• Duper.Eligibility.notEligible.format = Lean.toMessageData "notEligibile"
• Duper.Eligibility.potentiallyEligible.format = Lean.toMessageData "potentiallyEligibile"

instance Duper.instToMessageDataEligibility : Lean.ToMessageData Eligibility

Equations

• Duper.instToMessageDataEligibility = { toMessageData := Duper.Eligibility.format }

def Duper.eligibilityNoUnificationCheck (c : MClause) (alreadyReduced : Bool := true) (i : Nat) (strict : Bool := false) : RuleM.RuleM Bool

Checks whether a literal is eligible in rules without unification.

A literal L is (strictly) eligible in C if it is selected in C or there are no selected literals in C and L is (strictly) maximal in C.

Equations

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

def Duper.eligibilityPreUnificationCheck (c : MClause) (alreadyReduced : Bool := true) (i : Nat) : RuleM.RuleM Eligibility

Checks whether a literal might be eligible before attempting to run the unification algorithm.

A literal L is (strictly) eligible w.r.t. a substitution σ in C if it is selected in C or there are no selected literals in C and Lσ is (strictly) maximal in Cσ.

The alreadyReduced variable indicates whether c has been betaEta reduced as well as whether its mvars have been instantiated (alreadyReduced is only set to true if both of these things are true)

Equations

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

def Duper.eligibilityPostUnificationCheck (c : MClause) (alreadyReduced : Bool := false) (i : Nat) (preUnificationResult : Eligibility) (strict : Bool := false) : RuleM.RuleM Bool

Checks whether a literal might be eligible based on the result of eligibilityPreUnificationCheck.

A literal L is (strictly) eligible w.r.t. a substitution σ in C if it is selected in C or there are no selected literals in C and Lσ is (strictly) maximal in Cσ.

The alreadyReduced variable indicates whether c has been betaEta reduced as well as whether its mvars have been instantiated (alreadyReduced is only set to true if both of these things are true)

Equations

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