Spear / Spear frequently asked questions

(:keywords bit-vector arithmetic, decision procedure, frequently asked questions:)

  1. Is Windows version of Spear available?

Yes! Either install Cygwin or get cygwin1.dll and add it to your path, and Spear should happily run under DOS.

  1. Is the source code available?

Not yet. But, most likely, it will be eventually.

  1. I’m using OS X on machine Y, and no binaries are available...

See the previous question. If you can't wait, please let me know what do you need, and I’ll do my best to provide you with the suitable binary. However, if you are running Mach 3.0 on R2000, don’t expect too much.

  1. Certain sets of search parameters work really well on my instances, but I hate passing 25-or-so parameters to the solver each time. What do I do?

Please let me know what kind of instances you have, the set of parameters you use, and some proof that the found set of parameters works really well on those instances. The chances are that the same set of parameters will work well on similar instances other people have. If the parameters end up being effective, I will include them as a predefined set in the next release. You will be credited for finding the set.

  1. Which parameter set is currently the best in general?

Depends on your problem. Run Spear with --help and try several offered sets of parameters. Most of them were found by Frank Hutter with ParamILS — an automatic tool for parameter optimization based on iterated local search in configuration space. The sets were found on a 50 dual-processor machine cluster, after a couple of weeks of optimization.

  1. I’d like to use Spear incrementally, can I do that?

Yes, and no. Spear is fully incremental, and has some other cool features that I use in software verification, but currently the header files and dynamic/static libraries are not available.

  1. Spear is great, but I’m missing feature X, what can be done?

Nothing. I've stopped actively working on Spear. If someone else picks up the development, bug him/her. happy smiley If/when I release the source, you can also add the needed functionality yourself and submit a patch.

  1. Why is Spear distributed as bz2 file, and what kind of extension is that?

Extension .bz2 means that the file was compressed with Bzip2. Bzip2 has an excellent compression ratio and it is free. This saves both disk space and network bandwidth.

  1. I’m using Spear in my research, and need to cite something, what should I cite?

My thesis.

  1. Where can I find Spear documentation?

Pass --help to Spear. If you want to see all search parameters, pass --hidden.

  1. Can I use Spear commercially?

Send me an email.

  1. Does Spear bit-blast all bit-vector arithmetic operators?

It tries hard not to. For every term, Spear tries to simplify it away as much as possible at several different levels of abstraction. If no simplification worked, the term is bit-blasted.

  1. Is Spear a Satisfiability Modulo Theories (SMT) solver?

Strictly speaking, no. It's not based on the Nelson-Oppen framework.

Page last modified on January 29, 2011, at 04:45 PM