README

===============================================================================
 smtlib2polya
===============================================================================

  This is version 0.1 of smtlib2polya, a translator from the SMT-LIB input
  format to the Polya prover.

  http://github.com/avigad/polya
  http://smt-lib.org/

  smt2polya is free software released under the GPLv3. You should have received
  a copy of the GNU General Public License along with smtlib2polya (see file
  COPYING).

  smtlib2polya uses parsing code written by Aina Niemetz for the ddSMT project:
  http://fmv.jku.at/ddsmt/

===============================================================================
 Usage
===============================================================================

  smtlib2polya requires Python 2.7 to run. It has been tested on Kubuntu and
  OSX; the timeout alarm may cause errors on Windows.

  Make sure that Polya is installed, and that the main directory is in the
  Python path. (You should be able to run "import polya" from the Python
  command line interpreter without error.) It is not necessary to install the
  optional computational geometry packages.

  Download the smtlib2polya directory. Edit batch_translate.py to point smt_dir
  to a directory containing .smt2 files.

  Execute "python batch_translate.py" from the command line. This will run
  Polya in order on all .smt2 files in smt_dir, and print results to
  smt_dir/results.out.
  
  The executable 'polya' takes one argument, a path to an .smt2 file. It prints
  1 if unsat, -1 if Polya fails, and 0 if there is an error. It is generated
  and tested only on Kubuntu 14.04. single_translate.py has identical behavior.
  
  Usage:
    ./polya file_name.smt2
    python single_translate.py file_name.smt2
    
  These files can also take input from stdin:
    cat file_name.smt2 | ./polya STDIN
    cat file_name.smt2 | python single_translate.py STDIN
  
  To generate a binary of your own: install PyInstaller:
  
    https://github.com/pyinstaller/pyinstaller/wiki
  and from the root directory run
  
    pyinstaller -n polya -F single_translate.py
  
  The binary will appear in ./dist/polya/