Collect variable information

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

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

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

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

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

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

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

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

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

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

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

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

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