This is the main source repository of the Vampire project, an advanced tool for automated reasoning. The following is for end-users of Vampire: new developers should read the wiki as well.
Please see LICENCE. Note that Vampire links to some other projects with thanks:
- MiniSat, a SAT solver
- CaDiCaL, another SAT solver
- GMP, for arbitrary-precision arithmetic - specifically the
mini-gmppart - VIRAS, a quantifier elimination method
- Z3, an SMT solver (optional)
See releases - we likely have a pre-built binary for your platform. If not, you will need to build Vampire from source, but this is not too onerous.
The basic usage of Vampire is to save your problem in TPTP format and run
$ vampire problem.pwhich will run Vampire in its default mode with a 60 second time-limit.
However, consider running Vampire in portfolio mode:
$ vampire --mode casc problem.pwhich will try lots of different strategies. This often performs better than the default mode.
If you think the problem is satisfiable then you can also run
$ vampire --mode casc_sat problem.pwhich will use a set of strategies suited to satisfiable problems.
Note that all of these modes are really shortcuts for other combinations e.g. --mode casc is a shortcut for
$ vampire --mode portfolio --schedule casc --proof tptpTo see a full list of options, run
$ vampire --show_options on
