A decision procedure for quantifier-free linear arithmetic.

Version on this page:1.3.1
LTS Haskell 8.24:1.3.1
Stackage Nightly 2017-10-02:1.3.1
Latest on Hackage:1.3.1

See all snapshots presburger appears in

BSD-3-Clause licensed by Iavor S. Diatchki
Maintained by

Module documentation for 1.3.1

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

Depends on 3 packages:
Used by 1 package:
comments powered byDisqus