Description
Provides a decision procedure for quantifier-free linear arithmetic. Such procedures can determine whether certain arithmetic constraints are satisfiable without manually checking every case.
It is useful for verification tools, theorem provers, type-level checks, analyzers, and symbolic reasoning libraries. It is a developer library and not an interactive math solver.