presburger

A decision procedure for quantifier-free linear arithmetic.

http://github.com/yav/presburger

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

See all snapshots presburger appears in

BSD-3-Clause licensed by Iavor S. Diatchki
Maintained by [email protected]
This version can be pinned in stack with:presburger-1.3.1@sha256:7c88061e13bab0e63240c05dad36b9518ad50d7ad4ade0f8911efa7826eb4b5d,944

Module documentation for 1.3.1

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

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