Module linarith_solve 

The decision core for linear integer arithmetic: Fourier-Motzkin elimination that tracks the non-negative combination it eliminates with, so an unsatisfiable system yields its Farkas certificate — the multipliers λᵢ ≥ 0 on the original constraints such that Σ λᵢ·constraintᵢ is a positive constant ≤ 0 (a contradiction). The proof engine reconstructs a kernel proof from those multipliers via le_mul_nonneg/le_add_mono + the Bool no-confusion discriminator. Pure and self-contained — no kernel, no certificates here.

Structs

LinExpr

A linear expression Σ cⱼ·xⱼ + constant over the integers (zero coefficients pruned, so equality is canonical).

Functions

combine

Σ multipliers[i]·constraints[i]. For a valid Farkas certificate this is a bare positive constant (the variables cancel) — that constant is the d in the reconstructed contradiction 0 ≤ -d.

find_farkas

Given constraints cᵢ ≤ 0, find a non-negative integer combination Σ λᵢ·cᵢ = (positive constant) ≤ 0 — a Farkas refutation. Returns the multipliers λᵢ, or None if the system is satisfiable over ℚ (so no rational Farkas certificate exists).

parse_lin

Parse a ProofTerm into a linear expression, or None if it is non-linear (e.g. mul of two non-constants). Numeric constants are literals; other names are variables; add/sub/mul build the form.