Function reify_linear 

pub fn reify_linear(
    term: &Term,
    vars: &mut VarInterner,
) -> Result<LinearExpr, LiaError>

Reify a Syntax term to a linear expression.

Converts the deep embedding of terms (Syntax) into a linear expression suitable for Fourier-Motzkin elimination.

Supported Forms

• SLit n - Integer literal becomes a constant
• SVar i - De Bruijn variable becomes a linear variable
• SName "x" - Named global becomes a linear variable (interned)
• SApp (SApp (SName "add") a) b - Linear addition
• SApp (SApp (SName "sub") a) b - Linear subtraction
• SApp (SApp (SName "mul") c) x - Scaling (only if one operand is constant)

Every term reified for one goal (both sides of a comparison, hypotheses and conclusion) must share one vars interner, or their variable indices will not line up.

Errors

Returns LiaError::NonLinear if the term contains non-linear operations (e.g., multiplication of two variables).