Skip to content

Commit

Permalink
Removing boolector from docker image for testing purposes
Browse files Browse the repository at this point in the history
  • Loading branch information
ckirsch committed Dec 31, 2024
1 parent f921f9d commit 64e7456
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 38 deletions.
38 changes: 1 addition & 37 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -107,41 +107,6 @@ RUN mkdir -p $RISCV/bin \
&& cp /usr/bin/qemu-riscv32-static $RISCV/bin \
&& cp /usr/bin/qemu-system-riscv32 $RISCV/bin

########################################
# Boolector (SMT solver) builder image #
########################################
FROM ubuntu:latest AS boolectorbuilder

ENV TOP=/opt RISCV=/opt/riscv PATH=$PATH:/opt/riscv/bin

WORKDIR $TOP

# Setting non-interactive mode
RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections

# install tools to build boolector
RUN apt-get update \
&& apt-get install -y --no-install-recommends \
ca-certificates \
make git \
g++ \
curl cmake \
&& apt clean

RUN git clone https://github.com/Boolector/boolector

ENV MAKEFLAGS=-j4

# build boolector and dependencies
RUN mkdir -p $RISCV \
&& cd boolector \
&& ./contrib/setup-lingeling.sh \
&& ./contrib/setup-btor2tools.sh \
&& ./configure.sh --prefix $RISCV \
&& cd build \
&& make \
&& make install

#######################################
# Bitwuzla (SMT solver) builder image #
#######################################
Expand Down Expand Up @@ -199,11 +164,10 @@ RUN apt-get update \
xxd gettext curl \
&& apt clean

# copy spike, pk, qemu and boolector from builder images
# copy pk, spike, qemu, and bitwuzla from builder images
COPY --from=pkbuilder $RISCV/ $RISCV/
COPY --from=spikebuilder $RISCV/ $RISCV/
COPY --from=qemubuilder $RISCV/ $RISCV/
COPY --from=boolectorbuilder $RISCV/ $RISCV/
COPY --from=bitwuzlabuilder $RISCV/ $RISCV/

# add selfie sources to the image
Expand Down
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -347,7 +347,7 @@ btor2: beator-btor2 rotor-btor2
.PHONY: spike qemu assemble beator-32 rotor-32 32-bit boolector beator-btormc rotor-btormc btormc extras

# Run everything that requires non-standard tools
extras: spike qemu assemble beator-32 rotor-32 32-bit boolector btormc
extras: spike qemu assemble beator-32 rotor-32 32-bit

# Run selfie on spike
spike: selfie.m selfie.s
Expand Down

0 comments on commit 64e7456

Please sign in to comment.