vprover.github.io/usage.html at master · ibnyusuf/vprover.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
<!DOCTYPE html
	PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
	 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en-US" xml:lang="en-US">
<head>
<title>Usage</title>
<link href="vampire.css" rel="StyleSheet" type="text/css" />
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
</head>
<body>
<table style="border-collapse:collapse"><tr>
<script src="scripts/nav.js"></script>
<td class="content"> <h1>Usage</h1>

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

<h4>Manual</h4>
<p>Vampire manual is not finished yet. While there is no manual, you can
          use the preliminary version of our <a href="cav2013.pdf">CAV 2013 paper</a>, which describes
          main features of Vampire and some of its options.</p>

<h4>Basic Usage</h4>

<p>The most basic usage of Vampire is to save your problem in <a href="www.cs.miami.edu/~tptp/">TPTP</a> format and run

<pre>
<code>vampire problem.p </code>
</pre>

as this will run Vampire in <i>default</i> mode with a 60 second time-limit. However, a better way to run Vampire is in portfolio mode i.e.

<pre>
<code>vampire --mode portfolio -t 300 problem.p </code>
</pre>

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. If you think the problem is <i>satisfiable</i> then you can also run
<pre>
<code>vampire --mode casc_sat -t 300 problem.p </code>
</pre>
which will use a set of strategies suited to satisfiable problems (as entered into the most recent <a href="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
<pre>
<code>vampire --mode portfolio -t 300 --input_syntax smtlib2 problem.smt2 </code>
</pre>
to specify a different input language, or
<pre>
<code>vampire --mode smtcomp problem.p </code>
</pre>
to use the latest <a href="http://smtcomp.sourceforge.net/">SMT-COMP</a> schedule, which automatically selects the appropriate input language.

<h4>More Advanced Usage</h4>

For more advanced usage we recommend looking at a number of tutorials that have been given on Vampire. (Links to appear soon).

</td></tr></table>
</body>
</html>