Cooper's Quantifier Elimination Method for Presburger Arithmetic

Based on the paper:
  D. C. Cooper, "Theorem Proving in Arithmetic without Multiplication"

Author: Aaron R. Bradley
Last modified: May 4, 2006

To compile

  1. Modify the first line of Makefile and Makefile.opt to point to
     your O'Caml installation.

  2. Type "make -f Makefile" to compile a bytecode version, and
     "make -f Makefile.opt" to compile a native version.  The native
     version is significantly faster.

To run, type, for example, 

  cooper < examples/even

For verbose output, type 

  cooper -v < examples/even

While cryptic, the verbose output should be somewhat decipherable to
the user familiar with Cooper's method.

The input format should be apparent from the provided examples.

Questions or comments?  Contact me at arbrad@cs.stanford.edu.
