diff --git a/ghdl-formal.Dockerfile b/ghdl-formal.Dockerfile index cf49d0f..4828bb6 100644 --- a/ghdl-formal.Dockerfile +++ b/ghdl-formal.Dockerfile @@ -48,7 +48,8 @@ RUN apt-get update -qq && \ libc6-dev \ zlib1g-dev \ make \ - python3 && \ + python3 \ + libpython2.7 && \ apt-get -y upgrade && apt-get autoclean && apt-get clean && apt-get -y autoremove && \ update-ca-certificates && \ rm -rf /var/lib/apt/lists/* @@ -57,4 +58,4 @@ RUN apt-get update -qq && \ COPY --from=symbiyosys-ghdlsynth /opt /opt # Enhance path variable -ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/cvc4/bin:/opt/boolector/bin:$PATH" +ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/super_prove/bin:$PATH" diff --git a/packages/fix_super_prove_build.txt b/packages/fix_super_prove_build.txt new file mode 100644 index 0000000..06beb82 --- /dev/null +++ b/packages/fix_super_prove_build.txt @@ -0,0 +1,25 @@ +diff -r bde167bca3cd Bip/Main_bip.cc +--- a/Bip/Main_bip.cc Thu Sep 14 01:44:08 2017 -0700 ++++ b/Bip/Main_bip.cc Thu Aug 08 15:02:00 2019 +0200 +@@ -508,8 +508,8 @@ + void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis) + { + Vec > ffs, pis; +- For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w)); +- For_Gatetype(N, gate_PI , w) pis.push(tuple(attr_PI (w).number, w)); ++ For_Gatetype(N, gate_Flop, w) ffs.push(::tuple(attr_Flop(w).number, w)); ++ For_Gatetype(N, gate_PI , w) pis.push(::tuple(attr_PI (w).number, w)); + sort(ffs); + sort(pis); + +diff -r bde167bca3cd MetaSat/MiniSat2/System.cc +--- a/MetaSat/MiniSat2/System.cc Thu Sep 14 01:44:08 2017 -0700 ++++ b/MetaSat/MiniSat2/System.cc Thu Aug 08 15:02:00 2019 +0200 +@@ -20,6 +20,7 @@ + + #include + #include ++#include + + #include "System.hh" + diff --git a/packages/suprove b/packages/suprove new file mode 100644 index 0000000..9230d1e --- /dev/null +++ b/packages/suprove @@ -0,0 +1,3 @@ +#!/bin/bash +tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi +exec /opt/super_prove/bin/${tool}.sh "$@" diff --git a/symbiyosys.Dockerfile b/symbiyosys.Dockerfile index e65f937..c182240 100644 --- a/symbiyosys.Dockerfile +++ b/symbiyosys.Dockerfile @@ -37,13 +37,21 @@ RUN apt-get update -qq && \ FROM yosys AS symbiyosys +COPY packages/suprove /root/suprove +COPY packages/fix_super_prove_build.txt /root/fix_super_prove_build.txt + RUN apt-get update -qq && \ DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ autoconf \ gperf \ cmake \ curl \ - libgmp-dev && \ + libgmp-dev \ + ninja-build \ + g++ \ + python-setuptools \ + python-pip \ + mercurial && \ apt-get autoclean && apt-get clean && apt-get -y autoremove && \ rm -rf /var/lib/apt/lists/* && \ cd /root && \ @@ -80,4 +88,18 @@ RUN apt-get update -qq && \ mkdir /opt/boolector/bin && \ cp build/bin/boolector /opt/boolector/bin/ && \ cp build/bin/btor* /opt/boolector/bin/ && \ - cp deps/btor2tools/bin/btorsim /opt/boolector/bin/ + cp deps/btor2tools/bin/btorsim /opt/boolector/bin/ && \ + cd /root && \ + git clone --recursive https://github.com/sterin/super-prove-build && \ + cd super-prove-build/abc-zz && \ + patch -p1 < /root/fix_super_prove_build.txt && \ + cd .. && \ + mkdir build && \ + cd build && \ + cmake -DCMAKE_BUILD_TYPE=Release -G Ninja .. && \ + ninja && \ + ninja package && \ + tar -C /opt -xzf super_prove*.tar.gz && \ + mv /root/suprove /opt/super_prove/bin/ && \ + chmod +x /opt/super_prove/bin/suprove && \ + rm -rf /root/*