blob: 09473d46a5561b8e474481de67cf5bb70f84b3bb (
plain)
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
# Maintainer: Manuel Wiesinger <m {you know what belongs here} mmap {and here} at>
pkgbase=bitwuzla
pkgname=("${pkgbase}" "${pkgbase}-docs")
pkgver=0.9.1
pkgrel=1
pkgdesc='SMT solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations'
arch=('x86_64')
url='https://bitwuzla.github.io'
license=('MIT')
source=(
"$pkgname-$pkgver.tar.gz::https://github.com/bitwuzla/bitwuzla/archive/refs/tags/${pkgver}.tar.gz"
"0000-Use-installed-libraries.patch"
)
depends=(
'cryptominisat'
'glibc'
'gmp>=6.1'
'kissat'
'libgcc'
'libstdc++'
'mpfr'
)
makedepends=(
'cmake'
'cython'
'doxygen'
'git' # Version string gets generated from git
'gtest' # Needed even with --nocheck
'meson>=0.64'
'ninja'
'python-breathe'
'python-pytest' # Needed even with --nocheck
'python-sphinx'
'python-sphinx-tabs'
'python-sphinx_rtd_theme'
'python-sphinxcontrib-bibtex'
'python>=3.7'
'symfpu'
)
optdepends=(
'aiger: Utilities for And-Inverter Graphs (AIGs)'
'cadical: CaDiCaL support'
'python>=3.7: Python bindings'
)
provides=(
'libbitwuzlabv.so'
'libbitwuzlabb.so'
'libbitwuzlals.so'
'libbitwuzla.so'
)
b2sums=('b694149cd724ae569345d9f3386c0bcd8ae9f13259d7c10aa8f45d4d273b145c33a81aac30ab61aa70d2d31a0dc0d1847c300307f8ed4b888fa81387117f5086'
'96897dada985c929820c7285a4e968977786e58e18b632dff06414ed71572a9139c0dad7a20705c03ff462cc954e5ffccb331d1ead100cd085686a5fc1d79fa3')
options=('!lto')
prepare() {
cd "${srcdir}/${pkgname}-${pkgver}"
patch --forward --strip=1 --input=../0000-Use-installed-libraries.patch
}
build() {
cd "${srcdir}/${pkgname}-${pkgver}"
# aiger does not provide a library to link against. bitwuzla uses only .c/.h
# files during compilation. aiger is kept as meson subproject. Thus, there
# are no aiger run-time dependencies.
# cadical only provides a static library and requires header files from the
# source. Thus we use cadical as a subproject
./configure.py \
--prefix /usr \
--shared \
--python \
--testing \
--docs \
--kissat \
--cryptominisat \
--aiger \
release
cd build
meson compile
}
check() {
cd "${srcdir}/${pkgname}-${pkgver}"
meson test -C build
}
package_bitwuzla() {
cd "${srcdir}/${pkgbase}-${pkgver}"
install -Dm644 COPYING "${pkgdir}/usr/share/licenses/${pkgname}/COPYING"
install -Dm644 CONTRIBUTING.md "${pkgdir/}usr/share/doc/${pkgname}/CONTRIBUTING.md"
install -Dm644 NEWS.md "${pkgdir}/usr/share/doc/${pkgname}/NEWS.md"
cd build
DESTDIR="${pkgdir}" ninja install
}
package_bitwuzla-docs() {
pkgdesc="Documentation for the Bitwuzla SMT solver"
arch=('any')
depends=()
provides=()
cd "${srcdir}/${pkgbase}-${pkgver}"
install -Dm644 COPYING "${pkgdir}/usr/share/licenses/${pkgname}/COPYING"
install -Dm644 CONTRIBUTING.md "${pkgdir}/usr/share/doc/${pkgname}/CONTRIBUTING.md"
cd build/docs
# Do not copy documentation source files
find . \
-not -path "./.*" \
-not -path "./_sources*" \
-not -path "./conf.py" \
-not -path "./cli_usage.txt" \
-not -path "./c/xml*" \
-not -path "./c/Doxyfile" \
-not -path "./cpp/xml*" \
-not -path "./cpp/Doxyfile" \
-exec install -Dm644 {} "${pkgdir}/usr/share/doc/${pkgbase}/html/{}" \;
install -Dm644 cli_usage.txt "${pkgdir}/usr/share/doc/${pkgbase}/cli_usage.txt"
}
|