Module lia 

LIA Tactic: Linear Integer Arithmetic by Fourier-Motzkin Elimination

This module implements a decision procedure for linear arithmetic over rational numbers (with integer semantics handled by crate::omega).

Algorithm

The lia tactic works in four steps:

1. Reification: Convert Syntax terms to LinearExpr representation
2. Negation: Convert the goal to constraints (validity = negation is unsatisfiable)
3. Elimination: Use Fourier-Motzkin to eliminate variables one by one
4. Check: Verify the resulting constant constraints are contradictory

Fourier-Motzkin Elimination

This classical algorithm eliminates variables from a system of linear inequalities. For each variable x:

• Partition constraints into lower bounds (x >= L), upper bounds (x <= U), and independent
• Combine each lower with each upper: L <= U
• The resulting system has one fewer variable

Rational Arithmetic

The module uses exact rational arithmetic during elimination to avoid precision issues. Rationals are automatically normalized to lowest terms.

Supported Relations

• Lt (less than)
• Le (less than or equal)
• Gt (greater than)
• Ge (greater than or equal)

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

Exact rational number for arithmetic during Fourier-Motzkin elimination.

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.