Skip to main content

omega_unsat

logicaffeine_kernel::omega

Function omega_unsat 

Source 
pub fn omega_unsat(constraints: &[IntConstraint]) -> bool
Expand description

Check if integer constraints are unsatisfiable using the Omega test.

This is the main entry point for the omega decision procedure. It uses integer-aware Fourier-Motzkin elimination to check for contradictions.

§Integer Semantics

Unlike rational Fourier-Motzkin, this procedure:

  • Normalizes constraints by their GCD
  • Handles strict inequalities by integer shift (< k becomes <= k-1)
  • Detects integer-specific unsatisfiability

§Returns

  • true if no integer assignment satisfies all constraints (unsatisfiable)
  • false if the constraints may be satisfiable

§Usage for Validity

To prove a goal G is valid over integers, check if NOT(G) is unsatisfiable. If omega_unsat(negation_constraints) returns true, the goal is valid.