-
Notifications
You must be signed in to change notification settings - Fork 2
License
robertylewis/smtlib2polya
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
=============================================================================== 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/
About
No description, website, or topics provided.
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published