Module simplex 

Simplex algorithm for linear arithmetic.

This module implements the Simplex algorithm for solving linear programming problems and checking satisfiability of linear real arithmetic constraints.

The implementation follows the two-phase simplex method:

• Phase 1: Find a basic feasible solution (or prove infeasibility)
• Phase 2: Optimize the objective function (or detect unboundedness)

Reference: Z3’s math/simplex/ directory and standard LP textbooks.

Structs

Bound

A bound on a variable.

Conflict

Explanation for why a constraint caused unsatisfiability.

Row

A row in the simplex tableau represents: basic_var = constant + sum(coeff_i * nonbasic_var_i).

SimplexTableau

The Simplex tableau.

Enums

BoundType

Bound type for a variable.

SimplexResult

Result of a simplex operation.

VarClass

Variable classification in the tableau.

Type Aliases

ConstraintId

Constraint identifier.

VarId

Variable identifier for simplex.