LinSpire

LinSpire is an incremental linear feasibility solver over rational numbers.

It maintains variable bounds under linear equalities and inequalities, supports strict constraints, and allows constraints to be retracted and re-asserted by reason id.

Features

• Incremental solving: add constraints and call check() as needed.
• Dynamic updates: retract or re-assert constraints by id.
• Strict and non-strict inequalities: x < c, x <= c, x > c, x >= c, x == c.
• General linear constraints over multiple variables.
• Conflict explanations: retrieve the set of reason ids that caused unsatisfiability.
• Listener callbacks: observe variable updates during propagation/pivoting.

Quick Start

use linspire::{
    Engine,
    lin::{c, v, vc},
};

fn main() {
    let mut e = Engine::new();
    let x = e.add_var();
    let y = e.add_var();
    let z = e.add_var();

    let c_balance = e.add_constraint(); // x + y + z = 8
    let c_capacity = e.add_constraint(); // 2x + 3y - z <= 17
    let c_mix = e.add_constraint(); // x - 4y + 2z >= -3
    let c_positive_y = e.add_constraint(); // y > 0

    assert!(e.new_eq(&(v(x) + v(y) + v(z)), &c(8), Some(c_balance)));
    assert!(e.new_le(&(vc(x, 2) + vc(y, 3) - v(z)), &c(17), Some(c_capacity)));
    assert!(e.new_ge(&(v(x) - vc(y, 4) + vc(z, 2)), &c(-3), Some(c_mix)));
    assert!(e.new_gt(&v(y), &c(0), true, Some(c_positive_y)));

    assert!(e.check());

    // Inspect variable intervals and current assignment
    println!("x in [{}, {}], value {}", e.lb(x), e.ub(x), e.val(x));
}

Core API

• Engine::add_var() creates a variable and returns its index.
• Engine::add_constraint() creates a reason/constraint id.
• Engine::new_le/new_lt/new_ge/new_gt/new_eq(lhs, rhs, reason) adds linear relations.
• Engine::check() runs feasibility repair with pivoting.
• Engine::retract(id) removes active bounds introduced by a constraint id.
• Engine::assert(id) re-applies previously stored bounds for a constraint id.
• Engine::get_conflict_explanation() returns conflicting reason ids, if any.
• Engine::set_listener(var, callback) installs callbacks fired on variable updates.

Helper constructors in lin:

• c(k) builds a constant expression.
• v(i) builds x_i.
• vc(i, k) builds k*x_i.

How Strict Inequalities Work

LinSpire uses an infinitesimal component internally (InfRational) to represent strict bounds. Conceptually:

• x < 5 is represented as x <= 5 - eps
• x > 5 is represented as x >= 5 + eps

This keeps strict and non-strict arithmetic in the same solver without floating-point rounding issues.

Constraint Lifecycle

Typical flow:

1. Create variables and constraint ids.
2. Add constraints with a reason id (Some(id)).
3. Call check() to restore feasibility.
4. If unsat, inspect get_conflict_explanation().
5. Retract selected constraints with retract(id) and continue.

Example continuation from the quick start above:

// Add a contradictory general linear constraint:
// 2x + 3y - z >= 30  (conflicts with <= 17)
let c_conflict = e.add_constraint();
assert!(e.new_ge(&(vc(x, 2) + vc(y, 3) - v(z)), &c(30), Some(c_conflict)));
assert!(!e.check());

let conflict = e.get_conflict_explanation().unwrap();
assert!(conflict.contains(&c_capacity));
assert!(conflict.contains(&c_conflict));

e.retract(c_conflict);
assert!(e.check());

Development

Run tests:

cargo test --lib

Coverage (requires cargo-llvm-cov):

cargo llvm-cov --summary-only
cargo llvm-cov --open

Notes

• Lin expressions are displayed in deterministic variable order.
• The solver is currently single-engine, sequential mutation logic.