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

Equations

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