This page contains a number of utilities that might make your work with Spear more convenient and more pleasant. Also, this page contains scripts for automatic Spear optimization, which you can use to optimize Spear to your instances. All tools downloadable from this page are in the public domain, feel free to use them any way you want.

Syntax File

Vim SF syntax file [vim]. Type :help new-filetype in Vim to learn how to use it.

Format Translators

Note: For all translators here, create a directory, extract the archive into the directory, read INSTALL file.

• Translator from SMT QF_UFBV and QF_BV to SF format [tar.bz2]. It does not handle UIFs precisely, but still solves all SMT-LIB'06 benchmarks correctly.
• Translator from SF to SMT QF_BV format [tar.bz2]. This is free software, and contains a simple SF parser, which you are free to use and modify for your own purposes.

Automatic Parameter Tuning Scripts

Instances generated by the same tool often have similar properties and decision procedures can be much more effective if optimized for a specific set. Speedups of 2-3 orders of magnitude are not uncommon. However, until recently, this optimization process was manual and extremely tedious. Now, with ParamILS written by Frank Hutter, you can optimize Spear automatically for your application. You can find all the scripts you will need to optimize Spear here [tar.bz2]. Note: ParamILS and these scripts have not yet been thoroughly tested. Bug reports will be highly appreciated.

Testing Scripts

I used a random CNF instance generator and the corresponding testing framework for developing both Spear and HyperSAT.