Int expressions are normalized by the grind preprocessor, but we dynamically convert expressions from other types into Int expressions and these expressions must be normalized inside of the cutsat module.

partial def Lean.Meta.Grind.Arith.Cutsat.toLinearExpr (e : Expr) (generation : Nat := 0) : GoalM Int.Linear.Expr

Converts the given integer expression into Int.Linear.Expr