Duper.ProverM

Every clause is assigned a "distance" from the goal. This distance is the shortest number of inference rules to obtain the clause from an assumption that was originally part of the negated goal. Goal assumptions themselves have a goal distance of 0, and facts that are not at all connected to the goal (e.g. lemmas passed into duper or facts derived from said lemmas) are assigned the distance maxGoalDistance.

Equations

Duper.ProverM.maxGoalDistance = 15

Instances For

source

def Duper.ProverM.chooseGivenClause :

ProverM (Option Clause)

Equations

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

Instances For

source

def Duper.ProverM.markAsDescendantToGeneratingAncestors (c : Clause) (generatingAncestors : Array Clause) :

ProverM Unit

Given a clause c and a list of ancestors, markAsDescendantToGeneratingAncestors adds c to each generating ancestor's list of descendants

Equations

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

Instances For

source

def Duper.ProverM.addNewClause (c : Clause) (proof : RuleM.Proof) (goalDistance generationNumber : Nat) (generatingAncestors : Array Clause) :

ProverM ClauseInfo

Registers a new clause, but does not add it to active or passive set. Typically, you'll want to use addNewToPassive instead.

Equations

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

Instances For

source

def Duper.ProverM.addNewToUnsupportedFacts (c : Clause) (proof : RuleM.Proof) (goalDistance generationNumber : Nat) (generatingAncestors : Array Clause) :

ProverM Unit

Registers a new clause and adds it to the unsupported facts set.

Equations

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

Instances For

source

def Duper.ProverM.addNewToPassive (c : Clause) (proof : RuleM.Proof) (goalDistance generationNumber : Nat) (generatingAncestors : Array Clause) :

ProverM Unit

Registers a new clause and adds it to the passive set. The goalDistance and generationNumber arguments are used to by the clause selection strategy's heuristics. The generatingAncestors argument contains the list of clauses that were used to generate c (or c's ancestor which generated c by a modifying inference). See page 8 of "E – A Brainiac Theorem Prover"

Equations

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

Instances For

source

def Duper.ProverM.addClausifiedToPassive (c : Clause) :

ProverM Unit

Takes a clause that was generated by preprocessing clausification and re-adds it to the passive set and its associated heaps

Equations

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

Instances For

source

def Duper.ProverM.ProverM.runWithExprs {α : Type} (x : ProverM α) (es : List (Lean.Expr × Lean.Expr × Array Lean.Name × Bool × Bool)) (ctx : Context) (s : State) :

Lean.MetaM (α × State)

Runs the ProverM α function x after adding every clause in es to the passive set. es is a list containing:

The Prop to be reasoned about
The proof of the above Prop
Any needed paramNames
A bool which indicates whether the fact was part of the original goal (this impacts the clause selection strategy)
A bool which indicates whether the fact should be part of the set of support (extra facts are not added to the set of support)

Equations

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

Instances For

source

@[inline]

def Duper.ProverM.runRuleM {α : Type} (x : RuleM.RuleM α) :

ProverM α

Equations

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

Instances For

source

def Duper.ProverM.addPotentiallyVacuousClause (c : Clause) :

ProverM Unit

Equations

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

Instances For

source

def Duper.ProverM.addToSimplifyingIndices (c : Clause) :

ProverM Unit

Adds c to demodSidePremiseIdx and subsumptionTrie, which are the two indices that a potentiallyVacuous clause will not be added to in addToActive.

Equations

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

Instances For

source

def Duper.ProverM.addToActive (c : Clause) (canUseToSimplifyOtherClauses : Bool) :

ProverM Unit

Equations

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

Instances For

source

def Duper.ProverM.removeFromDiscriminationTrees (c : Clause) :

ProverM Unit

Remove c from mainPremiseIdx, supSidePremiseIdx, demodSidePremiseIdx, and subsumptionTrie

Equations

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

Instances For

source

def Duper.ProverM.removeDescendants (c : Clause) (ci : ClauseInfo) (protectedClauses : List Clause) :

ProverM Unit

If ci is the ClauseInfo corresponding to a clause c, then removeDescendants removes the direct descendants of c from the passive set. Additionally, it tags each direct descendant of c as "isOrphan" in allClauses so they can potentially be readded to the passive set. However, removeDescendants does not remove or mark any clause that appears in protectedClauses.

Equations

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

Instances For

source

def Duper.ProverM.removeClause (c : Clause) (protectedClauses : List Clause := []) :

ProverM Unit

removeClause does the following:

Removes c from the active set, passive set, unsupported facts set, potentiallyVacuousClauses set, and all discrimination trees
Tags c as "wasSimplified" in allClauses
Removes each direct descendant of c from the passive set
Tags each direct descendant of c as "isOrphan" in allClauses

protectedClauses is an additional argument that needs to be provided if a clause is being eliminated by a backward simplification rule. The idea is that protectedClauses contains the list of pre-existing clauses that appear in the conclusion of the backward simplification rule that eliminated c, and these clauses should not be removed even if they happen to be descendants of c. With backward simplification rules, it is possible for a clause to remove its ancestor (without intending to remove itself), so the protectedClauses argument ensures that no clause inadvertently removes itself in the process of simplifying away a different clause.

Equations

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

Instances For

source

def Duper.ProverM.immediateSimplification (givenClause resultClause : Clause) :

ProverM (Option Clause)

Checks whether any clause in resultClauses subsumes givenClause (by clause subsumption). If there is a clause c that subsumes givenClause, then some c is returned. Otherwise, none is returned.

Note: Currently, we only check for clause subsumption, and we only check clauses in resultClauses against the givenClause. But it may be good in the future to:

Check whether any result clause can eliminate givenClause by equality subsumption (or some other simplification rule)
Inter-simplify the clauses in resultClauses (this would change the return type but would be more faithful to how immediate simplification is described in http://www.cs.man.ac.uk/~korovink/my_pub/iprover_ijcar_app_2020.pdf. See table 1 to see which rules should be used for inter-simplification)

Equations

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

Instances For