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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
Boolector 1.4
Tue Jun 8 10:58:24 CEST 2010
Source code release of Boolector.
Boolector is an efficient SMT solver for the quantifier-free theory of
bit-vectors in combination with the quantifier-free extensional theory of
arrays.
For compilation please obtain the latest source code of PicoSAT from
http://fmv.jku.at/picosat
Then extract from the archive the PicoSAT sources in the same directory
in which you extracted the Boolector sources. Rename or link the
PicoSAT source directory to 'picosat'. Then compile PicoSAT. For
version 935 of PicoSAT this works as follows:
cd <directory-where-you-extracted-boolector-sources>
wget http://fmv.jku.at/picosat/picosat-935.tar.gz
tar xf picosat-935.tar.gz
ln -s picosat-935 picosat
cd picosat
./configure -O # this will improve performance
make
You may want to do the same with 'PrecoSAT', e.g. get the latest
PrecoSAT sources from
http://fmv.jku.at/precosat
extract the sources in the same directory, rename the PrecoSAT directory
and compile. For version 456 of PrecoSAT this works as follows:
cd <directory-where-you-extracted-boolector-sources>
wget http://fmv.jku.at/precosat/precosat-465r2-2ce82ba-100514.tar.gz
tar xf precosat-465r2-2ce82ba-100514.tar.gz
ln -s precosat-465r2-2ce82ba-100514 precosat
cd precosat
./configure
make
Note, that PicoSAT is required in any case and PrecoSAT is optional, but
it can give you substantial performance improvement for plain BV formulas.
Then issue
./configure
make
or
./configure -precosat
make
if you want to use PrecoSAT. Also note that PrecoSAT needs the
development version of 'zlib'. On Ubuntu you can install it with
sudo aptitude install zlib1g-dev
Using PrecoSAT will force 'libboolector.a' to depend not only on
'libz.so' but also on 'libstdc++.so'. Thus if you want to link
'libboolector.a' with PrecoSAT backend against your own programs,
then you need to use '-lz -lstdc++' as linking options.
This will produce the library 'libboolector.a' with its API
'boolector.h', the stand-alone SMT solver 'boolector', a
simple delta debugger 'deltabtor', and a small tool 'synthebtor',
which can be used to synthesize AIGs in Aiger format from BV.
In the 'examples' sub-directory you find two examples for using
the API, which are also described in the API documentation. You
can generate the documentation on the API with 'doxygen'. Run
doxygen
in the top level source directory. Then point your browser at
doc/html/index.html
You may find more information on Booleactor at the website
http://fmv.jku.at/boolector
See the COPYING file for license and copying information.
In particular, this version of Boolector uses GPL.
In essence you can not distribute a program that uses
this version of Boolector unless you make your program
available under GPL as well. If you need another license
in order to use Boolector as part of a program which
is not going to be distributed under GPL, please contact
Armin Biere <biere@jku.at>.
Robert Daniel Brummayer, Armin Biere,
Johannes Kepler University.
Linz, Austria, 2010.
|
