OmegaHyper.dockerfile

ARG UBUNTU_VERSION=24.04
ARG SPOT_VERSION=2.16
ARG GHC_VERSION=9.12.4
ARG CABAL_VERSION=3.16.1.0
ARG Z3_VERSION=5.1.0
ARG NUXMV_VERSION=2.2.0

# ---- spot ----

FROM ubuntu:${UBUNTU_VERSION} AS spot
ARG SPOT_VERSION
RUN apt-get update && apt-get install -y --no-install-recommends curl ca-certificates build-essential libgmp3-dev
WORKDIR /build
RUN curl -fsSL https://www.lrde.epita.fr/dload/spot/spot-${SPOT_VERSION}.tar.gz | tar -xz
RUN cd spot-${SPOT_VERSION} && ./configure --disable-python --disable-static && make -j"$(nproc)" && make install-strip

# ---- kofola ----

FROM spot AS kofola
RUN apt-get install -y --no-install-recommends cmake
COPY app/kofola /kofola
WORKDIR /kofola/build
RUN cmake .. -DCMAKE_BUILD_TYPE=Release -DBUILD_TESTS=OFF && make -j"$(nproc)" kofola

# ---- OmegaHyper, AutoHyper TOSEM ----

FROM mcr.microsoft.com/dotnet/sdk:9.0-noble AS dotnet
COPY src /src/OmegaHyper
RUN dotnet build /src/OmegaHyper -c Release -o /out/OmegaHyper
COPY docker/AutoHyperTOSEM /src/AutoHyperTOSEM
RUN dotnet build /src/AutoHyperTOSEM/src/AutoHyper -c Release -o /out/AutoHyperTOSEM -p:DOTNET_VERSION=net9

# ---- AutoHyper 2.0 ----

FROM mcr.microsoft.com/dotnet/sdk:8.0-noble AS dotnet8
COPY docker/AutoHyper/src /src/AutoHyper
RUN dotnet build /src/AutoHyper/AutoHyper -c Release -o /out/AutoHyper

# ---- HyperSMV, HyperLasso ----

FROM ubuntu:${UBUNTU_VERSION} AS haskell
ARG GHC_VERSION
ARG CABAL_VERSION
RUN apt-get update && apt-get install -y --no-install-recommends \
        curl ca-certificates build-essential libgmp3-dev libffi-dev libncurses-dev zlib1g-dev
ENV BOOTSTRAP_HASKELL_NONINTERACTIVE=1 \
    BOOTSTRAP_HASKELL_GHC_VERSION=${GHC_VERSION} \
    BOOTSTRAP_HASKELL_CABAL_VERSION=${CABAL_VERSION} \
    PATH=/root/.ghcup/bin:${PATH}
RUN curl -sSf https://get-ghcup.haskell.org | sh && cabal update

COPY docker/HyperSMV /HyperSMV
COPY docker/nightly-2026-10-06+sbv.config /HyperSMV/
COPY docker/cabal.project.hypersmv /HyperSMV/cabal.project
RUN cd /HyperSMV && cabal install -j2 --installdir=/out --install-method=copy exe:hypersmv && strip /out/hypersmv

COPY docker/HyperLasso /HyperLasso
COPY docker/nightly-2026-10-06+sbv.config /HyperLasso/
COPY docker/cabal.project.hyperlasso /HyperLasso/cabal.project
RUN cd /HyperLasso && cabal install -j2 --installdir=/out --install-method=copy exe:HyperLasso && strip /out/HyperLasso

# ---- z3 (release build) ----
FROM ubuntu:${UBUNTU_VERSION} AS z3
ARG Z3_VERSION
ARG TARGETARCH
RUN apt-get update && apt-get install -y --no-install-recommends curl ca-certificates unzip
RUN case "${TARGETARCH}" in amd64) asset=x64-glibc-2.39 ;; arm64) asset=arm64-glibc-2.38 ;; esac \
    && curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-${asset}.zip \
    && unzip -q z3.zip && mv z3-${Z3_VERSION}-${asset} /z3

# ---- HyperQB 2.0 ----
FROM ubuntu:${UBUNTU_VERSION} AS rust
RUN apt-get update && apt-get install -y --no-install-recommends curl ca-certificates build-essential pkg-config clang libclang-dev
RUN curl -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal
COPY --from=z3 /z3/bin/libz3.so /usr/local/lib/
COPY --from=z3 /z3/include /usr/local/include
ENV PATH=/root/.cargo/bin:${PATH} \
    Z3_SYS_Z3_HEADER=/usr/local/include/z3.h \
    LIBRARY_PATH=/usr/local/lib
COPY docker/HyperQB /HyperQB
RUN cd /HyperQB && cargo build --release

# ---- quabs (its libsolve fetches cryptominisat with git) ----
FROM ubuntu:${UBUNTU_VERSION} AS quabs
RUN apt-get update && apt-get install -y --no-install-recommends build-essential cmake zlib1g-dev git ca-certificates
COPY docker/quabs /quabs
WORKDIR /quabs/build
RUN cmake .. -DCMAKE_BUILD_TYPE=Release && make -j"$(nproc)"

# ---- nuXmv (x86_64 only; under qemu on arm64, with the libraries of an amd64 ubuntu) ----
FROM ubuntu:${UBUNTU_VERSION} AS nuxmv
ARG NUXMV_VERSION
RUN apt-get update && apt-get install -y --no-install-recommends curl ca-certificates xz-utils qemu-user-static
RUN curl -fsSL https://nuxmv.fbk.eu/downloads/${NUXMV_VERSION}/nuXmv-${NUXMV_VERSION}-linux64.tar.xz | tar -xJ \
    && mv nuXmv-${NUXMV_VERSION}-linux64 /nuXmv
FROM --platform=linux/amd64 ubuntu:${UBUNTU_VERSION} AS amd64

# ---- the image ----
FROM mcr.microsoft.com/dotnet/runtime:9.0-noble
RUN apt-get update && apt-get install -y --no-install-recommends libgmp10 libffi8 python3 openjdk-21-jre-headless \
    && rm -rf /var/lib/apt/lists/*
COPY --from=dotnet8 /usr/share/dotnet/shared /usr/share/dotnet/shared

COPY --from=spot /usr/local /usr/local
COPY --from=kofola /kofola/build/src/kofola /usr/local/bin/
COPY --from=z3 /z3/bin/z3 /usr/local/bin/
COPY --from=z3 /z3/bin/libz3.so /usr/local/lib/
COPY --from=haskell /out/hypersmv /out/HyperLasso /usr/local/bin/
COPY --from=rust /HyperQB/target/release/HyperRUSTY /usr/local/bin/
COPY --from=quabs /quabs/build/quabs /usr/local/bin/
COPY --from=nuxmv /nuXmv/usr/local/bin/nuXmv /opt/nuXmv/usr/local/bin/
COPY --from=nuxmv /nuXmv/usr/local/lib /opt/nuXmv/usr/local/lib
COPY --from=nuxmv /usr/bin/qemu-x86_64-static /usr/local/bin/qemu-x86_64
COPY --from=amd64 /lib/x86_64-linux-gnu /amd64-sysroot/lib/x86_64-linux-gnu
COPY --from=amd64 /lib/x86_64-linux-gnu/ld-linux-x86-64.so.2 /amd64-sysroot/lib64/
COPY docker/nuXmv /usr/local/bin/
RUN ldconfig

COPY --from=dotnet8 /out/AutoHyper /AutoHyper
COPY --from=dotnet /out/AutoHyperTOSEM /AutoHyperTOSEM
COPY docker/paths.json /AutoHyper/
COPY docker/paths.json /AutoHyperTOSEM/

COPY --from=dotnet /out/OmegaHyper /OmegaHyper/app
COPY app/*.jar /OmegaHyper/app/
COPY docker/paths.json /OmegaHyper/app/
COPY benchmarks /OmegaHyper/benchmarks
COPY README.md COPYRIGHT LICENSE /OmegaHyper/

ENV PATH=/OmegaHyper/app:${PATH} \
    AUTOHYPER=/AutoHyper/AutoHyper \
    AUTOHYPER_TOSEM=/AutoHyperTOSEM/AutoHyper \
    LANG=C.UTF-8
WORKDIR /OmegaHyper/benchmarks