Skip to main content

reify_int_linear

logicaffeine_kernel::omega

Function reify_int_linear 

Source 
pub fn reify_int_linear(term: &Term) -> Option<IntExpr>
Expand description

Reify a Syntax term to an integer linear expression.

Converts the deep embedding (Syntax) into an integer linear expression. Similar to crate::lia::reify_linear but produces integer coefficients.

§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)
  • add, sub, mul - Arithmetic operations (mul only if one operand is constant)

§Returns

Some(expr) on success, None if the term is non-linear or malformed.