def Lean.Meta.Grind.Arith.Linear.getAssignment? (s : Struct) (e : Expr) : Option Rat

def Lean.Meta.Grind.Arith.Linear.mkModel (goal : Goal) (structId : Nat) : MetaM (Array (Expr × Rat))

Construct a model that satisfies all constraints in the linarith model for the structure with id structId. It also assigns values to (integer) terms that have not been internalized by the linarith model.