Module omega 

Omega Test: True Integer Arithmetic Decision Procedure

This module implements the Omega test for linear integer arithmetic, handling the discrete nature of integers correctly.

Difference from LIA

Unlike crate::lia (which uses rational arithmetic), this module handles integers with proper semantics:

• x > 1 becomes x >= 2 (strict to non-strict for integers)
• 3x <= 10 implies x <= 3 (integer division with floor)
• 2x = 5 is unsatisfiable (odd number cannot equal even expression)

Algorithm

The algorithm is similar to Fourier-Motzkin elimination but with integer-aware semantics:

1. Normalize: Scale constraints and normalize by GCD
2. Convert strict: Transform < to <= using integer shift
3. Eliminate: Fourier-Motzkin with integer coefficient handling
4. Check: Verify constant constraints for contradictions

When to Use

Use omega when you need exact integer semantics. Use lia when rational arithmetic is acceptable (faster but may miss integer-specific unsatisfiability).

Structs

IntConstraint

Integer constraint representing expr <= 0 or expr < 0.

IntExpr

Integer linear expression of the form c + a₁x₁ + a₂x₂ + … + aₙxₙ.

Functions

extract_comparison

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

goal_to_negated_constraint

Convert a goal to constraints for validity checking using integer semantics.

omega_unsat

Check if integer constraints are unsatisfiable using the Omega test.

reify_int_linear

Reify a Syntax term to an integer linear expression.