usage.html

---
title: Usage
layout: default
---
{% include authors.html %}

<p>
This page gives information on how to use Vampire.
See <a href="/download.html">Download</a> for how to download Vampire.
</p>

<h2>Manual</h2>
<p>
Vampire manual is not finished yet.
While there is no manual, you can use the <a href="https://publik.tuwien.ac.at/files/PubDat_225994.pdf">CAV 2013 tutorial paper</a>, which describes main features of Vampire and some of its options.
</p>

<h2>Basic Usage</h2>
<p>
The most basic usage of Vampire is to save your problem in <a href="https://www.tptp.org/">TPTP</a> format and run
<code>
vampire problem.p 
</code>
as this will run Vampire in default mode with a 60 second time-limit.
</p>

<p>
However, a better way to run Vampire is in portfolio mode i.e.
<code>
vampire --mode casc -t 300 problem.p 
</code>
this will run for 300 seconds trying lots of different strategies. This will perform much better than default mode as it will try combinations of options, that are turned off by default, which may work well for your problem.
</p>

<p>
If you think the problem is satisfiable then you can also run
<code>
vampire --mode casc_sat -t 300 problem.p 
</code>
which will use a set of strategies suited to satisfiable problems (as entered into the most recent <a href="http://www.cs.miami.edu/~tptp/CASC/">CASC</a> competition).
</p>

<p>
Finally, if your problem is in <a href="http://smtlib.cs.uiowa.edu/">SMT-LIB</a> format you can run
<code>
vampire --input_syntax smtlib2 problem.smt2 
</code>
to specify a different input language, or
<code>
vampire --mode smtcomp problem.p 
</code>
to use the latest <a href="http://smtcomp.sourceforge.net/">SMT-COMP</a> schedule, which automatically selects the appropriate input language.
</p>

<p>
Note that all of these competition modes are really shortcuts for other combinations e.g. casc mode is a shortcut for
<code>
vampire --mode portflio --schedule casc -t 300s -p tptp
</code>

<h2>Options and More Advanced Usage</h2>
<p>
To see a full list of options with some explanations run
<code>
vampire --show_options on
</code>
if there is an option with an unsatisfactory explanation then please report it either via the Issues tab or directly to {{ reger }}.</p>
<p>
For more advanced usage we recommend looking at a number of tutorials that have been given on Vampire. For example, the recent <a href="https://github.com/vprover/ase17tutorial">ASE 2017 tutorial</a>.
</p>