README.md 3.22 KB
Newer Older
1
2
3
4
This repository contains raw benchmarks which have been submitted for inclusion
in the SMT-LIB benchmark library, but which have not yet been validated for
compliance with the SMT-LIB standard.  Anyone is welcome to download and use
these benchmarks, but please note that there is no guarantee that they are
5
6
7
8
compliant with the SMT-LIB standard.  To download benchmarks, please select
"HTTPS" in the drop-down menu above and then use "git clone" with the
corresponding URL.  Please do *not* use the buttons for downloading zip or tar
files as these can be very large and constructing them can overwhelm the server.
9

Pascal Fontaine's avatar
Pascal Fontaine committed
10
11
To submit new benchmarks, simply send the new benchmarks to one of the SMT-LIB
maintainers.  We encourage to distribute benchmarks under the
Mathias Preiner's avatar
Mathias Preiner committed
12
13
[Creative Commons Attribution 4.0 International License](https://creativecommons.org/licenses/by/4.0/),
but submitters can specify
Pascal Fontaine's avatar
Pascal Fontaine committed
14
15
their own licence in the benchmark itself using the ```(set-info :license
"licence string")``` command.
Clark Barrett's avatar
Clark Barrett committed
16

Pascal Fontaine's avatar
Pascal Fontaine committed
17
Each set of pending benchmarks should be stored here, one set per directory, below the directory specifying the logic of the benchmarks.  The directory should be named ```<date>-<application>-<submitter>```, ```<date>-<application>```, or ```<date>-<submitter>```.  We currently allow a deeper directory structure below the main directory.
Pascal Fontaine's avatar
Pascal Fontaine committed
18

19
The format of submitted benchmarks should be as follows:
20

Clark Barrett's avatar
Clark Barrett committed
21
```
Pascal Fontaine's avatar
Pascal Fontaine committed
22
(set-info :smt-lib-version <version>)
Clark Barrett's avatar
Clark Barrett committed
23
(set-logic <logic>)
Clark Barrett's avatar
Clark Barrett committed
24
(set-info :source |<description>|)
Clark Barrett's avatar
Clark Barrett committed
25
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
Pascal Fontaine's avatar
Pascal Fontaine committed
26
(set-info :category <category>)
Clark Barrett's avatar
Clark Barrett committed
27
28
29
(set-info :status <status>)
```
where:
Pascal Fontaine's avatar
Pascal Fontaine committed
30
- ```<version>``` is the SMT-LIB version number, e.g. 2.6.
Clark Barrett's avatar
Clark Barrett committed
31
- ```<logic>``` is one of the accepted SMT-LIB logics.
Clark Barrett's avatar
Clark Barrett committed
32
33
34
- ```<description>``` is a textual description containing:
  * Generated by: the name(s) of those who generated the benchmark;
  * Generated on: generation date with format YYYY-MM-DD;
35
  * Generator: tool which generated the benchmark (if any);
Clark Barrett's avatar
Clark Barrett committed
36
  * Application: the general goal;
37
38
39
  * Target solver: the solvers that were initially used to check the benchmarks;
  * Publications: references to related publications.
This can be followed by any other useful information in free text. 
Clark Barrett's avatar
Clark Barrett committed
40
- ```<category>``` is either "crafted", indicating that it was hand-made,
41
"random", indicating that it was generated randomly, or "industrial"
Clark Barrett's avatar
Clark Barrett committed
42
(everything else).  Note that the category should be in quotes.
Clark Barrett's avatar
Clark Barrett committed
43
- ```<status>``` is either sat or unsat according to the status of the benchmark,
Pascal Fontaine's avatar
Pascal Fontaine committed
44
45
  or unknown if not known.

Clark Barrett's avatar
Clark Barrett committed
46
47
48
Below is an example:

```
Pascal Fontaine's avatar
Pascal Fontaine committed
49
(set-info :smt-lib-version 2.6)
Clark Barrett's avatar
Clark Barrett committed
50
(set-logic QF_UFLIA)
Pascal Fontaine's avatar
Pascal Fontaine committed
51
52
53
54
55
56
57
(set-info :source |
Generated by: Clark Barrett, Pascal Fontaine, Cesare Tinelli
Generated on: 2016-12-31
Generator: Sledgehammer
Application: Isabelle proof of Gödel theorem
Target solver: CVC4
|)
58
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
Pascal Fontaine's avatar
Pascal Fontaine committed
59
60
(set-info :category "industrial")
(set-info :status unsat)
Clark Barrett's avatar
Clark Barrett committed
61
```
Pascal Fontaine's avatar
Pascal Fontaine committed
62

Clark Barrett's avatar
Clark Barrett committed
63
64
The workflow is as follows.  The benchmarks are:
1. put in this repository as soon as they are received
65
2. checked for conformance with the available tools 
Pascal Fontaine's avatar
Pascal Fontaine committed
66
3. sanitized if necessary
Clark Barrett's avatar
Clark Barrett committed
67
68
4. checked for status if their status is unknown (they are given a status if at least two solvers solve them)
5. moved to the official repository, in the devel branch