A decision procedure for quantifier-free linear arithmetic.

Latest on Hackage:[email protected]:2

See all snapshots presburger appears in

BSD-3-Clause licensed by Iavor S. Diatchki
Maintained by [email protected]

Module documentation for 1.3.1

This version can be pinned in stack with:[email protected]:7c88061e13bab0e63240c05dad36b9518ad50d7ad4ade0f8911efa7826eb4b5d,944

The decision procedure is based on the algorithm used in CVC4, which is itself based on the Omega test.

Used by 1 package in lts-6.35(full list with versions):