Struct SimplexTableau 

pub struct SimplexTableau { /* private fields */ }

The Simplex tableau.

Implementations

impl SimplexTableau

pub fn new() -> Self

Create a new empty tableau.

pub fn fresh_var(&mut self) -> VarId

Create a fresh variable.

pub fn add_var( &mut self, lower: Option<BigRational>, upper: Option<BigRational>, ) -> VarId

Add a variable with initial bounds.

pub fn add_row(&mut self, row: Row) -> Result<(), String>

Add a row to the tableau. The row represents: basic_var = constant + sum(coeffs).

pub fn add_bound( &mut self, var: VarId, bound_type: BoundType, value: BigRational, constraint_id: ConstraintId, ) -> Result<(), Conflict>

Add a bound constraint.

pub fn get_value(&self, var: VarId) -> Option<&BigRational>

Get the current assignment to a variable.

pub fn pivot( &mut self, basic_var: VarId, non_basic_var: VarId, ) -> Result<(), String>

Perform a pivot operation. Swap basic_var (currently basic) with non_basic_var (currently non-basic).

pub fn check(&mut self) -> Result<SimplexResult, Conflict>

Check feasibility and fix violations using pivoting.

pub fn check_dual(&mut self) -> Result<SimplexResult, Conflict>

Dual simplex algorithm for Linear Programming.

The dual simplex maintains dual feasibility (all reduced costs non-negative) while working toward primal feasibility (all variables within bounds).

This is particularly useful for:

• Reoptimization after adding constraints
• Branch-and-bound in integer programming
• Problems that naturally start dual-feasible

Reference: Standard LP textbooks and Z3’s dual simplex implementation.

pub fn vars(&self) -> Vec<VarId>

Get all variables.

pub fn basic_vars(&self) -> Vec<VarId>

Get all basic variables.

pub fn non_basic_vars(&self) -> Vec<VarId>

Get all non-basic variables.

pub fn num_rows(&self) -> usize

Get the number of rows in the tableau.

pub fn num_vars(&self) -> usize

Get the number of variables.

pub fn set_blands_rule(&mut self, enable: bool)

Enable or disable Bland’s anti-cycling rule.

pub fn get_model(&self) -> Option<FxHashMap<VarId, BigRational>>

Get the current model (satisfying assignment). Returns None if the system is not known to be satisfiable.

pub fn is_feasible(&self) -> bool

Check if the current assignment satisfies all bounds.

pub fn find_violated_bound(&self) -> Option<VarId>

Find a variable that violates its bounds, if any.

pub fn get_constraints(&self, var: VarId) -> Vec<ConstraintId>

Get all constraints associated with a variable.

pub fn get_unsat_core(&self, conflict: &Conflict) -> Vec<ConstraintId>

Extract a minimal conflicting core from constraints. This is a simple implementation that returns all constraints involved. A more sophisticated version would compute a true minimal unsat core.

pub fn propagate(&self) -> Vec<(VarId, BoundType, BigRational)>

Theory propagation: deduce new bounds from existing constraints. Returns a list of (var, bound_type, value) tuples representing deduced bounds.

pub fn assert_constraint( &mut self, coeffs: FxHashMap<VarId, BigRational>, constant: BigRational, bound_type: BoundType, constraint_id: ConstraintId, ) -> Result<VarId, Conflict>

Assert a linear constraint: sum(coeffs) + constant {<=, >=, ==} 0. Returns a new slack variable if needed, and the constraint ID.

Trait Implementations

impl Clone for SimplexTableau

fn clone(&self) -> SimplexTableau

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SimplexTableau

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SimplexTableau

fn default() -> Self

Returns the “default value” for a type.

impl Display for SimplexTableau

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.