Collect variable information

structure Lean.Meta.Grind.Arith.Cutsat.VarInfo : Type

• maxLowerCoeff : Nat
• maxUpperCoeff : Nat
• maxDvdCoeff : Nat

@[instance_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedVarInfo : Inhabited VarInfo

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedVarInfo = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedVarInfo.default }

We order variables in decreasing order of "cost". We use the lexicographical order of two different costs. The first one is the max (min lowerCoeff upperCoeff) dvdCoeff. Recall that we use cooper-left if the coefficient of the lower bound is smaller, and cooper-right otherwise. This is way we use the min lowerCoeff upperCoeff. The coefficient of the divisibility constraint also impacts the size of the search space. Then, we break ties using the max of all of them, and then the variable original order.

def Lean.Meta.Grind.Arith.Cutsat.cost₁ (info : VarInfo) : Nat

Equations

• Lean.Meta.Grind.Arith.Cutsat.cost₁ info = max info.maxDvdCoeff (min info.maxLowerCoeff info.maxUpperCoeff)

def Lean.Meta.Grind.Arith.Cutsat.cost₂ (info : VarInfo) : Nat

Equations

• Lean.Meta.Grind.Arith.Cutsat.cost₂ info = max info.maxDvdCoeff (max info.maxLowerCoeff info.maxUpperCoeff)

def Int.Internal.Linear.Poly.reorder (p : Poly) (old2new : Array Var) : Poly

Equations

• (Int.Internal.Linear.Poly.num k).reorder old2new = Int.Internal.Linear.Poly.num k
• (Int.Internal.Linear.Poly.add a x_1 p_1).reorder old2new = Int.Internal.Linear.Poly.add a old2new[x_1]! (p_1.reorder old2new)

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.reorder (c : DvdCnstr) (old2new : Array Var) : DvdCnstr

Equations

• c.reorder old2new = { d := c.d, p := c.p.reorder old2new, h := Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c }.norm

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.reorder (c : EqCnstr) (old2new : Array Var) : EqCnstr

Equations

• c.reorder old2new = { p := c.p.reorder old2new, h := Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c }.norm

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.reorder (c : LeCnstr) (old2new : Array Var) : LeCnstr

Equations

• c.reorder old2new = { p := c.p.reorder old2new, h := Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c }.norm

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.reorder (c : DiseqCnstr) (old2new : Array Var) : DiseqCnstr

Equations

• c.reorder old2new = { p := c.p.reorder old2new, h := Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c }.norm

def Lean.Meta.Grind.Arith.Cutsat.reorderVarMap {α : Type u_1} [Inhabited α] (m : PArray α) (new2old : Array Var) : PArray α

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.reorderDiseqSplits (m : PHashMap Poly FVarId) (old2new : Array Var) : PHashMap Poly FVarId

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.reorderVars : GoalM Unit

Reorders the variables according to cmp when it pays off. Variables created after a reordering (e.g., by later E-matching rounds) are appended to the order, so an expensive one may end up after the cheap ones it appears with, and the Cooper case splits that eliminate it enumerate its coefficient. The first reordering applies the full order; a later one is performed only when a variable with cost₁ > 1 is out of place, so that cheap problems do not accumulate epochs (see State.varsHistory).

Equations

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