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
|
##############################################################################
# #
# *Notice* #
# #
# This Docker image is based on Alpine Linux, which is a `musl` libc-based #
# distribution, and not `glibc`-based (e.g., like Ubuntu or Debian). #
# #
# To make Boolector work under `musl`, Boolector is "patched" using the #
# Windows patch-sets. These patch-sets (predominantly) are used to restrict #
# Boolector to the minimum amount of libc that is exposed via MinGW. #
# #
# For our purposes, restricting Boolector to the MinGW runtime also means #
# that Boolector builds and runs under `musl`. #
# #
# Any references to patching "for Windows" should be read as "patching for #
# a minimal libc". #
# #
##############################################################################
FROM alpine:3.9
MAINTAINER Andrew V. Jones "andrew.jones@vector.com"
ENV LC_ALL en_US.UTF-8
ENV LANG en_US.UTF-8
#
# Deps needed only for build
#
ENV BUILD_DEPS \
alpine-sdk \
cmake \
cython \
cython-dev \
g++ \
gcc \
git \
make \
python-dev \
python3 \
sed \
wget
#
# Deps needed for running afterwards
#
ENV PERSISTENT_DEPS \
bash \
libgcc \
libstdc++ \
python
#
# Which repo to build from?
#
ARG UPSTREAM=https://github.com/Boolector/boolector/archive
#
# Which Boolector branch to build?
#
ARG BRANCH=master
#
# Steps to build-up our image
#
RUN apk upgrade --update && \
apk add --no-cache --virtual .build-deps $BUILD_DEPS && \
apk add --no-cache --virtual .persistent-deps $PERSISTENT_DEPS && \
# \
# Musl does not provide /usr/include/sys/unistd.h, which Lingeling needs \
# \
echo "#include <unistd.h>" > /usr/include/sys/unistd.h && \
#
# Grab our Boolector tar (output is going to be "boolector-${BRANCH}".tar.gz)
#
wget "${UPSTREAM}/${BRANCH}.tar.gz" -O "boolector-${BRANCH}.tar.gz" && \
tar -xzvf "boolector-${BRANCH}.tar.gz" && \
#
# Move to sanitized location
#
mv "boolector-${BRANCH}" boolector && \
#
# Enter source tree
#
cd boolector && \
# \
# Musl does not provide quite enough of glibc, so we pretend we're Windows \
# \
sed -i "s#MINGW32#Linux#g" ./contrib/setup-utils.sh && \
# \
# Force -fPIC for CaDiCaL
# \
sed -i "s#export CXXFLAGS=\"\"#export CXXFLAGS=\"-fPIC\"#g" ./contrib/setup-cadical.sh && \
./contrib/setup-btor2tools.sh && \
./contrib/setup-picosat.sh && \
./contrib/setup-cadical.sh && \
./contrib/setup-lingeling.sh && \
./configure.sh --python --shared && \
cd build && \
make -j$(nproc) && \
# \
# Validate our build of Boolector
# \
ctest -j$(nproc) --output-on-failure \
apk del .build-deps
#
# When we're in the container, we want to have PYTHONPATH to include pyboolector
#
ENV PYTHONPATH "${PYTHONPATH}:/boolector/build/lib"
#
# Entry point to allow us to run .smt2 files "from the outside"
#
ENTRYPOINT ["/boolector/build/bin/boolector"]
# EOF
|
