Skip to main content

reify_int_linear

logicaffeine_kernel::omega

Function reify_int_linear 

Source 
pub fn reify_int_linear(term: &Term, vars: &mut VarInterner) -> 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 (interned)
  • add, sub, mul - Arithmetic operations (mul only if one operand is constant)

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

§Returns

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