Module lia 

Linear Integer Arithmetic via Fourier-Motzkin Elimination

This module implements a decision procedure for linear arithmetic over the rationals: reify a Syntax goal into LinearExpr constraints, then decide unsatisfiability with Fourier-Motzkin elimination.

Exactness

Coefficients are exact arbitrary-precision rationals (logicaffeine_base::numeric::Rational). The verdict feeds trusted reflection reductions, so the arithmetic must be exact at every magnitude: elimination multiplies coefficients pairwise, and a wrapped or declined product either flips a verdict (unsound) or loses a refutation (incomplete). There is no overflow path — the procedure is total.

Rational vs Integer Semantics

This procedure decides satisfiability over the RATIONALS. It is sound for integer goals (a rationally-unsatisfiable system has no integer solution either) but incomplete for integer-specific facts — use crate::omega when discreteness matters (x > 1 ⟹ x ≥ 2).

Structs

Constraint

A linear constraint representing either expr <= 0 or expr < 0.

LinearExpr

A linear expression of the form c₀ + c₁x₁ + c₂x₂ + … + cₙxₙ.

Rational

An exact rational number: a fraction kept in lowest terms with a strictly positive denominator. Built on BigInt, so it never rounds the way a JSON / f64 “number” does — 1/3 stays exactly 1/3, not 0.3333…, and a numerator past 2^53 survives instead of collapsing onto a double.

Enums

LiaError

Error during reification to linear expression

Functions

extract_comparison

Extract comparison from goal: (SApp (SApp (SName “Lt”|“Le”|“Gt”|“Ge”) lhs) rhs)

fourier_motzkin_unsat

Check if a constraint set is unsatisfiable using Fourier-Motzkin elimination.

goal_to_negated_constraint

Convert a goal to constraints for validity checking.

reify_linear

Reify a Syntax term to a linear expression.