Skip to main content

reify_linear

logicaffeine_kernel::lia

Function reify_linear 

Source 
pub fn reify_linear(term: &Term) -> Result<LinearExpr, LiaError>
Expand description

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 (hashed)
  • 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)

§Errors

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