Skip to content

Commit a32031d

Browse files
Update install solvers script to the one from Inox (+bitwuzla)
1 parent 189e976 commit a32031d

File tree

1 file changed

+60
-16
lines changed

1 file changed

+60
-16
lines changed

scripts/install_solvers.sh

Lines changed: 60 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,21 @@
11
#!/usr/bin/env sh
22

3+
if [ "$INSTALL_SOLVERS" != "1" ]; then
4+
echo "Skipping solver installation"
5+
exit 0
6+
fi
7+
8+
INFO_MSG="[INFO]"
9+
WARN_MSG="\033[33m[WARNING]\033[0m"
10+
ERROR_MSG="\033[1;31m[ERROR]\033[0m"
11+
12+
# curl command with default flags
13+
CURL='curl -L -s -C -'
14+
315
TEMP_DIR="$(pwd)/temp"
416
SOLVERS_DIR=${1:-"$(pwd)/solvers"}
517

18+
# check for set version or default to known working (for script) versions
619
Z3_VER=${2:-"4.15.1"}
720
CVC4_VER=${3:-"1.8"}
821
CVC5_VER=${4:-"1.2.1"}
@@ -14,45 +27,76 @@ SHORT_ARCH=$(uname -m | sed 's/x86_64/x64/;s/aarch64/arm64/;')
1427

1528
# libc linked against z3
1629
# (glibc for Linux, osx for macOS)
17-
LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
30+
Z3_LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
31+
32+
# os names as used by CVC5 builds
33+
CVC5_OS_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/macOS/;s/linux/Linux/;')
1834

1935
mkdir -p "$SOLVERS_DIR"
2036
mkdir -p "$TEMP_DIR"
37+
38+
reset_temp_dir() {
39+
rm -rf "$TEMP_DIR"
40+
mkdir -p "$TEMP_DIR"
41+
}
42+
43+
echo "$INFO_MSG Installing Solvers to $SOLVERS_DIR"
44+
2145
# cvc5
22-
wget -c "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-Linux-${ARCH}-static.zip" -O "$TEMP_DIR/cvc5.zip" -q
23-
unzip "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR"
46+
echo "$INFO_MSG Installing cvc5 (v${CVC5_VER})"
47+
48+
$CURL "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-${CVC5_OS_NAME}-${ARCH}-static.zip" --output "$TEMP_DIR/cvc5.zip"
49+
unzip -q "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR"
2450
CVC5_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*cvc5*")
2551
mv "$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5"
2652
chmod +x "$SOLVERS_DIR/cvc5"
27-
rm -rf "$TEMP_DIR"
2853

29-
# # CVC4
30-
wget -c "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" -O "$SOLVERS_DIR/cvc4" -q
54+
reset_temp_dir
55+
56+
# CVC4
57+
echo "$INFO_MSG Installing CVC4 (v${CVC4_VER})"
58+
59+
if [ "$CVC5_OS_NAME" = "macOS" ]; then
60+
echo "$WARN_MSG CVC4 installation on macOS; defaulting to only build available (x86_64 v1.8)"
61+
$CURL "https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-macos-opt" --output "$SOLVERS_DIR/cvc4"
62+
elif [ "$CVC5_OS_NAME" = "Linux" ]; then
63+
$CURL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" --output "$SOLVERS_DIR/cvc4"
64+
else
65+
echo "$ERROR_MSG CVC4 installation not supported on unknown OS: $CVC5_OS_NAME"
66+
exit 1
67+
fi
3168
chmod +x "$SOLVERS_DIR/cvc4"
3269

70+
reset_temp_dir
71+
3372
# z3
34-
mkdir -p "$TEMP_DIR"
35-
Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
73+
echo "$INFO_MSG Installing Z3 (v${Z3_VER})"
74+
75+
# z3 release file names contain libc versions in them, which makes them hard to
76+
# guess. Just get the correct one via the GitHub release API.
77+
Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${Z3_LIBC_NAME}" # followed by -<libcversion>.zip
3678
Z3_URL=$(
37-
curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
38-
grep "browser_download_url.*${Z3_FILE_PREFIX}" | #| # find url for the correct build
79+
$CURL "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
80+
grep "browser_download_url.*${Z3_FILE_PREFIX}" | # find url for the correct build
3981
sed 's/^.*: //;s/^"//;s/"$//' # strip non-url
4082
)
41-
wget -c "${Z3_URL}" -O "$TEMP_DIR/z3.zip" -q
42-
unzip "$TEMP_DIR/z3.zip" -d "$TEMP_DIR"
83+
$CURL "${Z3_URL}" --output "$TEMP_DIR/z3.zip"
84+
unzip -q "$TEMP_DIR/z3.zip" -d "$TEMP_DIR"
4385
Z3_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*z3*")
4486
mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
4587
chmod +x "$SOLVERS_DIR/z3"
4688
rm -rf "$TEMP_DIR"
4789

4890
# Bitwuzla
91+
echo "$INFO_MSG Installing Bitwuzla (v${BITWUZLA_VER})"
92+
4993
mkdir -p "$TEMP_DIR"
50-
wget -c https://github.com/bitwuzla/bitwuzla/releases/download/${BITWUZLA_VER}/Bitwuzla-Linux-x86_64-static.zip -O "$TEMP_DIR/bitwuzla.zip" -q
51-
unzip "$TEMP_DIR/bitwuzla.zip" -d "$TEMP_DIR"
94+
$CURL -L https://github.com/bitwuzla/bitwuzla/releases/download/${BITWUZLA_VER}/Bitwuzla-Linux-x86_64-static.zip --output "$TEMP_DIR/bitwuzla.zip"
95+
unzip -q "$TEMP_DIR/bitwuzla.zip" -d "$TEMP_DIR"
5296
BITWUZLA_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*Bitwuzla*")
5397
mv "$BITWUZLA_DIR/bin/bitwuzla" "$SOLVERS_DIR/bitwuzla"
5498
chmod +x "$SOLVERS_DIR/bitwuzla"
5599
rm -rf "$TEMP_DIR"
56100

57-
echo "************** Solvers Installed **************"
58-
exit 0
101+
echo "$INFO_MSG Solvers Installed"
102+
exit 0

0 commit comments

Comments
 (0)